awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
rw :
  Eq (α := (ZMod d)ˣ →* (ZMod n)ˣ)
    (Units.map (MonoidHom.comp (↑(castHom hm (ZMod n)) : ZMod m →* ZMod n) (↑(castHom hd (ZMod m)) : ZMod d →* ZMod m)))
    (Units.map (↑(castHom ⋯ (ZMod n)) : ZMod d →* ZMod n))
⊢ Eq (α := (ZMod d)ˣ →* (ZMod n)ˣ)
    (MonoidHom.comp (N := (ZMod m)ˣ) (Units.map (↑(castHom hm (ZMod n)) : ZMod m →* ZMod n))
      (Units.map (↑(castHom hd (ZMod m)) : ZMod d →* ZMod m)))
    (Units.map (↑(castHom ⋯ (ZMod n)) : ZMod d →* ZMod n))

Tactic:
rw [← Units.map_comp]

Premises used: Units.map_comp
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ Eq (α := (ZMod d)ˣ →* (ZMod n)ˣ)
    (Units.map (MonoidHom.comp (↑(castHom hm (ZMod n)) : ZMod m →* ZMod n) (↑(castHom hd (ZMod m)) : ZMod d →* ZMod m)))
    (Units.map (↑(castHom ⋯ (ZMod n)) : ZMod d →* ZMod n))

Tactic:
congr_arg Units.map <| congr_arg RingHom.toMonoidHom <| castHom_comp hm hd

Premises used: congr_arg, ZMod.castHom_comp, RingHom.toMonoidHom, Units.map
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ Eq (α := (ZMod d)ˣ →* (ZMod n)ˣ)
    (Units.map (MonoidHom.comp (↑(castHom hm (ZMod n)) : ZMod m →* ZMod n) (↑(castHom hd (ZMod m)) : ZMod d →* ZMod m)))
    (Units.map (↑(castHom ⋯ (ZMod n)) : ZMod d →* ZMod n))

Tactic:
exact congr_arg Units.map <| congr_arg RingHom.toMonoidHom <| castHom_comp hm hd

Premises used: congr_arg, ZMod.castHom_comp, RingHom.toMonoidHom, Units.map
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
⊢ unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ

Tactic:
simp [unitsMap, castHom_self]

Premises used: ZMod.unitsMap, ZMod.castHom_self
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
h : n ∣ m
a : (ZMod m)ˣ
⊢ Eq (α := ZMod n) (↑((unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) a) : ZMod n) (↑a : ZMod m).cast

Tactic:
rfl

Premises used: ZMod.cast, rfl
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : n ∣ m
a : (ZMod m)ˣ
⊢ IsUnit (M := ZMod n) (↑a : ZMod m).cast

Tactic:
Units.isUnit (unitsMap hm a)

Premises used: ZMod.unitsMap, ZMod.cast, Units.isUnit, DFunLike.coe
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
this : ∀ (x : ℕ), x.Coprime n → ∃ (k : ℕ), (x + k * n).Coprime m
x : (ZMod n)ˣ
have :
  ∀ (k : ℕ) (hk : ((↑x : ZMod n).val + k * n).Coprime m),
    ∃ (a : (ZMod m)ˣ), (unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) a = x
⊢ ∃ (a : (ZMod m)ˣ), (unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) a = x

Tactic:
have ⟨k, hk⟩ := this x.val.val (val_coe_unit_coprime x)
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
this : ∀ (x : ℕ), x.Coprime n → ∃ (k : ℕ), (x + k * n).Coprime m
x : (ZMod n)ˣ
k : ℕ
hk : ((↑x : ZMod n).val + k * n).Coprime m
⊢ ∃ (a : (ZMod m)ˣ), (unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) a = x

Tactic:
⟨unitOfCoprime _ hk, Units.ext ?_⟩

