-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem ext' {χ χ' : MulChar R R'} (h : ∀ a, χ a = χ' a) : χ = χ'

Proof state:
case mk.mk.e_toMonoidHom
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝¹).toFun a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  ∀ (a : R),
    { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } a =
      { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a
⊢ toMonoidHom✝¹ = toMonoidHom✝

Tactic:
exact MonoidHom.ext h

Result:
no goals

Proof state:
case mk.mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝¹).toFun a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  ∀ (a : R),
    { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } a =
      { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a
⊢ { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }

Tactic:
congr

Result:
case mk.mk.e_toMonoidHom
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝¹).toFun a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  ∀ (a : R),
    { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } a =
      { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a
⊢ toMonoidHom✝¹ = toMonoidHom✝

Proof state:
case mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ' : MulChar R R'
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h : ∀ (a : R), { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a = χ' a
⊢ { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } = χ'

Tactic:
cases χ'

Result:
case mk.mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝¹).toFun a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  ∀ (a : R),
    { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } a =
      { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a
⊢ { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : R), χ a = χ' a
⊢ χ = χ'

Tactic:
cases χ

Result:
case mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ' : MulChar R R'
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h : ∀ (a : R), { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a = χ' a
⊢ { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } = χ'