awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have linarith₂ : GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have linarith₆ : Real.sin (π - ∠ a b c) - Real.sin (∠ a c b) + (Real.sin (∠ a c b) - Real.sin (π - ∠ a b c)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have h6 : π - ∠ 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have h7 : ∠ 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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 = π
⊢ False
have h7₁ : ∠ a b c + ∠ a c b + ∠ c a b = π
Tactic: rw [angle_comm b c a] at h7
Cleared hypotheses: h7
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
have rw : ∠ b a c > 0
Tactic: rw [angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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 = π
⊢ ∠ b a c > 0
have h₁ : ¬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
Cleared hypotheses: h, hsin, hac, hsinabc, h1, h2, w, h3, h5, h6, h7
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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 = π
⊢ False
have h8 : ∠ 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have linarith : 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have linarith₂ : GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have linarith₆ : π - ∠ a b c - ∠ a c b + (∠ a b c + ∠ a c b + ∠ c a b - π) + (0 - ∠ c a b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ (P := P) {a, b, c}
⊢ ∠ a c b < ∠ a b c ↔ dist a b < dist a c
have constructor : ∠ a c b < ∠ a b c → dist a b < dist a c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ (P := P) {a, b, c}
constructor : ∠ a c b < ∠ a b c → dist a b < dist a c
⊢ ∠ a c b < ∠ a b c ↔ dist a b < dist a c
have constructor₁ : dist a b < dist a c → ∠ a c b < ∠ a b c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ (P := P) {a, b, c}
h1 : dist a b < dist a c
⊢ ∠ a c b < ∠ a b c
have by_contra! : ∀ (w : ∠ a b c ≤ ∠ a c b), False
Tactic: by_contra! w
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ (P := P) {a, b, c}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
⊢ False
have inl : ∀ (h2 : ∠ a b c = ∠ a c b), False
Tactic: rcases w.eq_or_lt with h2 | h3
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have inr : ∀ (h3 : ∠ a b c < ∠ a c b), False
Tactic: rcases w.eq_or_lt with h2 | h3
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
have apply : ∠ b a c ≠ π
Tactic: apply dist_eq_of_angle_eq_angle_of_angle_ne_pi h2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ ∠ b a c ≠ π
have h₁ : ¬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
Cleared hypotheses: h, h1, w, h2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ ∠ b a c ≠ π
have linarith : ∠ b a c = π → -(∠ b a c - π) + (∠ b a c - π) = 0
Tactic: linarith [angle_lt_pi_of_not_collinear h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have h4 : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have linarith : dist a b - dist a c + -(dist a b - dist a c) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have h₁ : ¬Collinear ℝ (P := P) {a, c, b}
Tactic: rw [show ({a, b, c} : Set P) = {a, c, b} by grind] at h
Cleared hypotheses: h, h1, w, h3
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have h5 : dist a c < dist a b
Tactic: have h5 := dist_lt_of_angle_lt h h3
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ False
have linarith : dist a b - dist a c + (dist a c - dist a b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ (P := P) {a, b, c}
case : ∀ (h1 : dist a b < dist a c), ∠ a c b < ∠ a b c
⊢ dist a b < dist a c → ∠ a c b < ∠ a b c
have case₁ : ∀ (h1 : dist a b < dist a c) (w : ∠ a b c ≤ ∠ a c b), False
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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ dist a b < dist a c → ∠ a c b < ∠ a b c
have inl : ∀ (h1 : dist a b < dist a c) (w : ∠ a b c ≤ ∠ a c b) (h2 : ∠ a b c = ∠ a c b), False
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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : 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
⊢ dist a b < dist a c → ∠ a c b < ∠ a b c
have inr : ∀ (h1 : dist a b < dist a c) (w : ∠ a b c ≤ ∠ a c b) (h3 : ∠ a b c < ∠ a c b), False
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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ (P := P) {a, b, c}
⊢ ∠ a c b ≤ ∠ a b c ↔ dist a b ≤ dist a c
have h₁ : ¬Collinear ℝ (P := P) {a, c, b}
Tactic: rw [show ({a, b, c} : Set P) = {a, c, b} by grind] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
⊢ π / 3 ≤ ∠ p₁ p₂ p₃
have pos : ∀ (h : p₂ = p₁), π / 3 ≤ ∠ p₁ p₂ p₃
Tactic: by_cases h : p₂ = p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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₃
⊢ π / 3 ≤ ∠ p₁ p₂ p₃
have neg : ∀ (h : ¬p₂ = p₁), π / 3 ≤ ∠ p₁ p₂ p₃
Tactic: by_cases h : p₂ = p₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : p₂ = p₁
⊢ π / 3 ≤ ∠ p₁ p₂ p₃
have pos : π / 3 ≤ π / 2
Tactic: rw [h, angle_self_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : p₂ = p₁
⊢ π / 3 ≤ π / 2
have linarith : π / 2 < π / 3 → 2 / 2 = 1
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
⊢ π / 3 ≤ π / 2
have linarith₁ : π / 2 < π / 3 → HMul.hMul (α := ℝ) 3 2 = 6
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
⊢ π / 3 ≤ π / 2
have linarith₂ : π / 2 < π / 3 → 3 / 3 = 1
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
⊢ π / 3 ≤ π / 2
have linarith₃ : π / 2 < π / 3 → HMul.hMul (α := ℝ) 2 3 = 6
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
⊢ π / 3 ≤ π / 2
have linarith₄ : π / 2 < π / 3 → GT.gt (α := ℝ) 6 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
⊢ π / 3 ≤ π / 2
have linarith₅ : π / 2 < π / 3 → 3 * π - 2 * π + (0 - π) = 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
⊢ π / 3 ≤ ∠ p₁ p₂ p₃
have linarith : ∠ p₁ p₂ p₃ < π / 3 → 3 / 3 = 1
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
⊢ π / 3 ≤ ∠ p₁ p₂ p₃
have linarith₁ : ∠ p₁ p₂ p₃ < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [angle_add_angle_add_angle_eq_pi p₃ h]