awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
d : FreeMonoid β
mpr :
  ∃ (a : FreeMonoid α),
    Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)
⊢ ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = d
have mpr₁ : ∀ (head : β) (tail : FreeMonoid β) (ih : ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = tail),
  ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = of head * tail
Tactic: induction d using FreeMonoid.inductionOn' with
  | one => use 1; rfl
  | mul_of head tail ih =>
    specialize fs head
    rcases fs with ⟨a, rfl⟩
    rcases ih with ⟨b, rfl⟩
    use FreeMonoid.of a * b
    rfl
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
x : α
xs : List α
⊢ Eq (α := FreeMonoid α)
    ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) { head := x, tail := xs : FreeSemigroup α } : FreeMonoid α)
    ((ofList : (a : List α) → FreeMonoid α) (x :: xs) : FreeMonoid α)
have suffices : ∀ (x : FreeMonoid α),
  List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of xs) =
    HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) xs : FreeMonoid α)
Tactic: suffices ∀ x : FreeMonoid α, (xs.map FreeMonoid.of).foldl (· * ·) x = x * ofList xs by
    simpa [← List.foldl_map, lift_mk_eq_foldl, toFreeMonoid, lift] using this (FreeMonoid.of x)
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
x : α
xs : List α
⊢ ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of xs) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) xs : FreeMonoid α)
have nil : ∀ (x : FreeMonoid α),
  List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of []) =
    HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) [] : FreeMonoid α)
Tactic: induction xs with grind [ofList_nil, ofList_cons]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
x : α
xs : List α
nil :
  ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of []) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) [] : FreeMonoid α)
⊢ ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of xs) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) xs : FreeMonoid α)
have cons : ∀ (head : α) (tail : List α),
  (∀ (x : FreeMonoid α),
      List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of tail) =
        HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) tail : FreeMonoid α)) →
    ∀ (x : FreeMonoid α),
      List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of (head :: tail)) =
        HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) (head :: tail) : FreeMonoid α)
Tactic: induction xs with grind [ofList_nil, ofList_cons]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (hypothesis)
Goal:
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h :
  Eq (α := FreeMonoid α)
    ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) { head := x, tail := xs : FreeSemigroup α } : FreeMonoid α)
    ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) { head := y, tail := ys : FreeSemigroup α } : FreeMonoid α)
⊢ { head := x, tail := xs : FreeSemigroup α } = { head := y, tail := ys }
have h₁ : x :: xs = y :: ys
Tactic: simp only [toFreeMonoid_mk_eq_cons, Equiv.apply_eq_iff_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
x : FreeSemigroup α
⊢ Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) x : FreeMonoid α) (1 : FreeMonoid α)
have ih1 : ∀ (x : α),
  Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x) : FreeMonoid α)
    (1 : FreeMonoid α)
Tactic: induction x with simp
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
x : FreeSemigroup α
ih1 :
  ∀ (x : α),
    Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x) : FreeMonoid α)
      (1 : FreeMonoid α)
⊢ Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) x : FreeMonoid α) (1 : FreeMonoid α)
have ih2 : ∀ (x : α) (y : FreeSemigroup α),
  Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x) : FreeMonoid α)
      (1 : FreeMonoid α) →
    Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) y : FreeMonoid α) (1 : FreeMonoid α) →
      Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x * y) : FreeMonoid α)
        (1 : FreeMonoid α)
Tactic: induction x with simp
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
⊢ Eq (α := Set (FreeMonoid α)) (Set.range (ι := FreeSemigroup α) (⇑toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α))
    {1}ᶜ
have h : ∀ (x : FreeMonoid α),
  Membership.mem (γ := Set (FreeMonoid α))
      (Set.range (ι := FreeSemigroup α) (⇑toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α)) x ↔
    Membership.mem (γ := Set (FreeMonoid α)) {1}ᶜ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
x : 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 α))
          x :
        WithOne (FreeSemigroup α)) =
    x
have one : 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: induction x with simp [*]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
x : FreeMonoid α
one :
  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 α)
