awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
exp : ℝ
exps : List ℝ
ih_1 :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
x : ℝ
h_pos : 0 < basis_hd x
ih :
  Eq (α := ℝ)
    ((fun (a : ℝ) ↦
        (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis_tl) :
          ℝ))
      x)
    ((fun (a : ℝ) ↦ ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis_tl))⁻¹ : ℝ)) x)
⊢ Eq (α := ℝ)
    ((fun (a : ℝ) ↦
        (List.prod
            (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps))
              (basis_hd :: basis_tl)) :
          ℝ))
      x)
    ((fun (a : ℝ) ↦
        ((List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)))⁻¹ : ℝ))
      x)
have cons : basis_hd x ^ (-exp) *
    List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis_tl) =
  (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) exps basis_tl))⁻¹ * (basis_hd x ^ exp)⁻¹
Tactic: simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹
basis : Basis
h_basis : WellFormedBasis basis
⊢ EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps)) basis))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) basis))⁻¹
have cons : ∀ (h_basis : WellFormedBasis []),
  EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps)) []))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) []))⁻¹
Tactic: cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]
Cleared hypotheses: basis, h_basis
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹
basis : Basis
h_basis : WellFormedBasis basis
cons :
  ∀ (h_basis : WellFormedBasis []),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps)) []))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) []))⁻¹
⊢ EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps)) basis))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) basis))⁻¹
have cons₁ : ∀ (basis_hd : ℝ → ℝ) (basis_tl : List (ℝ → ℝ)) (h_basis : WellFormedBasis (basis_hd :: basis_tl)),
  EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps))
          (basis_hd :: basis_tl)))
    fun (a : ℝ) ↦
    (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)))⁻¹
Tactic: cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]
Cleared hypotheses: basis, h_basis
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) m) basis))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) m basis))⁻¹
have nil : ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
  EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) []) basis))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) [] basis))⁻¹
Tactic: induction m generalizing basis with
  | nil => simp
  | cons exp exps ih =>
    cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]
Cleared hypotheses: m, basis, h_basis
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
nil :
  ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
    EventuallyEq (β := ℝ) atTop
      (fun (a : ℝ) ↦
        List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) []) basis))
      fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) [] basis))⁻¹
⊢ EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) m) basis))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) m basis))⁻¹
have cons : ∀ (exp : ℝ) (exps : List ℝ)
  (ih :
    ∀ {basis : Basis} (h_basis : WellFormedBasis basis),
      EventuallyEq (β := ℝ) atTop
        (fun (a : ℝ) ↦
          List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) exps) basis))
        fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) exps basis))⁻¹)
  {basis : Basis} (h_basis : WellFormedBasis basis),
  EventuallyEq (β := ℝ) atTop
    (fun (a : ℝ) ↦
      List.prod
        (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (List.map (fun (x : ℝ) ↦ -x) (exp :: exps)) basis))
    fun (a : ℝ) ↦ (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b a ^ exp) (exp :: exps) basis))⁻¹
Tactic: induction m generalizing basis with
  | nil => simp
  | cons exp exps ih =>
    cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]
Cleared hypotheses: m, basis, h_basis
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
coef : ℝ
basis : Basis
⊢ { coef := coef, unit := [] : Monomial }.toFun basis = fun (x : ℝ) ↦ coef
have h : ∀ (x : ℝ), { coef := coef, unit := [] : Monomial }.toFun basis x = coef
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
coef exp : ℝ
m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ { coef := coef, unit := exp :: m : Monomial }.toFun (basis_hd :: basis_tl) =
    basis_hd ^ exp * { coef := coef, unit := m : Monomial }.toFun basis_tl
have h : ∀ (x : ℝ),
  { coef := coef, unit := exp :: m : Monomial }.toFun (basis_hd :: basis_tl) x =
    (basis_hd ^ exp * { coef := coef, unit := m : Monomial }.toFun basis_tl) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
coef exp : ℝ
m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
x : ℝ
⊢ { coef := coef, unit := exp :: m : Monomial }.toFun (basis_hd :: basis_tl) x =
    (basis_hd ^ exp * { coef := coef, unit := m : Monomial }.toFun basis_tl) x
