awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
j : ι
y : E j
hy : dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < min ε 1
mp :
  ∀ (y : E i) (hy : dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) < min ε 1),
    Sigma.mk (β := fun (i : ι) ↦ E i) i y ∈ s
mp₁ : ∀ (hij : i ≠ j), Sigma.mk (β := fun (i : ι) ↦ E i) j y ∈ s
⊢ Sigma.mk (β := fun (i : ι) ↦ E i) j y ∈ s

Tactic:
rcases eq_or_ne i j with (rfl | hij)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
y : E i
hy : dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) < min ε 1
⊢ dist x y < ε ∧ dist x y < 1

Tactic:
simp only [Sigma.dist_same, lt_min_iff] at hy

Premises used: lt_min_iff, Metric.Sigma.dist_same
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
y : E i
hy : dist x y < ε ∧ dist x y < 1
⊢ Sigma.mk (β := fun (i : ι) ↦ E i) i y ∈ s

Tactic:
hε (mem_ball'.2 hy.1)

Premises used: Iff.mpr, Set.Mem, setOf, Set.preimage, And.left, Metric.mem_ball'
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
y : E i
hy : dist x y < ε ∧ dist x y < 1
⊢ Sigma.mk (β := fun (i : ι) ↦ E i) i y ∈ s

Tactic:
exact hε (mem_ball'.2 hy.1)

Premises used: Iff.mpr, And.left, Metric.mem_ball'
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
j : ι
y : E j
hy : dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < min ε 1
hij : i ≠ j
apply : LT.lt (α := ℝ) 1 1
⊢ Sigma.mk (β := fun (i : ι) ↦ E i) j y ∈ s

Tactic:
apply (lt_irrefl (1 : ℝ) _).elim

Premises used: lt_irrefl, False.elim, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
j : ι
y : E j
hy : dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < min ε 1
hij : i ≠ j
⊢ 1 ≤ Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y)

Tactic:
Sigma.one_le_dist_of_ne hij _ _

Premises used: Metric.Sigma.one_le_dist_of_ne
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
j : ι
y : E j
hy : dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < min ε 1
hij : i ≠ j
⊢ Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < 1

Tactic:
hy.trans_le (min_le_right _ _)

Premises used: LT.lt.trans_le, min_le_right
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
j : ι
y : E j
hy : dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < min ε 1
hij : i ≠ j
⊢ LT.lt (α := ℝ) 1 1

Tactic:
calc
        1 ≤ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
        _ < 1 := hy.trans_le (min_le_right _ _)

Premises used: Metric.Sigma.dist, LT.lt.trans_le, min_le_right, Metric.Sigma.one_le_dist_of_ne, Sigma.mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ (∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen[instTopologicalSpaceSigma] s

Tactic:
fun H => isOpen_sigma_iff.2 fun i => Metric.isOpen_iff.2 fun x hx => ?_

Premises used: Iff.mpr, Metric.isOpen_iff, isOpen_sigma_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
mpr :
  ∀ (H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) (i : ι) (x : E i)
    (hx : x ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s), ∃ ε > 0, ball x ε ⊆ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
⊢ (∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen[instTopologicalSpaceSigma] s

Tactic:
refine fun H => isOpen_sigma_iff.2 fun i => Metric.isOpen_iff.2 fun x hx => ?_

Premises used: Iff.mpr, Metric.isOpen_iff, isOpen_sigma_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
⊢ ∃ ε > 0, ∀ (y : (j : ι) × E j), dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) y < ε → y ∈ s

Tactic:
H ⟨i, x⟩ hx

Premises used: Sigma.mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
mpr :
  ∀ (ε : ℝ) (εpos : ε > 0) (hε : ∀ (y : (j : ι) × E j), dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) y < ε → y ∈ s),
    ∃ ε > 0, ball x ε ⊆ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
⊢ ∃ ε > 0, ball x ε ⊆ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ∀ y, dist (⟨i, x⟩ : Σ j, E j) y < ε → y ∈ s :=
      H ⟨i, x⟩ hx

Premises used: Sigma.mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) y < ε → y ∈ s
⊢ ∃ ε > 0, ball x ε ⊆ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s

Tactic:
⟨ε, εpos, fun y hy => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) y < ε → y ∈ s
mpr : ∀ (y : E i) (hy : y ∈ ball x ε), y ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
⊢ ∃ ε > 0, ball x ε ⊆ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s

