awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
zero : supDegree.{u_1, u_8, u_9} (R := R) D 1 = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
zero₁ : supDegree.{u_1, u_8, u_9} (R := R) D 1 = 0
zero₂ : supDegree.{u_1, u_8, u_9} (R := R) D (single 0 1) = 0
zero₃ : (if Eq.{u_1 + 1} (α := R) 1 0 then ⊥ else D 0) = 0
zero₄ : D 0 = 0
⊢ supDegree D (HPow.hPow (β := ℕ) p 0) = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
have zero₅ : Eq.{u_9 + 1} (α := B) 0 0
Tactic: rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n_1 : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
⊢ supDegree D (p ^ (n + 1)) = (n + 1) • supDegree D p
have succ : supDegree D (p * p ^ n) = (n + 1) • supDegree D p
Tactic: rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
      ih, succ_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n_1 : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
succ : supDegree D (p * p ^ n) = (n + 1) • supDegree D p
⊢ supDegree D (p ^ (n + 1)) = (n + 1) • supDegree D p
have succ₁ : supDegree D p + supDegree D (p ^ n) = (n + 1) • supDegree D p
Tactic: rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
      ih, succ_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n_1 : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
succ : supDegree D (p * p ^ n) = (n + 1) • supDegree D p
succ₁ : supDegree D p + supDegree D (p ^ n) = (n + 1) • supDegree D p
⊢ supDegree D (p ^ (n + 1)) = (n + 1) • supDegree D p
have succ₂ : supDegree D p + n • supDegree D p = (n + 1) • supDegree D p
Tactic: rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
      ih, succ_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n_1 : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
succ : supDegree D (p * p ^ n) = (n + 1) • supDegree D p
succ₁ : supDegree D p + supDegree D (p ^ n) = (n + 1) • supDegree D p
succ₂ : supDegree D p + n • supDegree D p = (n + 1) • supDegree D p
⊢ supDegree D (p ^ (n + 1)) = (n + 1) • supDegree D p
have succ₃ : supDegree D p + n • supDegree D p = supDegree D p + n • supDegree D p
Tactic: rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
      ih, succ_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
⊢ supDegree D (p ^ n) = n • supDegree D p
have zero : supDegree D (HPow.hPow (β := ℕ) p 0) = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
Tactic: induction n with
  | zero => rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
  | succ n ih => rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
      ih, succ_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
zero : supDegree D (HPow.hPow (β := ℕ) p 0) = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
⊢ supDegree D (p ^ n) = n • supDegree D p
have succ : ∀ (n : ℕ) (ih : supDegree D (p ^ n) = n • supDegree D p), supDegree D (p ^ (n + 1)) = (n + 1) • supDegree D p
Tactic: induction n with
  | zero => rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
  | succ n ih => rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
      ih, succ_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : SemilatticeInf T
