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 : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c b + ∠ a p c + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
ep : ∠ a p b + ∠ a p c = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have linarith : ∠ b a p + ∠ p a c < ∠ b a c →
  ∠ b a p + ∠ p a c - ∠ b a c + (∠ b a c + ∠ a c b + ∠ c b a - π) + -(∠ b a p + ∠ a p b + ∠ c b a - π) +
        -(∠ a c b + ∠ a p c + ∠ p a c - π) +
      (∠ a p b + ∠ a p c - π) =
    0
Tactic: linarith only [ea, eb, ec, ep]
-- 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 : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c b + ∠ a p c + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
ep : ∠ a p b + ∠ a p c = π
linarith :
  ∠ b a p + ∠ p a c < ∠ b a c →
    ∠ b a p + ∠ p a c - ∠ b a c + (∠ b a c + ∠ a c b + ∠ c b a - π) + -(∠ b a p + ∠ a p b + ∠ c b a - π) +
          -(∠ a c b + ∠ a p c + ∠ p a c - π) +
        (∠ a p b + ∠ a p c - π) =
      0
⊢ ∠ b a p + ∠ p a c = ∠ b a c
have linarith₁ : ∠ b a c < ∠ b a p + ∠ p a c →
  ∠ b a c - (∠ b a p + ∠ p a c) + -(∠ b a c + ∠ a c b + ∠ c b a - π) + (∠ b a p + ∠ a p b + ∠ c b a - π) +
        (∠ a c b + ∠ a p c + ∠ p a c - π) +
      -(∠ a p b + ∠ a p c - π) =
    0
Tactic: linarith only [ea, eb, ec, ep]
-- 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 : P
h : ∠ b p c = π
⊢ HPow.hPow (β := ℕ) (dist a b) 2 * dist c p + HPow.hPow (β := ℕ) (dist a c) 2 * dist b p =
    dist b c * (HPow.hPow (β := ℕ) (dist a p) 2 + dist b p * dist c p)
have rw : (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * -Real.cos (∠ a p c)) * dist c p +
    (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
  (dist b p + dist c p) * (HPow.hPow (β := ℕ) (dist a p) 2 + dist b p * dist c p)
Tactic: rw [pow_two, pow_two, law_cos a p b, law_cos a p c,
    eq_sub_of_add_eq (angle_add_angle_eq_pi_of_angle_eq_pi a h), Real.cos_pi_sub,
    dist_eq_add_dist_of_angle_eq_pi 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
⊢ HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
have pos : ∀ (hbc : b = c),
  HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
Tactic: by_cases hbc : b = c
-- 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
pos :
  ∀ (hbc : b = c),
    HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
      2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
⊢ HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
have neg : ∀ (hbc : ¬b = c),
  HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
Tactic: by_cases hbc : b = c
-- 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
hbc : ¬b = c
m : P := midpoint ℝ b c
⊢ HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
have this : dist b c ≠ 0
Tactic: have : dist b c ≠ 0 := (dist_pos.mpr hbc).ne'
-- 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
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
⊢ HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
have hm : HPow.hPow (β := ℕ) (dist a b) 2 * dist c m + HPow.hPow (β := ℕ) (dist a c) 2 * dist b m =
  dist b c * (HPow.hPow (β := ℕ) (dist a m) 2 + dist b m * dist c m)
Tactic: have hm := dist_sq_mul_dist_add_dist_sq_mul_dist a b c m (angle_midpoint_eq_pi b c hbc)
-- 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
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  HPow.hPow (β := ℕ) (dist a b) 2 * dist c m + HPow.hPow (β := ℕ) (dist a c) 2 * dist b m =
    dist b c * (HPow.hPow (β := ℕ) (dist a m) 2 + dist b m * dist c m)
⊢ HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
have hm₁ : HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c) =
  dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
Tactic: simp only [m, dist_left_midpoint, dist_right_midpoint, Real.norm_two] at hm
Cleared hypotheses: hm
-- 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
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c) =
    dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
⊢ 2 / dist b c *
      (HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c)) =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
have rw : 2 / dist b c * (dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))) =
  2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
Tactic: rw [hm]
-- 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
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c) =
    dist b c * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
⊢ HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (dist b c / 2) 2)
have dist : HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist a c) 2 =
  2 / dist b c *
    (HPow.hPow (β := ℕ) (dist a b) 2 * (2⁻¹ * dist b c) + HPow.hPow (β := ℕ) (dist a c) 2 * (2⁻¹ * dist b c))
