-- Mathlib/NumberTheory/MulChar/Basic.lean
/-- A multiplicative character `χ` into an integral domain is quadratic
if and only if `χ^2 = 1`. -/
lemma isQuadratic_iff_sq_eq_one {M R : Type*} [CommMonoid M] [CommRing R] [NoZeroDivisors R]
    [Nontrivial R] {χ : MulChar M R} :
    IsQuadratic χ ↔ χ ^ 2 = 1

Proof state:
case refine_1
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
⊢ (χ ^ 2) ↑x = 1 ↑x

Tactic:
rw [one_apply_coe, χ.pow_apply_coe]

Result:
case refine_1
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
⊢ χ ↑x ^ 2 = 1

Proof state:
case refine_1.inr.inr
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = -1
⊢ χ ↑x ^ 2 = 1

Tactic:
simp only [H, even_two, Even.neg_pow, one_pow]

Result:
no goals

Proof state:
case refine_1
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
⊢ χ ↑x ^ 2 = 1

Tactic:
rcases h x with H | H | H

Result:
case refine_1.inl
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = 0
⊢ χ ↑x ^ 2 = 1

case refine_1.inr.inl
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = 1
⊢ χ ↑x ^ 2 = 1

case refine_1.inr.inr
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = -1
⊢ χ ↑x ^ 2 = 1

Proof state:
case pos
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : IsUnit x
⊢ χ x = 0 ∨ χ x = 1 ∨ χ x = -1

Tactic:
refine .inr <| sq_eq_one_iff.mp ?_

Result:
case pos
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : IsUnit x
⊢ χ x ^ 2 = 1

Proof state:
case refine_1.inr.inl
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = 1
⊢ χ ↑x ^ 2 = 1

Tactic:
simp only [H, one_pow]

Result:
no goals

Proof state:
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
⊢ χ.IsQuadratic ↔ χ ^ 2 = 1

Tactic:
refine ⟨fun h ↦ ext (fun x ↦ ?_), fun h x ↦ ?_⟩

Result:
case refine_1
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
⊢ (χ ^ 2) ↑x = 1 ↑x

case refine_2
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
⊢ χ x = 0 ∨ χ x = 1 ∨ χ x = -1

Proof state:
case neg
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : ¬IsUnit x
⊢ χ x = 0 ∨ χ x = 1 ∨ χ x = -1

Tactic:
exact .inl <| map_nonunit χ hx

Result:
no goals

Proof state:
case pos
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : IsUnit x
⊢ χ x ^ 2 = 1

Tactic:
rw [← χ.pow_apply' two_ne_zero, h, MulChar.one_apply hx]

Result:
no goals

Proof state:
case refine_2
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
⊢ χ x = 0 ∨ χ x = 1 ∨ χ x = -1

Tactic:
by_cases hx : IsUnit x

Result:
case pos
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : IsUnit x
⊢ χ x = 0 ∨ χ x = 1 ∨ χ x = -1

case neg
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : ¬IsUnit x
⊢ χ x = 0 ∨ χ x = 1 ∨ χ x = -1

Proof state:
case refine_1.inl
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = 0
⊢ χ ↑x ^ 2 = 1

Tactic:
exact (not_isUnit_zero <| H ▸ IsUnit.map χ <| x.isUnit).elim

Result:
no goals