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}
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}
h1₁ : dist a b < dist a c
⊢ ∠ 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}
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}
h1₁ : dist a b < dist a c
w₁ : ∠ a b c ≤ ∠ a c b
⊢ ∠ 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) {b, a, c}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
linarith : ∠ b a c = π → -(∠ b a c - π) + (∠ b a c - π) = 0
⊢ ∠ b a c ≠ π

Tactic:
linarith [angle_lt_pi_of_not_collinear h]

Premises used: EuclideanGeometry.angle_lt_pi_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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
⊢ dist a b = dist a c

Tactic:
have h4 : dist a b = dist a c := by
        apply dist_eq_of_angle_eq_angle_of_angle_ne_pi h2
        rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at h
        linarith [angle_lt_pi_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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
h4 : dist a b = dist a c
linarith : dist a b - dist a c + -(dist a b - dist a 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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h3 : ∠ a b c < ∠ a c b
⊢ Eq (α := Set P) {a, b, c} {a, c, b}

Tactic:
grind
-- 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
h3 : ∠ a b c < ∠ a c b
⊢ ¬Collinear ℝ (P := P) {a, c, b}

Tactic:
rw [show ({a, b, c} : Set P) = {a, c, b} by grind] 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
h3 : ∠ a b c < ∠ a c b
h₁ : ¬Collinear ℝ (P := P) {a, c, b}
⊢ dist a b < dist a c

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

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

Tactic:
rw [show ({a, b, c} : Set P) = {a, c, b} by grind] 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, c, b}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h3 : ∠ a b c < ∠ a c b
⊢ dist a c < dist a b

Tactic:
have h5 := dist_lt_of_angle_lt h h3
-- 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, c, b}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h3 : ∠ a b c < ∠ a c b
h5 : dist a c < dist a b
linarith : dist a b - dist a c + (dist a 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}
case : ∀ (h1 : dist a b < dist a c), ∠ a c b < ∠ a b c
case₁ : ∀ (h1 : dist a b < dist a c) (w : ∠ a b c ≤ ∠ a c b), False
inl : ∀ (h1 : dist a b < dist a c) (w : ∠ a b c ≤ ∠ a c b) (h2 : ∠ a b c = ∠ a c b), False
inr inr₁ : ∀ (h1 : dist a b < dist a c) (w : ∠ a b c ≤ ∠ a c b) (h3 : ∠ a b c < ∠ a c b), False
⊢ dist a b < dist a c → ∠ a c b < ∠ a b c

Tactic:
case mpr =>
    intro h1
    by_contra! w
    rcases w.eq_or_lt with h2 | h3
    · have h4 : dist a b = dist a c := by
        apply dist_eq_of_angle_eq_angle_of_angle_ne_pi h2
        rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at h
        linarith [angle_lt_pi_of_not_collinear h]
      linarith
    · rw [show ({a, b, c} : Set P) = {a, c, b} by grind] at h
      have h5 := dist_lt_of_angle_lt h h3
      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}
⊢ Eq (α := Set P) {a, b, c} {a, c, b}

Tactic:
grind
-- 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}
⊢ ¬Collinear ℝ (P := P) {a, c, b}

Tactic:
rw [show ({a, b, c} : Set P) = {a, c, b} by grind] 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, c, b}
⊢ ∠ a c b ≤ ∠ a b c ↔ dist a b ≤ dist a c

Tactic:
simpa using (angle_lt_iff_dist_lt h).not

Premises used: EuclideanGeometry.angle_lt_iff_dist_lt, Iff.not
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
pos : ∀ (h : p₂ = p₁), π / 3 ≤ ∠ p₁ p₂ p₃
neg : ∀ (h : ¬p₂ = p₁), π / 3 ≤ ∠ p₁ p₂ p₃
⊢ π / 3 ≤ ∠ p₁ p₂ p₃

Tactic:
by_cases h : p₂ = p₁
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : p₂ = p₁
pos : π / 3 ≤ π / 2
⊢ π / 3 ≤ ∠ p₁ p₂ p₃

Tactic:
rw [h, angle_self_left]

Premises used: EuclideanGeometry.angle_self_left
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : p₂ = p₁
linarith : π / 2 < π / 3 → 2 / 2 = 1
linarith₁ : π / 2 < π / 3 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₂ : π / 2 < π / 3 → 3 / 3 = 1
linarith₃ : π / 2 < π / 3 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₄ : π / 2 < π / 3 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 2 < π / 3 → 3 * π - 2 * π + (0 - π) = 0
⊢ π / 3 ≤ π / 2

Tactic:
linarith [Real.pi_pos]

