awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ₀ χ₁ : MulChar R R'
h :
  Eq (α := (a : R) → R') ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun) χ₀)
    ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun) χ₁)
⊢ χ₀ = χ₁
have mk : ∀ (toMonoidHom : R →* R') (map_nonunit' : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom : OneHom R R').toFun a = 0)
  (h :
    Eq (α := (a : R) → R')
      ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun)
        { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' })
      ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun) χ₁)),
  { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' : MulChar R R' } = χ₁
Tactic: cases χ₀
Cleared hypotheses: χ₀, h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ₁ : MulChar R R'
toMonoidHom : R →* R'
map_nonunit' : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom : OneHom R R').toFun a = 0
h :
  Eq (α := (a : R) → R')
    ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun)
      { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' })
    ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun) χ₁)
⊢ { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' : MulChar R R' } = χ₁
have mk : ∀ (toMonoidHom_1 : R →* R') (map_nonunit'_1 : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom_1 : OneHom R R').toFun a = 0)
  (h :
    Eq (α := (a : R) → R')
      ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun)
        { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' })
      ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun)
        { toMonoidHom := toMonoidHom_1, map_nonunit' := map_nonunit'_1 })),
  { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' : MulChar R R' } =
    { toMonoidHom := toMonoidHom_1, map_nonunit' := map_nonunit'_1 }
