awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
⊢ Eq (α := E (firstDiff (E := E) x z)) (y (firstDiff (E := E) x z)) (z (firstDiff (E := E) x z))

Tactic:
apply_eq_of_lt_firstDiff H.2

Premises used: And.right, PiNat.apply_eq_of_lt_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
⊢ Eq (α := E (firstDiff (E := E) x z)) (x (firstDiff (E := E) x z)) (z (firstDiff (E := E) x z))

Tactic:
calc
    x (firstDiff x z) = y (firstDiff x z) := apply_eq_of_lt_firstDiff H.1
    _ = z (firstDiff x z) := apply_eq_of_lt_firstDiff H.2

Premises used: PiNat.firstDiff, And.right, And.left, PiNat.apply_eq_of_lt_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
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
⊢ cylinder (E := E) x n = (↑(Finset.range n) : Set ℕ).pi (α := E) fun (i : ℕ) ↦ {x i}

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
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:
simp [cylinder]

Premises used: PiNat.cylinder
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ cylinder (E := E) x 0 = univ

Tactic:
simp [cylinder_eq_pi]

Premises used: PiNat.cylinder_eq_pi
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
m n : ℕ
h : m ≤ n
⊢ cylinder (E := E) x n ⊆ cylinder (E := E) x m

Tactic:
fun _y hy i hi => hy i (hi.trans_le h)

Premises used: Set.Mem, setOf, PiNat.cylinder, Set.Subset, LT.lt.trans_le
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder (E := E) x n ↔ ∀ i < n, y i = x i

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, PiNat.cylinder
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
⊢ x ∈ cylinder (E := E) x n

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
mpr : cylinder (E := E) y n = cylinder (E := E) x n → y ∈ cylinder (E := E) x n
⊢ y ∈ cylinder (E := E) x n ↔ cylinder (E := E) y n = cylinder (E := E) x n

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
mp₁ : cylinder (E := E) x n ⊆ cylinder (E := E) y n
⊢ cylinder (E := E) y n = cylinder (E := E) x n

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
mp : z i = y i
⊢ z i = x i

Tactic:
rw [← hy i hi]
-- Module: Mathlib.Topology.MetricSpace.PiNat
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 = y i

Tactic:
hz i hi
-- Module: Mathlib.Topology.MetricSpace.PiNat
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 = y i

Tactic:
exact hz i hi
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
mp : z i = x i
⊢ z i = y i

Tactic:
rw [hy i hi]
-- Module: Mathlib.Topology.MetricSpace.PiNat
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 = x i

Tactic:
hz i hi
-- Module: Mathlib.Topology.MetricSpace.PiNat
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 = x i

Tactic:
exact hz i hi
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : cylinder (E := E) y n = cylinder (E := E) x n
mpr : y ∈ cylinder (E := E) y n
⊢ y ∈ cylinder (E := E) x n

Tactic:
rw [← h]
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) y n

Tactic:
self_mem_cylinder _ _

Premises used: PiNat.self_mem_cylinder
-- Module: Mathlib.Topology.MetricSpace.PiNat
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) y n

Tactic:
exact self_mem_cylinder _ _

Premises used: PiNat.self_mem_cylinder
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder (E := E) x n ↔ x ∈ cylinder (E := E) y n

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
mpr : i ≤ firstDiff (E := E) x y → x ∈ cylinder (E := E) y i
⊢ x ∈ cylinder (E := E) y i ↔ i ≤ firstDiff (E := E) x y

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder (E := E) y i
mp : ∀ (this : firstDiff (E := E) x y < i), False
⊢ i ≤ firstDiff (E := E) x y

Tactic:
by_contra!
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder (E := E) y i
this : firstDiff (E := E) x y < i
⊢ False

Tactic:
apply_firstDiff_ne hne (h _ this)

Premises used: PiNat.apply_firstDiff_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder (E := E) y i
this : firstDiff (E := E) x y < i
⊢ False

Tactic:
exact apply_firstDiff_ne hne (h _ this)

Premises used: PiNat.apply_firstDiff_ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
hi : i ≤ firstDiff (E := E) x y
j : ℕ
hj : j < i
⊢ x j = y j

Tactic:
apply_eq_of_lt_firstDiff (hj.trans_le hi)

Premises used: LT.lt.trans_le, PiNat.apply_eq_of_lt_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
hi : i ≤ firstDiff (E := E) x y
j : ℕ
hj : j < i
⊢ x j = y j

