awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ Eq (α := ZMod 1) 1⁻¹ 1

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ Eq (α := ZMod 1) 1⁻¹ 1

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
hn : n ≠ 1
⊢ Eq (α := ZMod n) 1⁻¹ 1

Tactic:
simpa [ZMod.val_one'' hn] using mul_inv_eq_gcd (1 : ZMod n)

Premises used: ZMod.val_one'', ZMod.mul_inv_eq_gcd, OfNat.ofNat
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a n : ℕ
⊢ Eq (α := ZMod n) (↑(a % n) : ZMod n) (↑a : ZMod n)

Tactic:
(CharP.cast_eq_mod (ZMod n) n a).symm

Premises used: CharP.cast_eq_mod, ZMod, Eq.symm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℤ
⊢ Eq (α := ZMod 2) (↑n : ZMod 2) 0 ↔ Even n

Tactic:
(CharP.intCast_eq_zero_iff (ZMod 2) 2 n).trans even_iff_two_dvd.symm

Premises used: ZMod, Iff.trans, even_iff_two_dvd, OfNat.ofNat, Iff.symm, CharP.intCast_eq_zero_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Eq (α := ZMod 2) (↑n : ZMod 2) 0 ↔ Even n

Tactic:
mod_cast intCast_eq_zero_iff_even (n := n)

Premises used: Int.cast, Int.cast_natCast, congrArg, Int.cast_zero, cast, Nat.cast, Int.even_coe_nat._simp_1, ZMod.intCast_eq_zero_iff_even, Iff, congr, Even, congrFun', Nat.cast_zero, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℤ
rw : n % (↑2 : ℤ) = HMod.hMod (α := ℤ) 1 (↑2 : ℤ) ↔ n % 2 = 1
⊢ Eq (α := ZMod 2) (↑n : ZMod 2) 1 ↔ Odd n

Tactic:
rw [← Int.cast_one, ZMod.intCast_eq_intCast_iff, Int.odd_iff, Int.ModEq]

Premises used: Int.odd_iff, ZMod.intCast_eq_intCast_iff, Int.ModEq, Int.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℤ
⊢ n % (↑2 : ℤ) = HMod.hMod (α := ℤ) 1 (↑2 : ℤ) ↔ n % 2 = 1

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Eq (α := ZMod 2) (↑n : ZMod 2) 1 ↔ Odd n

Tactic:
mod_cast intCast_eq_one_iff_odd (n := n)

Premises used: Int.cast, Int.cast_natCast, congrArg, Odd, cast, Nat.cast, Int.odd_coe_nat._simp_1, Iff, ZMod.intCast_eq_one_iff_odd, congr, congrFun', Eq.symm, Eq, Nat.cast_one, Int.cast_one, Eq.trans
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Ne (α := ZMod 2) (↑n : ZMod 2) 0 ↔ Odd n

Tactic:
simp [natCast_eq_zero_iff_even]

Premises used: ZMod.natCast_eq_zero_iff_even
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n x : ℕ
h : x.Coprime n
⊢ (x % n).gcd n = 1

Tactic:
rw [Nat.Coprime, Nat.gcd_comm, Nat.gcd_rec] at h

Premises used: Nat.Coprime, Nat.gcd_rec, Nat.gcd_comm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n x : ℕ
h : (x % n).gcd n = 1
rw : Eq (α := ZMod n) (↑((val (n := n) (↑x : ZMod n)).gcd n) : ZMod n) 1
rw₁ : Eq (α := ZMod n) (↑((x % n).gcd n) : ZMod n) 1
rw₂ : Eq (α := ZMod n) (↑1 : ZMod n) 1
rw₃ rw₄ : Eq (α := ZMod n) 1 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1

Tactic:
rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]

