awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ HPow.hPow (β := ℕ) (r * dist a b) 2 + HPow.hPow (β := ℕ) (r * dist c b) 2 -
      2 * (r * dist a b) * (r * dist c b) * Real.cos (∠ a b c) =
    HPow.hPow (β := ℕ) r 2 *
      (HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist c b) 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
simp : r * r * (dist a c * dist a c) = r * dist a c * (r * dist a c)
⊢ HPow.hPow (β := ℕ) r 2 *
      (HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist c b) 2 -
        2 * dist a b * dist c b * Real.cos (∠ a b c)) =
    HPow.hPow (β := ℕ) (r * dist a c) 2

Tactic:
simp [pow_two, ← law_cos a b c]

Premises used: pow_two, EuclideanGeometry.law_cos
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ r * r * (dist a c * dist a c) = r * dist a c * (r * dist a c)

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2

Tactic:
have h' : dist a' c' ^ 2 = (r * dist a c) ^ 2 := calc
    dist a' c' ^ 2 =
        dist a' b' ^ 2 + dist c' b' ^ 2 - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c') := by
      simp [pow_two, law_cos a' b' c']
    _ = r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c)) := by
      rw [h, hab, hcb]; ring
    _ = (r * dist a c) ^ 2 := by simp [pow_two, ← law_cos a b c]; ring
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
pos : ∀ (hab₁ : a = b), dist a' c' = r * dist a c
neg : ∀ (hab₁ : ¬a = b), dist a' c' = r * dist a c
⊢ dist a' c' = r * dist a c

Tactic:
by_cases hab₁ : a = b
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
rw : dist a' b' = 0
rw₁ : r * dist a b = 0
rw₂ : r * 0 = 0
rw₃ rw₄ : Eq (α := ℝ) 0 0
⊢ a' = b'

Tactic:
rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]

Premises used: Iff.mpr, MulZeroClass.mul_zero, dist_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
⊢ a' = b'

Tactic:
have hab'₁ : a' = b' := by
      rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
hab'₁ : a' = b'
pos : dist a' c' = r * dist b c
pos₁ : dist b' c' = r * dist b c
pos₂ : dist c' b' = r * dist b c
pos₃ : dist c' b' = r * dist c b
pos₄ pos₅ : r * dist c b = r * dist c b
⊢ dist a' c' = r * dist a c

Tactic:
rw [hab₁, hab'₁, dist_comm b' c', dist_comm b c, hcb]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
rw : 0 ≤ dist a' b'
⊢ 0 ≤ r * dist a b

Tactic:
rw [← hab]
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
⊢ 0 ≤ dist a' b'

Tactic:
dist_nonneg

Premises used: dist_nonneg
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
⊢ 0 ≤ dist a' b'

Tactic:
exact dist_nonneg

Premises used: dist_nonneg
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
⊢ 0 ≤ r * dist a b

Tactic:
have h1 : 0 ≤ r * dist a b := by rw [← hab]; exact dist_nonneg
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
h1 : 0 ≤ r * dist a b
⊢ 0 ≤ r

Tactic:
have h2 : 0 ≤ r := nonneg_of_mul_nonneg_left h1 (dist_pos.mpr hab₁)
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
h1 : 0 ≤ r * dist a b
h2 : 0 ≤ r
⊢ dist a' c' = r * dist a c

Tactic:
(sq_eq_sq₀ dist_nonneg (mul_nonneg h2 dist_nonneg)).mp h'

Premises used: mul_nonneg, dist_nonneg, Iff.mp, sq_eq_sq₀
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
h1 : 0 ≤ r * dist a b
h2 : 0 ≤ r
⊢ dist a' c' = r * dist a c

Tactic:
exact (sq_eq_sq₀ dist_nonneg (mul_nonneg h2 dist_nonneg)).mp h'

Premises used: mul_nonneg, dist_nonneg, Iff.mp, sq_eq_sq₀
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
⊢ Real.sin (∠ c b a) * dist b a = Real.sin (∠ a c b) * dist a c

Tactic:
have hsin := law_sin c b a
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ c b a) * dist b a = Real.sin (∠ a c b) * dist a c
⊢ Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c

Tactic:
rw [dist_comm b a, angle_comm c b a] at hsin

Premises used: EuclideanGeometry.angle_comm, dist_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
⊢ dist a c > 0

Tactic:
have hac : dist a c > 0 := dist_pos.mpr (ne₁₃_of_not_collinear h)
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hx : ∠ a b c ∈ Set.Icc 0 π
⊢ Real.sin (∠ a b c) ≥ 0

Tactic:
apply Real.sin_nonneg_of_mem_Icc

Premises used: Real.sin_nonneg_of_mem_Icc
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
⊢ ∠ a b c ∈ Set.Icc 0 π

Tactic:
simp [angle_nonneg, angle_le_pi]

Premises used: EuclideanGeometry.angle_le_pi, EuclideanGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
⊢ Real.sin (∠ a b c) ≥ 0

