-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem toGlue_commute (hΦ : Isometry Φ) (hΨ : Isometry Ψ) :
    toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ

Tactic:
let i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ

Result:
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ

Proof state:
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x✝ : Z
⊢ Quotient.mk'' (Sum.inl (Φ x✝)) = Quotient.mk'' (Sum.inr (Ψ x✝))

Tactic:
refine SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 ?_)

Result:
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x✝ : Z
⊢ dist (Sum.inl (Φ x✝)) (Sum.inr (Ψ x✝)) = 0

Proof state:
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x✝ : Z
⊢ dist (Sum.inl (Φ x✝)) (Sum.inr (Ψ x✝)) = 0

Tactic:
exact glueDist_glued_points Φ Ψ 0 _

Result:
no goals

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ

Tactic:
funext

Result:
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x✝ : Z
⊢ (toGlueL hΦ hΨ ∘ Φ) x✝ = (toGlueR hΦ hΨ ∘ Ψ) x✝

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ

Tactic:
let _ := i.toUniformSpace.toTopologicalSpace

Result:
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ

Proof state:
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x✝ : Z
⊢ (toGlueL hΦ hΨ ∘ Φ) x✝ = (toGlueR hΦ hΨ ∘ Ψ) x✝

Tactic:
simp only [comp, toGlueL, toGlueR]

Result:
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
x✝ : Z
⊢ Quotient.mk'' (Sum.inl (Φ x✝)) = Quotient.mk'' (Sum.inr (Ψ x✝))