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 : ∠ a b c ≤ π / 2
linarith : ∠ a c b < -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) ≤ ∠ a c b
have linarith₁ : ∠ a c b < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [angle_nonneg a c b]
-- 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 : ∠ a b c ≤ π / 2
linarith : ∠ a c b < -(π / 2) → 2 / 2 = 1
linarith₁ : ∠ a c b < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) ≤ ∠ a c b
have linarith₂ : ∠ a c b < -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith [angle_nonneg a c b]
-- 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 : ∠ 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
⊢ -(π / 2) ≤ ∠ a c b
have 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
Tactic: linarith [angle_nonneg a c b]
-- 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 : ∠ 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
⊢ -(π / 2) ≤ ∠ a c b
have linarith₈ : ∠ a c b < -(π / 2) → GT.gt (α := ℝ) 4 0
Tactic: linarith [angle_nonneg a c b]
-- 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 : ∠ a b c ≤ π / 2
⊢ dist a b < dist a c
have h3 : 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
-- 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 : ∠ a b c ≤ π / 2
h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
⊢ dist a b < dist a c
have pos : ∀ (w : dist a c ≤ dist a b), False
Tactic: by_contra! w
-- 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 : ∠ a b c ≤ π / 2
h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
w : dist a c ≤ dist a b
⊢ False
have h4 : 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
-- 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 : ∠ 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
⊢ 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 : ∠ 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
⊢ 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 : ∠ 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
⊢ 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 : ∠ 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
⊢ False
have 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
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
⊢ dist a b < dist a c
have neg : ∀ (w : dist a c ≤ dist a 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}
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)
have by_contra! : ∀ (w1 : Real.sin (∠ a c b) < Real.sin (∠ a b c)), False
Tactic: by_contra! w1
-- 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
w1 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
⊢ False
have h4 : 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
-- 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
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
⊢ 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
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
⊢ 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
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
⊢ 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
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
⊢ False
have 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
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
⊢ False
have h3 : 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
-- 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)
⊢ False
have h3₁ : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
Tactic: rw [← Real.sin_pi_sub (∠ a b c)] at h3
Cleared hypotheses: 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}
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
have linarith : π / 2 ≤ π - ∠ a b c → 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)
linarith : π / 2 ≤ π - ∠ a b c → 2 / 2 = 1
⊢ π - ∠ a b c < π / 2
have linarith₁ : π / 2 ≤ π - ∠ a b c → 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)
linarith : π / 2 ≤ π - ∠ a b c → 2 / 2 = 1
linarith₁ : π / 2 ≤ π - ∠ a b c → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π - ∠ a b c < π / 2
have linarith₂ : π / 2 ≤ π - ∠ a b c → 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)
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
⊢ π - ∠ a b c < π / 2
have linarith₆ : π / 2 ≤ π - ∠ a b c → 1 * π - 2 * ∠ a b c + (1 * π - (2 * π - 2 * ∠ 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)
⊢ False
have h5 : π - ∠ a b c < π / 2
Tactic: have h5 : π - ∠ a b c < π / 2 := by 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
⊢ π - ∠ a b c ≤ ∠ a c b
have by_contra! : ∀ (w1 : ∠ a c b < π - ∠ a b c), False
Tactic: by_contra! w1
-- 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
⊢ -(π / 2) ≤ ∠ a c b
have linarith : ∠ a c b < -(π / 2) → 2 / 2 = 1
Tactic: linarith [angle_nonneg a c b]
-- 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
linarith : ∠ a c b < -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) ≤ ∠ a c b
have linarith₁ : ∠ a c b < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [angle_nonneg a c b]
-- 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
linarith : ∠ a c b < -(π / 2) → 2 / 2 = 1
linarith₁ : ∠ a c b < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) ≤ ∠ a c b
have linarith₂ : ∠ a c b < -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith [angle_nonneg a c b]
-- 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
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
⊢ -(π / 2) ≤ ∠ a c b
have 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
Tactic: linarith [angle_nonneg a c b]
-- 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
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
⊢ -(π / 2) ≤ ∠ a c b
have linarith₁₁ : ∠ a c b < -(π / 2) → GT.gt (α := ℝ) 4 0
Tactic: linarith [angle_nonneg a c b]
-- 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
w1 : ∠ a c b < π - ∠ a b c
⊢ False
have this : 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
-- 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)
⊢ False
have linarith : 2 / 2 = 1
Tactic: linarith