awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
refine_2 :
  ∀ (h₁₃ : i ≠ i₃) (h₂₃ : j ≠ i₃) (h₁₂ : i ≠ j) (h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃))
    (h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
refine_2₁ :
  ∀ (h₂₃ : i ≠ i₃) (h₁₃ : j ≠ i₃) (h₁₂ : j ≠ i) (h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃))
    (h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
have refine_2₂ : ∀ (h₁₂ : i ≠ i₂) (h₂₃ : i₂ ≠ j) (h₁₃ : i ≠ j) (h₁ : dist (t.points i) (t.points i₂) = dist (t.points i) (t.points j))
  (h₂ : dist (t.points i) (t.points i₂) = dist (t.points i₂) (t.points j)),
  dist (t.points i) (t.points j) = dist (t.points i) (t.points i₂)
Tactic: rcases hi with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: i₁, i₃, h₁₂, h₁₃, h₂₃, hi, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
refine_2 :
  ∀ (h₁₃ : i ≠ i₃) (h₂₃ : j ≠ i₃) (h₁₂ : i ≠ j) (h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃))
    (h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
refine_2₁ :
  ∀ (h₂₃ : i ≠ i₃) (h₁₃ : j ≠ i₃) (h₁₂ : j ≠ i) (h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃))
    (h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
refine_2₂ :
  ∀ (h₁₂ : i ≠ i₂) (h₂₃ : i₂ ≠ j) (h₁₃ : i ≠ j) (h₁ : dist (t.points i) (t.points i₂) = dist (t.points i) (t.points j))
    (h₂ : dist (t.points i) (t.points i₂) = dist (t.points i₂) (t.points j)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points i₂)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
have refine_2₃ : ∀ (h₂₃ : i₂ ≠ i) (h₁₂ : j ≠ i₂) (h₁₃ : j ≠ i) (h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i))
  (h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)),
  dist (t.points i) (t.points j) = dist (t.points j) (t.points i₂)
Tactic: rcases hi with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: i₁, i₃, h₁₂, h₁₃, h₂₃, hi, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
refine_2 :
  ∀ (h₁₃ : i ≠ i₃) (h₂₃ : j ≠ i₃) (h₁₂ : i ≠ j) (h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃))
    (h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
refine_2₁ :
  ∀ (h₂₃ : i ≠ i₃) (h₁₃ : j ≠ i₃) (h₁₂ : j ≠ i) (h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃))
    (h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
refine_2₂ :
  ∀ (h₁₂ : i ≠ i₂) (h₂₃ : i₂ ≠ j) (h₁₃ : i ≠ j) (h₁ : dist (t.points i) (t.points i₂) = dist (t.points i) (t.points j))
    (h₂ : dist (t.points i) (t.points i₂) = dist (t.points i₂) (t.points j)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points i₂)
refine_2₃ :
  ∀ (h₂₃ : i₂ ≠ i) (h₁₂ : j ≠ i₂) (h₁₃ : j ≠ i) (h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i))
    (h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)),
    dist (t.points i) (t.points j) = dist (t.points j) (t.points i₂)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
have refine_2₄ : ∀ (h₁₂ : i₁ ≠ i) (h₁₃ : i₁ ≠ j) (h₂₃ : i ≠ j) (h₁ : dist (t.points i₁) (t.points i) = dist (t.points i₁) (t.points j))
  (h₂ : dist (t.points i₁) (t.points i) = dist (t.points i) (t.points j)),
  dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i)
Tactic: rcases hi with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: i₂, i₃, h₁₂, h₁₃, h₂₃, hi, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
refine_2 :
  ∀ (h₁₃ : i ≠ i₃) (h₂₃ : j ≠ i₃) (h₁₂ : i ≠ j) (h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃))
    (h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
refine_2₁ :
  ∀ (h₂₃ : i ≠ i₃) (h₁₃ : j ≠ i₃) (h₁₂ : j ≠ i) (h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃))
    (h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
refine_2₂ :
  ∀ (h₁₂ : i ≠ i₂) (h₂₃ : i₂ ≠ j) (h₁₃ : i ≠ j) (h₁ : dist (t.points i) (t.points i₂) = dist (t.points i) (t.points j))
    (h₂ : dist (t.points i) (t.points i₂) = dist (t.points i₂) (t.points j)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points i₂)
refine_2₃ :
  ∀ (h₂₃ : i₂ ≠ i) (h₁₂ : j ≠ i₂) (h₁₃ : j ≠ i) (h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i))
    (h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)),
    dist (t.points i) (t.points j) = dist (t.points j) (t.points i₂)
refine_2₄ :
  ∀ (h₁₂ : i₁ ≠ i) (h₁₃ : i₁ ≠ j) (h₂₃ : i ≠ j) (h₁ : dist (t.points i₁) (t.points i) = dist (t.points i₁) (t.points j))
    (h₂ : dist (t.points i₁) (t.points i) = dist (t.points i) (t.points j)),
    dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