Tactic:
exact apply_eq_of_lt_firstDiff (hj.trans_le hi)

Premises used: LT.lt.trans_le, PiNat.apply_eq_of_lt_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ x ∈ cylinder (E := E) y (firstDiff (E := E) x y)

Tactic:
fun _i hi =>
  apply_eq_of_lt_firstDiff hi

Premises used: Set.Mem, setOf, PiNat.cylinder, PiNat.apply_eq_of_lt_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff (E := E) x y
rw : x ∈ cylinder (E := E) y n
⊢ cylinder (E := E) x n = cylinder (E := E) y n

Tactic:
rw [← mem_cylinder_iff_eq]

Premises used: PiNat.mem_cylinder_iff_eq
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff (E := E) x y
i : ℕ
hi : i < n
⊢ x i = y i

Tactic:
apply_eq_of_lt_firstDiff (hi.trans_le hn)

Premises used: LT.lt.trans_le, PiNat.apply_eq_of_lt_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff (E := E) x y
i : ℕ
hi : i < n
⊢ x i = y i

Tactic:
exact apply_eq_of_lt_firstDiff (hi.trans_le hn)

Premises used: LT.lt.trans_le, PiNat.apply_eq_of_lt_firstDiff
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
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
⊢ ⋃ (k : E n), cylinder (E := E) (update (β := E) x n k) (n + 1) = cylinder (E := E) x n

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
⊢ 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:
simp only [mem_cylinder_iff, mem_iUnion]