inst_2 : OrderTop T
D : A → T
s : R[A]
hs : s.support.Nonempty
⊢ s.support.inf (WithTop.some ∘ D) = (↑(s.support.inf D) : WithTop T)
have rw : (↑(s.support.inf' hs D) : WithTop T) = (↑(s.support.inf D) : WithTop T)
Tactic: rw [← Finset.coe_inf' hs, Finset.inf'_eq_inf]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : SemilatticeInf T
inst_2 : OrderTop T
D : A → T
s : R[A]
hs : s.support.Nonempty
rw : (↑(s.support.inf' hs D) : WithTop T) = (↑(s.support.inf D) : WithTop T)
⊢ s.support.inf (WithTop.some ∘ D) = (↑(s.support.inf D) : WithTop T)
have rw₁ : (↑(s.support.inf D) : WithTop T) = (↑(s.support.inf D) : WithTop T)
Tactic: rw [← Finset.coe_inf' hs, Finset.inf'_eq_inf]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
⊢ x /ᵒᶠ 0 = x
have hfg : ∀ (m : G), Eq.{u_1 + 1} (α := k) ((x /ᵒᶠ 0 : (a : G) → k) m : k) ((x : (a : G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a b : G
⊢ x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b
have hfg : ∀ (m : G), Eq.{u_1 + 1} (α := k) ((x /ᵒᶠ (a + b) : (a : G) → k) m : k) ((x /ᵒᶠ a /ᵒᶠ b : (a : G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
a : G
x : k[G]
⊢ of' k G a * x /ᵒᶠ a = x
have hfg : ∀ (m : G), Eq.{u_1 + 1} (α := k) ((of' k G a * x /ᵒᶠ a : (a : G) → k) m : k) ((x : (a : G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
a : G
x : k[G]
m : G
⊢ Eq.{u_1 + 1} (α := k) ((of' k G a * x /ᵒᶠ a : (a : G) → k) m : k) ((x : (a : G) → k) m : k)
have hfg : ∀ m' ∈ x.support, a + m' = a + m ↔ m' = m
Tactic: rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a : G
⊢ x * of' k G a /ᵒᶠ a = x
have hfg : ∀ (m : G), Eq.{u_1 + 1} (α := k) ((x * of' k G a /ᵒᶠ a : (a : G) → k) m : k) ((x : (a : G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a m : G
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G a /ᵒᶠ a : (a : G) → k) m : k) ((x : (a : G) → k) m : k)
have hfg : ∀ m' ∈ x.support, m' + a = a + m ↔ m' = m
Tactic: rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a m c : G
hc : c ∈ x.support
⊢ c + a = a + m ↔ c = m
have hfg : a + c = a + m ↔ c = m
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
⊢ of' k G g * x %ᵒᶠ g = 0
have hfg : ∀ (g' : G), Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) ((0 : (a : G) → k) g' : k)
Tactic: ext g'
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
g' : G
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) ((0 : (a : G) → k) g' : k)
have hfg : Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
Tactic: rw [Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
g' : G
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
have hfg : ∀ (d : G), Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)
Tactic: obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
Cleared hypotheses: g'
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
g' : G
hfg : ∀ (d : G), Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
have hfg₁ : ∀ (h : ¬∃ (d : G), g' = g + d), Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
Tactic: obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
d : G
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)
have hfg : Eq.{u_1 + 1} (α := k) 0 0
Tactic: rw [modOf_apply_self_add]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ (d : G), g' = g + d
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
have hfg : Eq.{u_1 + 1} (α := k) ((of' k G g * x : (a : G) → k) g' : k) (0 : k)
Tactic: rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ (d : G), g' = g + d
hfg : Eq.{u_1 + 1} (α := k) ((of' k G g * x : (a : G) → k) g' : k) (0 : k)
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
have hfg₁ : Eq.{u_1 + 1} (α := k) ((single g 1 * x : (a : G) → k) g' : k) (0 : k)
Tactic: rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ (d : G), g' = g + d
hfg : Eq.{u_1 + 1} (α := k) ((of' k G g * x : (a : G) → k) g' : k) (0 : k)
hfg₁ : Eq.{u_1 + 1} (α := k) ((single g 1 * x : (a : G) → k) g' : k) (0 : k)
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * x %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
have hfg₂ : Eq.{u_1 + 1} (α := k) 0 0
Tactic: rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g : G
⊢ x * of' k G g %ᵒᶠ g = 0
have hfg : ∀ (g' : G), Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) ((0 : (a : G) → k) g' : k)
Tactic: ext g'
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) ((0 : (a : G) → k) g' : k)
have hfg : Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
Tactic: rw [Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
have hfg : ∀ (d : G), Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)
Tactic: obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
Cleared hypotheses: g'
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
hfg : ∀ (d : G), Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
have hfg₁ : ∀ (h : ¬∃ (d : G), g' = g + d), Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
Tactic: obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g d : G
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) (g + d) : k) (0 : k)
have hfg : Eq.{u_1 + 1} (α := k) 0 0
Tactic: rw [modOf_apply_self_add]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G g %ᵒᶠ g : (a : G) → k) g' : k) (0 : k)
have hfg : ¬∃ (d : G), g' = d + g
Tactic: rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, mul_single_apply_of_not_exists_add]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
⊢ of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x
have hfg : ∀ (g' : G), Eq.{u_1 + 1} (α := k) ((of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k)
Tactic: ext g'
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k)
have hfg : HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
  (x : (a : G) → k) g'
Tactic: rw [Finsupp.add_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
have hfg : ∀ (d : G),
  HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) (g + d) : k)
      ((x %ᵒᶠ g : (a : G) → k) (g + d) : k) =
    (x : (a : G) → k) (g + d)
Tactic: obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
Cleared hypotheses: g'
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
hfg :
  ∀ (d : G),
    HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) (g + d) : k)
        ((x %ᵒᶠ g : (a : G) → k) (g + d) : k) =
      (x : (a : G) → k) (g + d)
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
have hfg₁ : ∀ (h : ¬∃ (d : G), g' = g + d),
  HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
Tactic: obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
have hfg : HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k) =
  (x : (a : G) → k) g'
Tactic: rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h,
      zero_add]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
hfg :
  HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
have hfg₁ : HAdd.hAdd (α := k) (β := k) ((single g 1 * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k) =
  (x : (a : G) → k) g'
Tactic: rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h,
      zero_add]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
hfg :
  HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
hfg₁ :
  HAdd.hAdd (α := k) (β := k) ((single g 1 * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
have hfg₂ : HAdd.hAdd (α := k) (β := k) (0 : k) ((x : (a : G) → k) g' : k) = (x : (a : G) → k) g'
Tactic: rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h,
      zero_add]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ (d : G), g' = g + d
hfg :
  HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
hfg₁ :
  HAdd.hAdd (α := k) (β := k) ((single g 1 * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
hfg₂ : HAdd.hAdd (α := k) (β := k) (0 : k) ((x : (a : G) → k) g' : k) = (x : (a : G) → k) g'
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) g' : k) ((x %ᵒᶠ g : (a : G) → k) g' : k) =
    (x : (a : G) → k) g'
have hfg₃ : Eq.{u_1 + 1} (α := k) ((x : (a : G) → k) g' : k) ((x : (a : G) → k) g' : k)
Tactic: rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h,
      zero_add]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g d : G
⊢ HAdd.hAdd (α := k) (β := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) (g + d) : k)
      ((x %ᵒᶠ g : (a : G) → k) (g + d) : k) =
    (x : (a : G) → k) (g + d)
have hfg : Eq.{u_1 + 1} (α := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) (g + d) : k) ((x : (a : G) → k) (g + d) : k)
Tactic: rw [modOf_apply_self_add, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g d : G
⊢ Eq.{u_1 + 1} (α := k) ((of' k G g * (x /ᵒᶠ g) : (a : G) → k) (g + d) : k) ((x : (a : G) → k) (g + d) : k)
have hfg : ∀ m' ∈ (x /ᵒᶠ g).support, g + m' = g + d ↔ m' = d
Tactic: rw [of'_apply, single_mul_apply_aux, one_mul, divOf_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x
have rw : of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x
Tactic: rw [add_comm, divOf_add_modOf]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
rw : of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x
⊢ x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x
have rw₁ : x = x
Tactic: rw [add_comm, divOf_add_modOf]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
⊢ of' k G g ∣ x ↔ x %ᵒᶠ g = 0
have mp : of' k G g ∣ x → x %ᵒᶠ g = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
mp : of' k G g ∣ x → x %ᵒᶠ g = 0
⊢ of' k G g ∣ x ↔ x %ᵒᶠ g = 0
have mpr : x %ᵒᶠ g = 0 → of' k G g ∣ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
g : G
x : k[G]
⊢ of' k G g * x %ᵒᶠ g = 0
have mp : Eq (α := k[G]) 0 0
Tactic: rw [of'_mul_modOf]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Division (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ x
have mpr : of' k G g ∣ of' k G g * (x /ᵒᶠ g)
Tactic: rw [← divOf_add_modOf x g, h, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
⊢ Membership.mem (γ := Submodule R R[M]) (grade R m) a ↔ a.support ⊆ {m}
have rw : Membership.mem (γ := Submodule R R[M]) (grade R m) a ↔ (↑a.support : Set M) ⊆ {m}
Tactic: rw [← Finset.coe_subset, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
⊢ Membership.mem (γ := Submodule R R[M]) (grade R m) a ↔
    Membership.mem (γ := Submodule R R[M]) (LinearMap.range (Finsupp.lsingle m)) a
have rw : (∃ (b : R), a = Finsupp.single m b) ↔ Membership.mem (γ := Submodule R R[M]) (LinearMap.range (Finsupp.lsingle m)) a
Tactic: rw [mem_grade_iff, Finsupp.support_subset_singleton']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Grading (goal)
Goal:
M : Type u_1
R : Type u_3
inst : CommSemiring R
m : M
a : R[M]
⊢ (∃ (b : R), a = Finsupp.single m b) ↔ Membership.mem (γ := Submodule R R[M]) (LinearMap.range (Finsupp.lsingle m)) a
have h : ∀ (a_1 : R), a = Finsupp.single m a_1 ↔ (Finsupp.lsingle m : (a : R) → R[M]) a_1 = a
Tactic: apply exists_congr