Premises used: Real.pi_pos
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
linarith : ∠ p₁ p₂ p₃ < π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ∠ p₁ p₂ p₃ < π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ :
  ∠ p₁ p₂ p₃ < π / 3 →
    ∠ p₂ p₃ p₁ - ∠ p₁ p₂ p₃ + (∠ p₃ p₁ p₂ - ∠ p₁ p₂ p₃) + (3 * ∠ p₁ p₂ p₃ - 1 * π) +
        -(∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
⊢ π / 3 ≤ ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
pos : ∀ (h : p₂ = p₁), π / 3 < ∠ p₁ p₂ p₃
neg : ∀ (h : ¬p₂ = p₁), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
by_cases h : p₂ = p₁
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : p₂ = p₁
pos : π / 3 < π / 2
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
rw [h, angle_self_left]

Premises used: EuclideanGeometry.angle_self_left
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : p₂ = p₁
linarith : π / 2 ≤ π / 3 → 2 / 2 = 1
linarith₁ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₂ : π / 2 ≤ π / 3 → 3 / 3 = 1
linarith₃ : π / 2 ≤ π / 3 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₄ : π / 2 ≤ π / 3 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 2 ≤ π / 3 → 3 * π - 2 * π + (0 - π) = 0
⊢ π / 3 < π / 2

Tactic:
linarith [Real.pi_pos]

Premises used: Real.pi_pos
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
neg : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁), π / 3 < ∠ p₁ p₂ p₃
neg₁ : ∀ (hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂), π / 3 < ∠ p₁ p₂ p₃
neg₂ : ∀ (hne : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
rcases hne with hne | hne | hne
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁), π / 3 < ∠ p₁ p₂ p₃
neg₁ : ∀ (hne : ∠ p₂ p₃ p₁ < ∠ p₁ p₂ p₃), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
rcases hne.lt_or_gt with hne | hne

Premises used: Ne.lt_or_gt
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
neg : ∀ (hne : ∠ p₁ p₂ p₃ < ∠ p₃ p₁ p₂), π / 3 < ∠ p₁ p₂ p₃
neg₁ : ∀ (hne : ∠ p₃ p₁ p₂ < ∠ p₁ p₂ p₃), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
rcases hne.lt_or_gt with hne | hne

Premises used: Ne.lt_or_gt
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
neg : ∀ (hne : ∠ p₂ p₃ p₁ < ∠ p₃ p₁ p₂), π / 3 < ∠ p₁ p₂ p₃
neg₁ : ∀ (hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁), π / 3 < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
rcases hne.lt_or_gt with hne | hne

