awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : FreeMonoid α
b : α
y : FreeSemigroup α
⊢ HMul.hMul (β := FreeMonoid α) (FreeMonoid.of b)
        ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) y : FreeMonoid α) =
      1 ∨
    ∃ (y_1 : FreeSemigroup α),
      (toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) y_1 =
        HMul.hMul (β := FreeMonoid α) (FreeMonoid.of b)
          ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) y : FreeMonoid α)

Tactic:
exact Or.inr ⟨of b * y, by simp⟩

Premises used: Or.inr
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
h :
  ∀ (x : FreeMonoid α),
    Membership.mem (γ := Set (FreeMonoid α))
        (Set.range (ι := FreeSemigroup α) (⇑toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α)) x ↔
      Membership.mem (γ := Set (FreeMonoid α)) {1}ᶜ x
⊢ Eq (α := Set (FreeMonoid α)) (Set.range (ι := FreeSemigroup α) (⇑toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α))
    {1}ᶜ

Tactic:
ext x
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : FreeMonoid α
⊢ Membership.mem (γ := Set (FreeMonoid α))
      (Set.range (ι := FreeSemigroup α) (⇑toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α)) x ↔
    Membership.mem (γ := Set (FreeMonoid α)) {1}ᶜ x

Tactic:
grind [eq_one_or_toFreeMonoid x]

Premises used: FreeSemigroup.eq_one_or_toFreeMonoid
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := FreeMonoid α)
    ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
              toFreeMonoid :
            WithOne (FreeSemigroup α) →* FreeMonoid α) :
          (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
        (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
                (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
              (a : FreeMonoid α) → WithOne (FreeSemigroup α))
            1 :
          WithOne (FreeSemigroup α)) :
      FreeMonoid α)
    (1 : FreeMonoid α)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
⊢ (((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α) toFreeMonoid :
          WithOne (FreeSemigroup α) →* FreeMonoid α) :
        (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
      (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
              (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
            (a : FreeMonoid α) → WithOne (FreeSemigroup α))
          (of x) :
        WithOne (FreeSemigroup α)) =
    of x

Tactic:
simp [*]
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x y : FreeMonoid α
h :
  (((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α) toFreeMonoid :
          WithOne (FreeSemigroup α) →* FreeMonoid α) :
        (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
      (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
              (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
            (a : FreeMonoid α) → WithOne (FreeSemigroup α))
          x :
        WithOne (FreeSemigroup α)) =
    x
h_1 :
  (((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α) toFreeMonoid :
          WithOne (FreeSemigroup α) →* FreeMonoid α) :
        (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
      (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
              (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
            (a : FreeMonoid α) → WithOne (FreeSemigroup α))
          y :
        WithOne (FreeSemigroup α)) =
    y
⊢ (((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α) toFreeMonoid :
          WithOne (FreeSemigroup α) →* FreeMonoid α) :
        (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
      (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
              (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
            (a : FreeMonoid α) → WithOne (FreeSemigroup α))
          (x * y) :
        WithOne (FreeSemigroup α)) =
    x * y

Tactic:
simp [*]
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithOne (FreeSemigroup α))
    (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
            (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
          (a : FreeMonoid α) → WithOne (FreeSemigroup α))
        ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                  toFreeMonoid :
                WithOne (FreeSemigroup α) →* FreeMonoid α) :
              (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
            1 :
          FreeMonoid α) :
      WithOne (FreeSemigroup α))
    (1 : WithOne (FreeSemigroup α))

Tactic:
simp
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
⊢ ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
          (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
        (a : FreeMonoid α) → WithOne (FreeSemigroup α))
      ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                toFreeMonoid :
              WithOne (FreeSemigroup α) →* FreeMonoid α) :
            (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
          (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
        FreeMonoid α) =
    (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α))

Tactic:
simp_all
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
y : FreeSemigroup α
h :
  ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
          (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
        (a : FreeMonoid α) → WithOne (FreeSemigroup α))
      ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                toFreeMonoid :
              WithOne (FreeSemigroup α) →* FreeMonoid α) :
            (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
          (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
        FreeMonoid α) =
    (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α))
h_1 :
  ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
          (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
        (a : FreeMonoid α) → WithOne (FreeSemigroup α))
      ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                toFreeMonoid :
              WithOne (FreeSemigroup α) →* FreeMonoid α) :
            (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
          (↑y : WithOne (FreeSemigroup α)) :
        FreeMonoid α) =
    (↑y : WithOne (FreeSemigroup α))
⊢ ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
          (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
        (a : FreeMonoid α) → WithOne (FreeSemigroup α))
      ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                toFreeMonoid :
              WithOne (FreeSemigroup α) →* FreeMonoid α) :
            (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
          (↑(FreeSemigroup.of x * y) : WithOne (FreeSemigroup α)) :
        FreeMonoid α) =
    (↑(FreeSemigroup.of x * y) : WithOne (FreeSemigroup α))

Tactic:
simp_all
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : WithOne (FreeSemigroup α)
one :
  Eq.{u_1 + 1} (α := WithOne (FreeSemigroup α))
    (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
            (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
          (a : FreeMonoid α) → WithOne (FreeSemigroup α))
        ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                  toFreeMonoid :
                WithOne (FreeSemigroup α) →* FreeMonoid α) :
              (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
            1 :
          FreeMonoid α) :
      WithOne (FreeSemigroup α))
    (1 : WithOne (FreeSemigroup α))
coe :
  ∀ (a : FreeSemigroup α),
    ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
            (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
          (a : FreeMonoid α) → WithOne (FreeSemigroup α))
        ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                  toFreeMonoid :
                WithOne (FreeSemigroup α) →* FreeMonoid α) :
              (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
            (↑a : WithOne (FreeSemigroup α)) :
          FreeMonoid α) =
      (↑a : WithOne (FreeSemigroup α))
