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
z : E i
hij : i ≠ j
⊢ dist x z ≤ dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)
have dist : dist x z ≤ dist x sorry.some + 0 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + dist sorry.some z)
Tactic: calc
        dist x z ≤ dist x (Nonempty.some ⟨x⟩) + 0 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
          simpa only [zero_add, add_zero] using dist_triangle _ _ _
        _ ≤ _ := by apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]
-- 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
z : E i
hij : i ≠ j
dist : Dist.dist x z ≤ Dist.dist x ⋯.some + 0 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + Dist.dist ⋯.some z)
⊢ Dist.dist x z ≤ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some y + (Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z)
have dist₁ : Dist.dist x sorry.some + 0 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + Dist.dist sorry.some z) ≤
  Dist.dist x sorry.some + 1 + Dist.dist sorry.some y + (Dist.dist y sorry.some + 1 + Dist.dist sorry.some z)
Tactic: calc
        dist x z ≤ dist x (Nonempty.some ⟨x⟩) + 0 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
          simpa only [zero_add, add_zero] using dist_triangle _ _ _
        _ ≤ _ := by apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]
-- 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
k : ι
z : E k
hik : i ≠ k
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
have inr : ∀ (y : E i),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) i y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
Tactic: rcases eq_or_ne i j with (rfl | hij)
Cleared hypotheses: j, y
-- 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
k : ι
z : E k
hik : i ≠ k
inr :
  ∀ (y : E i),
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) +
        dist (Sigma.mk (β := fun (i : ι) ↦ E i) i y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
have inr₁ : ∀ (hij : i ≠ j),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
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
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) i y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
have inr : dist x sorry.some + 1 + dist sorry.some z ≤ dist x y + (dist y sorry.some + 1 + dist sorry.some z)
Tactic: simp only [Sigma.dist_ne hik, Sigma.dist_same]
-- 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
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x y + (dist y ⋯.some + 1 + dist ⋯.some z)
have dist : dist x sorry.some + 1 + dist sorry.some z ≤ dist x y + dist y sorry.some + 1 + dist sorry.some z
Tactic: calc
        dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
            dist x y + dist y (Nonempty.some ⟨y⟩) + 1 + dist (Nonempty.some ⟨z⟩) z := by
          apply_rules [add_le_add, le_rfl, dist_triangle]
        _ = _ := by abel
-- 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
k : ι
z : E k
hik : i ≠ k
y : E i
dist : Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤ Dist.dist x y + Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z
⊢ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤ Dist.dist x y + (Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z)
have dist₁ : Dist.dist x y + Dist.dist y sorry.some + 1 + Dist.dist sorry.some z =
  Dist.dist x y + (Dist.dist y sorry.some + 1 + Dist.dist sorry.some z)
Tactic: calc
        dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
            dist x y + dist y (Nonempty.some ⟨y⟩) + 1 + dist (Nonempty.some ⟨z⟩) z := by
          apply_rules [add_le_add, le_rfl, dist_triangle]
        _ = _ := by abel
-- 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
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
have inr : ∀ (z : E j) (hik : i ≠ j),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) j z)
Tactic: rcases eq_or_ne j k with (rfl | hjk)
Cleared hypotheses: k, z, hik
-- 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
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
inr :
  ∀ (z : E j) (hik : i ≠ j),
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j z) ≤
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
        dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) j z)
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
have inr₁ : ∀ (hjk : j ≠ k),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
Tactic: rcases eq_or_ne j k with (rfl | hjk)
-- 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
z : E j
hik : i ≠ j
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) j z)
have inr : dist x sorry.some + 1 + dist sorry.some z ≤ dist x sorry.some + 1 + dist sorry.some y + dist y z
Tactic: simp only [Sigma.dist_ne hij, Sigma.dist_same]
-- 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
z : E j
hik : i ≠ j
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + dist ⋯.some y + dist y z
have dist : dist x sorry.some + 1 + dist sorry.some z ≤ dist x sorry.some + 1 + (dist sorry.some y + dist y z)
Tactic: calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
              dist x (Nonempty.some ⟨x⟩) + 1 + (dist (Nonempty.some ⟨z⟩) y + dist y z) := by
            apply_rules [add_le_add, le_rfl, dist_triangle]
          _ = _ := by abel
-- 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
z : E j
hik : i ≠ j
dist : Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤ Dist.dist x ⋯.some + 1 + (Dist.dist ⋯.some y + Dist.dist y z)
⊢ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some y + Dist.dist y z
have dist₁ : Dist.dist x sorry.some + 1 + (Dist.dist sorry.some y + Dist.dist y z) =
  Dist.dist x sorry.some + 1 + Dist.dist sorry.some y + Dist.dist y z
Tactic: calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
              dist x (Nonempty.some ⟨x⟩) + 1 + (dist (Nonempty.some ⟨z⟩) y + dist y z) := by
            apply_rules [add_le_add, le_rfl, dist_triangle]
          _ = _ := by abel
-- 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
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
have inr : dist x sorry.some + 1 + dist sorry.some z ≤ dist x sorry.some + 1 + dist sorry.some y + (dist y sorry.some + 1 + dist sorry.some z)
Tactic: simp only [hik, hij, hjk, Sigma.dist_ne, Ne, not_false_iff]
-- 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
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)
have dist : dist x sorry.some + 1 + dist sorry.some z = dist x sorry.some + 1 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + dist sorry.some z)
Tactic: calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z =
              dist x (Nonempty.some ⟨x⟩) + 1 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
            simp only [add_zero, zero_add]
          _ ≤ _ := by apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]
