-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem inv_apply {R : Type*} [CommMonoidWithZero R] (χ : MulChar R R') (a : R) :
    χ⁻¹ a = χ (Ring.inverse a)

Proof state:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ χ a * Ring.inverse (χ a) = χ a * χ (Ring.inverse a)

Tactic:
rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, map_one]

Result:
no goals

Proof state:
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ χ⁻¹ a = χ (Ring.inverse a)

Tactic:
by_cases ha : IsUnit a

Result:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ χ⁻¹ a = χ (Ring.inverse a)

case neg
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ χ⁻¹ a = χ (Ring.inverse a)

Proof state:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ χ⁻¹ a = χ (Ring.inverse a)

Tactic:
rw [inv_apply_eq_inv]

Result:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ Ring.inverse (χ a) = χ (Ring.inverse a)

Proof state:
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
a✝ : Nontrivial R
⊢ ¬IsUnit a → χ⁻¹ a = χ (Ring.inverse a)

Tactic:
intro ha

Result:
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
a✝ : Nontrivial R
ha : ¬IsUnit a
⊢ χ⁻¹ a = χ (Ring.inverse a)

Proof state:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ Ring.inverse (χ a) = χ (Ring.inverse a)

Tactic:
have h := IsUnit.map χ ha

Result:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ Ring.inverse (χ a) = χ (Ring.inverse a)

Proof state:
case neg
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ ¬IsUnit a → χ⁻¹ a = χ (Ring.inverse a)

Tactic:
nontriviality R

Result:
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
a✝ : Nontrivial R
⊢ ¬IsUnit a → χ⁻¹ a = χ (Ring.inverse a)

Proof state:
case neg
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ χ⁻¹ a = χ (Ring.inverse a)

Tactic:
revert ha

Result:
case neg
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ ¬IsUnit a → χ⁻¹ a = χ (Ring.inverse a)

Proof state:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ (fun x => χ a * x) (Ring.inverse (χ a)) = (fun x => χ a * x) (χ (Ring.inverse a))

Tactic:
dsimp only

Result:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ χ a * Ring.inverse (χ a) = χ a * χ (Ring.inverse a)

Proof state:
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
a✝ : Nontrivial R
ha : ¬IsUnit a
⊢ χ⁻¹ a = χ (Ring.inverse a)

Tactic:
rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]

Result:
no goals