have refine_2₅ : ∀ (h₁₃ : i₁ ≠ i) (h₁₂ : i₁ ≠ j) (h₂₃ : j ≠ i) (h₁ : dist (t.points i₁) (t.points j) = dist (t.points i₁) (t.points i))
  (h₂ : dist (t.points i₁) (t.points j) = dist (t.points j) (t.points i)),
  dist (t.points i) (t.points j) = dist (t.points i₁) (t.points j)
Tactic: rcases hi with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
Cleared hypotheses: i₂, i₃, h₁₂, h₁₃, h₂₃, hi, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₂ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₂₃ : i₂ ≠ i
h₁₂ : j ≠ i₂
h₁₃ : j ≠ i
h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i)
h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i₂)
have refine_2 : dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
Tactic: rw [h₁, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₂ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₂₃ : i₂ ≠ i
h₁₂ : j ≠ i₂
h₁₃ : j ≠ i
h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i)
h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)
refine_2 : dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i₂)
have refine_2₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i)
Tactic: rw [h₁, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₁₂ : i₁ ≠ i
h₁₃ : i₁ ≠ j
h₂₃ : i ≠ j
h₁ : dist (t.points i₁) (t.points i) = dist (t.points i₁) (t.points j)
h₂ : dist (t.points i₁) (t.points i) = dist (t.points i) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i)
have refine_2 : dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
Tactic: rw [h₂, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₁₂ : i₁ ≠ i
h₁₃ : i₁ ≠ j
h₂₃ : i ≠ j
h₁ : dist (t.points i₁) (t.points i) = dist (t.points i₁) (t.points j)
h₂ : dist (t.points i₁) (t.points i) = dist (t.points i) (t.points j)
refine_2 : dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i)
have refine_2₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i)
Tactic: rw [h₂, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₁₃ : i₁ ≠ i
h₁₂ : i₁ ≠ j
h₂₃ : j ≠ i
h₁ : dist (t.points i₁) (t.points j) = dist (t.points i₁) (t.points i)
h₂ : dist (t.points i₁) (t.points j) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points j)
have refine_2 : dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
Tactic: rw [h₂, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₁₃ : i₁ ≠ i
h₁₂ : i₁ ≠ j
h₂₃ : j ≠ i
h₁ : dist (t.points i₁) (t.points j) = dist (t.points i₁) (t.points i)
h₂ : dist (t.points i₁) (t.points j) = dist (t.points j) (t.points i)
refine_2 : dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points j)
have refine_2₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i)
Tactic: rw [h₂, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NontriviallyNormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
F : IntermediateField K L
⊢ ∃ (x : ↥F), 1 < ‖x‖
have obtain : ∀ (k : K) (hk : 1 < ‖k‖), ∃ (x : ↥F), 1 < ‖x‖
Tactic: obtain ⟨k, hk⟩ := @NontriviallyNormedField.non_trivial K _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NontriviallyNormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
F : IntermediateField K L
k : K
hk : 1 < ‖k‖
⊢ ∃ (x : ↥F), 1 < ‖x‖
have h : 1 < norm.{u_2} (E := ↥F) ((algebraMap K ↥F : (a : K) → ↥F) k : ↥F)
Tactic: use algebraMap K F k
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Basic (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
⊢ CompactSpace (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
have rw : IsCompact (X := WeakDual 𝕜 A) (characterSpace 𝕜 A)
Tactic: rw [← isCompact_iff_compactSpace]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Basic (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A))
    (Set.preimage (β := StrongDual 𝕜 A) (⇑toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A)
      (Metric.closedBall 0 (norm.{u_2} (E := A) 1)))
    φ
have rw : norm (E := StrongDual 𝕜 A) ((toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A) φ : StrongDual 𝕜 A) ≤
  norm.{u_2} (E := A) 1
Tactic: rw [Set.mem_preimage, mem_closedBall_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Basic (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
⊢ IsCompact (X := WeakDual 𝕜 A) (characterSpace 𝕜 A)
have h : Subset (α := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A)
  (Set.preimage (β := StrongDual 𝕜 A) (⇑toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A)
    (Metric.closedBall 0 (norm.{u_2} (E := A) 1)))
Tactic: have h : characterSpace 𝕜 A ⊆ toStrongDual ⁻¹' Metric.closedBall 0 ‖(1 : A)‖ := by
    intro φ hφ
    rw [Set.mem_preimage, mem_closedBall_zero_iff]
    exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ :)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.DualNumber (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
inst_2 : UniformSpace R
inst_3 : IsTopologicalRing R
inst_4 : T2Space R
r : R
⊢ exp (HSMul.hSMul (β := R[ε]) r ε) = 1 + HSMul.hSMul (β := R[ε]) r ε
have rw : exp (HSMul.hSMul (β := R[ε]) r (inr 1)) = 1 + HSMul.hSMul (β := R[ε]) r (inr 1)
Tactic: rw [eps, ← inr_smul, exp_inr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.DualNumber (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
inst_2 : UniformSpace R
inst_3 : IsTopologicalRing R
inst_4 : T2Space R
r : R
rw : exp (HSMul.hSMul (β := R[ε]) r (inr 1)) = 1 + HSMul.hSMul (β := R[ε]) r (inr 1)
⊢ exp (HSMul.hSMul (β := R[ε]) r ε) = 1 + HSMul.hSMul (β := R[ε]) r ε
have rw₁ : exp (inr (HSMul.hSMul (β := R) r 1)) = HAdd.hAdd (α := R[ε]) 1 (inr (HSMul.hSMul (β := R) r 1))
Tactic: rw [eps, ← inr_smul, exp_inr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.DualNumber (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
inst_2 : UniformSpace R
inst_3 : IsTopologicalRing R
inst_4 : T2Space R
r : R
rw : exp (HSMul.hSMul (β := R[ε]) r (inr 1)) = 1 + HSMul.hSMul (β := R[ε]) r (inr 1)
rw₁ : exp (inr (HSMul.hSMul (β := R) r 1)) = HAdd.hAdd (α := R[ε]) 1 (inr (HSMul.hSMul (β := R) r 1))
⊢ exp (HSMul.hSMul (β := R[ε]) r ε) = 1 + HSMul.hSMul (β := R[ε]) r ε
have rw₂ : HAdd.hAdd (α := TrivSqZeroExt R R) 1 (inr (HSMul.hSMul (β := R) r 1)) =
  HAdd.hAdd (α := R[ε]) 1 (inr (HSMul.hSMul (β := R) r 1))
Tactic: rw [eps, ← inr_smul, exp_inr]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ofScalars 𝔸 fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹ : FormalMultilinearSeries 𝕂 𝔸 𝔸)
have simp_rw : ∀ (n : ℕ),
  Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (expSeries 𝕂 𝔸 n)
    (ofScalars 𝔸 (fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹) n)
Tactic: simp_rw [FormalMultilinearSeries.ext_iff, expSeries, ofScalars, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
simp_rw :
  ∀ (n : ℕ),
    Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (expSeries 𝕂 𝔸 n)
      (ofScalars 𝔸 (fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹) n)
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ofScalars 𝔸 fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹ : FormalMultilinearSeries 𝕂 𝔸 𝔸)
have simp_rw₁ : ∀ (n : ℕ),
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (↑n ! : 𝕂)⁻¹
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
    ofScalars 𝔸 (fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹) n
Tactic: simp_rw [FormalMultilinearSeries.ext_iff, expSeries, ofScalars, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
simp_rw :
  ∀ (n : ℕ),
    Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (expSeries 𝕂 𝔸 n)
      (ofScalars 𝔸 (fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹) n)
simp_rw₁ :
  ∀ (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (↑n ! : 𝕂)⁻¹
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
      ofScalars 𝔸 (fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹) n
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ofScalars 𝔸 fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹ : FormalMultilinearSeries 𝕂 𝔸 𝔸)
have simp_rw₂ : ∀ (n : ℕ), True
Tactic: simp_rw [FormalMultilinearSeries.ext_iff, expSeries, ofScalars, implies_true]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)
x : 𝔸
⊢ exp x = 1
have rw : Eq.{u_2 + 1} (α := 𝔸)
  (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
  else 1)
  1
Tactic: rw [exp, dif_neg (not_nonempty_iff.mpr ‹_›)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)
x : 𝔸
rw :
  Eq.{u_2 + 1} (α := 𝔸)
    (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
    else 1)
    1
⊢ exp x = 1
have rw₁ : Eq.{u_2 + 1} (α := 𝔸) 1 1
Tactic: rw [exp, dif_neg (not_nonempty_iff.mpr ‹_›)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : Algebra ℚ 𝔸
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) =
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸)
have h : ∀ (x : 𝔸),
  FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : Algebra ℚ 𝔸
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
have h : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
  (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n))
Tactic: simp_rw [expSeries_sum_eq, inv_natCast_smul_eq 𝕂 ℚ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : Algebra ℚ 𝔸
n : ℕ
⊢ Eq (α := (a : (i : Fin n) → 𝔸) → 𝔸) (⇑(expSeries 𝕂 𝔸 n) : (a : (i : Fin n) → 𝔸) → 𝔸)
    (⇑(expSeries ℚ 𝔸 n) : (a : (i : Fin n) → 𝔸) → 𝔸)
have h : ∀ (c : (i : Fin n) → 𝔸),
  Eq (α := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) c : 𝔸)
    ((expSeries ℚ 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) c : 𝔸)
Tactic: ext c
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
⊢ exp = FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸)
have h : ∀ (x : 𝔸), exp x = FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
⊢ exp x = FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
have h : (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
  else 1) =
  FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
Tactic: rw [exp, dif_pos ⟨RestrictScalars.algebra ℚ 𝕂 𝔸⟩, ← @expSeries_sum_eq_rat (𝕂 := 𝕂)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Exponential (goal)
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
h :
  (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
    else 1) =
    FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
⊢ exp x = FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
have h₁ : FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x =
  FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
Tactic: rw [exp, dif_pos ⟨RestrictScalars.algebra ℚ 𝕂 𝔸⟩, ← @expSeries_sum_eq_rat (𝕂 := 𝕂)]