case mk
α : Type ?u.32610
X : Type u_1
Y : Type u_2
Z : Type ?u.32619
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 : B ≤ B'
a : Quotient A.toSetoid
a✝ : X
⊢ ofLE h (map f cond (Quot.mk Setoid.r a✝)) = map f (_ : LEComap f A B') (Quot.mk Setoid.r a✝)
α : Type ?u.32610
X : Type u_1
Y : Type u_2
Z : Type ?u.32619
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 : B ≤ B'
a : Quotient A.toSetoid
⊢ ofLE h (map f cond a) = map f (_ : LEComap f A B') a
rcases a with ⟨⟩
no goals
case mk
α : Type ?u.32610
X : Type u_1
Y : Type u_2
Z : Type ?u.32619
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 : B ≤ B'
a : Quotient A.toSetoid
a✝ : X
⊢ ofLE h (map f cond (Quot.mk Setoid.r a✝)) = map f (_ : LEComap f A B') (Quot.mk Setoid.r a✝)
rfl