⊢ ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
          (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
        (a : FreeMonoid α) → WithOne (FreeSemigroup α))
      ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                toFreeMonoid :
              WithOne (FreeSemigroup α) →* FreeMonoid α) :
            (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
          x :
        FreeMonoid α) =
    x

Tactic:
induction x with
    | one => simp
    | coe a => induction a with simp_all

Premises used: WithOne.coe
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
⊢ ∀ (x y : FreeMonoid α),
    ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
            (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
          (a : FreeMonoid α) → WithOne (FreeSemigroup α))
        (x * y) =
      HMul.hMul (α := WithOne (FreeSemigroup α)) (β := WithOne (FreeSemigroup α))
        (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
                (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
              (a : FreeMonoid α) → WithOne (FreeSemigroup α))
            x :
          WithOne (FreeSemigroup α))
        (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
                (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
              (a : FreeMonoid α) → WithOne (FreeSemigroup α))
            y :
          WithOne (FreeSemigroup α))

Tactic:
simp
-- Module: Mathlib.Algebra.FreeMonoid.Symbols
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α) (symbols 1) ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.zero, Finset.empty, List.toFinset, Multiset.ofList, List.pwFilter, FreeMonoid.symbols, List.foldr, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Symbols
Goal:
α : Type u_1
inst : DecidableEq α
m : α
⊢ (of m).symbols = {m}

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.cons, List.toFinset, Multiset.ofList, List.pwFilter, FreeMonoid.symbols, List.foldr, rfl, ite
-- Module: Mathlib.Algebra.FreeMonoid.Symbols
Goal:
α : Type u_1
inst : DecidableEq α
a b : FreeMonoid α
⊢ (a * b).symbols = a.symbols ∪ b.symbols

Tactic:
List.toFinset_append

Premises used: List.toFinset_append, FreeMonoid.symbols
-- Module: Mathlib.Algebra.FreeMonoid.Symbols
Goal:
α : Type u_1
inst : DecidableEq α
m : α
a : FreeMonoid α
⊢ m ∈ a.symbols ↔ m ∈ a

Tactic:
List.mem_toFinset

Premises used: List.mem_toFinset, Set.Mem, setOf, FreeMonoid.mem
-- Module: Mathlib.Algebra.FreeMonoid.UniqueProds
Goal:
κ : Type u_1
⊢ TwoUniqueProds.{u_1} (FreeMonoid κ)

Tactic:
.of_mulHom ⟨Multiplicative.ofAdd ∘ List.length, fun _ _ ↦ congr_arg _ List.length_append⟩
    (fun _ _ _ _ h h' ↦ List.append_inj h <| Equiv.injective Multiplicative.ofAdd h'.1)

Premises used: Function.comp, List.length_append, congr_arg, MulHom.mk, And.left, Equiv.injective, Multiplicative.ofAdd, List.length, DFunLike.coe, TwoUniqueProds.of_mulHom, List.append_inj
-- Module: Mathlib.Algebra.FreeMonoid.UniqueProds
Goal:
κ : Type u_1
⊢ TwoUniqueSums.{u_1} (FreeAddMonoid κ)

