-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem IsQuadratic.inv {χ : MulChar R R'} (hχ : χ.IsQuadratic) : χ⁻¹ = χ

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ -1 = ↑(-1)

Tactic:
rw [Units.val_neg, Units.val_one]

Result:
no goals

Proof state:
case h.inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ Ring.inverse (χ ↑x) = χ ↑x

Tactic:
have : (-1 : R') = (-1 : R'ˣ) := by rw [Units.val_neg, Units.val_one]

Result:
case h.inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
this : -1 = ↑(-1)
⊢ Ring.inverse (χ ↑x) = χ ↑x

Proof state:
case h.inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
this : -1 = ↑(-1)
⊢ Ring.inverse (χ ↑x) = χ ↑x

Tactic:
rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ)]

Result:
case h.inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
this : -1 = ↑(-1)
⊢ ↑(-1)⁻¹ = ↑(-1)

Proof state:
case h.inr.inl
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₁ : χ ↑x = 1
⊢ Ring.inverse (χ ↑x) = χ ↑x

Tactic:
rw [h₁, Ring.inverse_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
⊢ χ⁻¹ = χ

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
⊢ χ⁻¹ ↑x = χ ↑x

Proof state:
case h.inl
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₀ : χ ↑x = 0
⊢ Ring.inverse (χ ↑x) = χ ↑x

Tactic:
rw [h₀, Ring.inverse_zero]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
⊢ Ring.inverse (χ ↑x) = χ ↑x

Tactic:
rcases hχ x with (h₀ | h₁ | h₂)

Result:
case h.inl
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₀ : χ ↑x = 0
⊢ Ring.inverse (χ ↑x) = χ ↑x

case h.inr.inl
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₁ : χ ↑x = 1
⊢ Ring.inverse (χ ↑x) = χ ↑x

case h.inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ Ring.inverse (χ ↑x) = χ ↑x

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
⊢ χ⁻¹ ↑x = χ ↑x

Tactic:
rw [inv_apply_eq_inv]

Result:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
⊢ Ring.inverse (χ ↑x) = χ ↑x

Proof state:
case h.inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
this : -1 = ↑(-1)
⊢ ↑(-1)⁻¹ = ↑(-1)

Tactic:
rfl

Result:
no goals