Premises used: ZMod.val_natCast, ZMod.mul_inv_eq_gcd, Nat.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
hmn : m.Coprime n
inl : ∀ (hmn : m.Coprime 0), HMul.hMul (α := ZMod 0) (↑m : ZMod 0) (↑(val (n := 0) (↑m : ZMod 0)⁻¹) : ZMod 0) = 1
inr : ∀ (hn : n ≠ 0), HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
⊢ HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m : ℕ
hmn : m.Coprime 0
⊢ HMul.hMul (α := ZMod 0) (↑m : ZMod 0) (↑(val (n := 0) (↑m : ZMod 0)⁻¹) : ZMod 0) = 1

Tactic:
simp [m.coprime_zero_right.1 hmn]

Premises used: Nat.coprime_zero_right, Iff.mp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
⊢ NeZero n

Tactic:
haveI : NeZero n := ⟨hn⟩
-- Module: Mathlib.Data.ZMod.Basic
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
inr₁ inr₂ : Eq (α := ZMod n) 1 1
⊢ HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1

Tactic:
rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]

Premises used: ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
hmn : m.Coprime n
rw : HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
rw₁ rw₂ : Eq (α := ZMod n) 1 1
⊢ HMul.hMul (α := ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) (↑m : ZMod n) = 1

Tactic:
rw [mul_comm, mul_val_inv hmn]

Premises used: ZMod.mul_val_inv, mul_comm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n_1 n x : ℕ
h : x.Coprime n
rw : HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
rw₁ rw₂ : Eq (α := ZMod n) 1 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n)⁻¹ (↑x : ZMod n) = 1

Tactic:
rw [mul_comm, coe_mul_inv_eq_one x h]

Premises used: mul_comm, ZMod.coe_mul_inv_eq_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n x : ℕ
h : x.Coprime n
⊢ (↑(unitOfCoprime x h) : ZMod n) = (↑x : ZMod n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
u : (ZMod n)ˣ
zero : ∀ (u : (ZMod 0)ˣ), (↑u : ZMod 0).val.Coprime 0
succ : ∀ (n : ℕ) (u : (ZMod (n + 1))ˣ), (↑u : ZMod (n + 1)).val.Coprime (n + 1)
⊢ (↑u : ZMod n).val.Coprime n

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
u : (ZMod 0)ˣ
zero : (val (n := 0) (↑1 : ZMod 0)).Coprime 0
zero₁ : (val (n := 0) (↑(-1) : ZMod 0)).Coprime 0
⊢ (↑u : ZMod 0).val.Coprime 0

Tactic:
rcases Int.units_eq_one_or u with (rfl | rfl)

Premises used: Int.units_eq_one_or, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ (val (n := 0) (↑1 : ZMod 0)).Coprime 0

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ (val (n := 0) (↑(-1) : ZMod 0)).Coprime 0

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
succ : (↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val ≡ 1 [MOD n + 1]
⊢ (↑u : ZMod (n + 1)).val.Coprime (n + 1)

Tactic:
apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val

Premises used: Units.val, Inv.inv, Nat.coprime_of_mul_modEq_one, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ (↑(u * u⁻¹) : ZMod (n + 1)) = (↑1 : ZMod (n + 1))

Tactic:
have := Units.ext_iff.1 (mul_inv_cancel u)
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
this : (↑(u * u⁻¹) : ZMod (n + 1)) = (↑1 : ZMod (n + 1))
⊢ (↑(u * u⁻¹) : ZMod (n + 1)) = 1

Tactic:
rw [Units.val_one] at this

Premises used: Units.val_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
u : (ZMod (n + 1))ˣ
this : (↑(u * u⁻¹) : ZMod (n + 1)) = 1
succ : (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1)) = (↑(u * u⁻¹) : ZMod (n + 1))
⊢ (↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val ≡ 1 [MOD n + 1]

Tactic:
rw [← natCast_eq_natCast_iff, Nat.cast_one, ← this]

Premises used: ZMod.natCast_eq_natCast_iff, Nat.cast_one
-- Module: Mathlib.Data.ZMod.Basic
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 * u⁻¹) : ZMod (n + 1)).val : ZMod (n + 1))
⊢ (↑((↑u : ZMod (n + 1)).val * (↑u⁻¹ : ZMod (n + 1)).val) : ZMod (n + 1)) = (↑(u * u⁻¹) : ZMod (n + 1))

