case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
⊢ ↑χ⁻¹ ↑x = ↑χ ↑x
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
⊢ χ⁻¹ = χ
ext x
case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
⊢ ↑χ⁻¹ ↑x = ↑χ ↑x
rw [inv_apply_eq_inv]
case h.inl
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₀ : ↑χ ↑x = 0
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x

case h.inr.inl
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₁ : ↑χ ↑x = 1
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x

case h.inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
rcases hχ x with (h₀ | h₁ | h₂)
no goals
case h.inl
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₀ : ↑χ ↑x = 0
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
rw [h₀, Ring.inverse_zero]
no goals
case h.inr.inl
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₁ : ↑χ ↑x = 1
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
rw [h₁, Ring.inverse_one]
case h.inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
this : -1 = ↑(-1)
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
case h.inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
have : (-1 : R') = (-1 : R'ˣ) := by rw [Units.val_neg, Units.val_one]
case h.inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
this : -1 = ↑(-1)
⊢ ↑(-1)⁻¹ = ↑(-1)
case h.inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
this : -1 = ↑(-1)
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ)]
no goals
case h.inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
this : -1 = ↑(-1)
⊢ ↑(-1)⁻¹ = ↑(-1)
rfl
no goals
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
⊢ -1 = ↑(-1)
rw [Units.val_neg, Units.val_one]