Tactic:
have hsinabc : Real.sin (∠ a b c) ≥ 0 := by
    apply Real.sin_nonneg_of_mem_Icc
    simp [angle_nonneg, angle_le_pi]
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
pos : ∀ (h2 : ∠ a b c ≤ π / 2), dist a b < dist a c
neg : ∀ (h2 : π / 2 < ∠ a b c), dist a b < dist a c
⊢ dist a b < dist a c

Tactic:
by_cases! h2 : ∠ a b c ≤ π / 2

Premises used: EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
linarith : ∠ a c b < -(π / 2) → 2 / 2 = 1
linarith₁ : ∠ a c b < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ∠ a c b < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : ∠ a c b < -(π / 2) → 2 / 2 = 1
linarith₄ : ∠ a c b < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ∠ a c b < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ :
  ∠ a c b < -(π / 2) →
    2 * (∠ a c b - ∠ a b c) + (2 * ∠ a b c - 1 * π) + (2 * ∠ a c b - -(1 * π)) + 4 * (0 - ∠ a c b) = 0
linarith₇ : ∠ a c b < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₈ : ∠ a c b < -(π / 2) → GT.gt (α := ℝ) 4 0
⊢ -(π / 2) ≤ ∠ a c b

Tactic:
linarith [angle_nonneg a c b]

Premises used: EuclideanGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
⊢ Real.sin (∠ a c b) < Real.sin (∠ a b c)

Tactic:
exact Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith [angle_nonneg a c b]) h2 h1

Premises used: Real.sin_lt_sin_of_lt_of_le_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
⊢ Real.sin (∠ a c b) < Real.sin (∠ a b c)

Tactic:
have h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c) := by
      exact Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith [angle_nonneg a c b]) h2 h1
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
pos : ∀ (w : dist a c ≤ dist a b), False
⊢ dist a b < dist a c

Tactic:
by_contra! w
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
w : dist a c ≤ dist a b
⊢ Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b

Tactic:
mul_lt_mul h3 w hac hsinabc

Premises used: mul_lt_mul
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
w : dist a c ≤ dist a b
⊢ Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b

Tactic:
exact mul_lt_mul h3 w hac hsinabc

Premises used: mul_lt_mul
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
w : dist a c ≤ dist a b
⊢ Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b

Tactic:
have h4 : Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b := by
      exact mul_lt_mul h3 w hac hsinabc
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
w : dist a c ≤ dist a b
h4 : Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ :
  Real.sin (∠ a b c) * dist a b - Real.sin (∠ a c b) * dist a c +
      (Real.sin (∠ a c b) * dist a c - Real.sin (∠ a b c) * dist a b) =
    0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
neg : ∀ (w : dist a c ≤ dist a b), False
⊢ dist a b < dist a c

Tactic:
by_contra! w
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
by_contra! : ∀ (w1 : Real.sin (∠ a c b) < Real.sin (∠ a b c)), False
⊢ Real.sin (∠ a b c) ≤ Real.sin (∠ a c b)

Tactic:
by_contra! w1
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
w1 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
⊢ Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b

Tactic:
mul_lt_mul w1 w hac hsinabc

Premises used: mul_lt_mul
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
w1 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
⊢ Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b

Tactic:
exact mul_lt_mul w1 w hac hsinabc

Premises used: mul_lt_mul
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
w1 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
⊢ Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b

Tactic:
have h4 : Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b := by
        exact mul_lt_mul w1 w hac hsinabc
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
w1 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
h4 : Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ :
  Real.sin (∠ a b c) * dist a b - Real.sin (∠ a c b) * dist a c +
      (Real.sin (∠ a c b) * dist a c - Real.sin (∠ a b c) * dist a b) =
    0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
⊢ Real.sin (∠ a b c) ≤ Real.sin (∠ a c b)

Tactic:
have h3 : Real.sin (∠ a b c) ≤ Real.sin (∠ a c b) := by
      by_contra! w1
      have h4 : Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b := by
        exact mul_lt_mul w1 w hac hsinabc
      linarith
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (∠ a b c) ≤ Real.sin (∠ a c b)
⊢ Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)

Tactic:
rw [← Real.sin_pi_sub (∠ a b c)] at h3

Premises used: Real.sin_pi_sub, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
linarith : π / 2 ≤ π - ∠ a b c → 2 / 2 = 1
linarith₁ : π / 2 ≤ π - ∠ a b c → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ π - ∠ a b c → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 ≤ π - ∠ a b c → 2 / 2 = 1
linarith₄ : π / 2 ≤ π - ∠ a b c → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 ≤ π - ∠ a b c → GT.gt (α := ℝ) 2 0
linarith₆ : π / 2 ≤ π - ∠ a b c → 1 * π - 2 * ∠ a b c + (1 * π - (2 * π - 2 * ∠ a b c)) = 0
⊢ π - ∠ a b c < π / 2

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
⊢ π - ∠ a b c < π / 2

Tactic:
have h5 : π - ∠ a b c < π / 2 := by linarith
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : P
h : ¬Collinear ℝ (P := P) {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
by_contra! : ∀ (w1 : ∠ a c b < π - ∠ a b c), False
⊢ π - ∠ a b c ≤ ∠ a c b

Tactic:
by_contra! w1