awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
have neg : Ne.{u_1 + 1} (α := 𝕜) 1 0
Tactic: rw [← mul_eq_one_iff_eq_inv₀ (h₁.meromorphicTrailingCoeffAt_ne_zero h₂),
      ← h₁.inv.meromorphicTrailingCoeffAt_mul h₁, meromorphicTrailingCoeffAt_congr_nhdsNE this,
      analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
neg : Ne.{u_1 + 1} (α := 𝕜) 1 0
⊢ meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹
have neg₁ : (𝓝[≠] x).EventuallyEq (β := 𝕜) 1 fun (z : 𝕜) ↦ HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - x) 0) 1
Tactic: rw [← mul_eq_one_iff_eq_inv₀ (h₁.meromorphicTrailingCoeffAt_ne_zero h₂),
      ← h₁.inv.meromorphicTrailingCoeffAt_mul h₁, meromorphicTrailingCoeffAt_congr_nhdsNE this,
      analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ (𝓝[≠] x).EventuallyEq (β := 𝕜) 1 fun (z : 𝕜) ↦ HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - x) 0) 1
have neg : (𝓝[≠] x).EventuallyEq (β := 𝕜) 1 fun (z : 𝕜) ↦ 1
Tactic: simp only [zpow_zero, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have neg : ∀ (h₂ : ¬meromorphicOrderAt f x = ⊤), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have pos : ∀ (h₃ : n = 0), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
Tactic: by_cases h₃ : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
pos : ∀ (h₃ : n = 0), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have neg : ∀ (h₃ : ¬n = 0), meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
Tactic: by_cases h₃ : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
h₃ : n = 0
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have pos : Eq (α := 𝕜) (meromorphicTrailingCoeffAt 1 x) 1
Tactic: simp only [h₃, zpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have neg : ∀ (g : 𝕜 → 𝕜) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
  (h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z),
  meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have neg : (g ^ n) x = g x ^ n
Tactic: rw [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
        (n := (meromorphicOrderAt f x).untop₀) h₂g h₃g,
      (h₁g.zpow h₂g (n := n)).meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
        (n := (meromorphicOrderAt (f ^ n) x).untop₀)
        (by simp_all [zpow_ne_zero])]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
neg : (g ^ n) x = g x ^ n
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have neg₁ : f ^ n =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (f ^ n) x).untop₀ • (g ^ n) z
Tactic: rw [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
        (n := (meromorphicOrderAt f x).untop₀) h₂g h₃g,
      (h₁g.zpow h₂g (n := n)).meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
        (n := (meromorphicOrderAt (f ^ n) x).untop₀)
        (by simp_all [zpow_ne_zero])]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
g : 𝕜 → 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ f ^ n =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (f ^ n) x).untop₀ • (g ^ n) z
have h : ∀ (a : 𝕜) (ha : f a = (a - x) ^ (meromorphicOrderAt f x).untop₀ • g a),
  (f ^ n) a = (a - x) ^ (meromorphicOrderAt (f ^ n) x).untop₀ • (g ^ n) a