⊢ (((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
have of : ∀ (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: induction x with simp [*]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
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 α))
have coe : ∀ (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: induction a with simp_all
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
x : 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
have 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 α))
Tactic: induction x with
    | one => simp
    | coe a => induction a with simp_all
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
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 α))
⊢ ((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
have 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 α))
Tactic: induction x with
    | one => simp
    | coe a => induction a with simp_all
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = 0
have simp : HMul.hMul (α := α) 0 (↑1 : α) = 0
Tactic: simp only [normUnit_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ HMul.hMul (α := α) 1 (↑(normUnit 1) : α) = 1
have rw : Eq.{u_1 + 1} (α := α) (↑1 : α) 1
Tactic: rw [normUnit_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x y : α
hx : x = 0
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
have rw : 0 * y * (↑(normUnit (0 * y)) : α) = HMul.hMul (α := α) 0 (↑(normUnit 0) : α) * (y * (↑(normUnit y) : α))
Tactic: rw [hx, zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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) : α))
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
have rw₁ : HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = HMul.hMul (α := α) 0 (↑(normUnit 0) : α) * (y * (↑(normUnit y) : α))
Tactic: rw [hx, zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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) : α))
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
have rw₂ : 0 = 0 * (y * (↑(normUnit y) : α))
Tactic: rw [hx, zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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) : α))
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
have rw₃ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [hx, zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x y : α
hx : ¬x = 0
hy : y = 0
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
have rw : x * 0 * (↑(normUnit (x * 0)) : α) = x * (↑(normUnit x) : α) * HMul.hMul (α := α) 0 (↑(normUnit 0) : α)
Tactic: rw [hy, mul_zero, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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) : α)
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
have rw₁ : HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = x * (↑(normUnit x) : α) * HMul.hMul (α := α) 0 (↑(normUnit 0) : α)
Tactic: rw [hy, mul_zero, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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) : α)
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
have rw₂ : 0 = x * (↑(normUnit x) : α) * 0
Tactic: rw [hy, mul_zero, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
have rw₃ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [hy, mul_zero, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x y : α
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y * (↑(normUnit (x * y)) : α) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
have simp : x * y * ((↑(normUnit x) : α) * (↑(normUnit y) : α)) = x * (↑(normUnit x) : α) * (y * (↑(normUnit y) : α))
Tactic: simp only [normUnit_mul hx hy, Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a : α
⊢ Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1
have a₁ : Nontrivial α
Tactic: nontriviality α using Subsingleton.elim a 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a : α
h : Nontrivial α
⊢ Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1
have inl : Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑(normUnit 0) : α))) 1
Tactic: obtain rfl | h := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a : α
h : Nontrivial α
inl : Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑(normUnit 0) : α))) 1
⊢ Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1
have inr : ∀ (h : a ≠ 0), Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1
Tactic: obtain rfl | h := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
h : Nontrivial α
⊢ Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑(normUnit 0) : α))) 1
have inl : Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑1 : α))) 1
Tactic: rw [normUnit_zero, zero_mul, normUnit_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
h : Nontrivial α
inl : Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑1 : α))) 1
⊢ Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑(normUnit 0) : α))) 1
have inl₁ : Eq.{u_1 + 1} (α := αˣ) (normUnit 0) 1
Tactic: rw [normUnit_zero, zero_mul, normUnit_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
h : Nontrivial α
inl : Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑1 : α))) 1
inl₁ : Eq.{u_1 + 1} (α := αˣ) (normUnit 0) 1
⊢ Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑(normUnit 0) : α))) 1
have inl₂ : Eq.{u_1 + 1} (α := αˣ) 1 1
Tactic: rw [normUnit_zero, zero_mul, normUnit_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a : α
h_1 : Nontrivial α
h : a ≠ 0
⊢ Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1
have inr : HMul.hMul (α := αˣ) (normUnit a) (normUnit (↑(normUnit a) : α)) = 1
Tactic: rw [normUnit_mul h (Units.ne_zero _), normUnit_coe_units, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a : α
h_1 : Nontrivial α
h : a ≠ 0
inr : HMul.hMul (α := αˣ) (normUnit a) (normUnit (↑(normUnit a) : α)) = 1
⊢ Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1
have inr₁ : HMul.hMul (α := αˣ) (normUnit a) (normUnit a)⁻¹ = 1
Tactic: rw [normUnit_mul h (Units.ne_zero _), normUnit_coe_units, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a : α
h_1 : Nontrivial α
h : a ≠ 0
inr : HMul.hMul (α := αˣ) (normUnit a) (normUnit (↑(normUnit a) : α)) = 1
inr₁ : HMul.hMul (α := αˣ) (normUnit a) (normUnit a)⁻¹ = 1
⊢ Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1
have inr₂ : Eq (α := αˣ) (normUnit a) (normUnit a)
Tactic: rw [normUnit_mul h (Units.ne_zero _), normUnit_coe_units, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a b : α
hab : a ∣ b
hba : b ∣ a
⊢ Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) b : α)
have a₁ : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a b : α
hab : a ∣ b
hba : b ∣ a
h : Nontrivial α
⊢ Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) b : α)
have rcases : ∀ (u : αˣ) (hab : a ∣ a * (↑u : α)) (hba : a * (↑u : α) ∣ a),
  Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) (a * (↑u : α)) : α)
Tactic: rcases associated_of_dvd_dvd hab hba with ⟨u, rfl⟩
Cleared hypotheses: b, hab, hba
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
⊢ Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) (a * (↑u : α)) : α)
have ha : a ≠ 0
Tactic: refine by_cases (by rintro rfl; simp) fun ha : a ≠ 0 => ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
ha : a ≠ 0
⊢ Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) (a * (↑u : α)) : α)
have suffices : a * (↑(normUnit a) : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)
Tactic: suffices a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹ by
    simpa only [normalize_apply, mul_assoc, normUnit_mul ha u.ne_zero, normUnit_coe_units]