awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
neg₁ : f ^ n =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (f ^ n) x).untop₀ • (g ^ n) z
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f 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])]

Premises used: AnalyticAt.zpow, AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
⊢ (g ^ n) x = g x ^ n

Tactic:
simp only [Pi.pow_apply]

Premises used: Pi.pow_apply
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
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
⊢ f ^ n =ᶠ[𝓝[≠] x] fun (z : 𝕜) ↦ (z - x) ^ (meromorphicOrderAt (f ^ n) x).untop₀ • (g ^ n) z

Tactic:
filter_upwards [h₃g] with a ha
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
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
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:
simp_all [mul_zpow, ← zpow_mul, meromorphicOrderAt_zpow h₁, mul_comm]

Premises used: zpow_mul, mul_zpow, mul_comm, meromorphicOrderAt_zpow
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (fun (z : 𝕜) ↦ f z ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
MeromorphicAt.meromorphicTrailingCoeffAt_zpow h₁

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_zpow
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (HPow.hPow (β := ℤ) f (↑n : ℤ)) x =
    HPow.hPow (β := ℤ) (meromorphicTrailingCoeffAt f x) (↑n : ℤ)

Tactic:
h₁.meromorphicTrailingCoeffAt_zpow (n := n)

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_zpow
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h : f ^ n = HPow.hPow (β := ℤ) f (↑n : ℤ)
h₂ : meromorphicTrailingCoeffAt f x ^ n = HPow.hPow (β := ℤ) (meromorphicTrailingCoeffAt f x) (↑n : ℤ)
⊢ meromorphicTrailingCoeffAt (f ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
convert! h₁.meromorphicTrailingCoeffAt_zpow (n := n)

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_zpow
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ f ^ n = HPow.hPow (β := ℤ) f (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt f x ^ n = HPow.hPow (β := ℤ) (meromorphicTrailingCoeffAt f x) (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
⊢ meromorphicTrailingCoeffAt (fun (z : 𝕜) ↦ f z ^ n) x = meromorphicTrailingCoeffAt f x ^ n

Tactic:
MeromorphicAt.meromorphicTrailingCoeffAt_pow h₁

Premises used: MeromorphicAt.meromorphicTrailingCoeffAt_pow
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂) = ‖c‖ * dist p₁ p₂

Tactic:
simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]

Premises used: norm_smul, dist_comm, AffineMap.homothety_def, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 : 𝕜
⊢ nndist p₁ ((homothety p₁ c : (a : P) → P) p₂) = ‖c‖₊ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_center_homothety _ _ _

Premises used: dist_center_homothety, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂
rw₁ rw₂ : ‖c‖ * dist p₁ p₂ = ‖c‖ * dist p₁ p₂
⊢ dist ((homothety p₁ c : (a : P) → P) p₂) p₁ = ‖c‖ * dist p₁ p₂

Tactic:
rw [dist_comm, dist_center_homothety]

Premises used: dist_center_homothety, dist_comm
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 : 𝕜
⊢ nndist ((homothety p₁ c : (a : P) → P) p₂) p₁ = ‖c‖₊ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_homothety_center _ _ _

Premises used: NNReal.eq, dist_homothety_center
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂ : 𝕜
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₁
⊢ 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₂]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₁

Tactic:
simp only [lineMap_apply, dist_eq_norm_vsub, vadd_vsub_vadd_cancel_right,
    ← sub_smul, norm_smul, vsub_eq_sub]

Premises used: norm_smul, sub_smul, vadd_vsub_vadd_cancel_right, AffineMap.lineMap_apply, dist_eq_norm_vsub, vsub_eq_sub
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂ : 𝕜
⊢ nndist.{u_2} (α := P) ((lineMap p₁ p₂ : (a : 𝕜) → P) c₁ : P) ((lineMap p₁ p₂ : (a : 𝕜) → P) c₂ : P) =
    nndist c₁ c₂ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_lineMap_lineMap _ _ _ _

Premises used: NNReal.eq, dist_lineMap_lineMap
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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
⊢ LipschitzWith.{u_5, u_2} (α := 𝕜) (β := P) (nndist p₁ p₂) (⇑(lineMap p₁ p₂) : (a : 𝕜) → P)

Tactic:
LipschitzWith.of_dist_le_mul fun c₁ c₂ =>
    ((dist_lineMap_lineMap p₁ p₂ c₁ c₂).trans (mul_comm _ _)).le

Premises used: Eq.le, mul_comm, Dist.dist, LipschitzWith.of_dist_le_mul, Eq.trans, dist_lineMap_lineMap
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 ((lineMap p₁ p₂ : (a : 𝕜) → P) c) p₁ = ‖c‖ * dist p₁ p₂

Tactic:
simpa only [lineMap_apply_zero, dist_zero_right] using dist_lineMap_lineMap p₁ p₂ c 0

Premises used: AffineMap.lineMap_apply_zero, OfNat.ofNat, dist_zero_right, dist_lineMap_lineMap
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 : 𝕜
⊢ nndist ((lineMap p₁ p₂ : (a : 𝕜) → P) c) p₁ = ‖c‖₊ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_lineMap_left _ _ _

Premises used: dist_lineMap_left, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₁ ((lineMap p₁ p₂ : (a : 𝕜) → P) c) = ‖c‖ * dist p₁ p₂

Tactic:
(dist_comm _ _).trans (dist_lineMap_left _ _ _)

Premises used: dist_lineMap_left, dist_comm, Eq.trans
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 : 𝕜
⊢ nndist p₁ ((lineMap p₁ p₂ : (a : 𝕜) → P) c) = ‖c‖₊ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_left_lineMap _ _ _

Premises used: NNReal.eq, dist_left_lineMap
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 ((lineMap p₁ p₂ : (a : 𝕜) → P) c) p₂ = ‖1 - c‖ * dist p₁ p₂

Tactic:
simpa only [lineMap_apply_one, dist_eq_norm'] using dist_lineMap_lineMap p₁ p₂ c 1

Premises used: dist_eq_norm', AffineMap.lineMap_apply_one, OfNat.ofNat, dist_lineMap_lineMap
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 : 𝕜
⊢ nndist ((lineMap p₁ p₂ : (a : 𝕜) → P) c) p₂ = ‖1 - c‖₊ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_lineMap_right _ _ _

Premises used: NNReal.eq, dist_lineMap_right
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂ ((lineMap p₁ p₂ : (a : 𝕜) → P) c) = ‖1 - c‖ * dist p₁ p₂

Tactic:
(dist_comm _ _).trans (dist_lineMap_right _ _ _)

Premises used: dist_lineMap_right, dist_comm, Eq.trans
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 : 𝕜
⊢ nndist p₂ ((lineMap p₁ p₂ : (a : 𝕜) → P) c) = ‖1 - c‖₊ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_right_lineMap _ _ _

Premises used: NNReal.eq, dist_right_lineMap
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂
rw₁ rw₂ : ‖1 - c‖ * dist p₁ p₂ = ‖1 - c‖ * dist p₁ p₂
⊢ dist ((homothety p₁ c : (a : P) → P) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂

Tactic:
rw [homothety_eq_lineMap, dist_lineMap_right]

Premises used: dist_lineMap_right, AffineMap.homothety_eq_lineMap
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 : 𝕜
⊢ nndist ((homothety p₁ c : (a : P) → P) p₂) p₂ = ‖1 - c‖₊ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_homothety_self _ _ _

Premises used: NNReal.eq, dist_homothety_self
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂
rw₁ rw₂ : ‖1 - c‖ * dist p₁ p₂ = ‖1 - c‖ * dist p₁ p₂
⊢ dist p₂ ((homothety p₁ c : (a : P) → P) p₂) = ‖1 - c‖ * dist p₁ p₂

Tactic:
rw [dist_comm, dist_homothety_self]

Premises used: dist_comm, dist_homothety_self
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 : 𝕜
⊢ nndist p₂ ((homothety p₁ c : (a : P) → P) p₂) = ‖1 - c‖₊ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_self_homothety _ _ _

Premises used: NNReal.eq, dist_self_homothety
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂
rw₄ 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₂

Tactic:
rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]

Premises used: dist_lineMap_left, dist_comm, norm_inv, invOf_eq_inv, midpoint
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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
⊢ nndist p₁ (midpoint 𝕜 p₁ p₂) = (nnnorm.{u_5} (E := 𝕜) 2)⁻¹ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_left_midpoint _ _

Premises used: dist_left_midpoint, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂
rw₁ 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₂

Tactic:
rw [dist_comm, dist_left_midpoint]

Premises used: dist_left_midpoint, dist_comm
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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
⊢ nndist (midpoint 𝕜 p₁ p₂) p₁ = (nnnorm.{u_5} (E := 𝕜) 2)⁻¹ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_midpoint_left _ _

Premises used: NNReal.eq, dist_midpoint_left
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂
rw₂ 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₂

Tactic:
rw [midpoint_comm, dist_midpoint_left, dist_comm]

Premises used: midpoint_comm, dist_comm, dist_midpoint_left
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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
⊢ nndist (midpoint 𝕜 p₁ p₂) p₂ = (nnnorm.{u_5} (E := 𝕜) 2)⁻¹ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_midpoint_right _ _

Premises used: dist_midpoint_right, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₁ 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₂

Tactic:
rw [dist_comm, dist_midpoint_right]

Premises used: dist_midpoint_right, dist_comm
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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
⊢ nndist p₂ (midpoint 𝕜 p₁ p₂) = (nnnorm.{u_5} (E := 𝕜) 2)⁻¹ * nndist p₁ p₂

Tactic:
NNReal.eq <| dist_right_midpoint _ _

Premises used: dist_right_midpoint, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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₂)
rw₁ rw₂ : (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂ = (norm.{u_5} (E := 𝕜) 2)⁻¹ * dist p₁ p₂
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = dist p₂ (midpoint 𝕜 p₁ p₂)

Tactic:
rw [dist_left_midpoint p₁ p₂, dist_right_midpoint p₁ p₂]

Premises used: dist_left_midpoint, dist_right_midpoint
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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
rw : ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2
⊢ dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist 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]

Premises used: midpoint_vsub_midpoint, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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
rw : ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / norm.{u_5} (E := 𝕜) 2 ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2
⊢ ‖midpoint 𝕜 (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)‖ ≤ (‖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]

Premises used: norm_smul, midpoint_eq_smul_add, norm_inv, invOf_eq_inv, div_eq_inv_mul
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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
grw grw₁ : (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2 ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2
⊢ ‖p₁ -ᵥ p₃ + (p₂ -ᵥ p₄)‖ / norm.{u_5} (E := 𝕜) 2 ≤ (‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖) / norm.{u_5} (E := 𝕜) 2

Tactic:
grw [norm_add_le]

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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
⊢ nndist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / nnnorm.{u_5} (E := 𝕜) 2

Tactic:
dist_midpoint_midpoint_le' _ _ _ _

Premises used: dist_midpoint_midpoint_le', NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
p q : P
⊢ dist ((Equiv.pointReflection p : (a : P) → P) q) p = dist p q

Tactic:
simp [dist_eq_norm_vsub V, Equiv.pointReflection_vsub_left (G := V)]

Premises used: dist_eq_norm_vsub, Equiv.pointReflection_vsub_left
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : PseudoMetricSpace P
inst_2 : NormedAddTorsor V P
p q : P
⊢ dist p ((Equiv.pointReflection p : (a : P) → P) q) = dist p q

Tactic:
(dist_comm _ _).trans (dist_pointReflection_left _ _)

Premises used: dist_comm, dist_pointReflection_left, Eq.trans
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 q : P
⊢ dist ((Equiv.pointReflection p : (a : P) → P) q) q = norm.{u_5} (E := 𝕜) 2 * dist p q

Tactic:
simp [dist_eq_norm_vsub V, Equiv.pointReflection_vsub_right (G := V), ← Nat.cast_smul_eq_nsmul 𝕜,
    norm_smul]

Premises used: norm_smul, Equiv.pointReflection_vsub_right, Nat.cast_smul_eq_nsmul, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsor
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 q : P
⊢ dist q ((Equiv.pointReflection p : (a : P) → P) q) = norm.{u_5} (E := 𝕜) 2 * dist p q

Tactic:
(dist_comm _ _).trans (dist_pointReflection_right 𝕜 _ _)

Premises used: dist_comm, dist_pointReflection_right, Eq.trans