awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
⊢ 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
have 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
Tactic: rcases eq_or_ne i j with (rfl | hij)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
⊢ Sigma.mk (β := fun (i : ι) ↦ E i) i x = Sigma.mk (β := fun (i : ι) ↦ E i) j y
have apply : LT.lt (α := ℝ) 1 1
Tactic: apply (lt_irrefl (1 : ℝ) _).elim
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
⊢ Sigma.dist (E := E) (Sigma.mk (β := fun (k : ι) ↦ E k) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < 1
have rw : LT.lt (α := ℝ) 0 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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 (α := ℝ) 1 1
have E₁ : Sigma.dist (E := E) (Sigma.mk (β := fun (k : ι) ↦ E k) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) < 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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)
have simp : IsComplete (α := (i : ι) × E i) (range (Sigma.mk (β := fun (i : ι) ↦ E i) i))
Tactic: simp only [s, ← range_sigmaMk]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
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}
⊢ CompleteSpace ((i : ι) × E i)
have hc : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
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)
⊢ CompleteSpace ((i : ι) × E i)
have hd : ∀ (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)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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)
have refine : IsComplete (α := (i : ι) × E i) univ
Tactic: refine completeSpace_of_isComplete_univ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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) univ
have h : Eq (α := Set ((i : ι) × E i)) univ (⋃ (i : ι), s i)
Tactic: convert! isComplete_iUnion_separated hc (dist_mem_uniformity zero_lt_one) hd
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
have h : ∀ (x : Z), (toGlueL hΦ hΨ ∘ Φ) x = (toGlueR hΦ hΨ ∘ Ψ) x
Tactic: funext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
x_1 : Z
⊢ Eq (α := GlueSpace hΦ hΨ) (Quotient.mk'' (Sum.inl (Φ x_1))) (Quotient.mk'' (Sum.inr (Ψ x_1)))
have h : dist (Sum.inl (Φ x_1)) (Sum.inr (Ψ x_1)) = 0
Tactic: refine SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ 0
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ 0
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have obtain : ∀ (i : ℕ) (x : X i) (hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0),
  inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x) y =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
Tactic: obtain ⟨i, x⟩ := x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
y : (n : ℕ) × X n
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ 0
i : ℕ
x : X i
hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x) y =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have obtain : ∀ (j : ℕ) (y : X j) (hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0),
  inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y) =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).snd (β := fun (n : ℕ) ↦ X n)))
Tactic: obtain ⟨j, y⟩ := y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
i : ℕ
x : X i
hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
j : ℕ
y : X j
hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) i x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y) =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) i x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).snd (β := fun (n : ℕ) ↦ X n)))
have obtain : ∀ (x : X 0) (hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0),
  inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y) =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).snd (β := fun (n : ℕ) ↦ X n)))
Tactic: obtain rfl : i = 0 := nonpos_iff_eq_zero.1 hx
Cleared hypotheses: i, x, hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
j : ℕ
y : X j
hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
x : X 0
hx : (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).fst (β := fun (n : ℕ) ↦ X n) ≤ 0
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) j y) =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) j y).snd (β := fun (n : ℕ) ↦ X n)))
have obtain : ∀ (y : X 0) (hy : (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 y).fst (β := fun (n : ℕ) ↦ X n) ≤ 0),
  inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 y) =
    dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) 0 y).snd (β := fun (n : ℕ) ↦ X n)))
Tactic: obtain rfl : j = 0 := nonpos_iff_eq_zero.1 hy
Cleared hypotheses: j, y, hy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have pos : ∀ (h : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1),
  inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
Tactic: by_cases h : max x.1 y.1 = (m + 1)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
pos :
  ∀ (h : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1),
    inductiveLimitDist (X := X) f x y =
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have neg : ∀ (h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1),
  inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
Tactic: by_cases h : max x.1 y.1 = (m + 1)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have pos : ∀ (m' : ℕ) (hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m') (hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m')
  (h : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m'),
  inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
Tactic: generalize m + 1 = m' at *
Cleared hypotheses: hx, hy, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m m' : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m'
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m'
h : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m'
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have pos : ∀ (hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)))
  (hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))),
  inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
Tactic: subst m'
Cleared hypotheses: m', hx, hy, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
Tactic: have : max x.1 y.1 ≤ succ m := by simp [hx, hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have this₁ : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m
Tactic: have : max x.1 y.1 ≤ m := by simpa [h] using of_le_succ this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this_1 : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have xm : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
Tactic: have xm : x.1 ≤ m := le_trans (le_max_left _ _) this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this_1 : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m
xm : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have ym : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
Tactic: have ym : y.1 ≤ m := le_trans (le_max_right _ _) this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m + 1
h : ¬max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) = m + 1
this_1 : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m.succ
this : max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n)) ≤ m
xm : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
ym : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x y =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
have neg : inductiveLimitDist (X := X) f x y =
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) xm (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
    (leRecOn (C := fun (x : ℕ) ↦ X x) ym (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
Tactic: rw [leRecOn_succ xm, leRecOn_succ ym, (I m).dist_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
⊢ inductiveLimitDist (X := X) f x y = inductiveLimitDist (X := X) f y x
have hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
Tactic: have hx : x.1 ≤ m := le_max_left _ _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x y = inductiveLimitDist (X := X) f y x
have hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
Tactic: have hy : y.1 ≤ m := le_max_right _ _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x y = inductiveLimitDist (X := X) f y x
have rw : dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
    (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) =
  inductiveLimitDist (X := X) f y x
Tactic: rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y x m hy hx,
      dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
rw :
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) =
    inductiveLimitDist (X := X) f y x
⊢ inductiveLimitDist (X := X) f x y = inductiveLimitDist (X := X) f y x
have rw₁ : dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
    (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) =
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
    (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
Tactic: rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y x m hy hx,
      dist_comm]