Premises used: ZMod.unitOfCoprime, Units.ext, Exists.intro
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
this : ∀ (x : ℕ), x.Coprime n → ∃ (k : ℕ), (x + k * n).Coprime m
x : (ZMod n)ˣ
k : ℕ
hk : ((↑x : ZMod n).val + k * n).Coprime m
refine :
  (↑((unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) (unitOfCoprime ((↑x : ZMod n).val + k * n) hk)) : ZMod n) =
    (↑x : ZMod n)
⊢ ∃ (a : (ZMod m)ˣ), (unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) a = x

Tactic:
refine ⟨unitOfCoprime _ hk, Units.ext ?_⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
this : ∀ (x : ℕ), x.Coprime n → ∃ (k : ℕ), (x + k * n).Coprime m
x : (ZMod n)ˣ
k : ℕ
hk : ((↑x : ZMod n).val + k * n).Coprime m
⊢ NeZero n

Tactic:
have : NeZero n := ⟨fun hn ↦ hm.out (eq_zero_of_zero_dvd (hn ▸ h))⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
this_1 : ∀ (x : ℕ), x.Coprime n → ∃ (k : ℕ), (x + k * n).Coprime m
x : (ZMod n)ˣ
k : ℕ
hk : ((↑x : ZMod n).val + k * n).Coprime m
this : NeZero n
⊢ (↑((unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) (unitOfCoprime ((↑x : ZMod n).val + k * n) hk)) : ZMod n) =
    (↑x : ZMod n)

Tactic:
simp [unitsMap_def, -castHom_apply]

Premises used: ZMod.castHom_apply, ZMod.unitsMap_def
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
suffices : ∀ (x : ℕ), x.Coprime n → ∃ (k : ℕ), (x + k * n).Coprime m
⊢ Function.Surjective (α := (ZMod m)ˣ) (β := (ZMod n)ˣ) (⇑(unitsMap h) : (a : (ZMod m)ˣ) → (ZMod n)ˣ)

Tactic:
suffices ∀ x : ℕ, x.Coprime n → ∃ k : ℕ, (x + k * n).Coprime m by
    intro x
    have ⟨k, hk⟩ := this x.val.val (val_coe_unit_coprime x)
    refine ⟨unitOfCoprime _ hk, Units.ext ?_⟩
    have : NeZero n := ⟨fun hn ↦ hm.out (eq_zero_of_zero_dvd (hn ▸ h))⟩
    simp [unitsMap_def, -castHom_apply]
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
h₁ : (x + ps.prod id * n).Coprime m
⊢ ∃ (k : ℕ), (x + k * n).Coprime m

Tactic:
use ps.prod id

Premises used: id, Finset.prod
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
h₁ : ∀ (k : ℕ), Nat.Prime k → k ∣ x + ps.prod id * n → ¬k ∣ m
⊢ (x + ps.prod id * n).Coprime m

Tactic:
apply Nat.coprime_of_dvd

Premises used: Nat.coprime_of_dvd
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
pos : ∀ (hpx : p ∣ x), False
neg : ∀ (hpx : ¬p ∣ x), False
⊢ False

Tactic:
by_cases hpx : p ∣ x
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
⊢ p ∣ x + ps.prod id * n - x

Tactic:
have h := Nat.dvd_sub hp hpx
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h : p ∣ x + ps.prod id * n - x
⊢ p ∣ ps.prod id * n

Tactic:
rw [add_comm, Nat.add_sub_cancel] at h

Premises used: add_comm, Nat.add_sub_cancel
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h : p ∣ ps.prod id * n
pos : ∀ (h : p ∣ ps.prod id), False
pos₁ : ∀ (h : p ∣ n), False
⊢ False

Tactic:
rcases pp.dvd_mul.mp h with h | h