Tactic:
.of_addHom ⟨_, fun _ _ => List.length_append⟩ (fun _ _ _ _ h h' ↦ List.append_inj h h'.1)

Premises used: TwoUniqueSums.of_addHom, List.length_append, And.left, AddHom.mk, List.append_inj
-- Module: Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
Goal:
R : Type u_1
X : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A
⊢ Eq (α := X → A) ((Equiv.symm (lift R) : (a : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) → X → A) F : X → A)
    (Function.comp (β := FreeNonUnitalNonAssocAlgebra R X) (⇑F : (a : FreeNonUnitalNonAssocAlgebra R X) → A) (of R) :
      X → A)

Tactic:
rfl

Premises used: FreeNonUnitalNonAssocAlgebra.of, rfl
-- Module: Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
Goal:
R : Type u_1
X : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
f : X → A
⊢ Function.comp (β := FreeNonUnitalNonAssocAlgebra R X)
      (⇑((lift R : (a : X → A) → FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) f :
            FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) :
        (a : FreeNonUnitalNonAssocAlgebra R X) → A)
      (of R) =
    f

Tactic:
(lift R).left_inv f

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, FreeNonUnitalNonAssocAlgebra.lift, Finset.sum, Equiv.left_inv
-- Module: Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
Goal:
R : Type u_1
X : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
f : X → A
F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A
⊢ Function.comp (β := FreeNonUnitalNonAssocAlgebra R X) (⇑F : (a : FreeNonUnitalNonAssocAlgebra R X) → A) (of R) = f ↔
    F = (lift R : (a : X → A) → FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) f

Tactic:
(lift R).symm_apply_eq

Premises used: Equiv.symm_apply_eq, FreeNonUnitalNonAssocAlgebra.lift, FreeNonUnitalNonAssocAlgebra.of
-- Module: Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
Goal:
R : Type u_1
X : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
f : X → A
x : X
⊢ (((lift R : (a : X → A) → FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) f : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A) :
        (a : FreeNonUnitalNonAssocAlgebra R X) → A)
      (of R x) =
    f x

Tactic:
congr_fun (of_comp_lift _ f) x

Premises used: FreeNonUnitalNonAssocAlgebra.of_comp_lift, congr_fun
-- Module: Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
Goal:
R : Type u_1
X : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A
⊢ (lift R : (a : X → A) → FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A)
      (Function.comp (β := FreeNonUnitalNonAssocAlgebra R X) (⇑F : (a : FreeNonUnitalNonAssocAlgebra R X) → A) (of R)) =
    F

Tactic:
(lift R).apply_symm_apply F

Premises used: Equiv.apply_symm_apply, FreeNonUnitalNonAssocAlgebra.lift, FreeNonUnitalNonAssocAlgebra.of
-- Module: Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
Goal:
R : Type u_1
X : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
F₁ F₂ : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A
h :
  ∀ (x : X),
    Eq.{u_3 + 1} (α := A) ((F₁ : (a : FreeNonUnitalNonAssocAlgebra R X) → A) (of R x) : A)
      ((F₂ : (a : FreeNonUnitalNonAssocAlgebra R X) → A) (of R x) : A)
⊢ F₁ = F₂

Tactic:
(lift R).symm.injective <| funext h

Premises used: funext, FreeNonUnitalNonAssocAlgebra.lift, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ Eq.{u_1 + 1} (α := αˣ) (normUnit 1) 1

Tactic:
normUnit_coe_units 1

Premises used: NormalizationMonoid.normUnit_coe_units, OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
simp : HMul.hMul (α := α) 0 (↑1 : α) = 0
⊢ HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = 0

Tactic:
simp only [normUnit_zero]

Premises used: NormalizationMonoid.normUnit_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ HMul.hMul (α := α) 0 (↑1 : α) = 0

Tactic:
mul_one (0 : α)

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ HMul.hMul (α := α) 0 (↑1 : α) = 0

Tactic:
exact mul_one (0 : α)

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
rw : Eq.{u_1 + 1} (α := α) (↑1 : α) 1
⊢ HMul.hMul (α := α) 1 (↑(normUnit 1) : α) = 1

Tactic:
rw [normUnit_one, one_mul]

Premises used: normUnit_one, one_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ Eq.{u_1 + 1} (α := α) (↑1 : α) 1

