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 : 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
w1 : ∠ a c b < π - ∠ a b c
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 / 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) →
    1 * π - 2 * ∠ a b c + 2 * (∠ a c b - (π - ∠ a b c)) + (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 : π / 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
w1 : ∠ a c b < π - ∠ a b c
⊢ Real.sin (∠ a c b) < Real.sin (π - ∠ a b c)

Tactic:
have := Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith [angle_nonneg a c b]) h5.le 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
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
w1 : ∠ a c b < π - ∠ a b c
this : Real.sin (∠ a c b) < Real.sin (π - ∠ a b c)
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : Real.sin (π - ∠ a b c) - Real.sin (∠ a c b) + (Real.sin (∠ a c b) - Real.sin (π - ∠ a b c)) = 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
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
⊢ π - ∠ a b c ≤ ∠ a c b

Tactic:
have h6 : π - ∠ a b c ≤ ∠ a c b := by
      by_contra! w1
      have := Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith [angle_nonneg a c b]) h5.le w1
      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
h6 : π - ∠ a b c ≤ ∠ a c b
⊢ ∠ a b c + ∠ b c a + ∠ c a b = π

Tactic:
have h7 := angle_add_angle_add_angle_eq_pi c (ne₁₂_of_not_collinear h).symm
-- 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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ b c a + ∠ c a b = π
⊢ ∠ a b c + ∠ a c b + ∠ c a b = π

Tactic:
rw [angle_comm b c a] at h7

Premises used: EuclideanGeometry.angle_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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
rw : ∠ b a c > 0
⊢ ∠ c a b > 0

Tactic:
rw [angle_comm]

Premises used: EuclideanGeometry.angle_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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
⊢ Eq (α := Set P) {a, b, c} {b, a, c}

Tactic:
Set.insert_comm a b {c}

Premises used: Set.insert_comm, Singleton.singleton
-- 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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
⊢ Eq (α := Set P) {a, b, c} {b, a, c}

Tactic:
exact Set.insert_comm a b {c}

Premises used: Set.insert_comm, Singleton.singleton
-- 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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
⊢ ¬Collinear ℝ (P := P) {b, a, c}

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, c}
⊢ Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, c}
hsin₁ : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
⊢ dist a c > 0

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, 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:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, 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
⊢ ∠ a c b < ∠ a b c

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, 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
⊢ π / 2 < ∠ a b c

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, 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
⊢ dist a c ≤ dist a b

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, 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:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, 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:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, 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
⊢ π - ∠ a b c ≤ ∠ a c b

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h₁ : ¬Collinear ℝ (P := P) {b, a, 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
h6₁ : π - ∠ a b c ≤ ∠ a c b
⊢ ∠ a b c + ∠ a c b + ∠ c a b = π

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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) {b, a, 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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
⊢ ∠ b a c > 0

Tactic:
angle_pos_of_not_collinear h

Premises used: EuclideanGeometry.angle_pos_of_not_collinear
-- 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) {b, a, 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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
⊢ ∠ b a c > 0

Tactic:
exact angle_pos_of_not_collinear h

Premises used: EuclideanGeometry.angle_pos_of_not_collinear
-- 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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
⊢ ∠ c a b > 0

Tactic:
have h8 : ∠ c a b > 0 := by
      rw [angle_comm]
      rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at h
      exact angle_pos_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
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
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
h8 : ∠ c a b > 0
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : π - ∠ a b c - ∠ a c b + (∠ a b c + ∠ a c b + ∠ c a b - π) + (0 - ∠ c 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}
constructor : ∠ a c b < ∠ a b c → dist a b < dist a c
constructor₁ : dist a b < dist a c → ∠ a c b < ∠ a b c
⊢ ∠ a c b < ∠ a b c ↔ dist a b < dist a c

Tactic:
constructor
-- 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}
⊢ ∠ a c b < ∠ a b c → dist a b < dist a c

Tactic:
dist_lt_of_angle_lt h

Premises used: EuclideanGeometry.dist_lt_of_angle_lt
-- 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}
⊢ ∠ a c b < ∠ a b c → dist a b < dist a c

Tactic:
exact dist_lt_of_angle_lt h

Premises used: EuclideanGeometry.dist_lt_of_angle_lt
-- 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}
⊢ ∠ a c b < ∠ a b c → dist a b < dist a c

Tactic:
case mp =>
    exact dist_lt_of_angle_lt h

Premises used: EuclideanGeometry.dist_lt_of_angle_lt
-- 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}
h1 : dist a b < dist a c
by_contra! : ∀ (w : ∠ a b c ≤ ∠ a c b), False
⊢ ∠ a c b < ∠ a b 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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
inl : ∀ (h2 : ∠ a b c = ∠ a c b), False
inr : ∀ (h3 : ∠ a b c < ∠ a c b), False
⊢ False

Tactic:
rcases w.eq_or_lt with h2 | h3

Premises used: LE.le.eq_or_lt
-- 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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
apply : ∠ b a c ≠ π
⊢ dist a b = dist a c

Tactic:
apply dist_eq_of_angle_eq_angle_of_angle_ne_pi h2

Premises used: EuclideanGeometry.dist_eq_of_angle_eq_angle_of_angle_ne_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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
⊢ Eq (α := Set P) {a, b, c} {b, a, c}

Tactic:
Set.insert_comm a b {c}

Premises used: Set.insert_comm, Singleton.singleton
-- 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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
⊢ Eq (α := Set P) {a, b, c} {b, a, c}

Tactic:
exact Set.insert_comm a b {c}

Premises used: Set.insert_comm, Singleton.singleton
-- 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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
⊢ ¬Collinear ℝ (P := P) {b, a, c}

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
h₁ : ¬Collinear ℝ (P := P) {b, a, c}
⊢ dist a b < dist a c

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at h