awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 β_1 : Type u
f : α_1 → β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x)) (pure (f <$> of x))
ih2 : Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) y) (pure (f <$> y))
rw :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse (pure ∘ f) (of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₁ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> traverse (pure ∘ f) y)
    (pure (f <$> (of x * y)))
rw₂ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y)) (pure (f <$> (of x * y)))
rw₃ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> pure (f <$> of x) <*> pure (f <$> y)) (pure (f <$> of x * f <$> y))
rw₄ :
  Eq (α := Id (FreeSemigroup β_1)) ((pure fun (x2 : FreeSemigroup β_1) ↦ f <$> of x * x2) <*> pure (f <$> y))
    (pure (f <$> of x * f <$> y))
rw₅ :
  Eq (α := Id (FreeSemigroup β_1))
    ((fun (h : FreeSemigroup β_1 → FreeSemigroup β_1) ↦ h (f <$> y)) <$>
      pure fun (x2 : FreeSemigroup β_1) ↦ f <$> of x * x2)
    (pure (f <$> of x * f <$> y))
rw₆ rw₇ :
  Eq (α := Id (FreeSemigroup β_1)) (pure ((fun (x2 : FreeSemigroup β_1) ↦ f <$> of x * x2) (f <$> y)))
    (pure (f <$> of x * f <$> y))
⊢ Eq (α := Id (FreeSemigroup β_1)) (traverse (pure ∘ f) (of x * y)) (pure (f <$> (of x * y)))

Tactic:
rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure]

Premises used: FreeSemigroup.traverse_mul, LawfulApplicative.seq_pure, FreeSemigroup.map_mul', LawfulApplicative.map_pure
-- Module: Mathlib.Algebra.Free
Goal:
α_1 β_1 : Type u
m : Type u → Type u
inst : Applicative m
F : α_1 → m β_1
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α β : Type u
f : α → F_1 β
x_1 : FreeSemigroup α
x : α
⊢ Eq (α := G (FreeSemigroup β)) ((fun {α : Type u} ↦ η.app α) (traverse f (pure x)))
    (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (pure x))

Tactic:
simp only [traverse_pure, functor_norm, Function.comp]

Premises used: Function.comp, FreeSemigroup.traverse_pure
-- Module: Mathlib.Algebra.Free
Goal:
α_1 β_1 : Type u
m : Type u → Type u
inst : Applicative m
F : α_1 → m β_1
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α β : Type u
f : α → F_1 β
x_1 : FreeSemigroup α
x : α
y : FreeSemigroup α
ih1 :
  Eq (α := G (FreeSemigroup β)) ((fun {α : Type u} ↦ η.app α) (traverse f (pure x)))
    (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (pure x))
ih2 :
  Eq (α := G (FreeSemigroup β)) ((fun {α : Type u} ↦ η.app α) (traverse f y))
    (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) y)
⊢ Eq (α := G (FreeSemigroup β)) ((fun {α : Type u} ↦ η.app α) (traverse f (pure x * y)))
    (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (pure x * y))

Tactic:
simp only [traverse_mul, functor_norm, ih1, ih2]

Premises used: FreeSemigroup.traverse_mul
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x : α
⊢ (toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) (of x) = FreeSemigroup.of x

Tactic:
rfl

Premises used: FreeSemigroup.of, FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
⊢ Eq.{u + 1} (α := α → FreeSemigroup α) ((⇑toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) ∘ of) FreeSemigroup.of

Tactic:
rfl

Premises used: FreeSemigroup.of, FreeMagma.liftAux, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
f : α → β
h :
  Eq (α := α → FreeSemigroup β) ((⇑(MulHom.comp toFreeSemigroup (map f)) : (a : FreeMagma α) → FreeSemigroup β) ∘ of)
    ((⇑((FreeSemigroup.map f).comp toFreeSemigroup) : (a : FreeMagma α) → FreeSemigroup β) ∘ of)
⊢ MulHom.comp toFreeSemigroup (map f) = (FreeSemigroup.map f).comp toFreeSemigroup

Tactic:
ext1
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
f : α → β
⊢ Eq (α := α → FreeSemigroup β) ((⇑(MulHom.comp toFreeSemigroup (map f)) : (a : FreeMagma α) → FreeSemigroup β) ∘ of)
    ((⇑((FreeSemigroup.map f).comp toFreeSemigroup) : (a : FreeMagma α) → FreeSemigroup β) ∘ of)

