case mk
α : Type ?u.13886
X : Type u_1
Y : Type ?u.13892
Z : Type ?u.13895
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
a✝ : X
⊢ ofLE h₂ (ofLE h₁ (Quot.mk Setoid.r a✝)) = ofLE (_ : A ≤ C) (Quot.mk Setoid.r a✝)
α : Type ?u.13886
X : Type u_1
Y : Type ?u.13892
Z : Type ?u.13895
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
⊢ ofLE h₂ (ofLE h₁ x) = ofLE (_ : A ≤ C) x
rcases x with ⟨⟩
no goals
case mk
α : Type ?u.13886
X : Type u_1
Y : Type ?u.13892
Z : Type ?u.13895
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S A B C : DiscreteQuotient X
h₁ : A ≤ B
h₂ : B ≤ C
x : Quotient A.toSetoid
a✝ : X
⊢ ofLE h₂ (ofLE h₁ (Quot.mk Setoid.r a✝)) = ofLE (_ : A ≤ C) (Quot.mk Setoid.r a✝)
rfl