awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Free (goal)
Goal:
α : Type u
⊢ Eq.{u + 1} (α := FreeSemigroup α →ₙ* FreeSemigroup α)
    (MulHom.comp (N := Magma.AssocQuotient (FreeMagma α))
      ((Magma.AssocQuotient.lift :
          (a : FreeMagma α →ₙ* FreeSemigroup α) → Magma.AssocQuotient (FreeMagma α) →ₙ* FreeSemigroup α)
        FreeMagma.toFreeSemigroup)
      ((FreeSemigroup.lift :
          (a : α → Magma.AssocQuotient (FreeMagma α)) → FreeSemigroup α →ₙ* Magma.AssocQuotient (FreeMagma α))
        ((⇑Magma.AssocQuotient.of : (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘ FreeMagma.of)))
    (MulHom.id (FreeSemigroup α))
have h : Eq.{u + 1} (α := α → FreeSemigroup α)
  ((⇑(MulHom.comp (N := Magma.AssocQuotient (FreeMagma α))
          ((Magma.AssocQuotient.lift :
              (a : FreeMagma α →ₙ* FreeSemigroup α) → Magma.AssocQuotient (FreeMagma α) →ₙ* FreeSemigroup α)
            FreeMagma.toFreeSemigroup)
          ((FreeSemigroup.lift :
              (a : α → Magma.AssocQuotient (FreeMagma α)) → FreeSemigroup α →ₙ* Magma.AssocQuotient (FreeMagma α))
            ((⇑Magma.AssocQuotient.of : (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘ FreeMagma.of))) :
      (a : FreeSemigroup α) → FreeSemigroup α) ∘
    FreeSemigroup.of)
  ((⇑(MulHom.id (FreeSemigroup α)) : (a : FreeSemigroup α) → FreeSemigroup α) ∘ FreeSemigroup.of)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
⊢ Eq.{u_1 + 1} (α := (X →₀ ℤ) →+ X →₀ ℤ) (AddMonoidHom.comp toFinsupp toFreeAbelianGroup) (AddMonoidHom.id (X →₀ ℤ))
have H : ∀ (x a : X),
  Eq (α := ℤ)
    (((AddMonoidHom.comp (AddMonoidHom.comp toFinsupp toFreeAbelianGroup) (singleAddHom x) : (a : ℤ) → X →₀ ℤ) 1 :
          (a : X) → ℤ)
        a :
      ℤ)
    (((AddMonoidHom.comp (AddMonoidHom.id (X →₀ ℤ)) (singleAddHom x) : (a : ℤ) → X →₀ ℤ) 1 : (a : X) → ℤ) a : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
⊢ Eq.{u_1 + 1} (α := FreeAbelianGroup X →+ FreeAbelianGroup X) (AddMonoidHom.comp toFreeAbelianGroup toFinsupp)
    (AddMonoidHom.id (FreeAbelianGroup X))
have H : ∀ (x : X),
  Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp toFreeAbelianGroup toFinsupp : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
⊢ Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp toFreeAbelianGroup toFinsupp : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
have H : Eq (α := FreeAbelianGroup X)
  ((AddMonoidHom.comp
          ((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
            (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) : (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
              (of x))
          toFinsupp :
        (a : FreeAbelianGroup X) → FreeAbelianGroup X)
      (of x) :
    FreeAbelianGroup X)
  ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
Tactic: rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift_apply_of,
    liftAddHom_apply_single, AddMonoidHom.flip_apply, smulAddHom_apply, one_smul,
    AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
H :
  Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp
            ((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
              (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) :
                  (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
                (of x))
            toFinsupp :
          (a : FreeAbelianGroup X) → FreeAbelianGroup X)
        (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
⊢ Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp toFreeAbelianGroup toFinsupp : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
have H₁ : Eq (α := FreeAbelianGroup X)
  ((AddMonoidHom.comp (N := X →₀ ℤ)
          ((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
            (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) : (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
              (of x))
          ((lift : (a : X → X →₀ ℤ) → FreeAbelianGroup X →+ X →₀ ℤ) fun (x : X) ↦ single x 1) :
        (a : FreeAbelianGroup X) → FreeAbelianGroup X)
      (of x) :
    FreeAbelianGroup X)
  ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
Tactic: rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift_apply_of,
    liftAddHom_apply_single, AddMonoidHom.flip_apply, smulAddHom_apply, one_smul,
    AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
H :
  Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp
            ((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
              (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) :
                  (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
                (of x))
            toFinsupp :
          (a : FreeAbelianGroup X) → FreeAbelianGroup X)
        (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
H₁ :
  Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp (N := X →₀ ℤ)
            ((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
              (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) :
                  (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
                (of x))
            ((lift : (a : X → X →₀ ℤ) → FreeAbelianGroup X →+ X →₀ ℤ) fun (x : X) ↦ single x 1) :
          (a : FreeAbelianGroup X) → FreeAbelianGroup X)
        (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
⊢ Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp toFreeAbelianGroup toFinsupp : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
have H₂ : Eq (α := FreeAbelianGroup X)
  (((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
          (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) : (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
            (of x) :
        (a : X →₀ ℤ) → FreeAbelianGroup X)
      (((lift : (a : X → X →₀ ℤ) → FreeAbelianGroup X →+ X →₀ ℤ) fun (x : X) ↦ single x 1 :
          (a : FreeAbelianGroup X) → X →₀ ℤ)
        (of x)) :
    FreeAbelianGroup X)
  ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
Tactic: rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift_apply_of,
    liftAddHom_apply_single, AddMonoidHom.flip_apply, smulAddHom_apply, one_smul,
    AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
H :
  Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp
            ((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
              (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) :
                  (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
                (of x))
            toFinsupp :
          (a : FreeAbelianGroup X) → FreeAbelianGroup X)
        (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
H₁ :
  Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp (N := X →₀ ℤ)
            ((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
              (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) :
                  (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
                (of x))
            ((lift : (a : X → X →₀ ℤ) → FreeAbelianGroup X →+ X →₀ ℤ) fun (x : X) ↦ single x 1) :
          (a : FreeAbelianGroup X) → FreeAbelianGroup X)
        (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
H₂ :
  Eq (α := FreeAbelianGroup X)
    (((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
            (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) : (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
              (of x) :
          (a : X →₀ ℤ) → FreeAbelianGroup X)
        (((lift : (a : X → X →₀ ℤ) → FreeAbelianGroup X →+ X →₀ ℤ) fun (x : X) ↦ single x 1 :
            (a : FreeAbelianGroup X) → X →₀ ℤ)
          (of x)) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
⊢ Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp toFreeAbelianGroup toFinsupp : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
have H₃ : Eq (α := FreeAbelianGroup X)
  (((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
          (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) : (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
            (of x) :
        (a : X →₀ ℤ) → FreeAbelianGroup X)
      (single x 1) :
    FreeAbelianGroup X)
  ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
Tactic: rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift_apply_of,
    liftAddHom_apply_single, AddMonoidHom.flip_apply, smulAddHom_apply, one_smul,
    AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_2
x : FreeAbelianGroup X
⊢ (toFreeAbelianGroup : (a : X →₀ ℤ) → FreeAbelianGroup X) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) x) = x
have rw : (AddMonoidHom.comp toFreeAbelianGroup toFinsupp : (a : FreeAbelianGroup X) → FreeAbelianGroup X) x = x
Tactic: rw [← AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_2
x : FreeAbelianGroup X
rw : (AddMonoidHom.comp toFreeAbelianGroup toFinsupp : (a : FreeAbelianGroup X) → FreeAbelianGroup X) x = x
⊢ (toFreeAbelianGroup : (a : X →₀ ℤ) → FreeAbelianGroup X) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) x) = x
have rw₁ : (AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) x = x
Tactic: rw [← AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_2
x : FreeAbelianGroup X
rw : (AddMonoidHom.comp toFreeAbelianGroup toFinsupp : (a : FreeAbelianGroup X) → FreeAbelianGroup X) x = x
rw₁ : (AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) x = x
⊢ (toFreeAbelianGroup : (a : X →₀ ℤ) → FreeAbelianGroup X) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) x) = x
have rw₂ : x = x
Tactic: rw [← AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
f : X →₀ ℤ
⊢ (toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ)
      ((toFreeAbelianGroup : (a : X →₀ ℤ) → FreeAbelianGroup X) f : FreeAbelianGroup X) =
    f
have rw : (AddMonoidHom.comp toFinsupp toFreeAbelianGroup : (a : X →₀ ℤ) → X →₀ ℤ) f = f
Tactic: rw [← AddMonoidHom.comp_apply, toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
f : X →₀ ℤ
rw : (AddMonoidHom.comp toFinsupp toFreeAbelianGroup : (a : X →₀ ℤ) → X →₀ ℤ) f = f
⊢ (toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ)
      ((toFreeAbelianGroup : (a : X →₀ ℤ) → FreeAbelianGroup X) f : FreeAbelianGroup X) =
    f
have rw₁ : (AddMonoidHom.id (X →₀ ℤ) : (a : X →₀ ℤ) → X →₀ ℤ) f = f
Tactic: rw [← AddMonoidHom.comp_apply, toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
f : X →₀ ℤ
rw : (AddMonoidHom.comp toFinsupp toFreeAbelianGroup : (a : X →₀ ℤ) → X →₀ ℤ) f = f
rw₁ : (AddMonoidHom.id (X →₀ ℤ) : (a : X →₀ ℤ) → X →₀ ℤ) f = f
⊢ (toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ)
      ((toFreeAbelianGroup : (a : X →₀ ℤ) → FreeAbelianGroup X) f : FreeAbelianGroup X) =
    f
have rw₂ : f = f
Tactic: rw [← AddMonoidHom.comp_apply, toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∈ a.support ↔ Ne (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)
have rw : Ne (α := ℤ) ((((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a : X →₀ ℤ) : (a : X) → ℤ) x : ℤ) (0 : ℤ) ↔
  Ne (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)
Tactic: rw [support, Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∉ a.support ↔ Eq (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)
have rw : Eq (α := ℤ) ((((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a : X →₀ ℤ) : (a : X) → ℤ) x : ℤ) (0 : ℤ) ↔
  Eq (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)
Tactic: rw [support, Finsupp.notMem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
⊢ (of x).support = {x}
have rw : Eq (α := Finset X) (Finsupp.support (M := ℤ) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) (of x))) {x}
Tactic: rw [support, toFinsupp_of, Finsupp.support_single _ one_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
rw : Eq (α := Finset X) (Finsupp.support (M := ℤ) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) (of x))) {x}
⊢ (of x).support = {x}
have rw₁ : Finsupp.support (M := ℤ) (single x 1) = {x}
Tactic: rw [support, toFinsupp_of, Finsupp.support_single _ one_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
rw : Eq (α := Finset X) (Finsupp.support (M := ℤ) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) (of x))) {x}
rw₁ : Finsupp.support (M := ℤ) (single x 1) = {x}
⊢ (of x).support = {x}
have rw₂ : Eq (α := Finset X) {x} {x}
Tactic: rw [support, toFinsupp_of, Finsupp.support_single _ one_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ (k • a).support = a.support
have h₁ : ∀ (x : X), x ∈ (k • a).support ↔ x ∈ a.support
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ (k • a).support = a.support
have apply : Ne (α := ℤ) (↑k : ℤ) 0
Tactic: apply support_zsmul k _ a
-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
a b : FreeAbelianGroup X
⊢ (a + b).support ⊆ a.support ∪ b.support
have simp : (HAdd.hAdd (α := X →₀ ℤ) (β := X →₀ ℤ) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a : X →₀ ℤ)
      ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) b : X →₀ ℤ)).support ⊆
  Finsupp.support (M := ℤ) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a) ∪
    Finsupp.support (M := ℤ) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) b)
Tactic: simp only [support, map_add]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have hX : #(FreeMonoid X) = max #X ℵ₀
Tactic: have hX := mk_freeMonoid X
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
    mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
    mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have rw₂ : max (Cardinal.lift.{u, v} #(FreeMonoid X)) (Cardinal.lift.{v, u} #R) =
  max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
    mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₂ :
  max (Cardinal.lift.{u, v} #(FreeMonoid X)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have rw₃ : max (Cardinal.lift.{u, v} (max #X ℵ₀)) (Cardinal.lift.{v, u} #R) =
  max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
    mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₂ :
  max (Cardinal.lift.{u, v} #(FreeMonoid X)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₃ :
  max (Cardinal.lift.{u, v} (max #X ℵ₀)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have rw₄ : max (max (Cardinal.lift.{u, v} #X) (Cardinal.lift.{u, v} ℵ₀)) (Cardinal.lift.{v, u} #R) =
  max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
    mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₂ :
  max (Cardinal.lift.{u, v} #(FreeMonoid X)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₃ :
  max (Cardinal.lift.{u, v} (max #X ℵ₀)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₄ :
  max (max (Cardinal.lift.{u, v} #X) (Cardinal.lift.{u, v} ℵ₀)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have rw₅ : max (max (Cardinal.lift.{u, v} #X) ℵ₀) (Cardinal.lift.{v, u} #R) =
  max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
    mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₂ :
  max (Cardinal.lift.{u, v} #(FreeMonoid X)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₃ :
  max (Cardinal.lift.{u, v} (max #X ℵ₀)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₄ :
  max (max (Cardinal.lift.{u, v} #X) (Cardinal.lift.{u, v} ℵ₀)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₅ :
  max (max (Cardinal.lift.{u, v} #X) ℵ₀) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have rw₆ : max (Cardinal.lift.{v, u} #R) (max (Cardinal.lift.{u, v} #X) ℵ₀) =
  max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
    mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]