Tactic: cases χ₁
Cleared hypotheses: χ₁, h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
toMonoidHom : R →* R'
map_nonunit' : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom : OneHom R R').toFun a = 0
toMonoidHom_1 : R →* R'
map_nonunit'_1 : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom_1 : OneHom R R').toFun a = 0
h :
  Eq (α := (a : R) → R')
    ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun)
      { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' })
    ((fun (χ : MulChar R R') ↦ (↑χ.toMonoidHom : OneHom R R').toFun)
      { toMonoidHom := toMonoidHom_1, map_nonunit' := map_nonunit'_1 })
⊢ { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' : MulChar R R' } =
    { toMonoidHom := toMonoidHom_1, map_nonunit' := map_nonunit'_1 }
have mk : toMonoidHom = toMonoidHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
⊢ (if IsUnit (x * y) then 1 else 0) = HMul.hMul (α := R') (if IsUnit x then 1 else 0) (if IsUnit y then 1 else 0)
have simp : Eq.{u_2 + 1} (α := R') (if IsUnit x ∧ IsUnit y then 1 else 0) (if IsUnit x then if IsUnit y then 1 else 0 else 0)
Tactic: simp only [IsUnit.mul_iff, boole_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
⊢ Eq.{u_2 + 1} (α := R') (if IsUnit x ∧ IsUnit y then 1 else 0) (if IsUnit x then if IsUnit y then 1 else 0 else 0)
have pos : IsUnit x ∧ IsUnit y → IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
pos : IsUnit x ∧ IsUnit y → IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 1 1
⊢ Eq.{u_2 + 1} (α := R') (if IsUnit x ∧ IsUnit y then 1 else 0) (if IsUnit x then if IsUnit y then 1 else 0 else 0)
have neg : IsUnit x ∧ IsUnit y → IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 1 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
pos : IsUnit x ∧ IsUnit y → IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 1 1
neg : IsUnit x ∧ IsUnit y → IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 1 0
⊢ Eq.{u_2 + 1} (α := R') (if IsUnit x ∧ IsUnit y then 1 else 0) (if IsUnit x then if IsUnit y then 1 else 0 else 0)
have neg₁ : IsUnit x ∧ IsUnit y → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 1 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
pos : IsUnit x ∧ IsUnit y → IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 1 1
neg : IsUnit x ∧ IsUnit y → IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 1 0
neg₁ : IsUnit x ∧ IsUnit y → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 1 0
⊢ Eq.{u_2 + 1} (α := R') (if IsUnit x ∧ IsUnit y then 1 else 0) (if IsUnit x then if IsUnit y then 1 else 0 else 0)
have pos₁ : ¬(IsUnit x ∧ IsUnit y) → IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
pos : IsUnit x ∧ IsUnit y → IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 1 1
neg : IsUnit x ∧ IsUnit y → IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 1 0
neg₁ : IsUnit x ∧ IsUnit y → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 1 0
pos₁ : ¬(IsUnit x ∧ IsUnit y) → IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 0 1
⊢ Eq.{u_2 + 1} (α := R') (if IsUnit x ∧ IsUnit y then 1 else 0) (if IsUnit x then if IsUnit y then 1 else 0 else 0)
have neg₂ : ¬(IsUnit x ∧ IsUnit y) → IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
pos : IsUnit x ∧ IsUnit y → IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 1 1
neg : IsUnit x ∧ IsUnit y → IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 1 0
neg₁ : IsUnit x ∧ IsUnit y → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 1 0
pos₁ : ¬(IsUnit x ∧ IsUnit y) → IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 0 1
neg₂ : ¬(IsUnit x ∧ IsUnit y) → IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
⊢ Eq.{u_2 + 1} (α := R') (if IsUnit x ∧ IsUnit y then 1 else 0) (if IsUnit x then if IsUnit y then 1 else 0 else 0)
have neg₃ : ¬(IsUnit x ∧ IsUnit y) → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : IsUnit x ∧ IsUnit y
h_1 : IsUnit x
h_2 : IsUnit y
⊢ Eq.{u_2 + 1} (α := R') 1 1
have pos : IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 1 1
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : IsUnit x ∧ IsUnit y
h_1 : IsUnit x
h_2 : ¬IsUnit y
left : IsUnit x
⊢ Eq.{u_2 + 1} (α := R') 1 0
have right : IsUnit y
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : IsUnit x ∧ IsUnit y
h_1 : ¬IsUnit x
⊢ Eq.{u_2 + 1} (α := R') 1 0
have left : IsUnit x
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : IsUnit x ∧ IsUnit y
h_1 : ¬IsUnit x
left : IsUnit x
⊢ Eq.{u_2 + 1} (α := R') 1 0
have right : IsUnit y
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : ¬(IsUnit x ∧ IsUnit y)
h_1 : IsUnit x
h_2 : IsUnit y
⊢ Eq.{u_2 + 1} (α := R') 0 1
have pos : IsUnit x → IsUnit y → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 1
Tactic: tauto
Cleared hypotheses: h, h_1, h_2
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : ¬(IsUnit x ∧ IsUnit y)
h_1 : IsUnit x
h_2 : IsUnit y
pos : IsUnit x → IsUnit y → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 1
⊢ Eq.{u_2 + 1} (α := R') 0 1
have pos₁ : IsUnit x → IsUnit y → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 1
Tactic: tauto
Cleared hypotheses: h, h_1, h_2
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : ¬(IsUnit x ∧ IsUnit y)
h_1 : IsUnit x
h_2 : ¬IsUnit y
⊢ Eq.{u_2 + 1} (α := R') 0 0
have neg : IsUnit x → ¬IsUnit y → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 0
Tactic: tauto
Cleared hypotheses: h, h_1, h_2
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : ¬(IsUnit x ∧ IsUnit y)
h_1 : IsUnit x
h_2 : ¬IsUnit y
neg : IsUnit x → ¬IsUnit y → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 0
⊢ Eq.{u_2 + 1} (α := R') 0 0
have neg₁ : IsUnit x → ¬IsUnit y → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
Tactic: tauto
Cleared hypotheses: h, h_1, h_2
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : ¬(IsUnit x ∧ IsUnit y)
h_1 : ¬IsUnit x
⊢ Eq.{u_2 + 1} (α := R') 0 0
have neg : ¬IsUnit x → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 0
Tactic: tauto
Cleared hypotheses: h, h_1
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
h : ¬(IsUnit x ∧ IsUnit y)
h_1 : ¬IsUnit x
neg : ¬IsUnit x → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 0
⊢ Eq.{u_2 + 1} (α := R') 0 0
have neg₁ : ¬IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
Tactic: tauto
Cleared hypotheses: h, h_1
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
⊢ (if IsUnit (x * y) then 1 else 0) = HMul.hMul (α := R') (if IsUnit x then 1 else 0) (if IsUnit y then 1 else 0)
have simp : Eq.{u_2 + 1} (α := R') (if IsUnit x ∧ IsUnit y then 1 else 0) (if IsUnit x then if IsUnit y then 1 else 0 else 0)
Tactic: classical
      simp only [IsUnit.mul_iff, boole_mul]
      split_ifs <;> tauto
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑a : R) : R') ((χ' : (a : R) → R') (↑a : R) : R')
⊢ χ = χ'
have h₁ : ∀ (a : R), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')
Tactic: apply ext'
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑a : R) : R') ((χ' : (a : R) → R') (↑a : R) : R')
a : R
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')
have pos : ∀ (ha : IsUnit a), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑a : R) : R') ((χ' : (a : R) → R') (↑a : R) : R')
a : R
pos : ∀ (ha : IsUnit a), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')
have neg : ∀ (ha : ¬IsUnit a), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑a : R) : R') ((χ' : (a : R) → R') (↑a : R) : R')
a : R
ha : ¬IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')
have neg : Eq.{u_2 + 1} (α := R') (0 : R') ((χ' : (a : R) → R') a : R')
Tactic: rw [map_nonunit χ ha, map_nonunit χ' ha]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑a : R) : R') ((χ' : (a : R) → R') (↑a : R) : R')
a : R
ha : ¬IsUnit a
neg : Eq.{u_2 + 1} (α := R') (0 : R') ((χ' : (a : R) → R') a : R')
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')
have neg₁ : Eq.{u_2 + 1} (α := R') 0 0
Tactic: rw [map_nonunit χ ha, map_nonunit χ' ha]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
⊢ Eq.{u_2 + 1} (α := R') (if hx : IsUnit.{u_1} (M := R) 1 then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) 1
have h1 : Eq.{u_1 + 1} (α := Rˣ) (IsUnit.unit sorry) 1
Tactic: have h1 : (isUnit_one.unit : Rˣ) = 1 := Units.ext rfl
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x y : R
⊢ (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
    HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
have pos : ∀ (hx : IsUnit x),
  (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
    HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
Tactic: by_cases hx : IsUnit x
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x y : R
pos :
  ∀ (hx : IsUnit x),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
⊢ (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
    HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
have neg : ∀ (hx : ¬IsUnit x),
  (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
    HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
Tactic: by_cases hx : IsUnit x
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x y : R
hx : IsUnit x
⊢ (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
    HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
have pos : (if h : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R') else 0) =
  HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R')
    (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
Tactic: simp only [hx, IsUnit.mul_iff, true_and, dif_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x y : R
hx : IsUnit x
⊢ (if h : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') else 0) =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
have pos : ∀ (hy : IsUnit y),
  (if h : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R') else 0) =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R')
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
Tactic: by_cases hy : IsUnit y
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x y : R
hx : IsUnit x
pos :
  ∀ (hy : IsUnit y),
    (if h : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') else 0) =
      HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
⊢ (if h : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') else 0) =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
have neg : ∀ (hy : ¬IsUnit y),
  (if h : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R') else 0) =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R')
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
Tactic: by_cases hy : IsUnit y
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x y : R
hx : IsUnit x
hy : IsUnit y
⊢ (if h : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') else 0) =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
have pos : (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R') =
  HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R') (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R')
Tactic: simp only [hy, dif_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x y : R
hx : IsUnit x
hy : IsUnit y
⊢ (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')
have hm : sorry.unit = hx.unit * hy.unit
Tactic: have hm : (hx.mul hy).unit = hx.unit * hy.unit := Units.ext rfl
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x y : R
hx : IsUnit x
hy : IsUnit y
hm : ⋯.unit = hx.unit * hy.unit
⊢ (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')
have pos : (↑(HMul.hMul (α := R'ˣ) (β := R'ˣ) ((f : (a : Rˣ) → R'ˣ) hx.unit : R'ˣ) ((f : (a : Rˣ) → R'ˣ) hy.unit : R'ˣ)) : R') =
  HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R') (↑((f : (a : Rˣ) → R'ˣ) sorry.unit) : R')
Tactic: rw [hm, map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
x y : R
hx : IsUnit x
hy : IsUnit y
hm : ⋯.unit = hx.unit * hy.unit
⊢ (↑(HMul.hMul (α := R'ˣ) (β := R'ˣ) ((f : (a : Rˣ) → R'ˣ) hx.unit : R'ˣ) ((f : (a : Rˣ) → R'ˣ) hy.unit : R'ˣ)) : R') =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')
have pos : HMul.hMul (α := R'ˣ) (β := R'ˣ) ((f : (a : Rˣ) → R'ˣ) hx.unit : R'ˣ) ((f : (a : Rˣ) → R'ˣ) hy.unit : R'ˣ) =
  HMul.hMul (α := R'ˣ) (β := R'ˣ) ((f : (a : Rˣ) → R'ˣ) sorry.unit : R'ˣ) ((f : (a : Rˣ) → R'ˣ) sorry.unit : R'ˣ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
intro intro₁ :
  ∀ (x y : R),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
⊢ ∀ (x y : R),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
have pos : ∀ (x y : R) (hx : IsUnit x),
  (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
    HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
Tactic: classical
      intro x y
      by_cases hx : IsUnit x
      · simp only [hx, IsUnit.mul_iff, true_and, dif_pos]
        by_cases hy : IsUnit y
        · simp only [hy, dif_pos]
          have hm : (hx.mul hy).unit = hx.unit * hy.unit := Units.ext rfl
          rw [hm, map_mul]
          norm_cast
        · simp only [hy, not_false_iff, dif_neg, mul_zero]
      · simp only [hx, IsUnit.mul_iff, false_and, not_false_iff, dif_neg, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
intro intro₁ :
  ∀ (x y : R),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
pos :
  ∀ (x y : R) (hx : IsUnit x),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
⊢ ∀ (x y : R),
    (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
      HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
        (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
have neg : ∀ (x y : R) (hx : ¬IsUnit x),
  (if hx : IsUnit (x * y) then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) =
    HMul.hMul (α := R') (if hx : IsUnit x then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
      (if hx : IsUnit y then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0)
Tactic: classical
      intro x y
      by_cases hx : IsUnit x
      · simp only [hx, IsUnit.mul_iff, true_and, dif_pos]
        by_cases hy : IsUnit y
        · simp only [hy, dif_pos]
          have hm : (hx.mul hy).unit = hx.unit * hy.unit := Units.ext rfl
          rw [hm, map_mul]
          norm_cast
        · simp only [hy, not_false_iff, dif_neg, mul_zero]
      · simp only [hx, IsUnit.mul_iff, false_and, not_false_iff, dif_neg, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
⊢ ofUnitHom χ.toUnitHom = χ
have h : ∀ (x : Rˣ),
  Eq.{u_2 + 1} (α := R') ((ofUnitHom χ.toUnitHom : (a : R) → R') (↑x : R) : R') ((χ : (a : R) → R') (↑x : R) : R')
Tactic: ext x