awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
g : G
inst_1 : Finite.{u_3 + 1} (G ⧸ H)
inst_2 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H)
⊢ H.index = ∑ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out
have have : ∀
  (this :
    (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype (↑(orbit (↥(zpowers g)) q.out) : Type u_3)),
  H.index = ∑ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out
Tactic: have (q : Quotient (MulAction.orbitRel (zpowers g) (G ⧸ H))) :
      Fintype (MulAction.orbit (zpowers g) q.out) := Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
g : G
inst_1 : Finite.{u_3 + 1} (G ⧸ H)
inst_2 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this_1 : Fintype (G ⧸ H)
this :
  (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype (↑(orbit (↥(zpowers g)) q.out) : Type u_3)
⊢ H.index = ∑ q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), minimalPeriod (fun (x : G ⧸ H) ↦ g • x) q.out
have simp : Fintype.card.{u_3} (G ⧸ H) =
  ∑ x : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), Fintype.card.{u_3} (↑(orbit (↥(zpowers g)) x.out) : Type u_3)
Tactic: simp only [MulAction.minimalPeriod_eq_card, index_eq_card, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientGroup (goal)
Goal:
G : Type u_3
inst : Group G
H : Subgroup G
g : G
inst_1 : Finite.{u_3 + 1} (G ⧸ H)
inst_2 : Fintype (Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H)))
this_1 : Fintype (G ⧸ H)
this :
  (q : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) → Fintype (↑(orbit (↥(zpowers g)) q.out) : Type u_3)
⊢ Fintype.card.{u_3} (G ⧸ H) =
    ∑ x : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)), Fintype.card.{u_3} (↑(orbit (↥(zpowers g)) x.out) : Type u_3)
have rw : Fintype.card.{u_3} (G ⧸ H) =
  Fintype.card.{u_3}
    ((x : Quotient (α := G ⧸ H) (orbitRel (↥(zpowers g)) (G ⧸ H))) × (↑(orbit (↥(zpowers g)) x.out) : Type u_3))
Tactic: rw [← Fintype.card_sigma]
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientRing (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ →+* HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
    (@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
      (↑(quotientSpanNatEquivZMod n).symm : ZMod n →+* ℤ ⧸ Ideal.span {(↑n : ℤ)}) (castRingHom (ZMod n)))
    (Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)}))
have a : ∀ (x : ℤ),
  Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
    ((@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
            (↑(quotientSpanNatEquivZMod n).symm : ZMod n →+* ℤ ⧸ Ideal.span {(↑n : ℤ)}) (castRingHom (ZMod n)) :
          (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)})
        x :
      HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑n : ℤ)}) : (a : ℤ) → ℤ ⧸ Ideal.span {(↑n : ℤ)}) x :
      HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {(↑n : ℤ)}))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.ZMod.QuotientRing (goal)
Goal:
n : ℤ
⊢ Eq (α := ℤ →+* HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
    (@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
      (↑n.quotientSpanEquivZMod.symm : ZMod n.natAbs →+* ℤ ⧸ Ideal.span {n}) (castRingHom (ZMod n.natAbs)))
    (Ideal.Quotient.mk (Ideal.span {n}))
have a : ∀ (x : ℤ),
  Eq (α := HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
    ((@RingHom.comp _ _ _ _ NonAssocRing.toNonAssocSemiring _
            (↑n.quotientSpanEquivZMod.symm : ZMod n.natAbs →+* ℤ ⧸ Ideal.span {n}) (castRingHom (ZMod n.natAbs)) :
          (a : ℤ) → ℤ ⧸ Ideal.span {n})
        x :
      HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
    ((Ideal.Quotient.mk (Ideal.span {n}) : (a : ℤ) → ℤ ⧸ Ideal.span {n}) x :
      HasQuotient.Quotient ℤ (B := Ideal ℤ) (Ideal.span {n}))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ 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))
have 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 sorry (ZMod n)) : ZMod d →* ZMod n))
Tactic: rw [← Units.map_comp]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
this : ∀ (x : ℕ), x.Coprime n → ∃ (k : ℕ), (x + k * n).Coprime m
x : (ZMod n)ˣ
⊢ ∃ (a : (ZMod m)ˣ), (unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) a = x
have have : ∀ (k : ℕ) (hk : ((↑x : ZMod n).val + k * n).Coprime m),
  ∃ (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)
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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
have refine : (↑((unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) (unitOfCoprime ((↑x : ZMod n).val + k * n) hk)) : ZMod n) = (↑x : ZMod n)
Tactic: refine ⟨unitOfCoprime _ hk, Units.ext ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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
⊢ (↑((unitsMap h : (a : (ZMod m)ˣ) → (ZMod n)ˣ) (unitOfCoprime ((↑x : ZMod n).val + k * n) hk)) : ZMod n) =
    (↑x : ZMod n)
have this₁ : NeZero n
Tactic: have : NeZero n := ⟨fun hn ↦ hm.out (eq_zero_of_zero_dvd (hn ▸ h))⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
⊢ Function.Surjective (α := (ZMod m)ˣ) (β := (ZMod n)ˣ) (⇑(unitsMap h) : (a : (ZMod m)ˣ) → (ZMod n)ˣ)
have suffices : ∀ (x : ℕ), x.Coprime n → ∃ (k : ℕ), (x + k * n).Coprime m
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]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
⊢ ∃ (k : ℕ), (x + k * n).Coprime m
have h₁ : (x + ps.prod id * n).Coprime m
Tactic: use ps.prod id
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
⊢ (x + ps.prod id * n).Coprime m
have h₁ : ∀ (k : ℕ), Nat.Prime k → k ∣ x + ps.prod id * n → ¬k ∣ m
Tactic: apply Nat.coprime_of_dvd
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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
⊢ False
have pos : ∀ (hpx : p ∣ x), False
Tactic: by_cases hpx : p ∣ x
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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
⊢ False
have neg : ∀ (hpx : ¬p ∣ x), False
Tactic: by_cases hpx : p ∣ x
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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
⊢ False
have h₁ : p ∣ x + ps.prod id * n - x
Tactic: have h := Nat.dvd_sub hp hpx
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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
⊢ False
have h₁ : p ∣ ps.prod id * n
Tactic: rw [add_comm, Nat.add_sub_cancel] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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
⊢ False
have pos : ∀ (h : p ∣ ps.prod id), False
Tactic: rcases pp.dvd_mul.mp h with h | h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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
⊢ False
have pos₁ : ∀ (h : p ∣ n), False
Tactic: rcases pp.dvd_mul.mp h with h | h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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
⊢ False
have pos : ∀ (q : ℕ) (hq : q ∈ ps) (hq' : p ∣ id q), False
Tactic: have ⟨q, hq, hq'⟩ := (pp.prime.dvd_finsetProd_iff id).mp h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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
⊢ False
have hq₁ : (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
Cleared hypotheses: hq, hq'
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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
⊢ False
have pps : p ∈ ps
Tactic: have pps : p ∈ ps := Finset.mem_filter.mpr ⟨Nat.mem_primeFactors.mpr ⟨pp, hpn, hm.out⟩, hpx⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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
⊢ False
have h₁ : 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)
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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
⊢ False
have h₁ : p ∣ x
Tactic: rw [Nat.add_sub_cancel] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n p : ℕ
h : p ∈ n.primeFactors
⊢ ¬IsUnit (M := ZMod n) (↑p : ZMod n)
have rw : ¬p.Coprime n
Tactic: rw [isUnit_iff_coprime]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
N : ℕ
a : ZMod N
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
have inl : ∀ (a : ZMod 0), ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
Tactic: rcases eq_or_ne N 0 with rfl | hN
Cleared hypotheses: N, a
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
N : ℕ
a : ZMod N
inl : ∀ (a : ZMod 0), ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
have inr : ∀ (hN : N ≠ 0), ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
Tactic: rcases eq_or_ne N 0 with rfl | hN
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
a : ZMod 0
⊢ ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
have inl : ∀ (a : ℤ), ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
Tactic: change ℤ at a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
a : ℤ
⊢ ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
have inl : ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ 0 = u * (↑d : ZMod 0)
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
a : ℤ
inl : ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ 0 = u * (↑d : ZMod 0)
⊢ ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
have inl₁ : ∀ (ha : a ≠ 0), ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
Tactic: rcases eq_or_ne a 0 with rfl | ha
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
⊢ 0 = HMul.hMul (α := ZMod 0) 1 (↑0 : ZMod 0)
have rw : 0 = HMul.hMul (α := ZMod 0) 1 0
Tactic: rw [Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
rw : 0 = HMul.hMul (α := ZMod 0) 1 0
⊢ 0 = HMul.hMul (α := ZMod 0) 1 (↑0 : ZMod 0)
have rw₁ : Eq (α := ZMod 0) 0 0
Tactic: rw [Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
a : ℤ
ha : a ≠ 0
⊢ ∃ (d : ℕ), d ∣ 0 ∧ ∃ (u : ZMod 0), IsUnit u ∧ a = u * (↑d : ZMod 0)
have inl : IsUnit a.sign
Tactic: refine ⟨a.natAbs, dvd_zero _, Int.sign a, ?_, (Int.sign_mul_natAbs a).symm⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
a : ℤ
ha : a ≠ 0
⊢ IsUnit a.sign
have inl : ∀ (h : a < 0), IsUnit a.sign
Tactic: rcases lt_or_gt_of_ne ha with h | h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
a : ℤ
ha : a ≠ 0
inl : ∀ (h : a < 0), IsUnit a.sign
⊢ IsUnit a.sign
have inl₁ : ∀ (h : 0 < a), IsUnit a.sign
Tactic: rcases lt_or_gt_of_ne ha with h | h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
have this : NeZero N
Tactic: have : NeZero N := ⟨hN⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
have hd : d ≠ 0
Tactic: have hd : d ≠ 0 := Nat.gcd_ne_zero_right hN
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
have inr : ∀ (a₀ : ℕ) (ha₀ : a.val = d * a₀), ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
Tactic: obtain ⟨a₀, (ha₀ : _ = d * _)⟩ := a.val.gcd_dvd_left N
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀
⊢ ∃ (d : ℕ), d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
have inr : ∀ (N₀ : ℕ) (hN₀ : N = d * 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
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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)
have inr : ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
Tactic: refine ⟨d, ⟨N₀, hN₀⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀)
have refine : IsCoprime (R := ℤ) (↑a₀ : ℤ) (↑N₀ : ℤ)
Tactic: refine (isUnit_iff_coprime _ _).mpr (Nat.isCoprime_iff_coprime.mp ?_)
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀
⊢ IsCoprime (R := ℤ) (↑a₀ : ℤ) (↑N₀ : ℤ)
have obtain : ∀ (p q : ℤ) (hpq : (↑d : ℤ) = (↑a.val : ℤ) * p + (↑N : ℤ) * q), IsCoprime (R := ℤ) (↑a₀ : ℤ) (↑N₀ : ℤ)
Tactic: obtain ⟨p, q, hpq⟩ : ∃ (p q : ℤ), d = a.val * p + N * q := ⟨_, _, Nat.gcd_eq_gcd_ab _ _⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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
⊢ IsCoprime (R := ℤ) (↑a₀ : ℤ) (↑N₀ : ℤ)
have hpq₁ : (↑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
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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₀
⊢ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
have hu₀ : 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⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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), IsUnit u ∧ a = u * (↑d : ZMod N)
have inr : ∀ (u : (ZMod N)ˣ) (hu : (unitsMap sorry : (a : (ZMod N)ˣ) → (ZMod N₀)ˣ) u = hu₀.unit),
  ∃ (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
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
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
⊢ ∃ (u : ZMod N), IsUnit u ∧ a = u * (↑d : ZMod N)
have hu₁ : Eq (α := ZMod N₀) ((castHom sorry (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
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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)
have inr : a = (↑u : ZMod N) * (↑d : ZMod N)
Tactic: refine ⟨u.val, u.isUnit, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀)
⊢ a = (↑u : ZMod N) * (↑d : ZMod N)
have inr : d * a₀ % N = d * (↑u : ZMod N).val % 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]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀)
⊢ d * a₀ % N = d * (↑u : ZMod N).val % N
have inr : a₀ % N₀ = (↑u : ZMod N).val % N₀
Tactic: simp only [hN₀, Nat.mul_mod_mul_left, Nat.mul_right_inj hd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀)
⊢ a₀ % N₀ = (↑u : ZMod N).val % N₀
have inr : a₀ ≡ (↑u : ZMod N).val [MOD N₀]
Tactic: rw [← Nat.ModEq, ← natCast_eq_natCast_iff, ← hu, natCast_val, castHom_apply]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀]
⊢ a₀ % N₀ = (↑u : ZMod N).val % N₀
have inr₁ : Eq (α := ZMod N₀) (↑a₀ : ZMod N₀) (↑(↑u : ZMod N).val : ZMod N₀)
Tactic: rw [← Nat.ModEq, ← natCast_eq_natCast_iff, ← hu, natCast_val, castHom_apply]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀)
⊢ a₀ % N₀ = (↑u : ZMod N).val % N₀
have inr₂ : Eq (α := ZMod N₀) ((castHom sorry (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀)
  ((↑(↑u : ZMod N).val : ZMod N₀) : ZMod N₀)
Tactic: rw [← Nat.ModEq, ← natCast_eq_natCast_iff, ← hu, natCast_val, castHom_apply]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀)
⊢ a₀ % N₀ = (↑u : ZMod N).val % N₀
have inr₃ : Eq (α := ZMod N₀) ((castHom sorry (ZMod N₀) : (a : ZMod N) → ZMod N₀) (↑u : ZMod N) : ZMod N₀)
  ((↑u : ZMod N).cast : ZMod N₀)
Tactic: rw [← Nat.ModEq, ← natCast_eq_natCast_iff, ← hu, natCast_val, castHom_apply]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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₀)
⊢ a₀ % N₀ = (↑u : ZMod N).val % N₀
have inr₄ : Eq (α := ZMod N₀) (↑u : ZMod N).cast (↑u : ZMod N).cast
Tactic: rw [← Nat.ModEq, ← natCast_eq_natCast_iff, ← hu, natCast_val, castHom_apply]