Tactic: calc
      dist a b ^ 2 + dist a c ^ 2 = 2 / dist b c * (dist a b ^ 2 *
        ((2 : ℝ)⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c)) := by
        field
      _ = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2) := by
        rw [hm]
        field
-- 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
hbc : ¬b = c
m : P := midpoint ℝ b c
this : Dist.dist b c ≠ 0
hm :
  HPow.hPow (β := ℕ) (Dist.dist a b) 2 * (2⁻¹ * Dist.dist b c) +
      HPow.hPow (β := ℕ) (Dist.dist a c) 2 * (2⁻¹ * Dist.dist b c) =
    Dist.dist b c * (HPow.hPow (β := ℕ) (Dist.dist a (midpoint ℝ b c)) 2 + 2⁻¹ * Dist.dist b c * (2⁻¹ * Dist.dist b c))
dist :
  HPow.hPow (β := ℕ) (Dist.dist a b) 2 + HPow.hPow (β := ℕ) (Dist.dist a c) 2 =
    2 / Dist.dist b c *
      (HPow.hPow (β := ℕ) (Dist.dist a b) 2 * (2⁻¹ * Dist.dist b c) +
        HPow.hPow (β := ℕ) (Dist.dist a c) 2 * (2⁻¹ * Dist.dist b c))
⊢ HPow.hPow (β := ℕ) (Dist.dist a b) 2 + HPow.hPow (β := ℕ) (Dist.dist a c) 2 =
    2 * (HPow.hPow (β := ℕ) (Dist.dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (Dist.dist b c / 2) 2)
have dist₁ : 2 / Dist.dist b c *
    (HPow.hPow (β := ℕ) (Dist.dist a b) 2 * (2⁻¹ * Dist.dist b c) +
      HPow.hPow (β := ℕ) (Dist.dist a c) 2 * (2⁻¹ * Dist.dist b c)) =
  2 * (HPow.hPow (β := ℕ) (Dist.dist a (midpoint ℝ b c)) 2 + HPow.hPow (β := ℕ) (Dist.dist b c / 2) 2)
Tactic: calc
      dist a b ^ 2 + dist a c ^ 2 = 2 / dist b c * (dist a b ^ 2 *
        ((2 : ℝ)⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c)) := by
        field
      _ = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2) := by
        rw [hm]
        field
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c') =
    HPow.hPow (β := ℕ) r 2 *
      (HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist c b) 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))
have rw : HPow.hPow (β := ℕ) (r * dist a b) 2 + HPow.hPow (β := ℕ) (r * dist c b) 2 -
    2 * (r * dist a b) * (r * dist c b) * Real.cos (∠ a b c) =
  HPow.hPow (β := ℕ) r 2 *
    (HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist c b) 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))
Tactic: rw [h, hab, hcb]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ HPow.hPow (β := ℕ) r 2 *
      (HPow.hPow (β := ℕ) (dist a b) 2 + HPow.hPow (β := ℕ) (dist c b) 2 -
        2 * dist a b * dist c b * Real.cos (∠ a b c)) =
    HPow.hPow (β := ℕ) (r * dist a c) 2
have simp : r * r * (dist a c * dist a c) = r * dist a c * (r * dist a c)
Tactic: simp [pow_two, ← law_cos a b c]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ dist a' c' = r * dist a c
have h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
Tactic: have h' : dist a' c' ^ 2 = (r * dist a c) ^ 2 := calc
    dist a' c' ^ 2 =
        dist a' b' ^ 2 + dist c' b' ^ 2 - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c') := by
      simp [pow_two, law_cos a' b' c']
    _ = r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c)) := by
      rw [h, hab, hcb]; ring
    _ = (r * dist a c) ^ 2 := by simp [pow_two, ← law_cos a b c]; ring
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
⊢ dist a' c' = r * dist a c
have pos : ∀ (hab₁ : a = b), dist a' c' = r * dist a c
Tactic: by_cases hab₁ : a = 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
pos : ∀ (hab₁ : a = b), dist a' c' = r * dist a c
⊢ dist a' c' = r * dist a c
have neg : ∀ (hab₁ : ¬a = b), dist a' c' = r * dist a c
Tactic: by_cases hab₁ : a = 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
⊢ a' = b'
have rw : dist a' b' = 0
Tactic: rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
rw : dist a' b' = 0
⊢ a' = b'
have rw₁ : r * dist a b = 0
Tactic: rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
rw : dist a' b' = 0
rw₁ : r * dist a b = 0
⊢ a' = b'
have rw₂ : r * 0 = 0
Tactic: rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
rw : dist a' b' = 0
rw₁ : r * dist a b = 0
rw₂ : r * 0 = 0
⊢ a' = b'
have rw₃ : Eq (α := ℝ) 0 0
Tactic: rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
⊢ dist a' c' = r * dist a c
have hab'₁ : a' = b'
Tactic: have hab'₁ : a' = b' := by
      rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