Premises used: Iff.mp, Nat.Prime.dvd_mul
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h_2 : p ∣ ps.prod id * n
h : p ∣ ps.prod id
pos : ∀ (q : ℕ) (hq : q ∈ ps) (hq' : p ∣ id q), False
⊢ False

Tactic:
have ⟨q, hq, hq'⟩ := (pp.prime.dvd_finsetProd_iff id).mp h
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h_2 : p ∣ ps.prod id * n
h : p ∣ ps.prod id
q : ℕ
hq : q ∈ ps
hq' : p ∣ id q
⊢ (Nat.Prime p ∧ p ∣ m ∧ m ≠ 0) ∧ ¬p ∣ x

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

Premises used: Finset.mem_filter, Nat.mem_primeFactors
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h_2 : p ∣ ps.prod id * n
h : p ∣ ps.prod id
q : ℕ
hq : q ∈ ps
hq' : p ∣ id q
hq₁ : (Nat.Prime p ∧ p ∣ m ∧ m ≠ 0) ∧ ¬p ∣ x
⊢ p ∣ id q

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

Premises used: Finset.mem_filter, Nat.mem_primeFactors
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h_2 : 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:
hq.2 hpx

Premises used: And.right
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h_2 : 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

Premises used: And.right
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h_2 : p ∣ ps.prod id * n
h : p ∣ n
⊢ False

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

Premises used: Iff.mpr, And.intro, Exists.intro, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h_2 : p ∣ ps.prod id * n
h : p ∣ n
⊢ False

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

Premises used: Iff.mpr, And.intro, Exists.intro, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
⊢ p ∈ ps

Tactic:
have pps : p ∈ ps := Finset.mem_filter.mpr ⟨Nat.mem_primeFactors.mpr ⟨pp, hpn, hm.out⟩, hpx⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
pps : p ∈ ps
⊢ p ∣ x + ps.prod id * n - (∏ i ∈ ps, id i) * n

Tactic:
have h := Nat.dvd_sub hp ((Finset.dvd_prod_of_mem id pps).mul_right n)
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
pps : p ∈ ps
h : p ∣ x + ps.prod id * n - (∏ i ∈ ps, id i) * n
⊢ p ∣ x

Tactic:
rw [Nat.add_sub_cancel] at h

Premises used: Nat.add_sub_cancel
-- Module: Mathlib.Data.ZMod.Units
Goal:
n m : ℕ
hm : NeZero m
h_1 : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
pps : p ∈ ps
h : p ∣ x
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.ZMod.Units
Goal:
n p : ℕ
h : p ∈ n.primeFactors
rw : ¬p.Coprime n
⊢ ¬IsUnit (M := ZMod n) (↑p : ZMod n)

Tactic:
rw [isUnit_iff_coprime]

Premises used: ZMod.isUnit_iff_coprime
-- Module: Mathlib.Data.ZMod.Units
Goal:
n p : ℕ
h : p ∈ n.primeFactors
⊢ ¬p.Coprime n

Tactic:
(Prime.dvd_iff_not_coprime <| prime_of_mem_primeFactors h).mp <| dvd_of_mem_primeFactors h

Premises used: Nat.dvd_of_mem_primeFactors, Nat.Prime.dvd_iff_not_coprime, Nat.prime_of_mem_primeFactors, Iff.mp
-- Module: Mathlib.Data.ZMod.Units
Goal:
n p : ℕ
h : p ∈ n.primeFactors
⊢ ¬p.Coprime n

Tactic:
exact (Prime.dvd_iff_not_coprime <| prime_of_mem_primeFactors h).mp <| dvd_of_mem_primeFactors h

Premises used: Nat.dvd_of_mem_primeFactors, Nat.Prime.dvd_iff_not_coprime, Nat.prime_of_mem_primeFactors, Iff.mp
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
inl : ∀ (a : ZMod 0), ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
inr : ∀ (hN : N ≠ 0), ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)

Tactic:
rcases eq_or_ne N 0 with rfl | hN

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ZMod.Units
Goal:
a : ZMod 0
inl : ∀ (a : ℤ), ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
⊢ ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)

