-- Mathlib/Data/ZMod/Units.lean
theorem unitsMap_surjective [hm : NeZero m] (h : n ∣ m) :
    Function.Surjective (unitsMap h)

Proof state:
case pos.inr
n m : ℕ
hm : NeZero m
h✝¹ : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h✝ : p ∣ ps.prod id * n
h : p ∣ n
⊢ False

Tactic:
exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, pp, hpx, h⟩ hx

Result:
no goals

Proof state:
case h.H
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
⊢ False

Tactic:
by_cases hpx : p ∣ x

Result:
case pos
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
⊢ False

case neg
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
⊢ False

Proof state:
case pos.inl
n m : ℕ
hm : NeZero m
h✝¹ : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h✝ : p ∣ ps.prod id * n
h : p ∣ ps.prod id
q : ℕ
hq : (Nat.Prime p ∧ p ∣ m ∧ m ≠ 0) ∧ ¬p ∣ x
hq' : p ∣ id q
⊢ False

Tactic:
exact hq.2 hpx

Result:
no goals

Proof state:
case pos.inl
n m : ℕ
hm : NeZero m
h✝¹ : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h✝ : p ∣ ps.prod id * n
h : p ∣ ps.prod id
q : ℕ
hq : q ∈ ps
hq' : p ∣ id q
⊢ False

Tactic:
rw [Finset.mem_filter, Nat.mem_primeFactors,
  ← (Nat.prime_dvd_prime_iff_eq pp hq.1.1).mp hq'] at hq

Result:
case pos.inl
n m : ℕ
hm : NeZero m
h✝¹ : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h✝ : p ∣ ps.prod id * n
h : p ∣ ps.prod id
q : ℕ
hq : (Nat.Prime p ∧ p ∣ m ∧ m ≠ 0) ∧ ¬p ∣ x
hq' : p ∣ id q
⊢ False

Proof state:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
⊢ ∃ k, (x + k * n).Coprime m

Tactic:
let ps := m.primeFactors.filter (fun p ↦ ¬p ∣ x)

Result:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
⊢ ∃ k, (x + k * n).Coprime m

Proof state:
n m : ℕ
hm : NeZero m
h : n ∣ m
this : ∀ (x : ℕ), x.Coprime n → ∃ k, (x + k * n).Coprime m
⊢ Function.Surjective ⇑(unitsMap h)

Tactic:
intro x

Result:
n m : ℕ
hm : NeZero m
h : n ∣ m
this : ∀ (x : ℕ), x.Coprime n → ∃ k, (x + k * n).Coprime m
x : (ZMod n)ˣ
⊢ ∃ a, (unitsMap h) a = x

Proof state:
case h.H
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
⊢ ∀ (k : ℕ), Nat.Prime k → k ∣ x + ps.prod id * n → ¬k ∣ m

Tactic:
intro p pp hp hpn

Result:
case h.H
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
⊢ False