-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
/-- If `e` is not primitive, then `e.mulShift d = 1` for some proper divisor `d` of `N`. -/
lemma exists_divisor_of_not_isPrimitive (he : ¬e.IsPrimitive) :
    ∃ d : ℕ, d ∣ N ∧ d < N ∧ e.mulShift d = 1

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2.h
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
y : ZMod N
⊢ ((e.mulShift ↑d).mulShift u) y = (e.mulShift (↑d * u)) y

Tactic:
rw [mulShift_apply, mulShift_apply, mulShift_apply, mul_assoc]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ e.mulShift ↑d = 1

Tactic:
rw [← mulShift_unit_eq_one_iff _ hu, ← hb, mul_comm]

Result:
case intro.intro.intro.intro.intro.intro.refine_2
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ (e.mulShift ↑d).mulShift u = e.mulShift (↑d * u)

Proof state:
case intro.intro.intro.intro.intro.intro
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Tactic:
refine ⟨d, hd, lt_of_le_of_ne (Nat.le_of_dvd (NeZero.pos _) hd) ?_, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.refine_1
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ d ≠ N

case intro.intro.intro.intro.intro.intro.refine_2
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ e.mulShift ↑d = 1

Proof state:
case intro.intro
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
b : ZMod N
hb_ne : b ≠ 0
hb : e.mulShift b = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Tactic:
obtain ⟨d, hd, u, hu, rfl⟩ := b.eq_unit_mul_divisor

Result:
case intro.intro.intro.intro.intro.intro
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ d ≠ N

Tactic:
exact fun h ↦ by simp only [h, ZMod.natCast_self, mul_zero, ne_eq, not_true_eq_false] at hb_ne

Result:
no goals

Proof state:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
he : ¬e.IsPrimitive
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Tactic:
simp_rw [IsPrimitive, not_forall, not_ne_iff] at he

Result:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
he : ∃ x, ∃ (_ : x ≠ 0), e.mulShift x = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Proof state:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
he : ∃ x, ∃ (_ : x ≠ 0), e.mulShift x = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Tactic:
rcases he with ⟨b, hb_ne, hb⟩

Result:
case intro.intro
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
b : ZMod N
hb_ne : b ≠ 0
hb : e.mulShift b = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Proof state:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
h : d = N
⊢ False

Tactic:
simp only [h, ZMod.natCast_self, mul_zero, ne_eq, not_true_eq_false] at hb_ne

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ (e.mulShift ↑d).mulShift u = e.mulShift (↑d * u)

Tactic:
ext1 y

Result:
case intro.intro.intro.intro.intro.intro.refine_2.h
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
y : ZMod N
⊢ ((e.mulShift ↑d).mulShift u) y = (e.mulShift (↑d * u)) y