Tactic:
change ℤ at a
-- Module: Mathlib.Data.ZMod.Units
Goal:
a : ℤ
inl : ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ 0 = u * (↑d : ZMod 0)
inl₁ : ∀ (ha : a ≠ 0), ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
⊢ ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ZMod.Units
Goal:
rw : 0 = HMul.hMul (α := ZMod 0) 1 0
rw₁ rw₂ : Eq (α := ZMod 0) 0 0
⊢ 0 = HMul.hMul (α := ZMod 0) 1 (↑0 : ZMod 0)

Tactic:
rw [Nat.cast_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.cast_zero
-- Module: Mathlib.Data.ZMod.Units
Goal:
⊢ ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ 0 = u * (↑d : ZMod 0)

Tactic:
refine ⟨0, dvd_zero _, 1, isUnit_one, by rw [Nat.cast_zero, mul_zero]⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
a : ℤ
ha : a ≠ 0
⊢ ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)

Tactic:
⟨a.natAbs, dvd_zero _, Int.sign a, ?_, (Int.sign_mul_natAbs a).symm⟩

Premises used: dvd_zero, Int.sign, And.intro, Int.natAbs, Exists.intro, Eq.symm, Int.sign_mul_natAbs
-- Module: Mathlib.Data.ZMod.Units
Goal:
a : ℤ
ha : a ≠ 0
inl : IsUnit a.sign
⊢ ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)

Tactic:
refine ⟨a.natAbs, dvd_zero _, Int.sign a, ?_, (Int.sign_mul_natAbs a).symm⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
a : ℤ
ha : a ≠ 0
inl : ∀ (h : a < 0), IsUnit a.sign
inl₁ : ∀ (h : 0 < a), IsUnit a.sign
⊢ IsUnit a.sign

Tactic:
rcases lt_or_gt_of_ne ha with h | h

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Data.ZMod.Units
Goal:
a : ℤ
ha : a ≠ 0
h : a < 0
⊢ IsUnit a.sign

Tactic:
simp only [Int.sign_eq_neg_one_of_neg h, IsUnit.neg_iff, isUnit_one]

Premises used: Int.sign_eq_neg_one_of_neg, IsUnit.neg_iff, isUnit_one
-- Module: Mathlib.Data.ZMod.Units
Goal:
a : ℤ
ha : a ≠ 0
h : 0 < a
⊢ IsUnit a.sign

Tactic:
simp only [Int.sign_eq_one_of_pos h, isUnit_one]

Premises used: isUnit_one, Int.sign_eq_one_of_pos
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
⊢ NeZero N

Tactic:
have : NeZero N := ⟨hN⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
⊢ d ≠ 0

Tactic:
have hd : d ≠ 0 := Nat.gcd_ne_zero_right hN
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
inr : ∀ (a₀ : ℕ) (ha₀ : a.val = d * a₀), ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)

Tactic:
obtain ⟨a₀, (ha₀ : _ = d * _)⟩ := a.val.gcd_dvd_left N

Premises used: Nat.gcd_dvd_left, ZMod.val
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
inr : ∀ (N₀ : ℕ) (hN₀ : N = d * N₀), ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)

Tactic:
obtain ⟨N₀, (hN₀ : _ = d * _)⟩ := a.val.gcd_dvd_right N

Premises used: Nat.gcd_dvd_right, ZMod.val
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)

Tactic:
⟨d, ⟨N₀, hN₀⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
inr : ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)

Tactic:
refine ⟨d, ⟨N₀, hN₀⟩, ?_⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)

Tactic:
(isUnit_iff_coprime _ _).mpr (Nat.isCoprime_iff_coprime.mp ?_)

Premises used: ZMod.isUnit_iff_coprime, Iff.mpr, Nat.isCoprime_iff_coprime, Iff.mp
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
refine : IsCoprime (R := ℤ) (↑a₀ : ℤ) (↑N₀ : ℤ)
⊢ IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)

Tactic:
refine (isUnit_iff_coprime _ _).mpr (Nat.isCoprime_iff_coprime.mp ?_)