Tactic:
refine ⟨ε, εpos, fun y hy => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
mpr : dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) (Sigma.mk (β := fun (j : ι) ↦ E j) i y) < ε
⊢ y ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s

Tactic:
apply hε ⟨i, y⟩

Premises used: Sigma.mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
mpr : dist x y < ε
⊢ dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) (Sigma.mk (β := fun (j : ι) ↦ E j) i y) < ε

Tactic:
rw [Sigma.dist_same]

Premises used: Metric.Sigma.dist_same
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist x y < ε

Tactic:
mem_ball'.1 hy

Premises used: Iff.mp, Metric.mem_ball'
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist x y < ε

Tactic:
exact mem_ball'.1 hy

Premises used: Iff.mp, Metric.mem_ball'
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
refine_1 : ∀ (x : (i : ι) × E i), Sigma.dist (E := E) x x = 0
refine_2 : ∀ (x y : (i : ι) × E i), Sigma.dist (E := E) x y = Sigma.dist (E := E) y x
refine_3 : ∀ (x y : (i : ι) × E i), Sigma.dist (E := E) x y = 0 → x = y
⊢ MetricSpace ((i : ι) × E i)

Tactic:
refine MetricSpace.ofDistTopology Sigma.dist ?_ ?_ Sigma.dist_triangle Sigma.isOpen_iff ?_

Premises used: Metric.Sigma.dist, Metric.Sigma.dist_triangle, MetricSpace.ofDistTopology, Metric.Sigma.isOpen_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
⊢ Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) = 0

Tactic:
simp [Sigma.dist]

Premises used: Metric.Sigma.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
refine_2 :
  ∀ (y : E i),
    Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) =
      Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) (Sigma.mk (β := fun (i : ι) ↦ E i) i x)
refine_2₁ :
  ∀ (h : i ≠ j),
    Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) =
      Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) i x)
⊢ Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) =
    Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) i x)

Tactic:
rcases eq_or_ne i j with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) =
    Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) (Sigma.mk (β := fun (i : ι) ↦ E i) i x)

Tactic:
simp [Sigma.dist, dist_comm]

Premises used: dist_comm, Metric.Sigma.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i ≠ j
refine_2 : dist x ⋯.some + 1 + dist y ⋯.some = dist y ⋯.some + 1 + dist x ⋯.some
⊢ Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) =
    Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) i x)

Tactic:
simp only [Sigma.dist, dist_comm, h, h.symm, not_false_iff, dif_neg]

Premises used: Ne.symm, dist_comm, dif_neg, Metric.Sigma.dist, not_false_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i ≠ j
⊢ dist x ⋯.some + 1 + dist y ⋯.some = dist y ⋯.some + 1 + dist x ⋯.some

Tactic:
abel
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
refine_3 :
  ∀ (y : E i),
    Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) = 0 →
      Sigma.mk (β := fun (i : ι) ↦ E i) i x = Sigma.mk (β := fun (i : ι) ↦ E i) i y
refine_3₁ :
  ∀ (hij : i ≠ j),
    Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) = 0 →
      Sigma.mk (β := fun (i : ι) ↦ E i) i x = Sigma.mk (β := fun (i : ι) ↦ E i) j y
⊢ Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) = 0 →
    Sigma.mk (β := fun (i : ι) ↦ E i) i x = Sigma.mk (β := fun (i : ι) ↦ E i) j y

Tactic:
rcases eq_or_ne i j with (rfl | hij)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) = 0 →
    Sigma.mk (β := fun (i : ι) ↦ E i) i x = Sigma.mk (β := fun (i : ι) ↦ E i) i y

Tactic:
simp [Sigma.dist]

Premises used: Metric.Sigma.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) = 0
apply : LT.lt (α := ℝ) 1 1
⊢ Sigma.mk (β := fun (i : ι) ↦ E i) i x = Sigma.mk (β := fun (i : ι) ↦ E i) j y

Tactic:
apply (lt_irrefl (1 : ℝ) _).elim

Premises used: lt_irrefl, False.elim, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) = 0
⊢ 1 ≤ Sigma.dist (E := E) (Sigma.mk (β := fun (k : ι) ↦ E k) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y)

Tactic:
Sigma.one_le_dist_of_ne hij _ _

