awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ_1 : Subgroup (GL (Fin 2) ℝ)
k_1 : ℤ
inst : FunLike F ℍ ℂ
ι : Type
s : Finset ι
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst_1 : Γ.HasDetPlusMinusOne
f : (i : ι) → SlashInvariantForm Γ k
⊢ (↑s.card : ℤ) * k = ∑ i ∈ s, (fun (i : ι) ↦ k) i

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
n : ℕ
⊢ Eq (α := (a : ℍ) → ℂ) (⇑(↑n : SlashInvariantForm Γ 0) : (a : ℍ) → ℂ) (↑n : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
z : ℤ
⊢ Eq (α := (a : ℍ) → ℂ) (⇑(↑z : SlashInvariantForm Γ 0) : (a : ℍ) → ℂ) (↑z : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj :
  j ∈
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ
⊢ g * j * g⁻¹ ∈ Γ

Tactic:
rw [map_inv, Γ.mem_inv_pointwise_smul_iff, toConjAct_smul] at hj

Premises used: map_inv, ConjAct.toConjAct_smul, Subgroup.mem_inv_pointwise_smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : g * j * g⁻¹ ∈ Γ
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k j
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))

Tactic:
simpa [← SlashAction.slash_mul] using congr_arg (· ∣[k] g) (slash_action_eqn f _ hj)

Premises used: congr_arg, SlashAction.map, SlashAction.slash_mul, SlashInvariantForm.slash_action_eqn
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
g : GL (Fin 2) ℝ
⊢ Eq (α := (a : ℍ) → ℂ) (⇑(translate f g) : (a : ℍ) → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))

Tactic:
rfl

Premises used: _private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.privateSlash, rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
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) χ₁)
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 χ₀
-- Module: Mathlib.NumberTheory.MulChar.Basic
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) χ₁)
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 }
⊢ { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' : MulChar R R' } = χ₁

Tactic:
cases χ₁
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 })
mk : toMonoidHom = toMonoidHom_1
⊢ { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' : MulChar R R' } =
    { toMonoidHom := toMonoidHom_1, map_nonunit' := map_nonunit'_1 }

Tactic:
congr
-- Module: Mathlib.NumberTheory.MulChar.Basic
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_1

Tactic:
apply MonoidHom.ext (fun _ => congr_fun h _)

Premises used: MonoidHom.ext, congr_fun
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
⊢ R → R'

Tactic:
exact fun x => if IsUnit x then 1 else 0

Premises used: IsUnit, OfNat.ofNat, ite
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
⊢ R → R'

Tactic:
classical exact fun x => if IsUnit x then 1 else 0

Premises used: IsUnit, OfNat.ofNat, ite
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
⊢ Eq.{u_2 + 1} (α := R') (if IsUnit.{u_1} (M := R) 1 then 1 else 0) 1

Tactic:
simp only [isUnit_one, if_true]

Premises used: if_true, isUnit_one
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
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)
⊢ (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)

Tactic:
simp only [IsUnit.mul_iff, boole_mul]