-- 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
k : ι
z : E k
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
dist :
  Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z =
    Dist.dist x ⋯.some + 1 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + Dist.dist ⋯.some z)
⊢ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤
    Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some y + (Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z)
have dist₁ : Dist.dist x sorry.some + 1 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + Dist.dist sorry.some z) ≤
  Dist.dist x sorry.some + 1 + Dist.dist sorry.some y + (Dist.dist y sorry.some + 1 + Dist.dist sorry.some z)
Tactic: calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z =
              dist x (Nonempty.some ⟨x⟩) + 1 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
            simp only [add_zero, zero_add]
          _ ≤ _ := by apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen[instTopologicalSpaceSigma] s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
have mp : IsOpen[instTopologicalSpaceSigma] s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
mp : IsOpen[instTopologicalSpaceSigma] s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
⊢ IsOpen[instTopologicalSpaceSigma] s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
have mpr : (∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen[instTopologicalSpaceSigma] s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y < ε → y ∈ s
have mp : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s),
  ∃ ε > 0, ∀ (y : (i : ι) × E i), dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y < ε → y ∈ s
Tactic: obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s :=
      Metric.isOpen_iff.1 (isOpen_sigma_iff.1 hs i) x hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y < ε → y ∈ s
have mp : ∀ (y : (i : ι) × E i), dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y < min ε 1 → y ∈ s
Tactic: refine ⟨min ε 1, lt_min εpos 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)
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
⊢ Sigma.mk (β := fun (i : ι) ↦ E i) j y ∈ s
have 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
Tactic: rcases eq_or_ne i j with (rfl | hij)
Cleared hypotheses: j, y, hy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
⊢ Sigma.mk (β := fun (i : ι) ↦ E i) j y ∈ s
have mp₁ : ∀ (hij : i ≠ j), Sigma.mk (β := fun (i : ι) ↦ E i) j y ∈ s
Tactic: rcases eq_or_ne i j with (rfl | hij)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
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
⊢ Sigma.mk (β := fun (i : ι) ↦ E i) i y ∈ s
have hy₁ : dist x y < ε ∧ dist x y < 1
Tactic: simp only [Sigma.dist_same, lt_min_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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.mk (β := fun (i : ι) ↦ E i) j y ∈ s
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)
s : Set ((i : ι) × E i)
⊢ (∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen[instTopologicalSpaceSigma] s
have 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
Tactic: refine fun H => isOpen_sigma_iff.2 fun i => Metric.isOpen_iff.2 fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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, ball x ε ⊆ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
have 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
Tactic: obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ∀ y, dist (⟨i, x⟩ : Σ j, E j) y < ε → y ∈ s :=
      H ⟨i, x⟩ hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
have mpr : ∀ (y : E i) (hy : y ∈ ball x ε), y ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
Tactic: refine ⟨ε, εpos, fun y hy => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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 ε
⊢ y ∈ Sigma.mk (β := fun (i : ι) ↦ E i) i ⁻¹' s
have mpr : dist (Sigma.mk (β := fun (j : ι) ↦ E j) i x) (Sigma.mk (β := fun (j : ι) ↦ E j) i y) < ε
Tactic: apply hε ⟨i, y⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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 (Sigma.mk (β := fun (j : ι) ↦ E j) i x) (Sigma.mk (β := fun (j : ι) ↦ E j) i y) < ε
have mpr : dist x y < ε
Tactic: rw [Sigma.dist_same]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
⊢ MetricSpace ((i : ι) × E i)
have refine_1 : ∀ (x : (i : ι) × E i), Sigma.dist (E := E) x x = 0
Tactic: refine MetricSpace.ofDistTopology Sigma.dist ?_ ?_ Sigma.dist_triangle Sigma.isOpen_iff ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
⊢ MetricSpace ((i : ι) × E i)
have refine_2 : ∀ (x y : (i : ι) × E i), Sigma.dist (E := E) x y = Sigma.dist (E := E) y x
Tactic: refine MetricSpace.ofDistTopology Sigma.dist ?_ ?_ Sigma.dist_triangle Sigma.isOpen_iff ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
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
⊢ MetricSpace ((i : ι) × E i)
have refine_3 : ∀ (x y : (i : ι) × E i), Sigma.dist (E := E) x y = 0 → x = y
Tactic: refine MetricSpace.ofDistTopology Sigma.dist ?_ ?_ Sigma.dist_triangle Sigma.isOpen_iff ?_
-- 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
⊢ 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)
have 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)
Tactic: rcases eq_or_ne i j with (rfl | h)
Cleared hypotheses: j, y
-- 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_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)
⊢ 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)
have 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)
Tactic: rcases eq_or_ne i j with (rfl | 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
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)
have refine_2 : dist x sorry.some + 1 + dist y sorry.some = dist y sorry.some + 1 + dist x sorry.some
Tactic: simp only [Sigma.dist, dist_comm, h, h.symm, not_false_iff, dif_neg]
-- 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
⊢ 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 : ∀ (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: rcases eq_or_ne i j with (rfl | hij)
Cleared hypotheses: j, y