Premises used: Metric.Sigma.one_le_dist_of_ne
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) = 0
rw : LT.lt (α := ℝ) 0 1
⊢ Sigma.dist (E := E) (Sigma.mk (β := fun (k : ι) ↦ E k) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < 1

Tactic:
rw [h]
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) = 0
⊢ LT.lt (α := ℝ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) = 0
⊢ LT.lt (α := ℝ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist (E := E) (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) = 0
E₁ : Sigma.dist (E := E) (Sigma.mk (β := fun (k : ι) ↦ E k) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < 1
⊢ LT.lt (α := ℝ) 1 1

Tactic:
calc
        1 ≤ Sigma.dist (⟨i, x⟩ : Σ k, E k) ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
        _ < 1 := by rw [h]; exact zero_lt_one

Premises used: Metric.Sigma.dist, Metric.Sigma.one_le_dist_of_ne, Sigma.mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ dist (Sigma.mk (β := E) i x) (Sigma.mk (β := E) i y) = dist x y

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
i : ι
simp : IsComplete (α := (i : ι) × E i) (range (Sigma.mk (β := fun (i : ι) ↦ E i) i))
⊢ IsComplete (s i)

Tactic:
simp only [s, ← range_sigmaMk]

Premises used: Set.range_sigmaMk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
i : ι
⊢ IsComplete (α := (i : ι) × E i) (range (Sigma.mk (β := fun (i : ι) ↦ E i) i))

Tactic:
(isometry_mk i).isUniformInducing.isComplete_range

Premises used: setOf, IsUniformInducing.isComplete_range, Isometry.isUniformInducing, Metric.Sigma.isometry_mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
i : ι
⊢ IsComplete (α := (i : ι) × E i) (range (Sigma.mk (β := fun (i : ι) ↦ E i) i))

Tactic:
exact (isometry_mk i).isUniformInducing.isComplete_range

Premises used: IsUniformInducing.isComplete_range, Isometry.isUniformInducing, Metric.Sigma.isometry_mk
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
⊢ ∀ (i : ι), IsComplete (s i)

Tactic:
have hc : ∀ i, IsComplete (s i) := fun i => by
    simp only [s, ← range_sigmaMk]
    exact (isometry_mk i).isUniformInducing.isComplete_range
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
hc : ∀ (i : ι), IsComplete (s i)
⊢ ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j

Tactic:
have hd : ∀ (i j), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j := fun i j x hx y hy hxy =>
    (Eq.symm hx).trans ((fst_eq_of_dist_lt_one _ _ hxy).trans hy)
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
⊢ CompleteSpace ((i : ι) × E i)

Tactic:
completeSpace_of_isComplete_univ ?_

Premises used: completeSpace_of_isComplete_univ
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
refine : IsComplete (α := (i : ι) × E i) univ
⊢ CompleteSpace ((i : ι) × E i)

Tactic:
refine completeSpace_of_isComplete_univ ?_

Premises used: completeSpace_of_isComplete_univ
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
⊢ IsComplete (α := (i : ι) × E i) (⋃ (i : ι), s i)

Tactic:
isComplete_iUnion_separated hc (dist_mem_uniformity zero_lt_one) hd

Premises used: zero_lt_one, isComplete_iUnion_separated, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
h : Eq (α := Set ((i : ι) × E i)) univ (⋃ (i : ι), s i)
⊢ IsComplete (α := (i : ι) × E i) univ

Tactic:
convert! isComplete_iUnion_separated hc (dist_mem_uniformity zero_lt_one) hd

Premises used: zero_lt_one, isComplete_iUnion_separated, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
inst_1 : ∀ (i : ι), CompleteSpace.{u_2} (E i)
s : ι → Set ((i : ι) × E i) := fun (i : ι) ↦ Sigma.fst (β := fun (i : ι) ↦ E i) ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p : ((k : ι) × E k) × (k : ι) × E k | dist p.1 p.2 < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
⊢ Eq (α := Set ((i : ι) × E i)) univ (⋃ (i : ι), s i)

Tactic:
simp only [s, ← preimage_iUnion, iUnion_of_singleton, preimage_univ]

Premises used: Set.preimage_univ, Set.preimage_iUnion, Set.iUnion_of_singleton
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : Nonempty Z
inst_1 : MetricSpace Z
inst_2 : MetricSpace X
inst_3 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x : TopologicalSpace (X ⊕ Y) := UniformSpace.toTopologicalSpace
h : ∀ (x : Z), (toGlueL hΦ hΨ ∘ Φ) x = (toGlueR hΦ hΨ ∘ Ψ) x
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ

Tactic:
funext