awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
simp_rw :
  (Finsupp.sum p fun (m₁ : A) (r₁ : R) ↦
      Finsupp.sum q fun (m₂ : A) (r₂ : R) ↦ if m₁ + m₂ = ap + aq then r₁ * r₂ else 0) =
    HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
simp_rw₁ :
  (∑ x ∈ p.support,
      ∑ x_1 ∈ q.support,
        if x + x_1 = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) x : R) ((q : (a : A) → R) x_1 : R)
        else 0) =
    HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
h₀ :
  ∀ b ∈ q.support,
    b ≠ aq →
      (if ap + b = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) b : R)
        else 0) =
        0
h₁ :
  aq ∉ q.support →
    (if ap + aq = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
      else 0) =
      0
h₂ :
  ∀ b ∈ p.support,
    b ≠ ap →
      Eq.{u_1 + 1} (α := R)
        (∑ x ∈ q.support,
          if b + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) b : R) ((q : (a : A) → R) x : R)
          else 0)
        0
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
have h₃ : ap ∉ p.support →
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ q.support,
      if ap + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) x : R) else 0)
    0
Tactic: classical
  simp_rw [mul_apply, Finsupp.sum]
  rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]
  · refine fun a ha hne => if_neg (fun he => ?_)
    apply_fun D at he; simp_rw [hadd] at he
    exact (add_lt_add_right (((Finset.le_sup ha).trans hq).lt_of_ne <| hD.ne_iff.2 hne) _).ne he
  · intro h; rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]
  · refine fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)
    apply_fun D at he
    simp_rw [hadd] at he
    have := addLeftMono_of_addLeftStrictMono B
    exact (add_lt_add_of_lt_of_le (((Finset.le_sup ha).trans hp).lt_of_ne <| hD.ne_iff.2 hne)
      <| (Finset.le_sup ha').trans hq).ne he
  · refine fun h => Finset.sum_eq_zero (fun a _ => ite_eq_right_iff.mpr <| fun _ => ?_)
    rw [Finsupp.notMem_support_iff.mp h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ leadingCoeff D (single a r) = r
have rw : (single a r : (a : A) → R) (Function.invFun D (if r = 0 then ⊥ else D a)) = r
Tactic: rw [leadingCoeff, supDegree_single]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ (single a r : (a : A) → R) (Function.invFun D (if r = 0 then ⊥ else D a)) = r
have pos : ∀ (hr : r = 0), (single a r : (a : A) → R) (Function.invFun D ⊥) = r
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
pos : ∀ (hr : r = 0), (single a r : (a : A) → R) (Function.invFun D ⊥) = r
⊢ (single a r : (a : A) → R) (Function.invFun D (if r = 0 then ⊥ else D a)) = r
have neg : ∀ (hr : ¬r = 0), (single a r : (a : A) → R) (Function.invFun D (D a)) = r
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
⊢ (single a r : (a : A) → R) (Function.invFun D (D a)) = r
have neg : (single a r : (a : A) → R) a = r
Tactic: rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
neg : (single a r : (a : A) → R) a = r
⊢ (single a r : (a : A) → R) (Function.invFun D (D a)) = r
have neg₁ : (if a = a then r else 0) = r
Tactic: rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
neg : (single a r : (a : A) → R) a = r
neg₁ : (if a = a then r else 0) = r
⊢ (single a r : (a : A) → R) (Function.invFun D (D a)) = r
have neg₂ : r = r
Tactic: rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ leadingCoeff D (single a r) = r
have rw : (single a r : (a : A) → R) (Function.invFun D (supDegree D (single a r))) = r
Tactic: classical
  rw [leadingCoeff, supDegree_single]
  split_ifs with hr
  · simp [hr]
  · rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
rw : (single a r : (a : A) → R) (Function.invFun D (supDegree D (single a r))) = r
⊢ leadingCoeff D (single a r) = r
have rw₁ : (single a r : (a : A) → R) (Function.invFun D (if r = 0 then ⊥ else D a)) = r
Tactic: classical
  rw [leadingCoeff, supDegree_single]
  split_ifs with hr
  · simp [hr]
  · rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
rw : (single a r : (a : A) → R) (Function.invFun D (supDegree D (single a r))) = r
rw₁ rw₂ rw₃ : (single a r : (a : A) → R) (Function.invFun D (if r = 0 then ⊥ else D a)) = r
⊢ leadingCoeff D (single a r) = r
have pos : ∀ (hr : r = 0), (single a r : (a : A) → R) (Function.invFun D ⊥) = r
Tactic: classical
  rw [leadingCoeff, supDegree_single]
  split_ifs with hr
  · simp [hr]
  · rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
rw : (single a r : (a : A) → R) (Function.invFun D (supDegree D (single a r))) = r
rw₁ rw₂ rw₃ : (single a r : (a : A) → R) (Function.invFun D (if r = 0 then ⊥ else D a)) = r
pos : ∀ (hr : r = 0), (single a r : (a : A) → R) (Function.invFun D ⊥) = r
⊢ leadingCoeff D (single a r) = r
have neg : ∀ (hr : ¬r = 0), (single a r : (a : A) → R) (Function.invFun D (D a)) = r
Tactic: classical
  rw [leadingCoeff, supDegree_single]
  split_ifs with hr
  · simp [hr]
  · rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : Nonempty A
inst_4 : Nontrivial R
hp : Monic D p
h : p = 0
simp_rw : False
⊢ False
have simp_rw₁ : ∀ (hp : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) 1), False
Tactic: simp_rw [Monic, h, leadingCoeff_zero, zero_ne_one] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : Nonempty A
inst_4 : Nontrivial R
hp : Monic D p
h : p = 0
simp_rw : False
simp_rw₁ : ∀ (hp : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) 1), False
⊢ False
have simp_rw₂ : ∀ (hp : Eq.{u_1 + 1} (α := R) 0 1), False
Tactic: simp_rw [Monic, h, leadingCoeff_zero, zero_ne_one] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
⊢ Monic.{u_1, u_3, u_5} (R := R) D 1
have rw : Eq.{u_1 + 1} (α := R) (leadingCoeff D 1) 1
Tactic: rw [Monic, one_def, leadingCoeff_single hD]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
rw : Eq.{u_1 + 1} (α := R) (leadingCoeff D 1) 1
⊢ Monic.{u_1, u_3, u_5} (R := R) D 1
have rw₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff D (single 0 1)) 1
Tactic: rw [Monic, one_def, leadingCoeff_single hD]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
rw : Eq.{u_1 + 1} (α := R) (leadingCoeff D 1) 1
rw₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff D (single 0 1)) 1
⊢ Monic.{u_1, u_3, u_5} (R := R) D 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [Monic, one_def, leadingCoeff_single hD]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
hp : p ≠ 0
⊢ supDegree D p ∈ Set.range D
have obtain : ∀ (a : A) (he : supDegree D p = D a), supDegree D p ∈ Set.range D
Tactic: obtain ⟨a, -, he⟩ := exists_supDegree_mem_support D hp
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
hs : s.Nonempty
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) < b
have refine : ⊥ < b
Tactic: refine supDegree_sum_le.trans_lt ((Finset.sup_lt_iff ?_).mpr h)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
hs : s.Nonempty
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
⊢ ⊥ < b
have obtain : ∀ (i : ι) (hi : i ∈ s), ⊥ < b
Tactic: obtain ⟨i, hi⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D q < supDegree D p
⊢ supDegree D (p + q) = supDegree D p
have apply : supDegree D p ≤ supDegree D (p + q)
Tactic: apply (supDegree_add_le.trans <| sup_le le_rfl h.le).antisymm
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D q < supDegree D p
⊢ supDegree D p ≤ supDegree D (p + q)
have obtain : ∀ (a : A) (ha : a ∈ p.support) (he : supDegree D p = D a), supDegree D p ≤ supDegree D (p + q)
Tactic: obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D (ne_zero_of_not_supDegree_le h.not_ge)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
ha : a ∈ p.support
he : supDegree D p = D a
⊢ supDegree D p ≤ supDegree D (p + q)
have rw : ∀ (h : supDegree D q < D a) (ha : a ∈ p.support) (he : supDegree D p = D a), D a ≤ supDegree D (p + q)
Tactic: rw [he] at h ⊢
Cleared hypotheses: h, ha, he
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ D a ≤ supDegree D (p + q)
have hb : a ∈ (p + q).support
Tactic: apply Finset.le_sup
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ a ∈ (p + q).support
have hb : Ne.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)
Tactic: rw [mem_support_iff, add_apply, apply_eq_zero_of_not_le_supDegree h.not_ge, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D p < supDegree D q
⊢ supDegree D (p + q) = supDegree D q
have rw : supDegree D (q + p) = supDegree D q
Tactic: rw [add_comm, supDegree_add_eq_left h]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D p < supDegree D q
rw : supDegree D (q + p) = supDegree D q
⊢ supDegree D (p + q) = supDegree D q
have rw₁ : supDegree D q = supDegree D q
Tactic: rw [add_comm, supDegree_add_eq_left h]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D q < supDegree D p
⊢ leadingCoeff D (p + q) = leadingCoeff D p
have obtain : ∀ (a : A) (he : D a = supDegree D p), leadingCoeff D (p + q) = leadingCoeff D p
Tactic: obtain ⟨a, he⟩ := supDegree_mem_range D (ne_zero_of_not_supDegree_le h.not_ge)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ leadingCoeff D (p + q) = leadingCoeff D p
have rw : ¬D (Function.invFun D (supDegree D p)) ≤ supDegree D q
Tactic: rw [leadingCoeff, supDegree_add_eq_left h, Finsupp.add_apply, ← leadingCoeff,
    apply_eq_zero_of_not_le_supDegree (D := D), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬D (Function.invFun D (supDegree D p)) ≤ supDegree D q
have rw : ¬supDegree D p ≤ supDegree D q
Tactic: rw [← he, Function.apply_invFun_apply (f := D), he]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D p < supDegree D q
⊢ leadingCoeff D (p + q) = leadingCoeff D q
have rw : leadingCoeff D (q + p) = leadingCoeff D q
Tactic: rw [add_comm, leadingCoeff_add_eq_left h]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
h : supDegree D p < supDegree D q
rw : leadingCoeff D (q + p) = leadingCoeff D q
⊢ leadingCoeff D (p + q) = leadingCoeff D q
have rw₁ : leadingCoeff D q = leadingCoeff D q
Tactic: rw [add_comm, leadingCoeff_add_eq_left h]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
⊢ Function.invFun D (supDegree D p) ∈ p.support
have obtain : ∀ (a : A) (ha : a ∈ p.support) (he : supDegree D p = D a), Function.invFun D (supDegree D p) ∈ p.support
Tactic: obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D hp
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
a : A
ha : a ∈ p.support
he : supDegree D p = D a
⊢ Function.invFun D (supDegree D p) ∈ p.support
have rwa : Function.invFun D (D a) ∈ p.support
Tactic: rwa [he, Function.leftInverse_invFun hD]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
⊢ leadingCoeff D p = 0 ↔ p = 0
have refine : ∀ (h : ¬p = 0), ¬leadingCoeff D p = 0
Tactic: refine ⟨(fun h => ?_).mtr, fun h => h ▸ leadingCoeff_zero⟩
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ ¬leadingCoeff D p = 0
have rw : Function.invFun D (supDegree D p) ∈ p.support
Tactic: rw [leadingCoeff, ← Ne, ← Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
⊢ supDegree D (p - q) < supDegree D p ∨ p = q
have rw : ¬p = q → supDegree D (p - q) < supDegree D p
Tactic: rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
⊢ ¬p = q → supDegree D (p - q) < supDegree D p
have refine_1 : ∀ (he : ¬p = q), max (supDegree D p) (supDegree D q) ≤ supDegree D p
Tactic: refine fun he => (supDegree_sub_le.trans ?_).lt_of_ne ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
refine_1 : ∀ (he : ¬p = q), max (supDegree D p) (supDegree D q) ≤ supDegree D p
⊢ ¬p = q → supDegree D (p - q) < supDegree D p
have refine_2 : ∀ (he : ¬p = q), supDegree D (p - q) ≠ supDegree D p
Tactic: refine fun he => (supDegree_sub_le.trans ?_).lt_of_ne ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ max (supDegree D p) (supDegree D q) ≤ supDegree D p
have refine_1 : max (supDegree D q) (supDegree D q) ≤ supDegree D q
Tactic: rw [hd, sup_idem]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
refine_1 : max (supDegree D q) (supDegree D q) ≤ supDegree D q
⊢ max (supDegree D p) (supDegree D q) ≤ supDegree D p
have refine_1₁ : supDegree D q ≤ supDegree D q
Tactic: rw [hd, sup_idem]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D (p - q) ≠ supDegree D p
have he₁ : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
Tactic: rw [← sub_eq_zero, ← leadingCoeff_eq_zero hD, leadingCoeff] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
⊢ supDegree D (p - q) ≠ supDegree D p
have refine_2 : ∀ (h : supDegree D (p - q) = supDegree D p),
  Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
Tactic: refine fun h => he ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
h : supDegree D (p - q) = supDegree D p
⊢ Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
have refine_2 : Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) (0 : R)
Tactic: rwa [h, Finsupp.sub_apply, ← leadingCoeff, hd, ← leadingCoeff, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
h : supDegree D (p - q) = supDegree D p
refine_2 : Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) (0 : R)
⊢ Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
have refine_2₁ : HSub.hSub (α := R) (β := R) ((p : (a : A) → R) (Function.invFun D (supDegree D p)) : R)
    ((q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) =
  0
Tactic: rwa [h, Finsupp.sub_apply, ← leadingCoeff, hd, ← leadingCoeff, sub_eq_zero]