Tactic: filter_upwards [h₃g] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have h : f ^ n = HPow.hPow (β := ℤ) f (↑n : ℤ)
Tactic: convert! h₁.meromorphicTrailingCoeffAt_zpow (n := n)
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.TrailingCoefficient (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h : f ^ n = HPow.hPow (β := ℤ) f (↑n : ℤ)
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n
have h₂ : meromorphicTrailingCoeffAt f x ^ n = HPow.hPow (β := ℤ) (meromorphicTrailingCoeffAt f x) (↑n : ℤ)
Tactic: convert! h₁.meromorphicTrailingCoeffAt_zpow (n := n)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist ((homothety p₁ c : (a : P) → P) p₂) p₁ = ‖c‖ * dist p₁ p₂
have rw : dist p₁ ((homothety p₁ c : (a : P) → P) p₂) = ‖c‖ * dist p₁ p₂
Tactic: rw [dist_comm, dist_center_homothety]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
rw : dist p₁ ((homothety p₁ c : (a : P) → P) p₂) = ‖c‖ * dist p₁ p₂
⊢ dist ((homothety p₁ c : (a : P) → P) p₂) p₁ = ‖c‖ * dist p₁ p₂
have rw₁ : ‖c‖ * dist p₁ p₂ = ‖c‖ * dist p₁ p₂
Tactic: rw [dist_comm, dist_center_homothety]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
p₁ p₂ : P
c₁ c₂ : 𝕜
⊢ dist.{u_2} (α := P) ((lineMap p₁ p₂ : (a : 𝕜) → P) c₁ : P) ((lineMap p₁ p₂ : (a : 𝕜) → P) c₂ : P) =
    dist c₁ c₂ * dist p₁ p₂
have rw : dist.{u_2} (α := P) ((lineMap p₁ p₂ : (a : 𝕜) → P) c₁ : P) ((lineMap p₁ p₂ : (a : 𝕜) → P) c₂ : P) =
  dist c₁ c₂ * dist p₂ p₁
Tactic: rw [dist_comm p₁ p₂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist ((homothety p₁ c : (a : P) → P) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂
have rw : dist ((lineMap p₁ p₂ : (a : 𝕜) → P) c) p₂ = ‖1 - c‖ * dist p₁ p₂
Tactic: rw [homothety_eq_lineMap, dist_lineMap_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
rw : dist ((lineMap p₁ p₂ : (a : 𝕜) → P) c) p₂ = ‖1 - c‖ * dist p₁ p₂
⊢ dist ((homothety p₁ c : (a : P) → P) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂
have rw₁ : ‖1 - c‖ * dist p₁ p₂ = ‖1 - c‖ * dist p₁ p₂
Tactic: rw [homothety_eq_lineMap, dist_lineMap_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist p₂ ((homothety p₁ c : (a : P) → P) p₂) = ‖1 - c‖ * dist p₁ p₂
have rw : dist ((homothety p₁ c : (a : P) → P) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂
Tactic: rw [dist_comm, dist_homothety_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
rw : dist ((homothety p₁ c : (a : P) → P) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂
⊢ dist p₂ ((homothety p₁ c : (a : P) → P) p₂) = ‖1 - c‖ * dist p₁ p₂
have rw₁ : ‖1 - c‖ * dist p₁ p₂ = ‖1 - c‖ * dist p₁ p₂
Tactic: rw [dist_comm, dist_homothety_self]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw : dist p₁ ((lineMap p₁ p₂ : (a : 𝕜) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
  (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
rw :
  dist p₁ ((lineMap p₁ p₂ : (a : 𝕜) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw₁ : dist ((lineMap p₁ p₂ : (a : 𝕜) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) p₁ =
  (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
rw :
  dist p₁ ((lineMap p₁ p₂ : (a : 𝕜) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
rw₁ :
  dist ((lineMap p₁ p₂ : (a : 𝕜) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) p₁ =
    (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw₂ : norm.{u_5} (E := 𝕜) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist p₁ p₂ =
  (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
rw :
  dist p₁ ((lineMap p₁ p₂ : (a : 𝕜) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
rw₁ :
  dist ((lineMap p₁ p₂ : (a : 𝕜) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) p₁ =
    (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
rw₂ :
  norm.{u_5} (E := 𝕜) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist p₁ p₂ =
    (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw₃ : norm.{u_5} (E := 𝕜) 2⁻¹ * dist p₁ p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
rw :
  dist p₁ ((lineMap p₁ p₂ : (a : 𝕜) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) =
    (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
rw₁ :
  dist ((lineMap p₁ p₂ : (a : 𝕜) → P) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) p₁ =
    (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
rw₂ :
  norm.{u_5} (E := 𝕜) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist p₁ p₂ =
    (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
rw₃ : norm.{u_5} (E := 𝕜) 2⁻¹ * dist p₁ p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw₄ : norm.{u_5} (E := 𝕜) 2⁻¹ * dist p₁ p₂ = norm.{u_5} (E := 𝕜) 2⁻¹ * dist p₁ p₂
Tactic: rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₁ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw : dist p₁ (midpoint 𝕜 p₁ p₂) = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [dist_comm, dist_left_midpoint]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
rw : dist p₁ (midpoint 𝕜 p₁ p₂) = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
⊢ dist (midpoint 𝕜 p₁ p₂) p₁ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw₁ : (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [dist_comm, dist_left_midpoint]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw : dist (midpoint 𝕜 p₂ p₁) p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [midpoint_comm, dist_midpoint_left, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
rw : dist (midpoint 𝕜 p₂ p₁) p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
⊢ dist (midpoint 𝕜 p₁ p₂) p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw₁ : (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₂ p₁ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [midpoint_comm, dist_midpoint_left, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
rw : dist (midpoint 𝕜 p₂ p₁) p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
rw₁ : (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₂ p₁ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
⊢ dist (midpoint 𝕜 p₁ p₂) p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw₂ : (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [midpoint_comm, dist_midpoint_left, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
⊢ dist p₂ (midpoint 𝕜 p₁ p₂) = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw : dist (midpoint 𝕜 p₁ p₂) p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [dist_comm, dist_midpoint_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
rw : dist (midpoint 𝕜 p₁ p₂) p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
⊢ dist p₂ (midpoint 𝕜 p₁ p₂) = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
have rw₁ : (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [dist_comm, dist_midpoint_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = dist p₂ (midpoint 𝕜 p₁ p₂)
have rw : (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂ = dist p₂ (midpoint 𝕜 p₁ p₂)
Tactic: rw [dist_left_midpoint p₁ p₂, dist_right_midpoint p₁ p₂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ : P
rw : (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂ = dist p₂ (midpoint 𝕜 p₁ p₂)
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = dist p₂ (midpoint 𝕜 p₁ p₂)
have rw₁ : (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
Tactic: rw [dist_left_midpoint p₁ p₂, dist_right_midpoint p₁ p₂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ p₃ p₄ : P
⊢ dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / norm.{u_5} (E := 𝕜) 2
have rw : ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ p₃ p₄ : P
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2
have rw : ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / norm.{u_5} (E := 𝕜) 2 ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2
Tactic: rw [midpoint_eq_smul_add, norm_smul, invOf_eq_inv, norm_inv, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / norm.{u_5} (E := 𝕜) 2 ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2
have h₁ : 0 ≤ norm.{u_5} (E := 𝕜) 2
Tactic: grw [norm_add_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 V
inst_5 : Invertible (α := 𝕜) 2
p₁ p₂ p₃ p₄ : P
h₁ : 0 ≤ norm.{u_5} (E := 𝕜) 2
⊢ ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / norm.{u_5} (E := 𝕜) 2 ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2
have grw : (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2 ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2
Tactic: grw [norm_add_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
W : Type u_3
Q : Type u_4
inst : NormedAddCommGroup W
inst_1 : MetricSpace Q
inst_2 : NormedAddTorsor W Q
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
⊢ dist c₁ c₂ ≤
    (↑(nndist p₁ p₂)⁻¹ : ℝ) *
      dist.{u_4} (α := Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₁ : Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₂ : Q)
have rw : dist c₁ c₂ ≤ (↑(nndist p₁ p₂)⁻¹ : ℝ) * (dist c₁ c₂ * dist p₁ p₂)
Tactic: rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
      inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
W : Type u_3
Q : Type u_4
inst : NormedAddCommGroup W
inst_1 : MetricSpace Q
inst_2 : NormedAddTorsor W Q
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
rw : dist c₁ c₂ ≤ (↑(nndist p₁ p₂)⁻¹ : ℝ) * (dist c₁ c₂ * dist p₁ p₂)
⊢ dist c₁ c₂ ≤
    (↑(nndist p₁ p₂)⁻¹ : ℝ) *
      dist.{u_4} (α := Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₁ : Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₂ : Q)
have rw₁ : dist c₁ c₂ ≤ (↑(nndist p₁ p₂) : ℝ)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
Tactic: rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
      inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]