Tactic:
rw [← natCast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]

Premises used: Units.val, HMul.hMul, ZMod.natCast_zmod_val, Inv.inv
-- Module: Mathlib.Data.ZMod.Basic
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))
succ₂ 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))
⊢ 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 [Units.val_mul, val_mul, natCast_mod]

Premises used: ZMod.val_mul, ZMod.natCast_mod, Units.val_mul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
⊢ IsUnit (M := ZMod n) (↑m : ZMod n) ↔ m.Coprime n

Tactic:
⟨fun H ↦ ?_, fun H ↦ (unitOfCoprime m H).isUnit⟩

Premises used: ZMod.unitOfCoprime, Iff.intro, Units.isUnit
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
refine : ∀ (H : IsUnit (M := ZMod n) (↑m : ZMod n)), m.Coprime n
⊢ IsUnit (M := ZMod n) (↑m : ZMod n) ↔ m.Coprime n

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ (unitOfCoprime m H).isUnit⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
H : IsUnit (M := ZMod n) (↑m : ZMod n)
⊢ (↑H.unit : ZMod n).val.Coprime n

Tactic:
have H' := val_coe_unit_coprime H.unit
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
H : IsUnit (M := ZMod n) (↑m : ZMod n)
H' : (↑H.unit : ZMod n).val.Coprime n
⊢ (m % n).gcd n = 1

Tactic:
rw [IsUnit.unit_spec, val_natCast, Nat.coprime_iff_gcd_eq_one] at H'

Premises used: Nat.coprime_iff_gcd_eq_one, ZMod.val_natCast, IsUnit.unit_spec
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
H : IsUnit (M := ZMod n) (↑m : ZMod n)
H' : (m % n).gcd n = 1
rw : n.gcd m = (m % n).gcd n
⊢ m.Coprime n

Tactic:
rw [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm, ← H']

Premises used: Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
H : IsUnit (M := ZMod n) (↑m : ZMod n)
H' : (m % n).gcd n = 1
⊢ n.gcd m = (m % n).gcd n

Tactic:
Nat.gcd_rec n m

Premises used: Nat.gcd_rec
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
H : IsUnit (M := ZMod n) (↑m : ZMod n)
H' : (m % n).gcd n = 1
⊢ n.gcd m = (m % n).gcd n

Tactic:
exact Nat.gcd_rec n m

Premises used: Nat.gcd_rec
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
this : (m % n).gcd n = m.gcd n
⊢ (m % n).Coprime n ↔ m.Coprime n

Tactic:
grind
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
suffices : (m % n).gcd n = m.gcd n
⊢ (m % n).Coprime n ↔ m.Coprime n

Tactic:
suffices (m % n).gcd n = m.gcd n by grind
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
⊢ m % n ≡ m [MOD n]

Tactic:
simp [Nat.ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ℕ
⊢ (m % n).gcd n = m.gcd n

Tactic:
exact Nat.ModEq.gcd_eq (by simp [Nat.ModEq])

Premises used: Nat.ModEq.gcd_eq
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n p : ℕ
hp : Nat.Prime p
rw : p.Coprime n ↔ ¬p ∣ n
rw₁ rw₂ : ¬p ∣ n ↔ ¬p ∣ n
⊢ IsUnit (M := ZMod n) (↑p : ZMod n) ↔ ¬p ∣ n

Tactic:
rw [isUnit_iff_coprime, Nat.Prime.coprime_iff_not_dvd hp]

Premises used: ZMod.isUnit_iff_coprime, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n p : ℕ
hp : Nat.Prime p
h : ¬p ∣ n
⊢ IsUnit (M := ZMod n) (↑p : ZMod n)

Tactic:
(isUnit_prime_iff_not_dvd hp).mpr h

Premises used: Iff.mpr, ZMod.isUnit_prime_iff_not_dvd
-- Module: Mathlib.Data.ZMod.Basic
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
rw₃ rw₄ : ¬p ∣ a ↔ ¬p ∣ a
⊢ IsUnit (M := ZMod (p ^ d)) (↑a : ZMod (p ^ d)) ↔ ¬p ∣ a

Tactic:
rw [isUnit_iff_coprime, Nat.coprime_pow_right_iff hd, Nat.coprime_comm,
    hp.coprime_iff_not_dvd]

Premises used: ZMod.isUnit_iff_coprime, Nat.coprime_pow_right_iff, Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p d : ℕ
hp : Nat.Prime p
hd : 0 < d
simp : d = 0 → p = 1
⊢ ¬IsUnit (M := ZMod (p ^ d)) (↑p : ZMod (p ^ d))

Tactic:
simp [isUnit_prime_iff_not_dvd hp]

Premises used: ZMod.isUnit_prime_iff_not_dvd
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p d : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ d = 0 → p = 1

Tactic:
lia
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
u : (ZMod n)ˣ
⊢ 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)
-- Module: Mathlib.Data.ZMod.Basic
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)⁻¹ = 1

