case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
⊢ ∀ (a : R), ↑χ a = ↑χ' a
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
⊢ χ = χ'
apply ext'
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
a : R
⊢ ↑χ a = ↑χ' a
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
⊢ ∀ (a : R), ↑χ a = ↑χ' a
intro a
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
a : R
ha : IsUnit a
⊢ ↑χ a = ↑χ' a

case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
a : R
ha : ¬IsUnit a
⊢ ↑χ a = ↑χ' a
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
a : R
⊢ ↑χ a = ↑χ' a
by_cases ha : IsUnit a
no goals
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
a : R
ha : IsUnit a
⊢ ↑χ a = ↑χ' a
exact h ha.unit
no goals
case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
a : R
ha : ¬IsUnit a
⊢ ↑χ a = ↑χ' a
rw [map_nonunit χ ha, map_nonunit χ' ha]