Tactic:
rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
f : α → β
x : FreeMagma α
⊢ Eq (α := FreeSemigroup β)
    ((toFreeSemigroup : (a : FreeMagma β) → FreeSemigroup β)
        ((map f : (a : FreeMagma α) → FreeMagma β) x : FreeMagma β) :
      FreeSemigroup β)
    ((FreeSemigroup.map f : (a : FreeSemigroup α) → FreeSemigroup β)
        ((toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) x) :
      FreeSemigroup β)

Tactic:
DFunLike.congr_fun (toFreeSemigroup_comp_map f) x

Premises used: DFunLike.congr_fun, FreeMagma.toFreeSemigroup_comp_map
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x_1 x y : FreeMagma α
hx : FreeSemigroup.length.{u} (α := α) ((toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) x) = x.length
hy : FreeSemigroup.length.{u} (α := α) ((toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) y) = y.length
rw : x.length + y.length = (x * y).length
⊢ FreeSemigroup.length.{u} (α := α) ((toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) (x * y)) = (x * y).length

Tactic:
rw [map_mul, FreeSemigroup.length_mul, hx, hy]

Premises used: map_mul, FreeSemigroup.length_mul
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x_1 x y : FreeMagma α
hx : FreeSemigroup.length.{u} (α := α) ((toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) x) = x.length
hy : FreeSemigroup.length.{u} (α := α) ((toFreeSemigroup : (a : FreeMagma α) → FreeSemigroup α) y) = y.length
⊢ x.length + y.length = (x * y).length