Premises used: Set.mem_iUnion, PiNat.mem_cylinder_iff
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
h₁ : (∀ i < n, y i = x i) → ∃ (i : E n), ∀ i_1 < n + 1, y i_1 = update (β := E) x n i i_1
⊢ (∃ (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
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
k : E n
hk : ∀ i < n + 1, y i = update (β := E) x n k i
i : ℕ
hi : i < n
⊢ y i = x i

Tactic:
simpa [hi.ne] using hk i (Nat.lt_succ_of_lt hi)

Premises used: Nat.lt_succ_of_lt, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
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

Tactic:
⟨y n, fun i hi => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
h : ∀ (i : ℕ) (hi : i < n + 1), y i = update (β := E) x n (y n) i
⊢ ∃ (i : E n), ∀ i_1 < n + 1, y i_1 = update (β := E) x n i i_1

Tactic:
refine ⟨y n, fun i hi => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
h₁ : ∀ (H : ∀ i_1 < i, y i_1 = x i_1) (hi : i < i + 1), y i = update (β := E) x i (y i) i
⊢ y i = update (β := E) x n (y n) i

Tactic:
rcases Nat.lt_succ_iff_lt_or_eq.1 hi with (h'i | rfl)

Premises used: Iff.mp, Nat.lt_succ_iff_lt_or_eq, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
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'i : i < n
⊢ y i = update (β := E) x n (y n) i

Tactic:
simp [H i h'i, h'i.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
i : ℕ
H : ∀ i_1 < i, y i_1 = x i_1
hi : i < i + 1
⊢ y i = update (β := E) x i (y i) i

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : E n
i : ℕ
hi : i < n
⊢ update (β := E) x n y i = x i

Tactic:
simp [hi.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x : ℕ → α
⊢ res x 0 = []

Tactic:
rfl

Premises used: rfl, PiNat.res
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
⊢ res x n.succ = x n :: res x n

Tactic:
rfl

Premises used: rfl, PiNat.res
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
zero : (res x 0).length = 0
succ : ∀ (n : ℕ), (res x n).length = n → (res x (n + 1)).length = n + 1
⊢ (res x n).length = n

Tactic:
induction n
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x : ℕ → α
⊢ (res x 0).length = 0

Tactic:
simp [*]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
h : (res x n).length = n
⊢ (res x (n + 1)).length = n + 1

Tactic:
simp [*]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x y : ℕ → α
n : ℕ
mp : res x n = res y n → ∀ ⦃m : ℕ⦄, m < n → x m = y m
mpr : (∀ ⦃m : ℕ⦄, m < n → x m = y m) → res x n = res y n
⊢ res x n = res y n ↔ ∀ ⦃m : ℕ⦄, m < n → x m = y m

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x y : ℕ → α
h : res x 0 = res y 0
⊢ ∀ ⦃m : ℕ⦄, m < 0 → x m = y m

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
⊢ m < n ∨ m = n

Tactic:
rw [Nat.lt_succ_iff_lt_or_eq] at hm

Premises used: Nat.lt_succ_iff_lt_or_eq
-- Module: Mathlib.Topology.MetricSpace.PiNat
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 n = y n ∧ res x n = res y n

Tactic:
simp only [res_succ, cons.injEq] at h

Premises used: List.cons.injEq, PiNat.res_succ
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
mp₁ : ∀ (hm : m = n), x m = y m
⊢ x m = y m

Tactic:
rcases hm with hm | hm
-- Module: Mathlib.Topology.MetricSpace.PiNat
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

Tactic:
ih h.2 hm

Premises used: And.right
-- Module: Mathlib.Topology.MetricSpace.PiNat
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

Tactic:
exact ih h.2 hm

Premises used: And.right
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
mp : x n = y n
⊢ x m = y m

Tactic:
rw [hm]
-- Module: Mathlib.Topology.MetricSpace.PiNat
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 n = y n

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.PiNat
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 n = y n

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
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
⊢ ∀ ⦃m : ℕ⦄, m < n → 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

Premises used: List.cons.injEq, PiNat.res_succ, Nat.lt_succ_iff_lt_or_eq
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x y : ℕ → α
h : ∀ ⦃m : ℕ⦄, m < 0 → x m = y m
⊢ res x 0 = res y 0

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
mpr : x n = y n ∧ res x n = res y n
⊢ res x (n + 1) = res y (n + 1)

Tactic:
simp only [res_succ, cons.injEq]

Premises used: List.cons.injEq, PiNat.res_succ
-- Module: Mathlib.Topology.MetricSpace.PiNat
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

Tactic:
⟨h (Nat.lt_succ_self _), ih fun m hm => ?_⟩

Premises used: Nat.lt_succ_self, And.intro
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
mpr : ∀ (m : ℕ) (hm : m < n), x m = y m
⊢ x n = y n ∧ res x n = res y n

Tactic:
refine ⟨h (Nat.lt_succ_self _), ih fun m hm => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
m : ℕ
hm : m < n
⊢ x m = y m

Tactic:
h (hm.trans (Nat.lt_succ_self _))

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
m : ℕ
hm : m < n
⊢ x m = y m

Tactic:
exact h (hm.trans (Nat.lt_succ_self _))

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.Topology.MetricSpace.PiNat
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
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)
⊢ res x n = res y n

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 _))

Premises used: List.cons.injEq, PiNat.res_succ
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x y : ℕ → α
h : res x = res y
h₁ : ∀ (n : ℕ), x n = y n
⊢ x = y

Tactic:
ext n
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x y : ℕ → α
h : res x = res y
n : ℕ
apply : res x n.succ = res y n.succ
⊢ x n = y n

Tactic:
apply res_eq_res.mp _ (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self, Iff.mp, PiNat.res_eq_res
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x y : ℕ → α
h : res x = res y
n : ℕ
rw rw₁ : res y n.succ = res y n.succ
⊢ res x n.succ = res y n.succ

Tactic:
rw [h]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
h :
  ∀ (y : (n : ℕ) → α),
    y ∈ cylinder (E := fun (n : ℕ) ↦ α) x n ↔ Membership.mem (γ := Set ((n : ℕ) → α)) {y : ℕ → α | res y n = res x n} y
⊢ cylinder (E := fun (n : ℕ) ↦ α) x n = {y : ℕ → α | res y n = res x n}

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
y : (n : ℕ) → α
h : (∀ i < n, y i = x i) ↔ res y n = res x n
⊢ y ∈ cylinder (E := fun (n : ℕ) ↦ α) x n ↔ Membership.mem (γ := Set ((n : ℕ) → α)) {y : ℕ → α | res y n = res x n} y

Tactic:
dsimp [cylinder]

Premises used: PiNat.cylinder
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
α : Type u_2
x : ℕ → α
n : ℕ
y : (n : ℕ) → α
h h₁ : (∀ i < n, y i = x i) ↔ ∀ ⦃m : ℕ⦄, m < n → y m = x m
⊢ (∀ i < n, y i = x i) ↔ res y n = res x n

Tactic:
rw [res_eq_res]

Premises used: PiNat.res_eq_res
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ dist x y = (1 / 2) ^ firstDiff (E := E) x y

Tactic:
simp [dist, h]

Premises used: Dist.dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ dist x x = 0

Tactic:
simp [dist]

Premises used: Dist.dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x y = dist y x

Tactic:
simp [dist, @eq_comm _ x y, firstDiff_comm]

Premises used: eq_comm, PiNat.firstDiff_comm, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x y = dist y x

Tactic:
classical
  simp [dist, @eq_comm _ x y, firstDiff_comm]

Premises used: eq_comm, PiNat.firstDiff_comm, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
inl : 0 ≤ dist x x
inr : ∀ (h : x ≠ y), 0 ≤ dist x y
⊢ 0 ≤ dist x y

Tactic:
rcases eq_or_ne x y with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ 0 ≤ dist x x

Tactic:
simp [dist]

Premises used: Dist.dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ 0 ≤ dist x y

Tactic:
simp [dist, h]

Premises used: Dist.dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
inl : dist x x ≤ 1
inr : ∀ (h : x ≠ y), dist x y ≤ 1
⊢ dist x y ≤ 1

Tactic:
rcases eq_or_ne x y with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ dist x x ≤ 1

Tactic:
simp [dist]

Premises used: Dist.dist
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
inr : (HPow.hPow (α := ℝ) 2 (firstDiff (E := E) x y))⁻¹ ≤ 1
⊢ dist x y ≤ 1

Tactic:
simp only [dist, ne_eq, h, not_false_eq_true, ↓reduceIte, one_div, inv_pow]

Premises used: inv_pow, ne_eq, one_div, reduceIte, Dist.dist, not_false_eq_true
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ (HPow.hPow (α := ℝ) 2 (firstDiff (E := E) x y))⁻¹ ≤ 1

Tactic:
bound
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
inl : dist x x ≤ max (dist x y) (dist y x)
inr : ∀ (hxz : x ≠ z), dist x z ≤ max (dist x y) (dist y z)
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
rcases eq_or_ne x z with (rfl | hxz)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x x ≤ max (dist x y) (dist y x)

Tactic:
simp [PiNat.dist_self x, PiNat.dist_nonneg]

Premises used: PiNat.dist_nonneg, PiNat.dist_self
-- Module: Mathlib.Topology.MetricSpace.PiNat
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)
inr₁ : ∀ (hxy : x ≠ y), dist x z ≤ max (dist x y) (dist y z)
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
rcases eq_or_ne x y with (rfl | hxy)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x z : (n : ℕ) → E n
hxz : x ≠ z
⊢ dist x z ≤ max (dist x x) (dist x z)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
inr : ∀ (hxz : x ≠ y), dist x y ≤ max (dist x y) (dist y y)
inr₁ : ∀ (hyz : y ≠ z), dist x z ≤ max (dist x y) (dist y z)
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
rcases eq_or_ne y z with (rfl | hyz)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy hxz : x ≠ y
⊢ dist x y ≤ max (dist x y) (dist y y)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
hxz : x ≠ z
hxy : x ≠ y
hyz : y ≠ z
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
simp only [dist_eq_of_ne, hxz, hxy, hyz, inv_le_inv₀, one_div, inv_pow, zero_lt_two, Ne,
    not_false_iff, le_max_iff, pow_le_pow_iff_right₀, one_lt_two, pow_pos,
    min_le_iff.1 (min_firstDiff_le x y z hxz)]

Premises used: pow_pos, min_le_iff, Ne, inv_pow, PiNat.dist_eq_of_ne, one_div, Iff.mp, one_lt_two, pow_le_pow_iff_right₀, zero_lt_two, not_false_iff, PiNat.min_firstDiff_le, le_max_iff, inv_le_inv₀
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
⊢ dist x z ≤ dist x y + dist y z

Tactic:
calc
    dist x z ≤ max (dist x y) (dist y z) := dist_triangle_nonarch x y z
    _ ≤ dist x y + dist y z := max_le_add_of_nonneg (PiNat.dist_nonneg _ _) (PiNat.dist_nonneg _ _)

Premises used: Trans.trans, PiNat.dist_triangle_nonarch, PiNat.dist_nonneg, max_le_add_of_nonneg
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hxy : dist x y = 0
inl : ∀ (hxy : dist x x = 0), x = x
inr : ∀ (h : x ≠ y), x = y
⊢ x = y

Tactic:
rcases eq_or_ne x y with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
E : ℕ → Type u_1
x : (n : ℕ) → E n
hxy : dist x x = 0
⊢ x = x

Tactic:
rfl