awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
hne : x ≠ c
inr : dist x c ≠ 0
⊢ inversion c (dist x c) x = x

Tactic:
rw [inversion, div_self, one_pow, one_smul, vsub_vadd]

Premises used: one_pow, one_smul, EuclideanGeometry.inversion, vsub_vadd, div_self
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
hne inr inr₁ inr₂ inr₃ : x ≠ c
⊢ dist x c ≠ 0

Tactic:
rwa [dist_ne_zero]

Premises used: dist_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
rw : inversion c (dist x c) x = x
rw₁ rw₂ : x = x
⊢ inversion c (dist c x) x = x

Tactic:
rw [dist_comm, inversion_dist_center]

Premises used: EuclideanGeometry.inversion_dist_center, dist_comm
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
h : x ∈ sphere c R
⊢ inversion c R x = x

Tactic:
h.out ▸ inversion_dist_center c x

Premises used: EuclideanGeometry.inversion_dist_center, Membership.mem.out, Eq.rec
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
inl : dist (inversion x R x) x = HPow.hPow (β := ℕ) R 2 / dist x x
inr : ∀ (hx : x ≠ c), dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c
⊢ dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c

Tactic:
rcases eq_or_ne x c with (rfl | hx)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
x : P
R : ℝ
⊢ dist (inversion x R x) x = HPow.hPow (β := ℕ) R 2 / dist x x

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
hx : x ≠ c
⊢ dist x c ≠ 0

Tactic:
have : dist x c ≠ 0 := dist_ne_zero.2 hx
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
hx : x ≠ c
this : dist x c ≠ 0
inr : dist (HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c) c = HPow.hPow (β := ℕ) R 2 / dist x c
⊢ dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c

Tactic:
simp only [inversion]

Premises used: EuclideanGeometry.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
hx : x ≠ c
this : dist x c ≠ 0
inr :
  dist x c * dist ((HPow.hPow (β := ℕ) R 2 / HPow.hPow (β := ℕ) (dist x c) 2) • (x -ᵥ c) +ᵥ c) c =
    HPow.hPow (β := ℕ) R 2
⊢ dist (HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c) c = HPow.hPow (β := ℕ) R 2 / dist x c

Tactic:
field_simp
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
hx : x ≠ c
this : dist x c ≠ 0
inr : dist x c * (R * R / (dist x c * dist x c) * dist x c) = R * R
⊢ dist x c * dist ((HPow.hPow (β := ℕ) R 2 / HPow.hPow (β := ℕ) (dist x c) 2) • (x -ᵥ c) +ᵥ c) c =
    HPow.hPow (β := ℕ) R 2

Tactic:
simp only [sq, dist_vadd_left, norm_smul, norm_div, norm_mul, Real.norm_eq_abs, abs_mul_abs_self,
    abs_dist, ← dist_eq_norm_vsub]

Premises used: norm_smul, norm_mul, sq, dist_vadd_left, norm_div, abs_dist, abs_mul_abs_self, dist_eq_norm_vsub, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist x c * (R * R / (dist x c * dist x c) * dist x c) = R * R

Tactic:
field
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
rw : dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist c x
rw₁ : dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c
rw₂ rw₃ : HPow.hPow (β := ℕ) R 2 / dist x c = HPow.hPow (β := ℕ) R 2 / dist x c
⊢ dist c (inversion c R x) = HPow.hPow (β := ℕ) R 2 / dist c x

Tactic:
rw [dist_comm c, dist_comm c, dist_inversion_center]

Premises used: dist_comm, EuclideanGeometry.dist_inversion_center
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inl : inversion x R (inversion x R x) = x
inr : ∀ (hne : x ≠ c), inversion c R (inversion c R x) = x
⊢ inversion c R (inversion c R x) = x

Tactic:
rcases eq_or_ne x c with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inl₁ inl₂ : x = x
⊢ inversion x R (inversion x R x) = x

Tactic:
rw [inversion_self, inversion_self]

Premises used: EuclideanGeometry.inversion_self
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inr : HPow.hPow (β := ℕ) R 2 ≠ 0
⊢ inversion c R (inversion c R x) = x

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]

Premises used: Iff.mpr, one_pow, dist_ne_zero, div_mul_cancel₀, EuclideanGeometry.inversion_vsub_center, div_mul_div_comm, smul_smul, sq, one_smul, EuclideanGeometry.inversion, vsub_vadd, mul_pow, EuclideanGeometry.dist_inversion_center, div_self
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ HPow.hPow (β := ℕ) R 2 ≠ 0

Tactic:
pow_ne_zero _ hR

Premises used: pow_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ HPow.hPow (β := ℕ) R 2 ≠ 0

Tactic:
exact pow_ne_zero _ hR

Premises used: pow_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ Involutive (inversion c R)

Tactic:
inversion_inversion c hR

Premises used: EuclideanGeometry.inversion_inversion, Function.Involutive
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ Surjective (inversion c R)

Tactic:
(inversion_involutive c hR).surjective