have h : coef * (basis_hd x ^ exp * m.toFun basis_tl x) = basis_hd x ^ exp * (coef * m.toFun basis_tl x)
Tactic: simp [toFun]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t : Monomial
basis : Basis
⊢ t.toFun basis = -t.neg.toFun basis
have h : ∀ (x : ℝ), t.toFun basis x = (-t.neg.toFun basis) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
⊢ (t1.mul t2).toFun basis =ᶠ[atTop] t1.toFun basis * t2.toFun basis
have simp : (t1.coef * t2.coef) • (t1.unit.mul t2.unit).toFun basis =ᶠ[atTop]
  t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)
Tactic: simp only [toFun, mul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
⊢ (t1.coef * t2.coef) • (t1.unit.mul t2.unit).toFun basis =ᶠ[atTop]
    t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)
have grw : (t1.coef * t2.coef) • (t1.unit.toFun basis * t2.unit.toFun basis) =ᶠ[atTop]
  t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)
Tactic: grw [UnitMonomial.mul_toFun h_basis h_length]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
⊢ (t1.coef * t2.coef) • (t1.unit.toFun basis * t2.unit.toFun basis) =ᶠ[atTop]
    t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)
have h : ∀ (t : ℝ),
  ((t1.coef * t2.coef) • (t1.unit.toFun basis * t2.unit.toFun basis)) t =
    (t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)) t