Premises used: IsUnit.mul_iff, boole_mul
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
neg₃ : ¬(IsUnit x ∧ IsUnit y) → ¬IsUnit x → 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)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 pos₁ pos₂ pos₃ pos₄ pos₅ pos₆ : IsUnit x → IsUnit y → Eq.{u_2 + 1} (α := R') 1 1
⊢ Eq.{u_2 + 1} (α := R') 1 1

Tactic:
tauto
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
⊢ IsUnit x

Tactic:
tauto
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
⊢ IsUnit y

Tactic:
tauto
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
⊢ IsUnit x

Tactic:
tauto
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
⊢ IsUnit y

Tactic:
tauto
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
pos₁ : IsUnit x → IsUnit y → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 1
⊢ Eq.{u_2 + 1} (α := R') 0 1

Tactic:
tauto
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
neg₁ neg₂ neg₃ neg₄ neg₅ neg₆ neg₇ : IsUnit x → ¬IsUnit y → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
⊢ Eq.{u_2 + 1} (α := R') 0 0

Tactic:
tauto
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
neg₁ : ¬IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
neg₂ : ¬IsUnit x → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 0
neg₃ : ¬IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
neg₄ : ¬IsUnit x → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 0
neg₅ : ¬IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
neg₆ neg₇ neg₈ : ¬IsUnit x → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 0
neg₉ neg₁₀ neg₁₁ : ¬IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
neg₁₂ : ¬IsUnit x → ¬IsUnit x → Eq.{u_2 + 1} (α := R') 0 0
neg₁₃ : ¬IsUnit x → ¬IsUnit y → Eq.{u_2 + 1} (α := R') 0 0
⊢ Eq.{u_2 + 1} (α := R') 0 0

Tactic:
tauto
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
x y : R
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)
⊢ (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)

Tactic:
classical
      simp only [IsUnit.mul_iff, boole_mul]
      split_ifs <;> tauto

Premises used: IsUnit.mul_iff, boole_mul
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
a : R
ha : ¬IsUnit a
⊢ Eq.{u_2 + 1} (α := R') (if IsUnit a then 1 else 0) 0

Tactic:
simp only [ha, if_false]

Premises used: if_false
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : R →* R'
hf : ∀ (a : R), ¬IsUnit a → (↑f : OneHom R R').toFun a = 0
⊢ Eq (α := (a : R) → R') (⇑{ toMonoidHom := f, map_nonunit' := hf : MulChar R R' } : (a : R) → R') (⇑f : (a : R) → R')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
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') ((χ' : (a : R) → R') a : R')
⊢ χ = χ'

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') (0 : R')

Tactic:
χ.map_nonunit' a ha

Premises used: MulChar.map_nonunit'
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
h₁ : ∀ (a : R), Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')
⊢ χ = χ'

Tactic:
apply ext'

Premises used: MulChar.ext'
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
neg : ∀ (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')

Tactic:
by_cases ha : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')

Tactic:
h ha.unit

Premises used: IsUnit.unit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')

Tactic:
exact h ha.unit

Premises used: IsUnit.unit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
neg₁ neg₂ : Eq.{u_2 + 1} (α := R') 0 0
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') a : R') ((χ' : (a : R) → R') a : R')

Tactic:
rw [map_nonunit χ ha, map_nonunit χ' ha]

Premises used: MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
⊢ Eq.{u_2 + 1} (α := R') ((↑((χ.toUnitHom : (a : Rˣ) → R'ˣ) a) : R') : R') ((χ : (a : R) → R') (↑a : R) : R')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
⊢ R → R'

Tactic:
exact fun x => if hx : IsUnit x then f hx.unit else 0
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
⊢ R → R'

Tactic:
classical exact fun x => if hx : IsUnit x then f hx.unit else 0
-- Module: Mathlib.NumberTheory.MulChar.Basic
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_1 + 1} (α := Rˣ) (IsUnit.unit ⋯) 1

Tactic:
have h1 : (isUnit_one.unit : Rˣ) = 1 := Units.ext rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommMonoidWithZero R'
f : MonoidHom.{u_1, u_2} Rˣ R'ˣ
h1 : Eq.{u_1 + 1} (α := Rˣ) (IsUnit.unit ⋯) 1
⊢ Eq.{u_2 + 1} (α := R') (if hx : IsUnit.{u_1} (M := R) 1 then (↑((f : (a : Rˣ) → R'ˣ) hx.unit) : R') else 0) 1

Tactic:
simp only [h1, dif_pos, Units.val_eq_one, map_one, isUnit_one]

Premises used: dif_pos, isUnit_one, map_one, Units.val_eq_one
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)
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)
⊢ (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

Premises used: IsUnit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 :
  (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 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:
simp only [hx, IsUnit.mul_iff, true_and, dif_pos]

Premises used: IsUnit.mul_iff, dif_pos, true_and
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)
neg :
  ∀ (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)

Tactic:
by_cases hy : IsUnit y

Premises used: IsUnit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
pos :
  (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')
⊢ (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)

Tactic:
simp only [hy, dif_pos]

Premises used: dif_pos
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
⊢ ⋯.unit = hx.unit * hy.unit

Tactic:
have hm : (hx.mul hy).unit = hx.unit * hy.unit := Units.ext rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
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'ˣ) ⋯.unit) : R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')
⊢ (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') =
    HMul.hMul (α := R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R') (↑((f : (a : Rˣ) → R'ˣ) ⋯.unit) : R')

Tactic:
rw [hm, map_mul]

Premises used: map_mul
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
pos pos₁ pos₂ 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'ˣ) ⋯.unit : R'ˣ) ((f : (a : Rˣ) → R'ˣ) ⋯.unit : R'ˣ)
⊢ (↑(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')

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)

Tactic:
simp only [hy, not_false_iff, dif_neg, mul_zero]

Premises used: dif_neg, MulZeroClass.mul_zero, not_false_iff
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)

Tactic:
simp only [hx, IsUnit.mul_iff, false_and, not_false_iff, dif_neg, zero_mul]

Premises used: IsUnit.mul_iff, MulZeroClass.zero_mul, false_and, dif_neg, not_false_iff