Premises used: ZMod.isUnit_iff_coprime, Iff.mpr, Nat.isCoprime_iff_coprime, Iff.mp
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ ∃ (p : ℤ) (q : ℤ), (↑d : ℤ) = (↑a.val : ℤ) * p + (↑N : ℤ) * q

Tactic:
⟨_, _, Nat.gcd_eq_gcd_ab _ _⟩

Premises used: Exists.intro, Nat.gcd_eq_gcd_ab
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
obtain : ∀ (p q : ℤ) (hpq : (↑d : ℤ) = (↑a.val : ℤ) * p + (↑N : ℤ) * q), IsCoprime (R := ℤ) (↑a₀ : ℤ) (↑N₀ : ℤ)
⊢ IsCoprime (R := ℤ) (↑a₀ : ℤ) (↑N₀ : ℤ)

Tactic:
obtain ⟨p, q, hpq⟩ : ∃ (p q : ℤ), d = a.val * p + N * q := ⟨_, _, Nat.gcd_eq_gcd_ab _ _⟩

Premises used: ZMod.val
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : (↑d : ℤ) = (↑a.val : ℤ) * p + (↑N : ℤ) * q
⊢ (↑d : ℤ) * (p * (↑a₀ : ℤ) + q * (↑N₀ : ℤ)) = (↑d : ℤ)

Tactic:
rw [ha₀, hN₀, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add, eq_comm,
      mul_comm _ p, mul_comm _ q] at hpq

Premises used: mul_assoc, eq_comm, Nat.cast_mul, mul_comm, mul_add
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : (↑d : ℤ) * (p * (↑a₀ : ℤ) + q * (↑N₀ : ℤ)) = (↑d : ℤ)
⊢ IsCoprime (R := ℤ) (↑a₀ : ℤ) (↑N₀ : ℤ)

Tactic:
⟨p, q, Int.eq_one_of_mul_eq_self_right (Nat.cast_ne_zero.mpr hd) hpq⟩

Premises used: Iff.mpr, Int.eq_one_of_mul_eq_self_right, Exists.intro, Nat.cast_ne_zero, IsCoprime
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : (↑d : ℤ) * (p * (↑a₀ : ℤ) + q * (↑N₀ : ℤ)) = (↑d : ℤ)
⊢ IsCoprime (R := ℤ) (↑a₀ : ℤ) (↑N₀ : ℤ)

Tactic:
exact ⟨p, q, Int.eq_one_of_mul_eq_self_right (Nat.cast_ne_zero.mpr hd) hpq⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)

Tactic:
have hu₀ : IsUnit (a₀ : ZMod N₀) := by
    refine (isUnit_iff_coprime _ _).mpr (Nat.isCoprime_iff_coprime.mp ?_)
    obtain ⟨p, q, hpq⟩ : ∃ (p q : ℤ), d = a.val * p + N * q := ⟨_, _, Nat.gcd_eq_gcd_ab _ _⟩
    rw [ha₀, hN₀, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add, eq_comm,
      mul_comm _ p, mul_comm _ q] at hpq
    exact ⟨p, q, Int.eq_one_of_mul_eq_self_right (Nat.cast_ne_zero.mpr hd) hpq⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)
inr :
  ∀ (u : (ZMod N)ˣ) (hu : (unitsMap ⋯ : (a : (ZMod N)ˣ) → (ZMod N₀)ˣ) u = hu₀.unit),
    ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
⊢ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)

Tactic:
obtain ⟨u, hu⟩ := (unitsMap_surjective (⟨d, mul_comm d N₀ ▸ hN₀⟩ : N₀ ∣ N)) hu₀.unit

