awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Perfect (goal)
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst_1 : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E : Set α // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → (hC : Perfect C) → (hnonempty : C.Nonempty) → {ε : ℝ≥0∞} → (hε : 0 < ε) → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 (C := C) hC hnonempty hε) ∧
      (C0 (C := C) hC hnonempty hε).Nonempty ∧ C0 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C0 (C := C) hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 (C := C) hC hnonempty hε) ∧
      (C1 (C := C) hC hnonempty hε).Nonempty ∧ C1 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C1 (C := C) hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 (C := C) hC hnonempty hε) (C1 (C := C) hC hnonempty hε)
DP : List Bool → P :=
  fun (l : List Bool) ↦
    List.rec (motive := fun (l : List Bool) ↦ P) (Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty) C ⋯)
      (fun (a : Bool) (l : List Bool) (ih : P) ↦
        Bool.casesOn (motive := fun (t : Bool) ↦ (h : a = t) → P) a
          (fun (h : a = false) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C0 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          (fun (h : a = true) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C1 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          ⋯)
      l
D : List Bool → Set α := fun (l : List Bool) ↦ (↑(DP l) : Set α)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
refine_1 :
  (range fun (x : ℕ → Bool) ↦
      (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
        (Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α))
          x ⋯)) ⊆
    C
refine_2 :
  Continuous.{0, u_1} (Y := α) fun (x : ℕ → Bool) ↦
    (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
      (Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x
        ⋯)
⊢ ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f
have refine_3 : Injective.{1, u_1 + 1} (β := α) fun (x : ℕ → Bool) ↦
  (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
    (Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x
      sorry)
Tactic: refine ⟨fun x => (inducedMap D).2 ⟨x, hdom⟩, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Perfect (goal)
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst_1 : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E : Set α // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → (hC : Perfect C) → (hnonempty : C.Nonempty) → {ε : ℝ≥0∞} → (hε : 0 < ε) → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 (C := C) hC hnonempty hε) ∧
      (C0 (C := C) hC hnonempty hε).Nonempty ∧ C0 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C0 (C := C) hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 (C := C) hC hnonempty hε) ∧
      (C1 (C := C) hC hnonempty hε).Nonempty ∧ C1 (C := C) hC hnonempty hε ⊆ C ∧ ediam (C1 (C := C) hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 (C := C) hC hnonempty hε) (C1 (C := C) hC hnonempty hε)
DP : List Bool → P :=
  fun (l : List Bool) ↦
    List.rec (motive := fun (l : List Bool) ↦ P) (Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty) C ⋯)
      (fun (a : Bool) (l : List Bool) (ih : P) ↦
        Bool.casesOn (motive := fun (t : Bool) ↦ (h : a = t) → P) a
          (fun (h : a = false) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C0 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          (fun (h : a = true) ↦
            Subtype.mk (p := fun (E : Set α) ↦ Perfect E ∧ E.Nonempty)
              (C1 (C := (↑ih : Set α)) ⋯ ⋯ (ε := u (l.length + 1)) ⋯) ⋯)
          ⋯)
      l
D : List Bool → Set α := fun (l : List Bool) ↦ (↑(DP l) : Set α)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
⊢ Continuous.{0, u_1} (Y := α) fun (x : ℕ → Bool) ↦
    (inducedMap D).snd (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)
      (Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x
        ⋯)
have refine_2 : Continuous (Y := (↑((inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) : Type)) fun (x : ℕ → Bool) ↦
  Subtype.mk (p := fun (x : ℕ → Bool) ↦ x ∈ (inducedMap D).fst (β := fun (s : Set (ℕ → Bool)) ↦ (↑s : Type) → α)) x sorry
Tactic: apply hdiam.map_continuous.comp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace α := TopologicalSpace.upgradeIsCompletelyMetrizable α
⊢ ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f
have obtain : ∀ (D : Set α) (hD : Perfect D) (Dnonempty : D.Nonempty) (hDC : D ⊆ C),
  ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f
Tactic: obtain ⟨D, hD, Dnonempty, hDC⟩ := exists_perfect_nonempty_of_isClosed_of_not_countable hC hunc
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Perfect (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace α := TopologicalSpace.upgradeIsCompletelyMetrizable α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
⊢ ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f
have obtain : ∀ (f : (ℕ → Bool) → α) (hfD : range f ⊆ D) (hf : Continuous f ∧ Injective f),
  ∃ (f : (ℕ → Bool) → α), range f ⊆ C ∧ Continuous f ∧ Injective f
Tactic: obtain ⟨f, hfD, hf⟩ := hD.exists_nat_bool_injection Dnonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ Ne (α := E (firstDiff (E := E) x y)) (x (firstDiff (E := E) x y)) (y (firstDiff (E := E) x y))
have rw : Ne (α := E (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) sorry)) (x (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) sorry))
  (y (Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) sorry))
Tactic: rw [firstDiff_def, dif_pos h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n < firstDiff (E := E) x y
⊢ x n = y n
have hn₁ : n < if h : x ≠ y then Nat.find (p := fun (n : ℕ) ↦ x n ≠ y n) sorry else 0
Tactic: rw [firstDiff_def] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
⊢ min (firstDiff (E := E) x y) (firstDiff (E := E) y z) ≤ firstDiff (E := E) x z
have by_contra! : ∀ (H : firstDiff (E := E) x z < min (firstDiff (E := E) x y) (firstDiff (E := E) y z)), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff (E := E) x z < min (firstDiff (E := E) x y) (firstDiff (E := E) y z)
⊢ False
have H₁ : firstDiff (E := E) x z < firstDiff (E := E) x y ∧ firstDiff (E := E) x z < firstDiff (E := E) y z
Tactic: rw [lt_min_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff (E := E) x z < firstDiff (E := E) x y ∧ firstDiff (E := E) x z < firstDiff (E := E) y z
⊢ False
have refine : Eq (α := E (firstDiff (E := E) x z)) (x (firstDiff (E := E) x z)) (z (firstDiff (E := E) x z))
Tactic: refine apply_firstDiff_ne h ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
⊢ cylinder (E := E) x n = (↑(Finset.range n) : Set ℕ).pi (α := E) fun (i : ℕ) ↦ {x i}
have h : ∀ (y : (n : ℕ) → E n),
  y ∈ cylinder (E := E) x n ↔
    Membership.mem (γ := Set ((n : ℕ) → E n)) ((↑(Finset.range n) : Set ℕ).pi (α := E) fun (i : ℕ) ↦ {x i}) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder (E := E) x n ↔ cylinder (E := E) y n = cylinder (E := E) x n
have mp : y ∈ cylinder (E := E) x n → cylinder (E := E) y n = cylinder (E := E) x n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
mp : y ∈ cylinder (E := E) x n → cylinder (E := E) y n = cylinder (E := E) x n
⊢ y ∈ cylinder (E := E) x n ↔ cylinder (E := E) y n = cylinder (E := E) x n
have mpr : cylinder (E := E) y n = cylinder (E := E) x n → y ∈ cylinder (E := E) x n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder (E := E) x n
⊢ cylinder (E := E) y n = cylinder (E := E) x n
have mp : cylinder (E := E) y n ⊆ cylinder (E := E) x n
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder (E := E) x n
mp : cylinder (E := E) y n ⊆ cylinder (E := E) x n
⊢ cylinder (E := E) y n = cylinder (E := E) x n
have mp₁ : cylinder (E := E) x n ⊆ cylinder (E := E) y n
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder (E := E) x n
z : (n : ℕ) → E n
hz : z ∈ cylinder (E := E) y n
i : ℕ
hi : i < n
⊢ z i = x i
have mp : z i = y i
Tactic: rw [← hy i hi]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder (E := E) x n
z : (n : ℕ) → E n
hz : z ∈ cylinder (E := E) x n
i : ℕ
hi : i < n
⊢ z i = y i
have mp : z i = x i
Tactic: rw [hy i hi]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : cylinder (E := E) y n = cylinder (E := E) x n
⊢ y ∈ cylinder (E := E) x n
have mpr : y ∈ cylinder (E := E) y n
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder (E := E) y i ↔ i ≤ firstDiff (E := E) x y
have mp : x ∈ cylinder (E := E) y i → i ≤ firstDiff (E := E) x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
mp : x ∈ cylinder (E := E) y i → i ≤ firstDiff (E := E) x y
⊢ x ∈ cylinder (E := E) y i ↔ i ≤ firstDiff (E := E) x y
have mpr : i ≤ firstDiff (E := E) x y → x ∈ cylinder (E := E) y i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder (E := E) y i
⊢ i ≤ firstDiff (E := E) x y
have mp : ∀ (this : firstDiff (E := E) x y < i), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff (E := E) x y
⊢ cylinder (E := E) x n = cylinder (E := E) y n
have rw : x ∈ cylinder (E := E) y n
Tactic: rw [← mem_cylinder_iff_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
⊢ ⋃ (k : E n), cylinder (E := E) (update (β := E) x n k) (n + 1) = cylinder (E := E) x n
have h : ∀ (y : (n : ℕ) → E n),
  Membership.mem (γ := Set ((n : ℕ) → E n)) (⋃ (k : E n), cylinder (E := E) (update (β := E) x n k) (n + 1)) y ↔
    y ∈ cylinder (E := E) x n
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ Membership.mem (γ := Set ((n : ℕ) → E n)) (⋃ (k : E n), cylinder (E := E) (update (β := E) x n k) (n + 1)) y ↔
    y ∈ cylinder (E := E) x n
have h : (∃ (i : E n), ∀ i_1 < n + 1, y i_1 = update (β := E) x n i i_1) ↔ ∀ i < n, y i = x i
Tactic: simp only [mem_cylinder_iff, mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ (i : E n), ∀ i_1 < n + 1, y i_1 = update (β := E) x n i i_1) ↔ ∀ i < n, y i = x i
have h : (∃ (i : E n), ∀ i_1 < n + 1, y i_1 = update (β := E) x n i i_1) → ∀ i < n, y i = x i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
h : (∃ (i : E n), ∀ i_1 < n + 1, y i_1 = update (β := E) x n i i_1) → ∀ i < n, y i = x i
⊢ (∃ (i : E n), ∀ i_1 < n + 1, y i_1 = update (β := E) x n i i_1) ↔ ∀ i < n, y i = x i
have h₁ : (∀ i < n, y i = x i) → ∃ (i : E n), ∀ i_1 < n + 1, y i_1 = update (β := E) x n i i_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
⊢ ∃ (i : E n), ∀ i_1 < n + 1, y i_1 = update (β := E) x n i i_1
have h : ∀ (i : ℕ) (hi : i < n + 1), y i = update (β := E) x n (y n) i
Tactic: refine ⟨y n, fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
⊢ y i = update (β := E) x n (y n) i
have h : ∀ (h'i : i < n), y i = update (β := E) x n (y n) i
Tactic: rcases Nat.lt_succ_iff_lt_or_eq.1 hi with (h'i | rfl)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
h : ∀ (h'i : i < n), y i = update (β := E) x n (y n) i
⊢ y i = update (β := E) x n (y n) i
have h₁ : ∀ (H : ∀ i_1 < i, y i_1 = x i_1) (hi : i < i + 1), y i = update (β := E) x i (y i) i
Tactic: rcases Nat.lt_succ_iff_lt_or_eq.1 hi with (h'i | rfl)
Cleared hypotheses: n, H, hi
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
⊢ (res x n).length = n
have zero : (res x 0).length = 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
zero : (res x 0).length = 0
⊢ (res x n).length = n
have succ : ∀ (n : ℕ), (res x n).length = n → (res x (n + 1)).length = n + 1
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
⊢ res x n = res y n ↔ ∀ ⦃m : ℕ⦄, m < n → x m = y m
have mp : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
mp : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
⊢ res x n = res y n ↔ ∀ ⦃m : ℕ⦄, m < n → x m = y m
have mpr : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
ih : ∀ (h : res x n = res y n) ⦃m : ℕ⦄, m < n → x m = y m
h : res x (n + 1) = res y (n + 1)
m : ℕ
hm : m < n + 1
⊢ x m = y m
have hm₁ : m < n ∨ m = n
Tactic: rw [Nat.lt_succ_iff_lt_or_eq] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
ih : ∀ (h : res x n = res y n) ⦃m : ℕ⦄, m < n → x m = y m
h : res x (n + 1) = res y (n + 1)
m : ℕ
hm : m < n ∨ m = n
⊢ x m = y m
have h₁ : x n = y n ∧ res x n = res y n
Tactic: simp only [res_succ, cons.injEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
ih : ∀ (h : res x n = res y n) ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
hm : m < n ∨ m = n
h : x n = y n ∧ res x n = res y n
⊢ x m = y m
have mp : ∀ (hm : m < n), x m = y m
Tactic: rcases hm with hm | hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
ih : ∀ (h : res x n = res y n) ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
hm : m < n ∨ m = n
h : x n = y n ∧ res x n = res y n
mp : ∀ (hm : m < n), x m = y m
⊢ x m = y m
have mp₁ : ∀ (hm : m = n), x m = y m
Tactic: rcases hm with hm | hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
ih : ∀ (h : res x n = res y n) ⦃m : ℕ⦄, m < n → x m = y m
m : ℕ
h : x n = y n ∧ res x n = res y n
hm : m = n
⊢ x m = y m
have mp : x n = y n
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
h : res x n = res y n
⊢ ∀ ⦃m : ℕ⦄, m < n → x m = y m
have mp : ∀ (h : res x 0 = res y 0) ⦃m : ℕ⦄, m < 0 → x m = y m
Tactic: induction n with
    | zero => simp
    | succ n ih =>
      intro m hm
      rw [Nat.lt_succ_iff_lt_or_eq] at hm
      simp only [res_succ, cons.injEq] at h
      rcases hm with hm | hm
      · exact ih h.2 hm
      rw [hm]
      exact h.1
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
h : res x n = res y n
mp : ∀ (h : res x 0 = res y 0) ⦃m : ℕ⦄, m < 0 → x m = y m
⊢ ∀ ⦃m : ℕ⦄, m < n → x m = y m
have mp₁ : ∀ (n : ℕ) (ih : ∀ (h : res x n = res y n) ⦃m : ℕ⦄, m < n → x m = y m) (h : res x (n + 1) = res y (n + 1)) ⦃m : ℕ⦄,
  m < n + 1 → x m = y m
Tactic: induction n with
    | zero => simp
    | succ n ih =>
      intro m hm
      rw [Nat.lt_succ_iff_lt_or_eq] at hm
      simp only [res_succ, cons.injEq] at h
      rcases hm with hm | hm
      · exact ih h.2 hm
      rw [hm]
      exact h.1
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
ih : ∀ (h : ∀ ⦃m : ℕ⦄, m < n → x m = y m), res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < n + 1 → x m = y m
⊢ res x (n + 1) = res y (n + 1)
have mpr : x n = y n ∧ res x n = res y n
Tactic: simp only [res_succ, cons.injEq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
ih : ∀ (h : ∀ ⦃m : ℕ⦄, m < n → x m = y m), res x n = res y n
h : ∀ ⦃m : ℕ⦄, m < n + 1 → x m = y m
⊢ x n = y n ∧ res x n = res y n
have mpr : ∀ (m : ℕ) (hm : m < n), x m = y m
Tactic: refine ⟨h (Nat.lt_succ_self _), ih fun m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
h : ∀ ⦃m : ℕ⦄, m < n → x m = y m
⊢ res x n = res y n
have mpr : ∀ (h : ∀ ⦃m : ℕ⦄, m < 0 → x m = y m), res x 0 = res y 0
Tactic: induction n with
    | zero => simp
    | succ n ih =>
      simp only [res_succ, cons.injEq]
      refine ⟨h (Nat.lt_succ_self _), ih fun m hm => ?_⟩
      exact h (hm.trans (Nat.lt_succ_self _))
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
h : ∀ ⦃m : ℕ⦄, m < n → x m = y m
mpr : ∀ (h : ∀ ⦃m : ℕ⦄, m < 0 → x m = y m), res x 0 = res y 0
⊢ res x n = res y n
have mpr₁ : ∀ (n : ℕ) (ih : ∀ (h : ∀ ⦃m : ℕ⦄, m < n → x m = y m), res x n = res y n) (h : ∀ ⦃m : ℕ⦄, m < n + 1 → x m = y m),
  res x (n + 1) = res y (n + 1)
Tactic: induction n with
    | zero => simp
    | succ n ih =>
      simp only [res_succ, cons.injEq]
      refine ⟨h (Nat.lt_succ_self _), ih fun m hm => ?_⟩
      exact h (hm.trans (Nat.lt_succ_self _))
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
h : res x = res y
⊢ x = y
have h₁ : ∀ (n : ℕ), x n = y n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ x n = y n
have apply : res x n.succ = res y n.succ
Tactic: apply res_eq_res.mp _ (Nat.lt_succ_self _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ res x n.succ = res y n.succ
have rw : res y n.succ = res y n.succ
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
⊢ cylinder (E := fun (n : ℕ) ↦ α) x n = {y : ℕ → α | res y n = res x n}
have h : ∀ (y : (n : ℕ) → α),
  y ∈ cylinder (E := fun (n : ℕ) ↦ α) x n ↔ Membership.mem (γ := Set ((n : ℕ) → α)) {y : ℕ → α | res y n = res x n} y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
y : (n : ℕ) → α
⊢ y ∈ cylinder (E := fun (n : ℕ) ↦ α) x n ↔ Membership.mem (γ := Set ((n : ℕ) → α)) {y : ℕ → α | res y n = res x n} y
have h : (∀ i < n, y i = x i) ↔ res y n = res x n
Tactic: dsimp [cylinder]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
y : (n : ℕ) → α
⊢ (∀ i < n, y i = x i) ↔ res y n = res x n
have h : (∀ i < n, y i = x i) ↔ ∀ ⦃m : ℕ⦄, m < n → y m = x m
Tactic: rw [res_eq_res]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ 0 ≤ dist x y
have inl : 0 ≤ dist x x
Tactic: rcases eq_or_ne x y with (rfl | h)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
inl : 0 ≤ dist x x
⊢ 0 ≤ dist x y
have inr : ∀ (h : x ≠ y), 0 ≤ dist x y
Tactic: rcases eq_or_ne x y with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x y ≤ 1
have inl : dist x x ≤ 1
Tactic: rcases eq_or_ne x y with (rfl | h)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
inl : dist x x ≤ 1
⊢ dist x y ≤ 1
have inr : ∀ (h : x ≠ y), dist x y ≤ 1
Tactic: rcases eq_or_ne x y with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ dist x y ≤ 1
have inr : (HPow.hPow (α := ℝ) 2 (firstDiff (E := E) x y))⁻¹ ≤ 1
Tactic: simp only [dist, ne_eq, h, not_false_eq_true, ↓reduceIte, one_div, inv_pow]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
⊢ dist x z ≤ max (dist x y) (dist y z)
have inl : dist x x ≤ max (dist x y) (dist y x)
Tactic: rcases eq_or_ne x z with (rfl | hxz)
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
inl : dist x x ≤ max (dist x y) (dist y x)
⊢ dist x z ≤ max (dist x y) (dist y z)
have inr : ∀ (hxz : x ≠ z), dist x z ≤ max (dist x y) (dist y z)
Tactic: rcases eq_or_ne x z with (rfl | hxz)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ max (dist x y) (dist y z)
have inr : dist x z ≤ max (dist x x) (dist x z)
Tactic: rcases eq_or_ne x y with (rfl | hxy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
inr : dist x z ≤ max (dist x x) (dist x z)
⊢ dist x z ≤ max (dist x y) (dist y z)
have inr₁ : ∀ (hxy : x ≠ y), dist x z ≤ max (dist x y) (dist y z)
Tactic: rcases eq_or_ne x y with (rfl | hxy)