Premises used: Ne.lt_or_gt
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ : ∠ p₁ p₂ p₃ ≤ π / 3 → ∠ p₂ p₃ p₁ - ∠ p₁ p₂ p₃ + (∠ p₁ p₂ p₃ - ∠ p₂ p₃ p₁) = 0
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₂ p₃ p₁ < ∠ p₁ p₂ p₃
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ :
  ∠ p₁ p₂ p₃ ≤ π / 3 →
    ∠ p₃ p₁ p₂ - ∠ p₁ p₂ p₃ + (∠ p₂ p₃ p₁ - ∠ p₁ p₂ p₃) + (3 * ∠ p₁ p₂ p₃ - 1 * π) +
        -(∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ < ∠ p₃ p₁ p₂
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ : ∠ p₁ p₂ p₃ ≤ π / 3 → ∠ p₃ p₁ p₂ - ∠ p₁ p₂ p₃ + (∠ p₁ p₂ p₃ - ∠ p₃ p₁ p₂) = 0
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₁ p₂ p₃
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ :
  ∠ p₁ p₂ p₃ ≤ π / 3 →
    ∠ p₂ p₃ p₁ - ∠ p₁ p₂ p₃ + (∠ p₃ p₁ p₂ - ∠ p₁ p₂ p₃) + (3 * ∠ p₁ p₂ p₃ - 1 * π) +
        -(∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₂ p₃ p₁ < ∠ p₃ p₁ p₂
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ :
  ∠ p₁ p₂ p₃ ≤ π / 3 →
    2 * (∠ p₃ p₁ p₂ - ∠ p₁ p₂ p₃) + (∠ p₂ p₃ p₁ - ∠ p₃ p₁ p₂) + (3 * ∠ p₁ p₂ p₃ - 1 * π) +
        -(∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
linarith₄ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 2 0
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne_1 : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁
linarith : ∠ p₁ p₂ p₃ ≤ π / 3 → 3 / 3 = 1
linarith₁ : ∠ p₁ p₂ p₃ ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ :
  ∠ p₁ p₂ p₃ ≤ π / 3 →
    2 * (∠ p₂ p₃ p₁ - ∠ p₁ p₂ p₃) + (∠ p₃ p₁ p₂ - ∠ p₂ p₃ p₁) + (3 * ∠ p₁ p₂ p₃ - 1 * π) +
        -(∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
linarith₄ : ∠ p₁ p₂ p₃ ≤ π / 3 → GT.gt (α := ℝ) 2 0
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
pos : ∀ (h : p₂ = p₁), ∠ p₁ p₂ p₃ ≤ π / 3
neg : ∀ (h : ¬p₂ = p₁), ∠ p₁ p₂ p₃ ≤ π / 3
⊢ ∠ p₁ p₂ p₃ ≤ π / 3

Tactic:
by_cases h : p₂ = p₁
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : p₂ = p₁
pos :
  ∀ (h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂) (h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂) (hnd : p₂ ≠ p₂ ∨ p₂ ≠ p₃ ∨ p₂ ≠ p₃),
    ∠ p₂ p₂ p₃ ≤ π / 3
⊢ ∠ p₁ p₂ p₃ ≤ π / 3

Tactic:
subst 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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hnd : p₂ ≠ p₂ ∨ p₂ ≠ p₃ ∨ p₂ ≠ p₃
pos : ∀ (h₂₃₁ : π / 2 ≤ 0) (hnd : ¬p₂ = p₃), π / 2 ≤ π / 3
⊢ ∠ p₂ p₂ p₃ ≤ π / 3

Tactic:
simp_all [angle_self_of_ne]

Premises used: EuclideanGeometry.angle_self_of_ne
-- 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
p₂ p₃ : P
h₂₃₁ : π / 2 ≤ 0
hnd : ¬p₂ = p₃
linarith : π / 3 < π / 2 → 3 / 3 = 1
linarith₁ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 2 3 = 6
linarith₂ : π / 3 < π / 2 → 2 / 2 = 1
linarith₃ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 3 2 = 6
linarith₄ : π / 3 < π / 2 → GT.gt (α := ℝ) 6 0
linarith₅ : π / 3 < π / 2 → 2 / 2 = 1
linarith₆ : π / 3 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π / 3 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₈ : π / 3 < π / 2 → 1 * π - HMul.hMul (α := ℝ) 2 0 + (2 * π - 3 * π) = 0
⊢ π / 2 ≤ π / 3

Tactic:
linarith [Real.pi_pos]

Premises used: Real.pi_pos
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : ¬p₂ = p₁
linarith : π / 3 < ∠ p₁ p₂ p₃ → 3 / 3 = 1
linarith₁ : π / 3 < ∠ p₁ p₂ p₃ → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 < ∠ p₁ p₂ p₃ → GT.gt (α := ℝ) 3 0
linarith₃ :
  π / 3 < ∠ p₁ p₂ p₃ →
    ∠ p₁ p₂ p₃ - ∠ p₂ p₃ p₁ + (∠ p₁ p₂ p₃ - ∠ p₃ p₁ p₂) + (1 * π - 3 * ∠ p₁ p₂ p₃) +
        (∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ - π) =
      0
⊢ ∠ p₁ p₂ p₃ ≤ π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Premises used: EuclideanGeometry.angle_add_angle_add_angle_eq_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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
pos : ∀ (h : p₂ = p₁), ∠ p₁ p₂ p₃ < π / 3
neg : ∀ (h : ¬p₂ = p₁), ∠ p₁ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
by_cases h : p₂ = p₁
-- 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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : p₂ = p₁
pos :
  ∀ (h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂) (h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂)
    (hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂), ∠ p₂ p₂ p₃ < π / 3
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
subst 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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
pos : ∀ (h₂₃ : p₂ = p₃), ∠ p₂ p₂ p₃ < π / 3
neg : ∀ (h₂₃ : ¬p₂ = p₃), ∠ p₂ p₂ p₃ < π / 3
⊢ ∠ p₂ p₂ p₃ < π / 3

Tactic:
by_cases h₂₃ : p₂ = p₃
-- 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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : p₂ = p₃
pos :
  ∀ (h₂₃₁ h₃₁₂ : ∠ p₂ p₂ p₂ ≤ ∠ p₂ p₂ p₂)
    (hne : ∠ p₂ p₂ p₂ ≠ ∠ p₂ p₂ p₂ ∨ ∠ p₂ p₂ p₂ ≠ ∠ p₂ p₂ p₂ ∨ ∠ p₂ p₂ p₂ ≠ ∠ p₂ p₂ p₂), ∠ p₂ p₂ p₂ < π / 3
⊢ ∠ p₂ p₂ p₃ < π / 3

Tactic:
subst 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
p₂ : P
h₂₃₁ h₃₁₂ : ∠ p₂ p₂ p₂ ≤ ∠ p₂ p₂ p₂
hne : ∠ p₂ p₂ p₂ ≠ ∠ p₂ p₂ p₂ ∨ ∠ p₂ p₂ p₂ ≠ ∠ p₂ p₂ p₂ ∨ ∠ p₂ p₂ p₂ ≠ ∠ p₂ p₂ p₂
⊢ ∠ p₂ p₂ p₂ < π / 3

Tactic:
simp at hne
-- 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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : ¬p₂ = p₃
neg : ∀ (h₂₃₁ : π / 2 ≤ 0) (h₂₃ : ¬p₂ = p₃), π / 2 < π / 3
⊢ ∠ p₂ p₂ p₃ < π / 3

Tactic:
simp_all [angle_self_of_ne]

Premises used: EuclideanGeometry.angle_self_of_ne