Premises used: ZMod.unitsMap_surjective, Eq.rec, Exists.intro, mul_comm, IsUnit.unit
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)
u : (ZMod N)ˣ
hu : (unitsMap ⋯ : (a : (ZMod N)ˣ) → (ZMod N₀)ˣ) u = hu₀.unit
⊢ Eq (α := ZMod N₀) ((castHom ⋯ (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀) ((↑a₀ : ZMod N₀) : ZMod N₀)

Tactic:
rw [unitsMap_def, ← Units.val_inj, Units.coe_map, IsUnit.unit_spec, MonoidHom.coe_coe] at hu

Premises used: Units.coe_map, MonoidHom.coe_coe, Units.val_inj, IsUnit.unit_spec, ZMod.unitsMap_def
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)
u : (ZMod N)ˣ
hu :
  Eq (α := ZMod N₀) ((castHom ⋯ (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀) ((↑a₀ : ZMod N₀) : ZMod N₀)
⊢ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)

Tactic:
⟨u.val, u.isUnit, ?_⟩

Premises used: Units.val, And.intro, Exists.intro, Units.isUnit
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)
u : (ZMod N)ˣ
hu :
  Eq (α := ZMod N₀) ((castHom ⋯ (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀) ((↑a₀ : ZMod N₀) : ZMod N₀)
inr : a = (↑u : ZMod N) * (↑d : ZMod N)
⊢ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)

Tactic:
refine ⟨u.val, u.isUnit, ?_⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)
u : (ZMod N)ˣ
hu :
  Eq (α := ZMod N₀) ((castHom ⋯ (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀) ((↑a₀ : ZMod N₀) : ZMod N₀)
inr : d * a₀ % N = d * (↑u : ZMod N).val % N
⊢ a = (↑u : ZMod N) * (↑d : ZMod N)

Tactic:
rw [← natCast_zmod_val a, ← natCast_zmod_val u.1, ha₀, ← Nat.cast_mul,
    natCast_eq_natCast_iff, mul_comm _ d, Nat.ModEq]

Premises used: Units.val, ZMod.natCast_zmod_val, Nat.ModEq, Nat.cast_mul, mul_comm, ZMod.natCast_eq_natCast_iff
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)
u : (ZMod N)ˣ
hu :
  Eq (α := ZMod N₀) ((castHom ⋯ (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀) ((↑a₀ : ZMod N₀) : ZMod N₀)
inr : a₀ % N₀ = (↑u : ZMod N).val % N₀
⊢ d * a₀ % N = d * (↑u : ZMod N).val % N

Tactic:
simp only [hN₀, Nat.mul_mod_mul_left, Nat.mul_right_inj hd]

Premises used: Nat.mul_right_inj, Nat.mul_mod_mul_left
-- Module: Mathlib.Data.ZMod.Units
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit (M := ZMod N₀) (↑a₀ : ZMod N₀)
u : (ZMod N)ˣ
hu :
  Eq (α := ZMod N₀) ((castHom ⋯ (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀) ((↑a₀ : ZMod N₀) : ZMod N₀)
inr : a₀ ≡ (↑u : ZMod N).val [MOD N₀]
inr₁ : Eq (α := ZMod N₀) (↑a₀ : ZMod N₀) (↑(↑u : ZMod N).val : ZMod N₀)
inr₂ :
  Eq (α := ZMod N₀) ((castHom ⋯ (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀)
    ((↑(↑u : ZMod N).val : ZMod N₀) : ZMod N₀)
inr₃ :
  Eq (α := ZMod N₀) ((castHom ⋯ (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀)
    ((↑u : ZMod N).cast : ZMod N₀)
inr₄ inr₅ : Eq (α := ZMod N₀) (↑u : ZMod N).cast (↑u : ZMod N).cast
⊢ a₀ % N₀ = (↑u : ZMod N).val % N₀

Tactic:
rw [← Nat.ModEq, ← natCast_eq_natCast_iff, ← hu, natCast_val, castHom_apply]

Premises used: ZMod.castHom_apply, ZMod.natCast_val, Nat.ModEq, ZMod.natCast_eq_natCast_iff
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
pos : ∀ (hn : n = 0), HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
neg : ∀ (hn : ¬n = 0), HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1

Tactic:
by_cases hn : n = 0