Tactic:
rw [← mul_inv_eq_gcd, Nat.cast_one] at this

Premises used: ZMod.mul_inv_eq_gcd, Nat.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
u : (ZMod n)ˣ
this : (↑u : ZMod n) * (↑u : ZMod n)⁻¹ = 1
⊢ (↑u : ZMod n)⁻¹ = (↑u⁻¹ : ZMod n)

Tactic:
(Units.inv_eq_of_mul_eq_one_right this).symm

Premises used: Units.inv_eq_of_mul_eq_one_right, Eq.symm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
u : (ZMod n)ˣ
this : (↑u : ZMod n) * (↑u : ZMod n)⁻¹ = 1
⊢ (↑u : ZMod n)⁻¹ = (↑u⁻¹ : ZMod n)

Tactic:
exact (Units.inv_eq_of_mul_eq_one_right this).symm

Premises used: Units.inv_eq_of_mul_eq_one_right, Eq.symm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
h : IsUnit a
rcases : ∀ (u : (ZMod n)ˣ), (↑u : ZMod n) * (↑u : ZMod n)⁻¹ = 1
⊢ a * a⁻¹ = 1

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
u : (ZMod n)ˣ
rw : (↑u : ZMod n) * (↑u⁻¹ : ZMod n) = 1
rw₁ rw₂ : Eq (α := ZMod n) 1 1
⊢ (↑u : ZMod n) * (↑u : ZMod n)⁻¹ = 1

Tactic:
rw [inv_coe_unit, u.mul_inv]

Premises used: ZMod.inv_coe_unit, Units.mul_inv
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
h : IsUnit a
rw : a * a⁻¹ = 1
rw₁ rw₂ : Eq (α := ZMod n) 1 1
⊢ a⁻¹ * a = 1

Tactic:
rw [mul_comm, mul_inv_of_unit a h]

Premises used: ZMod.mul_inv_of_unit, mul_comm
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a b : ZMod n
h : a * b = 1
⊢ a⁻¹ = b

Tactic:
left_inv_eq_right_inv (inv_mul_of_unit a ⟨⟨a, b, h, mul_comm a b ▸ h⟩, rfl⟩) h

Premises used: Eq.rec, left_inv_eq_right_inv, ZMod.inv_mul_of_unit, Units.mk, Exists.intro, mul_comm, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ HMul.hMul (α := ZMod n) (-1) (-1) = 1

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
⟨fun H ↦ ?_, fun H ↦ H ▸ a.inv_mul_of_unit ha⟩