Tactic: filter_upwards [] with t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t : Monomial
basis : Basis
c : ℝ
⊢ (t.smul c).toFun basis = c • t.toFun basis
have h : ∀ (x : ℝ), (t.smul c).toFun basis x = (c • t.toFun basis) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t : Monomial
basis : Basis
c x : ℝ
⊢ (t.smul c).toFun basis x = (c • t.toFun basis) x
have h : c * t.coef * t.unit.toFun basis x = c * (t.coef * t.unit.toFun basis x)
Tactic: simp [smul, toFun]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ t.inv.toFun basis =ᶠ[atTop] (t.toFun basis)⁻¹
have simp : t.coef⁻¹ • t.unit.inv.toFun basis =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹
Tactic: simp only [toFun, inv]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ t.coef⁻¹ • t.unit.inv.toFun basis =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹
have grw : t.coef⁻¹ • (t.unit.toFun basis)⁻¹ =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹
Tactic: grw [UnitMonomial.inv_toFun h_basis]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ t.coef⁻¹ • (t.unit.toFun basis)⁻¹ =ᶠ[atTop] (t.coef • t.unit.toFun basis)⁻¹
have h : ∀ (x : ℝ), (t.coef⁻¹ • (t.unit.toFun basis)⁻¹) x = (t.coef • t.unit.toFun basis)⁻¹ x
Tactic: filter_upwards [] with x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
⊢ (t.coef⁻¹ • (t.unit.toFun basis)⁻¹) x = (t.coef • t.unit.toFun basis)⁻¹ x
have h : t.coef⁻¹ * (t.unit.toFun basis x)⁻¹ = (t.unit.toFun basis x)⁻¹ * t.coef⁻¹
Tactic: simp [Pi.smul_apply, Pi.inv_apply]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates (goal)
Goal:
n : ℕ
⊢ AllZero (List.replicate n 0)
have zero : AllZero (List.replicate 0 0)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates (goal)
Goal:
n : ℕ
zero : AllZero (List.replicate 0 0)
⊢ AllZero (List.replicate n 0)
have succ : ∀ (n : ℕ), AllZero (List.replicate n 0) → AllZero (List.replicate (n + 1) 0)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a b : R
f g : R[X]
h_add_left : f.coeff n = a
h_add_right : g.coeff n = b
⊢ (f + g).coeff n = a + b
have subst : (f + g).coeff n = f.coeff n + g.coeff n
Tactic: subst ‹_› ‹_›
Cleared hypotheses: a, b, h_add_left, h_add_right
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
⊢ (f * g).coeff d = if d = df + dg then a * b else 0
have pos : ∀ (h : d = df + dg), (f * g).coeff d = a * b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
pos : ∀ (h : d = df + dg), (f * g).coeff d = a * b
⊢ (f * g).coeff d = if d = df + dg then a * b else 0
have neg : ∀ (h : ¬d = df + dg), (f * g).coeff d = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : d = df + dg
⊢ (f * g).coeff d = a * b
have pos : ∀ (ddf : df + dg ≤ df + dg), (f * g).coeff (df + dg) = f.coeff df * g.coeff dg
Tactic: subst h_mul_left h_mul_right h
Cleared hypotheses: d, a, b, h_mul_left, h_mul_right, ddf, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).coeff d = 0
have neg : (f * g).natDegree < d
Tactic: apply coeff_eq_zero_of_natDegree_lt
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).natDegree < d
have apply : (f * g).natDegree ≤ df + dg
Tactic: apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ddf ?_)
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left_1 : f.natDegree ≤ df
h_mul_right_1 : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
apply : (f * g).natDegree ≤ df + dg
⊢ (f * g).natDegree < d
have apply₁ : df + dg ≠ d
Tactic: apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ddf ?_)
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
⊢ (p ^ m).coeff o = if o = m * n then a ^ m else 0
have pos : ∀ (h : o = m * n), (p ^ m).coeff o = a ^ m
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
pos : ∀ (h : o = m * n), (p ^ m).coeff o = a ^ m
⊢ (p ^ m).coeff o = if o = m * n then a ^ m else 0
have neg : ∀ (h : ¬o = m * n), (p ^ m).coeff o = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : o = m * n
⊢ (p ^ m).coeff o = a ^ m
have pos : ∀ (h_exp : m * n ≤ m * n), (p ^ m).coeff (m * n) = p.coeff n ^ m
Tactic: subst h h_pow_bas
Cleared hypotheses: o, a, h_exp, h_pow_bas, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).coeff o = 0
have neg : (p ^ m).natDegree < o
Tactic: apply coeff_eq_zero_of_natDegree_lt
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree < o
have apply : (p ^ m).natDegree ≤ m * n
Tactic: apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ‹_› ?_)
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
apply : (p ^ m).natDegree ≤ m * n
⊢ (p ^ m).natDegree < o
have apply₁ : m * n ≠ o
Tactic: apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ‹_› ?_)
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
deg m o : ℕ
c : R
p : R[X]
h_natDeg_le : p.natDegree ≤ m
coeff_eq : p.coeff o = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.natDegree = deg
have subst : ∀ (coeff_ne_zero : p.coeff o ≠ 0) (h_natDeg_le : p.natDegree ≤ o), p.natDegree = o
Tactic: subst coeff_eq deg_eq_deg coeff_eq_deg
Cleared hypotheses: deg, m, c, h_natDeg_le, coeff_eq, coeff_ne_zero, deg_eq_deg, coeff_eq_deg
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
deg m o : WithBot ℕ
c : R
p : R[X]
h_deg_le : p.degree ≤ m
coeff_eq : p.coeff (WithBot.unbotD 0 deg) = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.degree = deg
have subst : ∀ (coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0), p.degree = m
Tactic: subst coeff_eq coeff_eq_deg deg_eq_deg
Cleared hypotheses: deg, o, c, coeff_eq, coeff_ne_zero, deg_eq_deg, coeff_eq_deg
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
⊢ p.degree = m
have inl : ∀ (h_deg_le : p.degree ≤ ⊥) (coeff_ne_zero : p.coeff (WithBot.unbotD 0 ⊥) ≠ 0), p.degree = ⊥
Tactic: rcases eq_or_ne m ⊥ with rfl | hh
Cleared hypotheses: m, h_deg_le, coeff_ne_zero
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
inl : ∀ (h_deg_le : p.degree ≤ ⊥) (coeff_ne_zero : p.coeff (WithBot.unbotD 0 ⊥) ≠ 0), p.degree = ⊥
⊢ p.degree = m
have inr : ∀ (hh : m ≠ ⊥), p.degree = m
Tactic: rcases eq_or_ne m ⊥ with rfl | hh
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
hh : m ≠ ⊥
⊢ p.degree = m
have inr : ∀ (m : ℕ) (h_deg_le : p.degree ≤ (↑m : WithBot ℕ)) (coeff_ne_zero : p.coeff (WithBot.unbotD 0 (↑m : WithBot ℕ)) ≠ 0)
  (hh : (↑m : WithBot ℕ) ≠ ⊥), p.degree = (↑m : WithBot ℕ)
