case pos
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)

case neg
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
by_cases ha : IsUnit a
case pos
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ Ring.inverse (↑χ a) = ↑χ (Ring.inverse a)
case pos
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
rw [inv_apply_eq_inv]
case pos
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ Ring.inverse (↑χ a) = ↑χ (Ring.inverse a)
case pos
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ Ring.inverse (↑χ a) = ↑χ (Ring.inverse a)
have h := IsUnit.map χ ha
case pos.a
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ (fun x x_1 => x * x_1) (↑χ a) (Ring.inverse (↑χ a)) = (fun x x_1 => x * x_1) (↑χ a) (↑χ (Ring.inverse a))
case pos
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ Ring.inverse (↑χ a) = ↑χ (Ring.inverse a)
apply IsUnit.mul_right_injective h
case pos.a
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ ↑χ a * Ring.inverse (↑χ a) = ↑χ a * ↑χ (Ring.inverse a)
case pos.a
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ (fun x x_1 => x * x_1) (↑χ a) (Ring.inverse (↑χ a)) = (fun x x_1 => x * x_1) (↑χ a) (↑χ (Ring.inverse a))
dsimp only
case pos.a
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ 1 = ↑χ 1
case pos.a
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ ↑χ a * Ring.inverse (↑χ a) = ↑χ a * ↑χ (Ring.inverse a)
erw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha]
no goals
case pos.a
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ 1 = ↑χ 1
exact (MulChar.map_one χ).symm
case neg
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ ¬IsUnit a → ↑χ⁻¹ a = ↑χ (Ring.inverse a)
case neg
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
revert ha
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
✝ : Nontrivial R
⊢ ¬IsUnit a → ↑χ⁻¹ a = ↑χ (Ring.inverse a)
case neg
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ ¬IsUnit a → ↑χ⁻¹ a = ↑χ (Ring.inverse a)
nontriviality R
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
✝ : Nontrivial R
ha : ¬IsUnit a
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
✝ : Nontrivial R
⊢ ¬IsUnit a → ↑χ⁻¹ a = ↑χ (Ring.inverse a)
intro ha
no goals
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
✝ : Nontrivial R
ha : ¬IsUnit a
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]