Premises used: Eq.rec, ZMod.inv_mul_of_unit, Iff.intro
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
refine : ∀ (H : a⁻¹ * b = 1), a = b
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H ▸ a.inv_mul_of_unit ha⟩
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a⁻¹ * b = 1
⊢ a * (a⁻¹ * b) = a * 1

Tactic:
apply_fun (a * ·) at H

Premises used: HMul.hMul
-- Module: Mathlib.Data.ZMod.Basic
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
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (H : a = b), a = b
⊢ a = b

Tactic:
rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H

Premises used: mul_assoc, ZMod.mul_inv_of_unit, eq_comm, mul_one, one_mul
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
x : { x : ZMod n // x.val.Coprime n }
val : ZMod n
property : val.val.Coprime n
⊢ Eq (α := { x : ZMod n // x.val.Coprime n })
    ((fun (x : (ZMod n)ˣ) ↦
        (Subtype.mk (p := fun (x : ZMod n) ↦ x.val.Coprime n) (↑x : ZMod n) ⋯ : { x : ZMod n // x.val.Coprime n }))
      ((fun (x : { x : ZMod n // x.val.Coprime n }) ↦ unitOfCoprime (↑x : ZMod n).val ⋯)
        (Subtype.mk (p := fun (x : ZMod n) ↦ x.val.Coprime n) val property)))
    (Subtype.mk (p := fun (x : ZMod n) ↦ x.val.Coprime n) val property)

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m_1 n_1 m n : ℕ
h : m.Coprime n
⊢ m.lcm n ∣ m * n

Tactic:
simp [Nat.lcm_dvd_iff]

Premises used: Nat.lcm_dvd_iff
-- Module: Mathlib.Data.ZMod.Basic
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
inr :
  ∀ (h : Nat.Coprime 1 0),
    let to_fun : ZMod (HMul.hMul (α := ℕ) 1 0) → ZMod 1 × ZMod 0 :=
      (⇑(castHom ⋯ (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
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
rcases h.eq_of_mul_eq_zero hmn0 with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Premises used: Nat.Coprime.eq_of_mul_eq_zero, rfl
-- Module: Mathlib.Data.ZMod.Basic
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
inl₁ : RightInverse inv_fun to_fun
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.Basic
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 (HMul.hMul (α := ℕ) 0 1)
⊢ inv_fun (to_fun x) = x

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
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
inl : to_fun (inv_fun (x, (fun (i : Fin (0 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (0 + 1)))) = (x, (fun (i : Fin (0 + 1)) ↦ i) ⟨0, ⋯⟩)
⊢ to_fun (inv_fun (x, y)) = (x, y)

Tactic:
fin_cases y
-- Module: Mathlib.Data.ZMod.Basic
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
⊢ to_fun (inv_fun (x, (fun (i : Fin (0 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (0 + 1)))) = (x, (fun (i : Fin (0 + 1)) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]

Premises used: Prod.ext_iff, eq_iff_true_of_subsingleton, ZMod.castHom
-- Module: Mathlib.Data.ZMod.Basic
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
inr₁ : RightInverse inv_fun to_fun
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.Basic
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 (HMul.hMul (α := ℕ) 1 0)
⊢ inv_fun (to_fun x) = x

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.Basic
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
inr : to_fun (inv_fun ((fun (i : Fin (0 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (0 + 1)), y)) = ((fun (i : Fin (0 + 1)) ↦ i) ⟨0, ⋯⟩, y)
⊢ to_fun (inv_fun (x, y)) = (x, y)

Tactic:
fin_cases x
-- Module: Mathlib.Data.ZMod.Basic
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
y : ZMod 0
⊢ to_fun (inv_fun ((fun (i : Fin (0 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (0 + 1)), y)) = ((fun (i : Fin (0 + 1)) ↦ i) ⟨0, ⋯⟩, y)

Tactic:
simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]

Premises used: Prod.ext_iff, eq_iff_true_of_subsingleton, ZMod.castHom