Tactic: obtain ⟨m, rfl⟩ := WithBot.ne_bot_iff_exists.mp hh
Cleared hypotheses: m, h_deg_le, coeff_ne_zero, hh
-- Lean 4 proof step from Mathlib.Tactic.ComputeDegree (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a b : R
f g : R[X]
hf : f.coeff n = a
hg : g.coeff n = b
⊢ (f - g).coeff n = a - b
have subst : (f - g).coeff n = f.coeff n - g.coeff n
Tactic: subst hf hg
Cleared hypotheses: a, b, hf, hg
-- Lean 4 proof step from Mathlib.Tactic.CongrExclamation (goal)
Goal:
α α' : Sort u
β β' : Sort v
h : α = α'
h' : ∀ (a : α'), β = β'
⊢ Eq (α := Sort (imax u v)) (α → β) (α' → β')
have refl : ∀ (h' : ∀ (a : α), β = β'), Eq (α := Sort (imax u v)) (α → β) (α → β')
Tactic: cases h
Cleared hypotheses: α', h, h'
-- Lean 4 proof step from Mathlib.Tactic.CongrExclamation (goal)
Goal:
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
⊢ Eq (α := Sort (imax u v)) ((x : α) → (fun (x : α) ↦ β) x) (α → β')
have refl : Eq (α := Sort (imax u v)) ((x : α) → (fun (x : α) ↦ β') x) (α → β')
Tactic: rw [funext h']
-- Lean 4 proof step from Mathlib.Tactic.CongrExclamation (goal)
Goal:
α : Sort u_1
x y : α
p : x ≍ y → Prop
h : ∀ (he : x = y), p ⋯
he : x ≍ y
⊢ p he
have refl : ∀ {p : x ≍ x → Prop} (h : ∀ (he : x = x), p sorry), p sorry
Tactic: cases he
Cleared hypotheses: y, p, h, he
-- Lean 4 proof step from Mathlib.Tactic.CongrExclamation (goal)
Goal:
x y : Prop
p : x = y → Prop
h : ∀ (he : x ↔ y), p ⋯
he : x = y
⊢ p he
have refl : ∀ {p : x = x → Prop} (h : ∀ (he : x ↔ x), p sorry), p sorry
Tactic: cases he
Cleared hypotheses: y, p, h, he
-- Lean 4 proof step from Mathlib.Tactic.DepRewrite (goal)
Goal:
α : Sort u
a a' : α
β : (a' : α) → a = a' → Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β a' h
⊢ Eq (α := β a ⋯) (f a ⋯) (Eq.rec (motive := fun (x : α) (h' : a' = x) ↦ β x ⋯) (f a' h) ⋯)
have refl : f a sorry = Eq.rec (motive := fun (x : α) (h' : a = x) ↦ β x sorry) (f a sorry) sorry
Tactic: cases h
Cleared hypotheses: a', h
-- Lean 4 proof step from Mathlib.Tactic.DepRewrite (goal)
Goal:
α : Sort u
a a' : α
β : Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β
⊢ f a ⋯ = f a' h
have refl : f a sorry = f a sorry
Tactic: cases h
Cleared hypotheses: a', h
-- Lean 4 proof step from Mathlib.Tactic.DepRewrite (goal)
Goal:
α β : Sort u
a : α
b : β
h : a ≍ b
⊢ a = cast ⋯ b
have refl : a = cast sorry a
Tactic: cases h
Cleared hypotheses: β, b, h
-- Lean 4 proof step from Mathlib.Tactic.DepRewrite (goal)
Goal:
α β : Sort u
a : α
b : β
h : a ≍ b
⊢ cast ⋯ a = b
have refl : cast sorry a = a
Tactic: cases h
Cleared hypotheses: β, b, h
-- Lean 4 proof step from Mathlib.Tactic.DeriveCountable (goal)
Goal:
p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ Nat.pair a b = Nat.pair a' b' → p
have rwa : a = a' ∧ b = b' → p
Tactic: rwa [Nat.pair_eq_pair, and_imp]
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
n : ℕ
h : (Nat.unpair n).1 ≠ 0
⊢ (Nat.unpair n).2 < n
have obtain : ∀ (a b : ℕ) (h : (Nat.unpair ((Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b))).1 ≠ 0),
  (Nat.unpair ((Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b))).2 < (Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b)
Tactic: obtain ⟨⟨a, b⟩, rfl⟩ := Nat.pairEquiv.surjective n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Tactic.DeriveEncodable (goal)
Goal:
a b : ℕ
h : (Nat.unpair ((Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b))).1 ≠ 0
⊢ (Nat.unpair ((Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b))).2 < (Nat.pairEquiv : (a : ℕ × ℕ) → ℕ) (a, b)
have simp : ∀ (h : a ≠ 0), b < Nat.pair a b
Tactic: simp only [Nat.pairEquiv_apply, Function.uncurry_apply_pair, Nat.unpair_pair] at *
Cleared hypotheses: h