awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
rw : 2 * a * b = 2 * a * b * 1
⊢ 2 * a * b = 2 * a * b * (ε * ε⁻¹)
have rw₁ : 2 * a * b = 2 * a * b
Tactic: rw [mul_inv_cancel₀ hε.ne', mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
⊢ 2 * a * b * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹
have simp_rw : 2 * (a * (b * (ε * ε⁻¹))) = 2 * (ε * (a * (b * ε⁻¹)))
Tactic: simp_rw [mul_assoc, mul_comm ε, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
simp_rw : 2 * (a * (b * (ε * ε⁻¹))) = 2 * (ε * (a * (b * ε⁻¹)))
⊢ 2 * a * b * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹
have simp_rw₁ : 2 * (a * (b * (ε⁻¹ * ε))) = 2 * (a * (b * ε⁻¹) * ε)
Tactic: simp_rw [mul_assoc, mul_comm ε, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
⊢ 2 * (ε * a) * b * ε⁻¹ ≤ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹
have ha : 0 ≤ ε⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
⊢ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have rw : ε⁻¹ * (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) =
  ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
rw :
  ε⁻¹ * (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
⊢ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have rw₁ : ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) =
  ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
rw :
  ε⁻¹ * (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₁ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
⊢ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have rw₂ : ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2) + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
  ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
rw :
  ε⁻¹ * (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₁ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₂ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2) + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
⊢ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have rw₃ : ε⁻¹ * HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
  ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
rw :
  ε⁻¹ * (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₁ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₂ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2) + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₃ :
  ε⁻¹ * HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
⊢ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have rw₄ : ε⁻¹ * (ε * ε) * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
  ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
rw :
  ε⁻¹ * (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₁ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₂ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2) + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₃ :
  ε⁻¹ * HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₄ :
  ε⁻¹ * (ε * ε) * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
⊢ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have rw₅ : ε⁻¹ * ε * ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
  ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
rw :
  ε⁻¹ * (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₁ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₂ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2) + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₃ :
  ε⁻¹ * HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₄ :
  ε⁻¹ * (ε * ε) * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₅ :
  ε⁻¹ * ε * ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
⊢ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have rw₆ : 1 * ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
  ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
rw :
  ε⁻¹ * (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₁ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₂ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2) + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₃ :
  ε⁻¹ * HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₄ :
  ε⁻¹ * (ε * ε) * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₅ :
  ε⁻¹ * ε * ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₆ :
  1 * ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
⊢ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have rw₇ : ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 = ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
⊢ 2 * a * b ≤ ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have calc : 2 * a * b = 2 * a * b * (ε * ε⁻¹)
Tactic: calc 2 * a * b
  _ = 2 * a * b * (ε * ε⁻¹) := by rw [mul_inv_cancel₀ hε.ne', mul_one]
  _ = (2 * (ε * a) * b) * ε⁻¹ := by simp_rw [mul_assoc, mul_comm ε, mul_assoc]
  _ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ := by gcongr; exact inv_nonneg.mpr hε.le
  _ = ε * a ^ 2 + ε⁻¹ * b ^ 2 := by
    rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
calc : 2 * a * b = 2 * a * b * (ε * ε⁻¹)
⊢ 2 * a * b ≤ ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have calc₁ : 2 * a * b * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹
Tactic: calc 2 * a * b
  _ = 2 * a * b * (ε * ε⁻¹) := by rw [mul_inv_cancel₀ hε.ne', mul_one]
  _ = (2 * (ε * a) * b) * ε⁻¹ := by simp_rw [mul_assoc, mul_comm ε, mul_assoc]
  _ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ := by gcongr; exact inv_nonneg.mpr hε.le
  _ = ε * a ^ 2 + ε⁻¹ * b ^ 2 := by
    rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
calc : 2 * a * b = 2 * a * b * (ε * ε⁻¹)
calc₁ : 2 * a * b * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹
⊢ 2 * a * b ≤ ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have calc₂ : 2 * (ε * a) * b * ε⁻¹ ≤ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹
Tactic: calc 2 * a * b
  _ = 2 * a * b * (ε * ε⁻¹) := by rw [mul_inv_cancel₀ hε.ne', mul_one]
  _ = (2 * (ε * a) * b) * ε⁻¹ := by simp_rw [mul_assoc, mul_comm ε, mul_assoc]
  _ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ := by gcongr; exact inv_nonneg.mpr hε.le
  _ = ε * a ^ 2 + ε⁻¹ * b ^ 2 := by
    rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
calc : 2 * a * b = 2 * a * b * (ε * ε⁻¹)
calc₁ : 2 * a * b * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹
calc₂ : 2 * (ε * a) * b * ε⁻¹ ≤ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹
⊢ 2 * a * b ≤ ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have calc₃ : (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
  ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
Tactic: calc 2 * a * b
  _ = 2 * a * b * (ε * ε⁻¹) := by rw [mul_inv_cancel₀ hε.ne', mul_one]
  _ = (2 * (ε * a) * b) * ε⁻¹ := by simp_rw [mul_assoc, mul_comm ε, mul_assoc]
  _ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ := by gcongr; exact inv_nonneg.mpr hε.le
  _ = ε * a ^ 2 + ε⁻¹ * b ^ 2 := by
    rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Canonical (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : IsStrictOrderedRing α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
⊢ (a - b) / c = a / c - b / c
have simp_rw : (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
Tactic: simp_rw [div_eq_mul_inv, tsub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : x ≠ 0
h1 : x < 1
n : ℕ
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹
have rw : ∀ (h0 : 0 < x) (h1 : x < 1) (n : ℕ), ∑ i ∈ range n, x ^ i < (1 - x)⁻¹
Tactic: rw [← pos_iff_ne_zero] at h0
Cleared hypotheses: h0, h1, n
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹
have rw : LT.lt.{u_1} (α := K) 0 1 ∧ 0 < x ^ n
Tactic: rw [geom_sum_of_lt_one h1, div_lt_iff₀, inv_mul_cancel₀, tsub_lt_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
rw : LT.lt.{u_1} (α := K) 0 1 ∧ 0 < x ^ n
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹
have rw₁ : 1 - x ≠ 0
Tactic: rw [geom_sum_of_lt_one h1, div_lt_iff₀, inv_mul_cancel₀, tsub_lt_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
rw : LT.lt.{u_1} (α := K) 0 1 ∧ 0 < x ^ n
rw₁ : 1 - x ≠ 0
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹
have rw₂ : 0 < 1 - x
Tactic: rw [geom_sum_of_lt_one h1, div_lt_iff₀, inv_mul_cancel₀, tsub_lt_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 1 - x ≠ 0
have rwa : ¬1 - x = 0
Tactic: rwa [ne_eq, tsub_eq_zero_iff_le, not_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
rwa : ¬1 - x = 0
⊢ 1 - x ≠ 0
have rwa₁ : ¬1 ≤ x
Tactic: rwa [ne_eq, tsub_eq_zero_iff_le, not_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
have inl : ∀ (hmn : m ≤ n), ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
Tactic: rcases le_or_gt m n with (hmn | hmn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
inl : ∀ (hmn : m ≤ n), ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
have inr : ∀ (hmn : n < m), ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
Tactic: rcases le_or_gt m n with (hmn | hmn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
have inl : (x ^ m - x ^ n) / (1 - x) ≤ x ^ m / (1 - x)
Tactic: rw [geom_sum_Ico' h'x.ne hmn]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : m ≤ n
⊢ (x ^ m - x ^ n) / (1 - x) ≤ x ^ m / (1 - x)
have apply : x ^ m - x ^ n ≤ x ^ m
Tactic: apply div_le_div₀ (pow_nonneg hx _) _ (sub_pos.2 h'x) le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
have inr : 0 ≤ x ^ m / (1 - x)
Tactic: rw [Ico_eq_empty, sum_empty]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
inr : 0 ≤ x ^ m / (1 - x)
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)
have inr₁ : ¬m < n
Tactic: rw [Ico_eq_empty, sum_empty]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.GeomSum (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ 0 ≤ x ^ m / (1 - x)
have inr : 0 ≤ 1 - x
Tactic: apply div_nonneg (pow_nonneg hx _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro : ∀ (val : Fintype ι), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro : IsEmpty ι → ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
intro : IsEmpty ι → ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro₁ : Nonempty ι → ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro : ∀ (a : α) (ha : a ≠ 0), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Tactic: obtain ⟨a, ha⟩ := exists_ne (0 : α)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha : a ≠ 0
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro : ∀ (ha : a < 0), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Tactic: obtain ha | ha := ha.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha : a ≠ 0
intro : ∀ (ha : a < 0), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro₁ : ∀ (ha : 0 < a), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Tactic: obtain ha | ha := ha.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha_1 : a ≠ 0
ha : a < 0
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro : ∀ (b : α) (hb : 0 < b), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Tactic: obtain ⟨b, hb, -⟩ := exists_pos_add_of_lt' ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Pi (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelAddMonoid α
inst_3 : Nontrivial α
inst_4 : DenselyOrdered α
inst_5 : ExistsAddOfLE α
inst_6 : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val : Fintype ι
h_1 : IsEmpty ι
a : α
ha_1 : a ≠ 0
ha : 0 < a
⊢ ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
have intro : ∀ (b : α) (hb : 0 < b), ∃ (ε : α), 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Tactic: obtain ⟨b, hb, -⟩ := exists_pos_add_of_lt' ha