Tactic:
rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x y : α
hx : x = 0
rw : 0 * y * (↑(normUnit (0 * y)) : α) = HMul.hMul (α := α) 0 (↑(normUnit 0) : α) * (y * (↑(normUnit y) : α))
rw₁ : HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = HMul.hMul (α := α) 0 (↑(normUnit 0) : α) * (y * (↑(normUnit y) : α))
rw₂ : 0 = 0 * (y * (↑(normUnit y) : α))
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) 0 0
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))

Tactic:
rw [hx, zero_mul, zero_mul, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x y : α
hx : ¬x = 0
hy : y = 0
rw : x * 0 * (↑(normUnit (x * 0)) : α) = x * (↑(normUnit x) : α) * HMul.hMul (α := α) 0 (↑(normUnit 0) : α)
rw₁ : HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = x * (↑(normUnit x) : α) * HMul.hMul (α := α) 0 (↑(normUnit 0) : α)
rw₂ : 0 = x * (↑(normUnit x) : α) * 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) 0 0
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))

Tactic:
rw [hy, mul_zero, zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x y : α
hx : ¬x = 0
hy : ¬y = 0
simp : x * y * ((↑(normUnit x) : α) * (↑(normUnit y) : α)) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))

Tactic:
simp only [normUnit_mul hx hy, Units.val_mul]

Premises used: NormalizationMonoid.normUnit_mul, Units.val_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x y : α
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y * ((↑(normUnit x) : α) * (↑(normUnit y) : α)) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))

Tactic:
simp only [mul_assoc, mul_left_comm y]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x : α
⊢ Associated x ((normalize : (a : α) → α) x)

Tactic:
⟨_, rfl⟩

Premises used: Associated, Exists.intro, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x : α
⊢ Associated ((normalize : (a : α) → α) x) x

Tactic:
(associated_normalize _).symm

Premises used: Associated.symm, associated_normalize
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x y : α
⊢ Associated x ((normalize : (a : α) → α) y) ↔ Associated x y

Tactic:
⟨fun h => h.trans (normalize_associated y), fun h => h.trans (associated_normalize y)⟩

Premises used: Associated.trans, Iff.intro, normalize_associated, associated_normalize
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x y : α
⊢ Associated ((normalize : (a : α) → α) x) y ↔ Associated x y

Tactic:
⟨fun h => (associated_normalize _).trans h, fun h => (normalize_associated _).trans h⟩

Premises used: Associated.trans, Iff.intro, normalize_associated, associated_normalize
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x : α
⊢ Eq (α := Associates α) (Associates.mk ((normalize : (a : α) → α) x) : Associates α) (Associates.mk x : Associates α)

Tactic:
Associates.mk_eq_mk_iff_associated.2 (normalize_associated _)

Premises used: Iff.mpr, Associates.mk_eq_mk_iff_associated, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x : α
⊢ (normalize : (a : α) → α) x = x * (↑(normUnit x) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 0 : α) (0 : α)

Tactic:
normalize.map_zero

Premises used: MonoidWithZeroHom.map_zero, normalize
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 1 : α) (1 : α)

Tactic:
normalize.map_one

Premises used: MonoidWithZeroHom.map_one, normalize
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
u : αˣ
⊢ Eq (α := α) ((normalize : (a : α) → α) (↑u : α) : α) (1 : α)

Tactic:
simp [normalize_apply]

Premises used: normalize_apply
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 0 : α) (0 : α)

Tactic:
normalize_zero

Premises used: normalize_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 0 : α) (0 : α)

Tactic:
exact normalize_zero

Premises used: normalize_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x : α
⊢ Eq (α := α) ((normalize : (a : α) → α) x : α) (1 : α) ↔ IsUnit x

Tactic:
⟨fun hx => isUnit_iff_exists_inv.2 ⟨_, hx⟩, fun ⟨u, hu⟩ => hu ▸ normalize_coe_units u⟩

Premises used: Iff.mpr, Units.val, Eq.rec, isUnit_iff_exists_inv, normalize_coe_units, _private.0.normalize_eq_one.match_1, Iff.intro, Exists.intro, normalize, OfNat.ofNat, Eq, DFunLike.coe, NormalizationMonoid.normUnit
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a : α
⊢ Nontrivial α

Tactic:
nontriviality α using Subsingleton.elim a 0
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a : α
h : Nontrivial α
inl : Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑(normUnit 0) : α))) 1
inr : ∀ (h : a ≠ 0), Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1
⊢ Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1

Tactic:
obtain rfl | h := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl