awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
V : Type u_4
inst_3 : AddCommMonoid V
inst_4 : Module k V
inst_5 : Module (SkewMonoidAlgebra k G) V
inst_6 : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h :
  ∀ (g : G),
    ∀ v ∈ W,
      HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G)
          v ∈
        W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ (↑W : Set V)
⊢ f • v ∈ (↑W : Set V)
have rw : ∑ i ∈ f.toFinsupp.support,
    HSMul.hSMul (α := SkewMonoidAlgebra k G) (single i ((f.toFinsupp : (a : G) → k) i) : SkewMonoidAlgebra k G) v ∈
  (↑W : Set V)
Tactic: rw [← sum_single f, sum_def, Finsupp.sum, Finset.sum_smul]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Lift (goal)
Goal:
k : Type u_1
G : Type u_2
H : Type u_3
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
V : Type u_4
inst_3 : AddCommMonoid V
inst_4 : Module k V
inst_5 : Module (SkewMonoidAlgebra k G) V
inst_6 : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h :
  ∀ (g : G),
    ∀ v ∈ W,
      HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) g : SkewMonoidAlgebra k G)
          v ∈
        W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ (↑W : Set V)
⊢ ∑ i ∈ f.toFinsupp.support,
      HSMul.hSMul (α := SkewMonoidAlgebra k G) (single i ((f.toFinsupp : (a : G) → k) i) : SkewMonoidAlgebra k G) v ∈
    (↑W : Set V)
have simp_rw : ∑ x ∈ f.toFinsupp.support,
    HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((f.toFinsupp : (a : G) → k) x : k)
      (HSMul.hSMul (α := SkewMonoidAlgebra k G) ((of k G : (a : G) → SkewMonoidAlgebra k G) x : SkewMonoidAlgebra k G)
        v) ∈
  (↑W : Set V)
Tactic: simp_rw [← smul_of, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
inst_1 : DecidableEq α
⊢ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) = f.support.erase a
have h : ∀ (a_1 : α),
  Membership.mem (γ := Finset α)
      (support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)) a_1 ↔
    a_1 ∈ f.support.erase a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
⊢ HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α) =
    f
have a₁ : (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
  f.toFinsupp
Tactic: apply toFinsupp_injective
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
⊢ (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
have a₁ : (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
      { toFinsupp := Finsupp.single a (f.coeff a) : SkewMonoidAlgebra M α }
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
  f.toFinsupp
Tactic: rw [single, ← toFinsupp_apply, toFinsupp_add, erase_apply_toFinsupp,
    Finsupp.single_add_erase]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
a₁ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
        { toFinsupp := Finsupp.single a (f.coeff a) : SkewMonoidAlgebra M α }
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
⊢ (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
have a₂ : (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
      ({ toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) } : SkewMonoidAlgebra M α)
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
  f.toFinsupp
Tactic: rw [single, ← toFinsupp_apply, toFinsupp_add, erase_apply_toFinsupp,
    Finsupp.single_add_erase]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
a₁ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
        { toFinsupp := Finsupp.single a (f.coeff a) : SkewMonoidAlgebra M α }
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
a₂ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
        ({ toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) } : SkewMonoidAlgebra M α)
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
⊢ (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
have a₃ : HAdd.hAdd (α := α →₀ M) (β := α →₀ M)
    (toFinsupp { toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) : SkewMonoidAlgebra M α } : α →₀ M)
    (toFinsupp ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) : α →₀ M) =
  f.toFinsupp
Tactic: rw [single, ← toFinsupp_apply, toFinsupp_add, erase_apply_toFinsupp,
    Finsupp.single_add_erase]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
a₁ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
        { toFinsupp := Finsupp.single a (f.coeff a) : SkewMonoidAlgebra M α }
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
a₂ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
        ({ toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) } : SkewMonoidAlgebra M α)
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
a₃ :
  HAdd.hAdd (α := α →₀ M) (β := α →₀ M)
      (toFinsupp { toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) : SkewMonoidAlgebra M α } : α →₀ M)
      (toFinsupp ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) : α →₀ M) =
    f.toFinsupp
⊢ (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
have a₄ : HAdd.hAdd (α := α →₀ M)
    (toFinsupp { toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) : SkewMonoidAlgebra M α } : α →₀ M)
    (Finsupp.erase a f.toFinsupp) =
  f.toFinsupp
Tactic: rw [single, ← toFinsupp_apply, toFinsupp_add, erase_apply_toFinsupp,
    Finsupp.single_add_erase]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
a₁ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
        { toFinsupp := Finsupp.single a (f.coeff a) : SkewMonoidAlgebra M α }
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
a₂ :
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
        ({ toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) } : SkewMonoidAlgebra M α)
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
a₃ :
  HAdd.hAdd (α := α →₀ M) (β := α →₀ M)
      (toFinsupp { toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) : SkewMonoidAlgebra M α } : α →₀ M)
      (toFinsupp ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) : α →₀ M) =
    f.toFinsupp
a₄ :
  HAdd.hAdd (α := α →₀ M)
      (toFinsupp { toFinsupp := Finsupp.single a ((f.toFinsupp : (a : α) → M) a) : SkewMonoidAlgebra M α } : α →₀ M)
      (Finsupp.erase a f.toFinsupp) =
    f.toFinsupp
⊢ (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
        ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)).toFinsupp =
    f.toFinsupp
have a₅ : f.toFinsupp = f.toFinsupp
Tactic: rw [single, ← toFinsupp_apply, toFinsupp_add, erase_apply_toFinsupp,
    Finsupp.single_add_erase]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
this :
  p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
⊢ p f
have rwa : ∀ (this : p f), p f
Tactic: rwa [single_add_erase] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p f
have suffices : p
  (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
    ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
Tactic: suffices p (single a (f.coeff a) + f.erase a) by rwa [single_add_erase] at this
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
have a₁ : a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
Tactic: apply ha
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
⊢ p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
have a₂ : f.coeff a ≠ 0
Tactic: apply ha
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
a₂ : f.coeff a ≠ 0
⊢ p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
have a₃ : p ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
Tactic: apply ha
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
have a₁ : ¬(a ≠ a ∧ a ∈ f.support)
Tactic: rw [support_erase, Finset.mem_erase]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
have a₁ : support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) = s
Tactic: apply ih
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) = s
have a₁ : f.support.erase a = s
Tactic: rw [support_erase, hf, Finset.erase_cons]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : f.support.erase a = s
⊢ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) = s
have a₂ : (Finset.cons a s has).erase a = s
Tactic: rw [support_erase, hf, Finset.erase_cons]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : f.support.erase a = s
a₂ : (Finset.cons a s has).erase a = s
⊢ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) = s
have a₃ : s = s
Tactic: rw [support_erase, hf, Finset.erase_cons]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
have a₁ : a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
Tactic: classical
    apply ha
    · rw [support_erase, Finset.mem_erase]
      exact fun H ↦ H.1 rfl
    · simp only [← mem_support_iff, hf, Finset.mem_cons_self]
    · apply ih
      rw [support_erase, hf, Finset.erase_cons]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
⊢ p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
have a₂ : f.coeff a ≠ 0
Tactic: classical
    apply ha
    · rw [support_erase, Finset.mem_erase]
      exact fun H ↦ H.1 rfl
    · simp only [← mem_support_iff, hf, Finset.mem_cons_self]
    · apply ih
      rw [support_erase, hf, Finset.erase_cons]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f_1 : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s_1 : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
a₁ : a ∉ support.{u_4, u_5} (k := M) ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
a₂ : f.coeff a ≠ 0
⊢ p
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α) (single a (f.coeff a))
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α))
have a₃ : p ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f)
Tactic: classical
    apply ha
    · rw [support_erase, Finset.mem_erase]
      exact fun H ↦ H.1 rfl
    · simp only [← mem_support_iff, hf, Finset.mem_cons_self]
    · apply ih
      rw [support_erase, hf, Finset.erase_cons]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
⊢ f.update a (f.coeff a) = f
have rcases : ∀ (f : α →₀ M),
  { toFinsupp := f : SkewMonoidAlgebra M α }.update a ({ toFinsupp := f : SkewMonoidAlgebra M α }.coeff a) =
    { toFinsupp := f }
Tactic: rcases f with ⟨f⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
a : α
f : α →₀ M
⊢ { toFinsupp := f : SkewMonoidAlgebra M α }.update a ({ toFinsupp := f : SkewMonoidAlgebra M α }.coeff a) =
    { toFinsupp := f }
have a₁ : ({ toFinsupp := f : SkewMonoidAlgebra M α }.update a ({ toFinsupp := f : SkewMonoidAlgebra M α }.coeff a)).toFinsupp =
  { toFinsupp := f }.toFinsupp
Tactic: apply toFinsupp_injective
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
inst_1 : DecidableEq α
⊢ (f.update a b).coeff = Function.update (β := fun (a : α) ↦ M) f.coeff a b
have simp : Eq (α := α → M) (Function.update (β := fun (a : α) ↦ M) (⇑f.toFinsupp : (a : α) → M) a b)
  (Function.update (β := fun (a : α) ↦ M) (⇑f.toFinsupp : (a : α) → M) a b)
Tactic: simp only [coeff, update, Finsupp.update, Finsupp.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
inst_1 : DecidableEq α
⊢ (f.update a b).coeff a' = if a' = a then b else f.coeff a'
have rw : Function.update (β := fun (a : α) ↦ M) f.coeff a b a' = if a' = a then b else f.coeff a'
Tactic: rw [coeff_update, Function.update_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
inst_1 : DecidableEq α
rw : Function.update (β := fun (a : α) ↦ M) f.coeff a b a' = if a' = a then b else f.coeff a'
⊢ (f.update a b).coeff a' = if a' = a then b else f.coeff a'
have rw₁ : (if a' = a then b else f.coeff a') = if a' = a then b else f.coeff a'
Tactic: rw [coeff_update, Function.update_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
⊢ (f.update a b).coeff a = b
have rw : (if a = a then b else f.coeff a) = b
Tactic: rw [f.coeff_update_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
rw : (if a = a then b else f.coeff a) = b
⊢ (f.update a b).coeff a = b
have rw₁ : b = b
Tactic: rw [f.coeff_update_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
⊢ (f.update a b).coeff a = b
have rw : (if a = a then b else f.coeff a) = b
Tactic: classical
  rw [f.coeff_update_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
rw : (if a = a then b else f.coeff a) = b
⊢ (f.update a b).coeff a = b
have rw₁ : b = b
Tactic: classical
  rw [f.coeff_update_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
h : a' ≠ a
⊢ (f.update a b).coeff a' = f.coeff a'
have rw : (if a' = a then b else f.coeff a') = f.coeff a'
Tactic: rw [f.coeff_update_apply, if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
h : a' ≠ a
rw : (if a' = a then b else f.coeff a') = f.coeff a'
⊢ (f.update a b).coeff a' = f.coeff a'
have rw₁ : f.coeff a' = f.coeff a'
Tactic: rw [f.coeff_update_apply, if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
h : a' ≠ a
⊢ (f.update a b).coeff a' = f.coeff a'
have rw : (if a' = a then b else f.coeff a') = f.coeff a'
Tactic: classical
  rw [f.coeff_update_apply, if_neg h]