case mk
α : Type ?u.34804
X : Type u_1
Y : Type u_2
Z : Type ?u.34813
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
a✝ : X
⊢ map f cond (ofLE h (Quot.mk Setoid.r a✝)) = map f (_ : LEComap f A' B) (Quot.mk Setoid.r a✝)
α : Type ?u.34804
X : Type u_1
Y : Type u_2
Z : Type ?u.34813
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
⊢ map f cond (ofLE h c) = map f (_ : LEComap f A' B) c
rcases c with ⟨⟩
no goals
case mk
α : Type ?u.34804
X : Type u_1
Y : Type u_2
Z : Type ?u.34813
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
a✝ : X
⊢ map f cond (ofLE h (Quot.mk Setoid.r a✝)) = map f (_ : LEComap f A' B) (Quot.mk Setoid.r a✝)
rfl