awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
R : ℝ
hR : R ≠ 0
x : P
⊢ inversion x R (inversion x R x) = x
have inl : inversion x R x = x
Tactic: rw [inversion_self, inversion_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
R : ℝ
hR : R ≠ 0
x : P
inl : inversion x R x = x
⊢ inversion x R (inversion x R x) = x
have inl₁ : x = x
Tactic: rw [inversion_self, inversion_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ inversion c R (inversion c R x) = x
have inr : HPow.hPow (β := ℕ) R 2 ≠ 0
Tactic: rw [inversion, dist_inversion_center, inversion_vsub_center, smul_smul, ← mul_pow,
      div_mul_div_comm, div_mul_cancel₀ _ (dist_ne_zero.2 hne), ← sq, div_self, one_pow, one_smul,
      vsub_vadd]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x : P
R : ℝ
⊢ inversion c R x = c ↔ x = c ∨ R = 0
have pos : ∀ (hR : R = 0), inversion c R x = c ↔ x = c ∨ R = 0
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x : P
R : ℝ
pos : ∀ (hR : R = 0), inversion c R x = c ↔ x = c ∨ R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0
have neg : ∀ (hR : ¬R = 0), inversion c R x = c ↔ x = c ∨ R = 0
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist (inversion c R x) (inversion c R y) = HPow.hPow (β := ℕ) R 2 / (dist x c * dist y c) * dist x y
have dsimp : dist (HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c) (HPow.hPow (β := ℕ) (R / dist y c) 2 • (y -ᵥ c) +ᵥ c) =
  HPow.hPow (β := ℕ) R 2 / (dist x c * dist y c) * dist x y
Tactic: dsimp only [inversion]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist (HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c) (HPow.hPow (β := ℕ) (R / dist y c) 2 • (y -ᵥ c) +ᵥ c) =
    HPow.hPow (β := ℕ) R 2 / (dist x c * dist y c) * dist x y
have simp_rw : dist (HPow.hPow (β := ℕ) (R / ‖x -ᵥ c‖) 2 • (x -ᵥ c)) (HPow.hPow (β := ℕ) (R / ‖y -ᵥ c‖) 2 • (y -ᵥ c)) =
  HPow.hPow (β := ℕ) R 2 / (‖x -ᵥ c‖ * ‖y -ᵥ c‖) * dist x y
Tactic: simp_rw [dist_vadd_cancel_right, dist_eq_norm_vsub V _ c]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
have inl : dist (inversion c 0 x) y * dist x c = dist x (inversion c 0 y) * dist y c
Tactic: rcases eq_or_ne R 0 with rfl | hR
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
inl : dist (inversion c 0 x) y * dist x c = dist x (inversion c 0 y) * dist y c
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
have inr : ∀ (hR : R ≠ 0), dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
Tactic: rcases eq_or_ne R 0 with rfl | hR
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
have hy' : inversion c R y ≠ c
Tactic: have hy' : inversion c R y ≠ c := by simp [*]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
| dist (inversion c R x) y
have rw : dist (inversion c R x) (inversion c R (inversion c R y))
Tactic: rw [← inversion_inversion c hR y]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
have inr : dist (inversion c R x) (inversion c R (inversion c R y)) * dist x c = dist x (inversion c R y) * dist y c
Tactic: conv in dist _ y => rw [← inversion_inversion c hR y]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ dist (inversion c R x) (inversion c R (inversion c R y)) * dist x c = dist x (inversion c R y) * dist y c
have inr : HPow.hPow (β := ℕ) R 2 / (dist x c * (HPow.hPow (β := ℕ) R 2 / dist y c)) * dist x (inversion c R y) * dist x c =
  dist x (inversion c R y) * dist y c
Tactic: rw [dist_inversion_inversion hx hy', dist_inversion_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have inl : dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d
Tactic: rcases eq_or_ne b a with (rfl | hb)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
inl : dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have inr : ∀ (hb : b ≠ a), dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
Tactic: rcases eq_or_ne b a with (rfl | hb)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
⊢ dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d
have inl : dist b c * dist b d ≤ 0 * dist c d + dist b c * dist b d
Tactic: rw [dist_self, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
inl : dist b c * dist b d ≤ 0 * dist c d + dist b c * dist b d
⊢ dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d
have inl₁ : dist b c * dist b d ≤ 0 + dist b c * dist b d
Tactic: rw [dist_self, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
inl : dist b c * dist b d ≤ 0 * dist c d + dist b c * dist b d
inl₁ : dist b c * dist b d ≤ 0 + dist b c * dist b d
⊢ dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d
have inl₂ : dist b c * dist b d ≤ dist b c * dist b d
Tactic: rw [dist_self, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have inr : ∀ (hb : b ≠ c), dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d
Tactic: rcases eq_or_ne c a with (rfl | hc)
Cleared hypotheses: a, hb
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
inr : ∀ (hb : b ≠ c), dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have inr₁ : ∀ (hc : c ≠ a), dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
Tactic: rcases eq_or_ne c a with (rfl | hc)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
hb : b ≠ c
⊢ dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d
have inr : 0 ≤ dist c b * dist c d + dist b c * dist c d
Tactic: rw [dist_self, zero_mul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have inr : ∀ (hb : b ≠ d) (hc : c ≠ d), dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
Tactic: rcases eq_or_ne d a with (rfl | hd)
Cleared hypotheses: a, hb, hc
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
inr : ∀ (hb : b ≠ d) (hc : c ≠ d), dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have inr₁ : ∀ (hd : d ≠ a), dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
Tactic: rcases eq_or_ne d a with (rfl | hd)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
have inr : dist d c * dist b d ≤ dist d b * dist c d + dist b c * 0
Tactic: rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
inr : dist d c * dist b d ≤ dist d b * dist c d + dist b c * 0
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
have inr₁ : dist d c * dist b d ≤ dist d b * dist c d + 0
Tactic: rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
inr : dist d c * dist b d ≤ dist d b * dist c d + dist b c * 0
inr₁ : dist d c * dist b d ≤ dist d b * dist c d + 0
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
have inr₂ : dist d c * dist b d ≤ dist d b * dist c d
Tactic: rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
inr : dist d c * dist b d ≤ dist d b * dist c d + dist b c * 0
inr₁ : dist d c * dist b d ≤ dist d b * dist c d + 0
inr₂ : dist d c * dist b d ≤ dist d b * dist c d
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
have inr₃ : dist c d * dist b d ≤ dist d b * dist c d
Tactic: rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
inr : dist d c * dist b d ≤ dist d b * dist c d + dist b c * 0
inr₁ : dist d c * dist b d ≤ dist d b * dist c d + 0
inr₂ : dist d c * dist b d ≤ dist d b * dist c d
inr₃ : dist c d * dist b d ≤ dist d b * dist c d
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
have inr₄ : dist c d * dist b d ≤ dist b d * dist c d
Tactic: rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
inr : dist d c * dist b d ≤ dist d b * dist c d + dist b c * 0
inr₁ : dist d c * dist b d ≤ dist d b * dist c d + 0
inr₂ : dist d c * dist b d ≤ dist d b * dist c d
inr₃ : dist c d * dist b d ≤ dist d b * dist c d
inr₄ : dist c d * dist b d ≤ dist b d * dist c d
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
have inr₅ : dist b d * dist c d ≤ dist b d * dist c d
Tactic: rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have H : dist (inversion a 1 b) (inversion a 1 d) ≤
  dist (inversion a 1 b) (inversion a 1 c) + dist (inversion a 1 c) (inversion a 1 d)
Tactic: have H := dist_triangle (inversion a 1 b) (inversion a 1 c) (inversion a 1 d)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H :
  dist (inversion a 1 b) (inversion a 1 d) ≤
    dist (inversion a 1 b) (inversion a 1 c) + dist (inversion a 1 c) (inversion a 1 d)
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have H₁ : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
Tactic: rw [dist_inversion_inversion hb hd, dist_inversion_inversion hb hc,
    dist_inversion_inversion hc hd, one_pow] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have hb₁ : 0 < dist b a
Tactic: rw [← dist_pos] at hb hc hd
Cleared hypotheses: hb, hc, hd, H
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
hb₁ : 0 < dist b a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have hc₁ : 0 < dist c a
Tactic: rw [← dist_pos] at hb hc hd
Cleared hypotheses: hb, hc, hd, H
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
hb₁ : 0 < dist b a
hc₁ : 0 < dist c a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have hd₁ : 0 < dist d a
Tactic: rw [← dist_pos] at hb hc hd
Cleared hypotheses: hb, hc, hd, H
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
have inr : dist a c * dist b d / (dist b a * (dist c a * dist d a)) ≤
  (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a))
Tactic: rw [← div_le_div_iff_of_pos_right (mul_pos hb (mul_pos hc hd))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d / (dist b a * (dist c a * dist d a)) ≤
    (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a))
have h : dist a c * dist b d / (dist b a * (dist c a * dist d a)) = 1 / (dist b a * dist d a) * dist b d
Tactic: convert! H using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
h : dist a c * dist b d / (dist b a * (dist c a * dist d a)) = 1 / (dist b a * dist d a) * dist b d
⊢ dist a c * dist b d / (dist b a * (dist c a * dist d a)) ≤
    (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a))
have h₁ : (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a)) =
  1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
Tactic: convert! H using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a)) =
    1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
have h : dist b a * dist c d + dist b c * dist d a = dist b c * dist d a + dist b a * dist c d
Tactic: simp [field, dist_comm a]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableAt ℝ c a
hR : DifferentiableAt ℝ R a
hx : DifferentiableAt ℝ x a
hne : x a ≠ c a
⊢ DifferentiableAt.{0, u_1, u_2} ℝ (F := F) (fun (a : E) ↦ inversion (c a) (R a) (x a)) a
have rw : ∀ (hc : DifferentiableWithinAt ℝ c univ a) (hR : DifferentiableWithinAt ℝ R univ a)
  (hx : DifferentiableWithinAt ℝ x univ a) (hne : x a ≠ c a),
  DifferentiableWithinAt.{0, u_1, u_2} ℝ (F := F) (fun (a : E) ↦ inversion (c a) (R a) (x a)) univ a
Tactic: rw [← differentiableWithinAt_univ] at *
Cleared hypotheses: hc, hR, hx, hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c x : F
R : ℝ
hx : x ≠ c
⊢ HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist x c) 2)
      (↑(↑(Submodule.reflection (ℝ ∙ (x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F))
    x
have rcases : ∀ (x : F) (hx : (fun (x : F) ↦ c + x) x ≠ c),
  HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist ((fun (x : F) ↦ c + x) x) c) 2)
      (↑(↑(Submodule.reflection (ℝ ∙ ((fun (x : F) ↦ c + x) x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F))
    ((fun (x : F) ↦ c + x) x)
Tactic: rcases add_left_surjective c x with ⟨x, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
⊢ HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)
have simp : HasFDerivAt (fun (x : F) ↦ HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c)
  (HSMul.hSMul (β := F →L[ℝ] F)
      (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
      (ContinuousLinearMap.id ℝ F) +
    (HPow.hPow (β := ℕ) R 2 •
          -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
            HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
              (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
      (_root_.id (c + x) - c))
  (c + x)
Tactic: simp +unfoldPartialApp only [inversion]