Premises used: EuclideanGeometry.inversion_involutive, Function.Involutive.surjective
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ Injective (inversion c R)

Tactic:
(inversion_involutive c hR).injective

Premises used: EuclideanGeometry.inversion_involutive, Function.Involutive.injective
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ Bijective (inversion c R)

Tactic:
(inversion_involutive c hR).bijective

Premises used: EuclideanGeometry.inversion_involutive, Function.Involutive.bijective
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
hR : R ≠ 0
⊢ inversion c R x = c ↔ x = c

Tactic:
(inversion_injective c hR).eq_iff' <| inversion_self _ _

Premises used: Function.Injective.eq_iff', EuclideanGeometry.inversion_injective, EuclideanGeometry.inversion_self
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
neg : ∀ (hR : ¬R = 0), inversion c R x = c ↔ x = c ∨ R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0

Tactic:
by_cases hR : R = 0
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
hR : R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0

Tactic:
simp [inversion_eq_center, hR]

Premises used: EuclideanGeometry.inversion_eq_center
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
hR : ¬R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0

Tactic:
simp [inversion_eq_center, hR]

Premises used: EuclideanGeometry.inversion_eq_center
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
hR : R ≠ 0
⊢ c = inversion c R x ↔ x = c

Tactic:
eq_comm.trans (inversion_eq_center hR)

Premises used: eq_comm, EuclideanGeometry.inversion_eq_center, Iff.trans
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
⊢ c = inversion c R x ↔ x = c ∨ R = 0

Tactic:
eq_comm.trans inversion_eq_center'

Premises used: eq_comm, Iff.trans, EuclideanGeometry.inversion_eq_center'
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
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
⊢ dist (inversion c R x) (inversion c R y) = HPow.hPow (β := ℕ) R 2 / (dist x c * dist y c) * dist x y

Tactic:
dsimp only [inversion]

Premises used: EuclideanGeometry.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 : ℝ
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
⊢ 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:
simp_rw [dist_vadd_cancel_right, dist_eq_norm_vsub V _ c]

Premises used: dist_vadd_cancel_right, dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 / ‖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:
simpa only [dist_vsub_cancel_right] using
    dist_div_norm_sq_smul (vsub_ne_zero.2 hx) (vsub_ne_zero.2 hy) R

Premises used: Iff.mpr, vsub_ne_zero, dist_vsub_cancel_right, dist_div_norm_sq_smul
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inr : ∀ (hR : R ≠ 0), dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ dist (inversion c 0 x) y * dist x c = dist x (inversion c 0 y) * dist y c

Tactic:
simp [dist_comm, mul_comm]

Premises used: dist_comm, mul_comm
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ inversion c R y ≠ c

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ inversion c R y ≠ c

Tactic:
have hy' : inversion c R y ≠ c := by simp [*]
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
rw : dist (inversion c R x) (inversion c R (inversion c R y))
| dist (inversion c R x) y

Tactic:
rw [← inversion_inversion c hR y]

Premises used: EuclideanGeometry.inversion_inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
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
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c

Tactic:
conv in dist _ y => rw [← inversion_inversion c hR y]

Premises used: EuclideanGeometry.inversion_inversion, Dist.dist
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
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
⊢ 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:
rw [dist_inversion_inversion hx hy', dist_inversion_center]

Premises used: EuclideanGeometry.dist_inversion_inversion, EuclideanGeometry.dist_inversion_center
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ 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:
field [dist_ne_zero.2 hx]

Premises used: Iff.mpr, dist_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inr : ∀ (hb : b ≠ a), dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
⊢ 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)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inl₂ inl₃ : dist b c * dist b 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

Tactic:
rw [dist_self, zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, zero_add, dist_self
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inr₁ : ∀ (hc : c ≠ a), dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
⊢ 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)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inr : 0 ≤ dist c b * dist c d + dist b c * dist c d
⊢ dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d

Tactic:
rw [dist_self, zero_mul]

Premises used: MulZeroClass.zero_mul, dist_self
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ 0 ≤ dist c b * dist c d + dist b c * dist c d

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inr₁ : ∀ (hd : d ≠ a), dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
⊢ 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)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
inr₅ inr₆ : dist b d * dist c 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

Tactic:
rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]

Premises used: dist_comm, MulZeroClass.mul_zero, dist_self, mul_comm, add_zero
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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 (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)
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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)
⊢ 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

Premises used: one_pow, EuclideanGeometry.dist_inversion_inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ 0 < dist b a

Tactic:
rw [← dist_pos] at hb hc hd

Premises used: dist_pos
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ 0 < dist c a

Tactic:
rw [← dist_pos] at hb hc hd

Premises used: dist_pos
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ 0 < dist d a

Tactic:
rw [← dist_pos] at hb hc hd

Premises used: dist_pos
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
hd₁ : 0 < dist d a
⊢ 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_pos] at hb hc hd

Premises used: dist_pos
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
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))
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Tactic:
rw [← div_le_div_iff_of_pos_right (mul_pos hb (mul_pos hc hd))]

Premises used: div_le_div_iff_of_pos_right, mul_pos