Tactic:
rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
h :
  ∀ (x : α),
    Eq (α := Magma.AssocQuotient (FreeMagma α))
      (((⇑(MulHom.comp
                (MulHom.comp (N := FreeSemigroup α)
                  ((FreeSemigroup.lift :
                      (a : α → Magma.AssocQuotient (FreeMagma α)) →
                        FreeSemigroup α →ₙ* Magma.AssocQuotient (FreeMagma α))
                    ((⇑Magma.AssocQuotient.of : (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘ FreeMagma.of))
                  ((Magma.AssocQuotient.lift :
                      (a : FreeMagma α →ₙ* FreeSemigroup α) → Magma.AssocQuotient (FreeMagma α) →ₙ* FreeSemigroup α)
                    FreeMagma.toFreeSemigroup))
                Magma.AssocQuotient.of) :
            (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘
          FreeMagma.of)
        x)
      (((⇑(MulHom.comp (MulHom.id (Magma.AssocQuotient (FreeMagma α))) Magma.AssocQuotient.of) :
            (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘
          FreeMagma.of)
        x)
⊢ Eq.{u + 1} (α := Magma.AssocQuotient (FreeMagma α) →ₙ* Magma.AssocQuotient (FreeMagma α))
    (MulHom.comp (N := FreeSemigroup α)
      ((FreeSemigroup.lift :
          (a : α → Magma.AssocQuotient (FreeMagma α)) → FreeSemigroup α →ₙ* Magma.AssocQuotient (FreeMagma α))
        ((⇑Magma.AssocQuotient.of : (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘ FreeMagma.of))
      ((Magma.AssocQuotient.lift :
          (a : FreeMagma α →ₙ* FreeSemigroup α) → Magma.AssocQuotient (FreeMagma α) →ₙ* FreeSemigroup α)
        FreeMagma.toFreeSemigroup))
    (MulHom.id (Magma.AssocQuotient (FreeMagma α)))

Tactic:
ext
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x : α
⊢ Eq (α := Magma.AssocQuotient (FreeMagma α))
    (((⇑(MulHom.comp
              (MulHom.comp (N := FreeSemigroup α)
                ((FreeSemigroup.lift :
                    (a : α → Magma.AssocQuotient (FreeMagma α)) → FreeSemigroup α →ₙ* Magma.AssocQuotient (FreeMagma α))
                  ((⇑Magma.AssocQuotient.of : (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘ FreeMagma.of))
                ((Magma.AssocQuotient.lift :
                    (a : FreeMagma α →ₙ* FreeSemigroup α) → Magma.AssocQuotient (FreeMagma α) →ₙ* FreeSemigroup α)
                  FreeMagma.toFreeSemigroup))
              Magma.AssocQuotient.of) :
          (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘
        FreeMagma.of)
      x)
    (((⇑(MulHom.comp (MulHom.id (Magma.AssocQuotient (FreeMagma α))) Magma.AssocQuotient.of) :
          (a : FreeMagma α) → Magma.AssocQuotient (FreeMagma α)) ∘
        FreeMagma.of)
      x)

Tactic:
rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
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)
⊢ 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 α))

Tactic:
ext1
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
⊢ 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:
rfl
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
x : X
⊢ Eq (α := X →₀ ℤ) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) (of x) : X →₀ ℤ) (Finsupp.single x 1 : X →₀ ℤ)

Tactic:
simp [toFinsupp]

Premises used: FreeAbelianGroup.toFinsupp
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
x : X
n : ℤ
⊢ (toFreeAbelianGroup : (a : X →₀ ℤ) → FreeAbelianGroup X) (single x n) = n • FreeAbelianGroup.of x

Tactic:
simp [toFreeAbelianGroup]

Premises used: Finsupp.toFreeAbelianGroup
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
x : X
⊢ AddMonoidHom.comp toFreeAbelianGroup (singleAddHom x) =
    (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) : (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X) (of x)

Tactic:
AddMonoidHom.ext <| toFreeAbelianGroup_single _

Premises used: Finsupp.toFreeAbelianGroup_single, AddMonoidHom.ext
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
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 : ℤ)
⊢ Eq.{u_1 + 1} (α := (X →₀ ℤ) →+ X →₀ ℤ) (AddMonoidHom.comp toFinsupp toFreeAbelianGroup) (AddMonoidHom.id (X →₀ ℤ))

Tactic:
ext
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
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:
simp
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
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)
⊢ Eq.{u_1 + 1} (α := FreeAbelianGroup X →+ FreeAbelianGroup X) (AddMonoidHom.comp toFreeAbelianGroup toFinsupp)
    (AddMonoidHom.id (FreeAbelianGroup X))

Tactic:
ext
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
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
rw₂ rw₃ : x = x
⊢ (toFreeAbelianGroup : (a : X →₀ ℤ) → FreeAbelianGroup X) ((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) x) = x

Tactic:
rw [← AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp, AddMonoidHom.id_apply]

Premises used: AddMonoidHom.id_apply, AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
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
rw₂ rw₃ : f = f
⊢ (toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ)
      ((toFreeAbelianGroup : (a : X →₀ ℤ) → FreeAbelianGroup X) f : FreeAbelianGroup X) =
    f

Tactic:
rw [← AddMonoidHom.comp_apply, toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.id_apply]

Premises used: AddMonoidHom.id_apply, FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.comp_apply
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
x : X
a : FreeAbelianGroup X
rw :
  Ne (α := ℤ) ((((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a : X →₀ ℤ) : (a : X) → ℤ) x : ℤ) (0 : ℤ) ↔
    Ne (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)
⊢ x ∈ a.support ↔ Ne (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)

Tactic:
rw [support, Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff, FreeAbelianGroup.support
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ Ne (α := ℤ) ((((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a : X →₀ ℤ) : (a : X) → ℤ) x : ℤ) (0 : ℤ) ↔
    Ne (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ Ne (α := ℤ) ((((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a : X →₀ ℤ) : (a : X) → ℤ) x : ℤ) (0 : ℤ) ↔
    Ne (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
x : X
a : FreeAbelianGroup X
rw :
  Eq (α := ℤ) ((((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a : X →₀ ℤ) : (a : X) → ℤ) x : ℤ) (0 : ℤ) ↔
    Eq (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)
⊢ x ∉ a.support ↔ Eq (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)

Tactic:
rw [support, Finsupp.notMem_support_iff]

Premises used: FreeAbelianGroup.support, Finsupp.notMem_support_iff
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ Eq (α := ℤ) ((((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a : X →₀ ℤ) : (a : X) → ℤ) x : ℤ) (0 : ℤ) ↔
    Eq (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ Eq (α := ℤ) ((((toFinsupp : (a : FreeAbelianGroup X) → X →₀ ℤ) a : X →₀ ℤ) : (a : X) → ℤ) x : ℤ) (0 : ℤ) ↔
    Eq (α := ℤ) ((coeff x : (a : FreeAbelianGroup X) → ℤ) a : ℤ) (0 : ℤ)

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset X) (support 0) ∅

Tactic:
simp only [support, Finsupp.support_zero, map_zero]

Premises used: Finsupp.support_zero, FreeAbelianGroup.support, map_zero
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
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}
rw₂ rw₃ : Eq (α := Finset X) {x} {x}
⊢ (of x).support = {x}

Tactic:
rw [support, toFinsupp_of, Finsupp.support_single _ one_ne_zero]

Premises used: Finsupp.support_single, FreeAbelianGroup.support, FreeAbelianGroup.toFinsupp_of, one_ne_zero
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
a : FreeAbelianGroup X
⊢ (-a).support = a.support

Tactic:
simp only [support, map_neg, Finsupp.support_neg]

Premises used: FreeAbelianGroup.support, map_neg, Finsupp.support_neg
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
h₁ : ∀ (x : X), x ∈ (k • a).support ↔ x ∈ a.support
⊢ (k • a).support = a.support

Tactic:
ext x
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ x ∈ (k • a).support ↔ x ∈ a.support

Tactic:
simp [h]
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
apply : Ne (α := ℤ) (↑k : ℤ) 0
⊢ (k • a).support = a.support

Tactic:
apply support_zsmul k _ a

Premises used: Nat.cast, FreeAbelianGroup.support_zsmul
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ Ne (α := ℤ) (↑k : ℤ) 0

Tactic:
mod_cast h

Premises used: congrArg, cast, Ne, Nat.cast, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ Ne (α := ℤ) (↑k : ℤ) 0

Tactic:
exact mod_cast h
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
a b : FreeAbelianGroup X
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)
⊢ (a + b).support ⊆ a.support ∪ b.support

Tactic:
simp only [support, map_add]

Premises used: FreeAbelianGroup.support, map_add
-- Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp
Goal:
X : Type u_1
a b : FreeAbelianGroup X
⊢ (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:
apply Finsupp.support_add

Premises used: Finsupp.support_add
-- Module: Mathlib.Algebra.FreeAbelianGroup.UniqueSums
Goal:
σ : Type u_1
⊢ TwoUniqueSums.{u_1} (FreeAbelianGroup σ)

Tactic:
(FreeAbelianGroup.equivFinsupp σ).twoUniqueSums_iff.mpr inferInstance

Premises used: Iff.mpr, inferInstance, AddEquiv.twoUniqueSums_iff, FreeAbelianGroup.equivFinsupp
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
⊢ #(FreeMonoid X) = max #X ℵ₀

Tactic:
have hX := mk_freeMonoid X
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
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)) ℵ₀
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)) ℵ₀
rw₇ rw₈ :
  max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #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)) ℵ₀

Tactic:
rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
    mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]

Premises used: Cardinal.mk_finsupp_lift_of_infinite, sup_assoc, sup_comm, MonoidAlgebra, FreeAlgebra.equivMonoidAlgebraFreeMonoid, Cardinal.lift_aleph0, AlgEquiv.toEquiv, Cardinal.lift_max, Equiv.cardinal_eq
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : IsEmpty X
⊢ Cardinal.lift.{u, max u v} #(Finsupp.{v, u} (FreeMonoid X) R) = Cardinal.lift.{max u v, u} #R

Tactic:
have := lift_mk_eq'.2 ⟨show (FreeMonoid X →₀ R) ≃ R from Finsupp.uniqueEquiv 1⟩
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : IsEmpty X
this : Cardinal.lift.{u, max u v} #(Finsupp.{v, u} (FreeMonoid X) R) = Cardinal.lift.{max u v, u} #R
⊢ #(Finsupp.{v, u} (FreeMonoid X) R) = Cardinal.lift.{v, u} #R

Tactic:
rw [lift_id'.{u, v}, lift_umax] at this

Premises used: Cardinal.lift_umax
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : IsEmpty X
this : #(Finsupp.{v, u} (FreeMonoid X) R) = Cardinal.lift.{v, u} #R
rwa : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = Cardinal.lift.{v, u} #R
rwa₁ rwa₂ rwa₃ rwa₄ : #(Finsupp.{v, u} (FreeMonoid X) R) = Cardinal.lift.{v, u} #R
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R

Tactic:
rwa [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra]

Premises used: MonoidAlgebra, FreeAlgebra.equivMonoidAlgebraFreeMonoid, AlgEquiv.toEquiv, Equiv.cardinal_eq
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Subsingleton R
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = 1
rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = 1
rw₂ rw₃ : Eq (α := Cardinal.{max v u}) 1 1
⊢ #(FreeAlgebra R X) = 1

Tactic:
rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra, mk_eq_one]

Premises used: MonoidAlgebra, FreeAlgebra.equivMonoidAlgebraFreeMonoid, Cardinal.mk_eq_one, AlgEquiv.toEquiv, Equiv.cardinal_eq
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inl : Subsingleton R → #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
inr : Nontrivial R → #(FreeAlgebra R 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)) ℵ₀

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial