awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
inr : HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑m : ZMod n)⁻¹ = 1
⊢ HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
have inr₁ : Eq (α := ZMod n) 1 1
Tactic: rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
⊢ HMul.hMul (α := ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) (↑m : ZMod n) = 1
have rw : HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
Tactic: rw [mul_comm, mul_val_inv hmn]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
rw : HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
⊢ HMul.hMul (α := ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) (↑m : ZMod n) = 1
have rw₁ : Eq (α := ZMod n) 1 1
Tactic: rw [mul_comm, mul_val_inv hmn]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n_1 n x : ℕ
h : x.Coprime n
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n)⁻¹ (↑x : ZMod n) = 1
have rw : HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
Tactic: rw [mul_comm, coe_mul_inv_eq_one x h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n_1 n x : ℕ
h : x.Coprime n
rw : HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n)⁻¹ (↑x : ZMod n) = 1
have rw₁ : Eq (α := ZMod n) 1 1
Tactic: rw [mul_comm, coe_mul_inv_eq_one x h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod n)ˣ
⊢ (↑u : ZMod n).val.Coprime n
have zero : ∀ (u : (ZMod 0)ˣ), (↑u : ZMod 0).val.Coprime 0
Tactic: rcases n with - | n
Cleared hypotheses: n, u
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod n)ˣ
zero : ∀ (u : (ZMod 0)ˣ), (↑u : ZMod 0).val.Coprime 0
⊢ (↑u : ZMod n).val.Coprime n
have succ : ∀ (n : ℕ) (u : (ZMod (n + 1))ˣ), (↑u : ZMod (n + 1)).val.Coprime (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n, u
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
u : (ZMod 0)ˣ
⊢ (↑u : ZMod 0).val.Coprime 0
have zero : (val (n := 0) (↑1 : ZMod 0)).Coprime 0
Tactic: rcases Int.units_eq_one_or u with (rfl | rfl)
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
u : (ZMod 0)ˣ
zero : (val (n := 0) (↑1 : ZMod 0)).Coprime 0
⊢ (↑u : ZMod 0).val.Coprime 0
have zero₁ : (val (n := 0) (↑(-1) : ZMod 0)).Coprime 0
Tactic: rcases Int.units_eq_one_or u with (rfl | rfl)
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u : ZMod (n + 1)).val.Coprime (n + 1)
have succ : (↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val ≡ 1 [MOD n + 1]
Tactic: apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val ≡ 1 [MOD n + 1]
have this : (↑(u * u⁻¹) : ZMod (n + 1)) = (↑1 : ZMod (n + 1))
Tactic: have := Units.ext_iff.1 (mul_inv_cancel u)
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
this : (↑(u * u⁻¹) : ZMod (n + 1)) = (↑1 : ZMod (n + 1))
⊢ (↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val ≡ 1 [MOD n + 1]
have this₁ : (↑(u * u⁻¹) : ZMod (n + 1)) = 1
Tactic: rw [Units.val_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
this : (↑(u * u⁻¹) : ZMod (n + 1)) = 1
⊢ (↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val ≡ 1 [MOD n + 1]
have succ : (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1)) = (↑(u * u⁻¹) : ZMod (n + 1))
Tactic: rw [← natCast_eq_natCast_iff, Nat.cast_one, ← this]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1)) = (↑(u * u⁻¹) : ZMod (n + 1))
have succ : Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
  (↑(↑(u * u⁻¹) : ZMod (n + 1)).val : ZMod (n + 1))
Tactic: rw [← natCast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
    (↑(↑(u * u⁻¹) : ZMod (n + 1)).val : ZMod (n + 1))
have succ : Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
  (↑((↑u : ZMod (n + 1)) * (↑u⁻¹ : ZMod (n + 1))).val : ZMod (n + 1))
Tactic: rw [Units.val_mul, val_mul, natCast_mod]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
succ :
  Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
    (↑((↑u : ZMod (n + 1)) * (↑u⁻¹ : ZMod (n + 1))).val : ZMod (n + 1))
⊢ Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
    (↑(↑(u * u⁻¹) : ZMod (n + 1)).val : ZMod (n + 1))
have succ₁ : Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
  (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val % (n + 1)) : ZMod (n + 1))
Tactic: rw [Units.val_mul, val_mul, natCast_mod]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
succ :
  Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
    (↑((↑u : ZMod (n + 1)) * (↑u⁻¹ : ZMod (n + 1))).val : ZMod (n + 1))
succ₁ :
  Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
    (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val % (n + 1)) : ZMod (n + 1))
⊢ Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
    (↑(↑(u * u⁻¹) : ZMod (n + 1)).val : ZMod (n + 1))
have succ₂ : Eq (α := ZMod (n + 1)) (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
  (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1))
Tactic: rw [Units.val_mul, val_mul, natCast_mod]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
⊢ IsUnit (M := ZMod n) (↑m : ZMod n) ↔ m.Coprime n
have refine : ∀ (H : IsUnit (M := ZMod n) (↑m : ZMod n)), m.Coprime n
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ (unitOfCoprime m H).isUnit⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
m n : ℕ
H : IsUnit (M := ZMod n) (↑m : ZMod n)
⊢ m.Coprime n
have H' : (↑H.unit : ZMod n).val.Coprime n
Tactic: have H' := val_coe_unit_coprime H.unit
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
m n : ℕ
H : IsUnit (M := ZMod n) (↑m : ZMod n)
H' : (↑H.unit : ZMod n).val.Coprime n
⊢ m.Coprime n
have H'₁ : (m % n).gcd n = 1
Tactic: rw [IsUnit.unit_spec, val_natCast, Nat.coprime_iff_gcd_eq_one] at H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
H : IsUnit (M := ZMod n) (↑m : ZMod n)
H' : (m % n).gcd n = 1
⊢ m.Coprime n
have rw : n.gcd m = (m % n).gcd n
Tactic: rw [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm, ← H']
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
⊢ (m % n).Coprime n ↔ m.Coprime n
have suffices : (m % n).gcd n = m.gcd n
Tactic: suffices (m % n).gcd n = m.gcd n by grind
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n p : ℕ
hp : Nat.Prime p
⊢ IsUnit (M := ZMod n) (↑p : ZMod n) ↔ ¬p ∣ n
have rw : p.Coprime n ↔ ¬p ∣ n
Tactic: rw [isUnit_iff_coprime, Nat.Prime.coprime_iff_not_dvd hp]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n p : ℕ
hp : Nat.Prime p
rw : p.Coprime n ↔ ¬p ∣ n
⊢ IsUnit (M := ZMod n) (↑p : ZMod n) ↔ ¬p ∣ n
have rw₁ : ¬p ∣ n ↔ ¬p ∣ n
Tactic: rw [isUnit_iff_coprime, Nat.Prime.coprime_iff_not_dvd hp]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p d a : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ IsUnit (M := ZMod (p ^ d)) (↑a : ZMod (p ^ d)) ↔ ¬p ∣ a
have rw : a.Coprime (p ^ d) ↔ ¬p ∣ a
Tactic: rw [isUnit_iff_coprime, Nat.coprime_pow_right_iff hd, Nat.coprime_comm,
    hp.coprime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p d a : ℕ
hp : Nat.Prime p
hd : 0 < d
rw : a.Coprime (p ^ d) ↔ ¬p ∣ a
⊢ IsUnit (M := ZMod (p ^ d)) (↑a : ZMod (p ^ d)) ↔ ¬p ∣ a
have rw₁ : a.Coprime p ↔ ¬p ∣ a
Tactic: rw [isUnit_iff_coprime, Nat.coprime_pow_right_iff hd, Nat.coprime_comm,
    hp.coprime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p d a : ℕ
hp : Nat.Prime p
hd : 0 < d
rw : a.Coprime (p ^ d) ↔ ¬p ∣ a
rw₁ : a.Coprime p ↔ ¬p ∣ a
⊢ IsUnit (M := ZMod (p ^ d)) (↑a : ZMod (p ^ d)) ↔ ¬p ∣ a
have rw₂ : p.Coprime a ↔ ¬p ∣ a
Tactic: rw [isUnit_iff_coprime, Nat.coprime_pow_right_iff hd, Nat.coprime_comm,
    hp.coprime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p d a : ℕ
hp : Nat.Prime p
hd : 0 < d
rw : a.Coprime (p ^ d) ↔ ¬p ∣ a
rw₁ : a.Coprime p ↔ ¬p ∣ a
rw₂ : p.Coprime a ↔ ¬p ∣ a
⊢ IsUnit (M := ZMod (p ^ d)) (↑a : ZMod (p ^ d)) ↔ ¬p ∣ a
have rw₃ : ¬p ∣ a ↔ ¬p ∣ a
Tactic: rw [isUnit_iff_coprime, Nat.coprime_pow_right_iff hd, Nat.coprime_comm,
    hp.coprime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
p d : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ ¬IsUnit (M := ZMod (p ^ d)) (↑p : ZMod (p ^ d))
have simp : d = 0 → p = 1
Tactic: simp [isUnit_prime_iff_not_dvd hp]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
u : (ZMod n)ˣ
⊢ (↑u : ZMod n)⁻¹ = (↑u⁻¹ : ZMod n)
have this : Eq (α := ZMod n) (↑((↑u : ZMod n).val.gcd n) : ZMod n) (↑1 : ZMod n)
Tactic: have := congr_arg ((↑) : ℕ → ZMod n) (val_coe_unit_coprime u)
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
u : (ZMod n)ˣ
this : Eq (α := ZMod n) (↑((↑u : ZMod n).val.gcd n) : ZMod n) (↑1 : ZMod n)
⊢ (↑u : ZMod n)⁻¹ = (↑u⁻¹ : ZMod n)
have this₁ : (↑u : ZMod n) * (↑u : ZMod n)⁻¹ = 1
Tactic: rw [← mul_inv_eq_gcd, Nat.cast_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
h : IsUnit a
⊢ a * a⁻¹ = 1
have rcases : ∀ (u : (ZMod n)ˣ), (↑u : ZMod n) * (↑u : ZMod n)⁻¹ = 1
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod n)ˣ
⊢ (↑u : ZMod n) * (↑u : ZMod n)⁻¹ = 1
have rw : (↑u : ZMod n) * (↑u⁻¹ : ZMod n) = 1
Tactic: rw [inv_coe_unit, u.mul_inv]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
u : (ZMod n)ˣ
rw : (↑u : ZMod n) * (↑u⁻¹ : ZMod n) = 1
⊢ (↑u : ZMod n) * (↑u : ZMod n)⁻¹ = 1
have rw₁ : Eq (α := ZMod n) 1 1
Tactic: rw [inv_coe_unit, u.mul_inv]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
h : IsUnit a
⊢ a⁻¹ * a = 1
have rw : a * a⁻¹ = 1
Tactic: rw [mul_comm, mul_inv_of_unit a h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
h : IsUnit a
rw : a * a⁻¹ = 1
⊢ a⁻¹ * a = 1
have rw₁ : Eq (α := ZMod n) 1 1
Tactic: rw [mul_comm, mul_inv_of_unit a h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
⊢ a⁻¹ * b = 1 ↔ a = b
have refine : ∀ (H : a⁻¹ * b = 1), a = b
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ H ▸ a.inv_mul_of_unit ha⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a⁻¹ * b = 1
⊢ a = b
have H₁ : a * (a⁻¹ * b) = a * 1
Tactic: apply_fun (a * ·) at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a * (a⁻¹ * b) = a * 1
⊢ a = b
have rwa : ∀ (H : a * a⁻¹ * b = a * 1), a = b
Tactic: rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a * (a⁻¹ * b) = a * 1
rwa : ∀ (H : a * a⁻¹ * b = a * 1), a = b
⊢ a = b
have rwa₁ : ∀ (H : 1 * b = a * 1), a = b
Tactic: rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a * (a⁻¹ * b) = a * 1
rwa : ∀ (H : a * a⁻¹ * b = a * 1), a = b
rwa₁ : ∀ (H : 1 * b = a * 1), a = b
⊢ a = b
have rwa₂ : ∀ (H : b = a * 1), a = b
Tactic: rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a * (a⁻¹ * b) = a * 1
rwa : ∀ (H : a * a⁻¹ * b = a * 1), a = b
rwa₁ : ∀ (H : 1 * b = a * 1), a = b
rwa₂ : ∀ (H : b = a * 1), a = b
⊢ a = b
have rwa₃ : ∀ (H : b = a), a = b
Tactic: rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a * (a⁻¹ * b) = a * 1
rwa : ∀ (H : a * a⁻¹ * b = a * 1), a = b
rwa₁ : ∀ (H : 1 * b = a * 1), a = b
rwa₂ : ∀ (H : b = a * 1), a = b
rwa₃ : ∀ (H : b = a), a = b
⊢ a = b
have rwa₄ : ∀ (H : a = b), a = b
Tactic: rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : m * n = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have inl : ∀ (h : Nat.Coprime 0 1),
  let to_fun : ZMod (HMul.hMul (α := ℕ) 0 1) → ZMod 0 × ZMod 1 :=
    (⇑(castHom sorry (ZMod 0 × ZMod 1)) : (a : ZMod (0 * 1)) → ZMod 0 × ZMod 1);
  let inv_fun : ZMod 0 × ZMod 1 → ZMod (HMul.hMul (α := ℕ) 0 1) := fun (x : ZMod 0 × ZMod 1) ↦
    if HMul.hMul (α := ℕ) 0 1 = 0 then
      if Eq (α := ℕ) 0 1 then cast (n := 1) ((RingHom.snd (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 1) x)
      else cast (n := 0) ((RingHom.fst (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 0) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (0 * 1));
  ∀ (hmn0 : HMul.hMul (α := ℕ) 0 1 = 0), LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
Tactic: rcases h.eq_of_mul_eq_zero hmn0 with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
Cleared hypotheses: m, n, h, to_fun, inv_fun, hmn0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : m * n = 0
inl :
  ∀ (h : Nat.Coprime 0 1),
    let to_fun : ZMod (HMul.hMul (α := ℕ) 0 1) → ZMod 0 × ZMod 1 :=
      (⇑(castHom ⋯ (ZMod 0 × ZMod 1)) : (a : ZMod (0 * 1)) → ZMod 0 × ZMod 1);
    let inv_fun : ZMod 0 × ZMod 1 → ZMod (HMul.hMul (α := ℕ) 0 1) := fun (x : ZMod 0 × ZMod 1) ↦
      if HMul.hMul (α := ℕ) 0 1 = 0 then
        if Eq (α := ℕ) 0 1 then cast (n := 1) ((RingHom.snd (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 1) x)
        else cast (n := 0) ((RingHom.fst (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 0) x)
      else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (0 * 1));
    ∀ (hmn0 : HMul.hMul (α := ℕ) 0 1 = 0), LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have inr : ∀ (h : Nat.Coprime 1 0),
  let to_fun : ZMod (HMul.hMul (α := ℕ) 1 0) → ZMod 1 × ZMod 0 :=
    (⇑(castHom sorry (ZMod 1 × ZMod 0)) : (a : ZMod (1 * 0)) → ZMod 1 × ZMod 0);
  let inv_fun : ZMod 1 × ZMod 0 → ZMod (HMul.hMul (α := ℕ) 1 0) := fun (x : ZMod 1 × ZMod 0) ↦
    if HMul.hMul (α := ℕ) 1 0 = 0 then
      if Eq (α := ℕ) 1 1 then cast (n := 0) ((RingHom.snd (ZMod 1) (ZMod 0) : (a : ZMod 1 × ZMod 0) → ZMod 0) x)
      else cast (n := 1) ((RingHom.fst (ZMod 1) (ZMod 0) : (a : ZMod 1 × ZMod 0) → ZMod 1) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (1 * 0));
  ∀ (hmn0 : HMul.hMul (α := ℕ) 1 0 = 0), LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
Tactic: rcases h.eq_of_mul_eq_zero hmn0 with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
Cleared hypotheses: m, n, h, to_fun, inv_fun, hmn0
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (HMul.hMul (α := ℕ) 0 1) → ZMod 0 × ZMod 1 :=
  (⇑(castHom ⋯ (ZMod 0 × ZMod 1)) : (a : ZMod (0 * 1)) → ZMod 0 × ZMod 1)
inv_fun : ZMod 0 × ZMod 1 → ZMod (HMul.hMul (α := ℕ) 0 1) :=
  fun (x : ZMod 0 × ZMod 1) ↦
    if HMul.hMul (α := ℕ) 0 1 = 0 then
      if Eq (α := ℕ) 0 1 then cast (n := 1) ((RingHom.snd (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 1) x)
      else cast (n := 0) ((RingHom.fst (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 0) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (0 * 1))
hmn0 : HMul.hMul (α := ℕ) 0 1 = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have inl : LeftInverse inv_fun to_fun
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (HMul.hMul (α := ℕ) 0 1) → ZMod 0 × ZMod 1 :=
  (⇑(castHom ⋯ (ZMod 0 × ZMod 1)) : (a : ZMod (0 * 1)) → ZMod 0 × ZMod 1)
inv_fun : ZMod 0 × ZMod 1 → ZMod (HMul.hMul (α := ℕ) 0 1) :=
  fun (x : ZMod 0 × ZMod 1) ↦
    if HMul.hMul (α := ℕ) 0 1 = 0 then
      if Eq (α := ℕ) 0 1 then cast (n := 1) ((RingHom.snd (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 1) x)
      else cast (n := 0) ((RingHom.fst (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 0) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (0 * 1))
hmn0 : HMul.hMul (α := ℕ) 0 1 = 0
inl : LeftInverse inv_fun to_fun
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have inl₁ : RightInverse inv_fun to_fun
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (HMul.hMul (α := ℕ) 0 1) → ZMod 0 × ZMod 1 :=
  (⇑(castHom ⋯ (ZMod 0 × ZMod 1)) : (a : ZMod (0 * 1)) → ZMod 0 × ZMod 1)
inv_fun : ZMod 0 × ZMod 1 → ZMod (HMul.hMul (α := ℕ) 0 1) :=
  fun (x : ZMod 0 × ZMod 1) ↦
    if HMul.hMul (α := ℕ) 0 1 = 0 then
      if Eq (α := ℕ) 0 1 then cast (n := 1) ((RingHom.snd (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 1) x)
      else cast (n := 0) ((RingHom.fst (ZMod 0) (ZMod 1) : (a : ZMod 0 × ZMod 1) → ZMod 0) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (0 * 1))
hmn0 : HMul.hMul (α := ℕ) 0 1 = 0
x : ZMod 0
y : ZMod 1
⊢ to_fun (inv_fun (x, y)) = (x, y)
have inl : to_fun (inv_fun (x, (fun (i : Fin (0 + 1)) ↦ i) (⟨0, sorry⟩ : Fin (0 + 1)))) = (x, (fun (i : Fin (0 + 1)) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (HMul.hMul (α := ℕ) 1 0) → ZMod 1 × ZMod 0 :=
  (⇑(castHom ⋯ (ZMod 1 × ZMod 0)) : (a : ZMod (1 * 0)) → ZMod 1 × ZMod 0)
inv_fun : ZMod 1 × ZMod 0 → ZMod (HMul.hMul (α := ℕ) 1 0) :=
  fun (x : ZMod 1 × ZMod 0) ↦
    if HMul.hMul (α := ℕ) 1 0 = 0 then
      if Eq (α := ℕ) 1 1 then cast (n := 0) ((RingHom.snd (ZMod 1) (ZMod 0) : (a : ZMod 1 × ZMod 0) → ZMod 0) x)
      else cast (n := 1) ((RingHom.fst (ZMod 1) (ZMod 0) : (a : ZMod 1 × ZMod 0) → ZMod 1) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (1 * 0))
hmn0 : HMul.hMul (α := ℕ) 1 0 = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have inr : LeftInverse inv_fun to_fun
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (HMul.hMul (α := ℕ) 1 0) → ZMod 1 × ZMod 0 :=
  (⇑(castHom ⋯ (ZMod 1 × ZMod 0)) : (a : ZMod (1 * 0)) → ZMod 1 × ZMod 0)
inv_fun : ZMod 1 × ZMod 0 → ZMod (HMul.hMul (α := ℕ) 1 0) :=
  fun (x : ZMod 1 × ZMod 0) ↦
    if HMul.hMul (α := ℕ) 1 0 = 0 then
      if Eq (α := ℕ) 1 1 then cast (n := 0) ((RingHom.snd (ZMod 1) (ZMod 0) : (a : ZMod 1 × ZMod 0) → ZMod 0) x)
      else cast (n := 1) ((RingHom.fst (ZMod 1) (ZMod 0) : (a : ZMod 1 × ZMod 0) → ZMod 1) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (1 * 0))
hmn0 : HMul.hMul (α := ℕ) 1 0 = 0
inr : LeftInverse inv_fun to_fun
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have inr₁ : RightInverse inv_fun to_fun
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (goal)
Goal:
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (HMul.hMul (α := ℕ) 1 0) → ZMod 1 × ZMod 0 :=
  (⇑(castHom ⋯ (ZMod 1 × ZMod 0)) : (a : ZMod (1 * 0)) → ZMod 1 × ZMod 0)
inv_fun : ZMod 1 × ZMod 0 → ZMod (HMul.hMul (α := ℕ) 1 0) :=
  fun (x : ZMod 1 × ZMod 0) ↦
    if HMul.hMul (α := ℕ) 1 0 = 0 then
      if Eq (α := ℕ) 1 1 then cast (n := 0) ((RingHom.snd (ZMod 1) (ZMod 0) : (a : ZMod 1 × ZMod 0) → ZMod 0) x)
      else cast (n := 1) ((RingHom.fst (ZMod 1) (ZMod 0) : (a : ZMod 1 × ZMod 0) → ZMod 1) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (1 * 0))
hmn0 : HMul.hMul (α := ℕ) 1 0 = 0
x : ZMod 1
y : ZMod 0
⊢ to_fun (inv_fun (x, y)) = (x, y)
have inr : to_fun (inv_fun ((fun (i : Fin (0 + 1)) ↦ i) (⟨0, sorry⟩ : Fin (0 + 1)), y)) = ((fun (i : Fin (0 + 1)) ↦ i) ⟨0, sorry⟩, y)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have this : NeZero (m * n)
Tactic: haveI : NeZero (m * n) := ⟨hmn0⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have this₁ : NeZero m
Tactic: haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Basic (hypothesis)
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := (⇑(castHom ⋯ (ZMod m × ZMod n)) : (a : ZMod (m * n)) → ZMod m × ZMod n)
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun (x : ZMod m × ZMod n) ↦
    if m * n = 0 then
      if m = 1 then cast (n := n) ((RingHom.snd (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod n) x)
      else cast (n := m) ((RingHom.fst (ZMod m) (ZMod n) : (a : ZMod m × ZMod n) → ZMod m) x)
    else (↑(↑(Nat.chineseRemainder h x.1.val x.2.val) : ℕ) : ZMod (m * n))
hmn0 : ¬m * n = 0
this_1 : NeZero (m * n)
this : NeZero m
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
have this₁ : NeZero n
Tactic: haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