hab'₁ : a' = b'
⊢ dist a' c' = r * dist a c
have pos : dist a' c' = r * dist b c
Tactic: rw [hab₁, hab'₁, dist_comm b' c', dist_comm b c, hcb]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
hab'₁ : a' = b'
pos : dist a' c' = r * dist b c
⊢ dist a' c' = r * dist a c
have pos₁ : dist b' c' = r * dist b c
Tactic: rw [hab₁, hab'₁, dist_comm b' c', dist_comm b c, hcb]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
hab'₁ : a' = b'
pos : dist a' c' = r * dist b c
pos₁ : dist b' c' = r * dist b c
⊢ dist a' c' = r * dist a c
have pos₂ : dist c' b' = r * dist b c
Tactic: rw [hab₁, hab'₁, dist_comm b' c', dist_comm b c, hcb]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : a = b
hab'₁ : a' = b'
pos : dist a' c' = r * dist b c
pos₁ : dist b' c' = r * dist b c
pos₂ : dist c' b' = r * dist b c
pos₃ : dist c' b' = r * dist c b
⊢ dist a' c' = r * dist a c
have pos₄ : r * dist c b = r * dist c b
Tactic: rw [hab₁, hab'₁, dist_comm b' c', dist_comm b c, hcb]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
⊢ 0 ≤ r * dist a b
have rw : 0 ≤ dist a' b'
Tactic: rw [← hab]
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
⊢ dist a' c' = r * dist a c
have h1 : 0 ≤ r * dist a b
Tactic: have h1 : 0 ≤ r * dist a b := by rw [← hab]; exact dist_nonneg
-- 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 a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : HPow.hPow (β := ℕ) (dist a' c') 2 = HPow.hPow (β := ℕ) (r * dist a c) 2
hab₁ : ¬a = b
h1 : 0 ≤ r * dist a b
⊢ dist a' c' = r * dist a c
have h2 : 0 ≤ r
Tactic: have h2 : 0 ≤ r := nonneg_of_mul_nonneg_left h1 (dist_pos.mpr hab₁)
-- 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 hsin : Real.sin (∠ c b a) * dist b a = Real.sin (∠ a c b) * dist a c
Tactic: have hsin := law_sin c b a
-- 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 (∠ c b a) * dist b a = Real.sin (∠ a c b) * dist a c
⊢ ∠ a c b < ∠ a b c → dist a b < dist a c
have hsin₁ : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
Tactic: rw [dist_comm b a, angle_comm c b a] at hsin
Cleared hypotheses: hsin
-- 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
⊢ ∠ a c b < ∠ a b c → dist a b < dist a c
have hac : dist a c > 0
Tactic: have hac : dist a c > 0 := dist_pos.mpr (ne₁₃_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
⊢ Real.sin (∠ a b c) ≥ 0
have hx : ∠ a b c ∈ Set.Icc 0 π
Tactic: apply Real.sin_nonneg_of_mem_Icc
-- 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
⊢ ∠ a c b < ∠ a b c → dist a b < dist a c
have hsinabc : Real.sin (∠ a b c) ≥ 0
Tactic: have hsinabc : Real.sin (∠ a b c) ≥ 0 := by
    apply Real.sin_nonneg_of_mem_Icc
    simp [angle_nonneg, angle_le_pi]
-- 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
⊢ dist a b < dist a c
have pos : ∀ (h2 : ∠ a b c ≤ π / 2), dist a b < dist a c
Tactic: by_cases! h2 : ∠ a b c ≤ π / 2
-- 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
pos : ∀ (h2 : ∠ a b c ≤ π / 2), dist a b < dist a c
⊢ dist a b < dist a c
have neg : ∀ (h2 : π / 2 < ∠ a b c), dist a b < dist a c
Tactic: by_cases! h2 : ∠ a b c ≤ π / 2
-- 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
⊢ -(π / 2) ≤ ∠ a c b
have linarith : ∠ a c b < -(π / 2) → 2 / 2 = 1
Tactic: linarith [angle_nonneg a c b]