awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : n = 0
⊢ IsUnit x

Tactic:
simp only [hn, Nat.cast_zero, isCoprime_zero_right] at h

Premises used: isCoprime_zero_right, Nat.cast_zero
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
hn : n = 0
h : IsUnit x
pos : ∀ (h : x = 1), HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
pos₁ : ∀ (h : x = -1), HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1

Tactic:
rcases Int.isUnit_eq_one_or h with h | h

Premises used: Int.isUnit_eq_one_or
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
hn : n = 0
h_1 : IsUnit x
h : x = 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1

Tactic:
simp [h]
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
hn : n = 0
h_1 : IsUnit x
h : x = -1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1

Tactic:
simp [h]
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : ¬n = 0
⊢ NeZero n

Tactic:
haveI : NeZero n := ⟨hn⟩
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : ¬n = 0
this : NeZero n
neg : HMul.hMul (α := ZMod n) (↑(val (n := n) (↑x : ZMod n)) : ZMod n) (↑(val (n := n) (↑x : ZMod n)) : ZMod n)⁻¹ = 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1

Tactic:
rw [← natCast_zmod_val x]

Premises used: Int.cast, ZMod.natCast_zmod_val
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : ¬n = 0
this : NeZero n
neg : (val (n := n) (↑x : ZMod n)).Coprime n
⊢ HMul.hMul (α := ZMod n) (↑(val (n := n) (↑x : ZMod n)) : ZMod n) (↑(val (n := n) (↑x : ZMod n)) : ZMod n)⁻¹ = 1

Tactic:
apply coe_mul_inv_eq_one

Premises used: ZMod.coe_mul_inv_eq_one
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : ¬n = 0
this : NeZero n
neg : ∀ (h : x.gcd (↑n : ℤ) = 1) (hn : ¬n = 0) (this : NeZero n), (val (n := n) (↑x : ZMod n)).Coprime n
neg₁ : ∀ (h : (x % (↑n : ℤ)).gcd (↑n : ℤ) = 1) (hn : ¬n = 0) (this : NeZero n), (val (n := n) (↑x : ZMod n)).Coprime n
neg₂ neg₃ neg₄ neg₅ :
  ∀ (h : Int.gcd (↑(val (n := n) (↑x : ZMod n)) : ℤ) (↑n : ℤ) = 1) (hn : ¬n = 0) (this : NeZero n),
    (val (n := n) (↑x : ZMod n)).Coprime n
⊢ (val (n := n) (↑x : ZMod n)).Coprime n

Tactic:
rwa [Int.isCoprime_iff_gcd_eq_one, ← Int.gcd_emod, ← val_intCast] at h

Premises used: Int.gcd_emod, Int.isCoprime_iff_gcd_eq_one, ZMod.val_intCast
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑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_int_mul_inv_eq_one h]

Premises used: mul_comm, ZMod.coe_int_mul_inv_eq_one
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
inst : NeZero n
m : ℤ
h : IsCoprime m (↑n : ℤ)
rw : HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑m : ZMod n)⁻¹ = 1
rw₁ rw₂ : Eq (α := ZMod n) 1 1
⊢ HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1

Tactic:
rw [natCast_zmod_val, coe_int_mul_inv_eq_one h]

Premises used: ZMod.natCast_zmod_val, ZMod.coe_int_mul_inv_eq_one
-- Module: Mathlib.Data.ZMod.Units
Goal:
n : ℕ
inst : NeZero n
m : ℤ
h : IsCoprime m (↑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, coe_int_mul_val_inv h]

Premises used: ZMod.coe_int_mul_val_inv, mul_comm
-- Module: Mathlib.Data.ZMod.Units
Goal:
m : ℕ
n : ℤ
h : IsCoprime n (↑m : ℤ)
⊢ (↑(unitOfIsCoprime n h) : ZMod m) = (↑n : ZMod m)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ZMod.Units
Goal:
m : ℕ
n : ℤ
h : IsUnit (M := ZMod m) (↑n : ZMod m)
rw : ∃ (b : ZMod m), (↑n : ZMod m)⁻¹ * b = 1 ∧ b * (↑n : ZMod m)⁻¹ = 1
⊢ IsUnit (M := ZMod m) (↑n : ZMod m)⁻¹

Tactic:
rw [isUnit_iff_exists]

Premises used: isUnit_iff_exists
-- Module: Mathlib.Data.ZMod.Units
Goal:
m : ℕ
n : ℤ
h : IsUnit (M := ZMod m) (↑n : ZMod m)
⊢ ∃ (b : ZMod m), (↑n : ZMod m)⁻¹ * b = 1 ∧ b * (↑n : ZMod m)⁻¹ = 1

Tactic:
⟨n, inv_mul_of_unit _ h, mul_inv_of_unit _ h⟩

Premises used: Int.cast, ZMod.mul_inv_of_unit, ZMod.inv_mul_of_unit, And.intro, Exists.intro
-- Module: Mathlib.Data.ZMod.Units
Goal:
m : ℕ
n : ℤ
h : IsUnit (M := ZMod m) (↑n : ZMod m)
⊢ ∃ (b : ZMod m), (↑n : ZMod m)⁻¹ * b = 1 ∧ b * (↑n : ZMod m)⁻¹ = 1

Tactic:
exact ⟨n, inv_mul_of_unit _ h, mul_inv_of_unit _ h⟩
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
x : ZMod 0
⊢ x.valMinAbs = x

Tactic:
rfl

Premises used: ZMod.valMinAbs, rfl
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
h : NeZero (R := ℕ) 0
x : ZMod 0
⊢ x.valMinAbs = if x.val ≤ 0 / 2 then (↑x.val : ℤ) else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑0 : ℤ)

Tactic:
cases NeZero.ne 0 rfl

Premises used: OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
k n : ℕ
h : k = n + 1
x : ZMod (namedPattern k (n + 1) h)
pos : x.val ≤ namedPattern k (n + 1) h / 2 → (↑(↑x.val : ℤ) : ZMod (namedPattern k (n + 1) h)) = x
neg :
  ¬x.val ≤ namedPattern k (n + 1) h / 2 →
    (↑(HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑(namedPattern k (n + 1) h) : ℤ)) : ZMod (namedPattern k (n + 1) h)) = x
⊢ (↑(if x.val ≤ namedPattern k (n + 1) h / 2 then (↑x.val : ℤ)
        else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑(namedPattern k (n + 1) h) : ℤ)) :
      ZMod (namedPattern k (n + 1) h)) =
    x

Tactic:
split_ifs
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
k n : ℕ
h : k = n + 1
x : ZMod (namedPattern k (n + 1) h)
h_1 : x.val ≤ namedPattern k (n + 1) h / 2
pos : (↑x.val : ZMod (namedPattern k (n + 1) h)) = x
pos₁ pos₂ : x = x
⊢ (↑(↑x.val : ℤ) : ZMod (namedPattern k (n + 1) h)) = x

Tactic:
rw [Int.cast_natCast, natCast_zmod_val]

Premises used: Int.cast_natCast, ZMod.natCast_zmod_val
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
k n : ℕ
h : k = n + 1
x : ZMod (namedPattern k (n + 1) h)
h_1 : ¬x.val ≤ namedPattern k (n + 1) h / 2
neg :
  HSub.hSub (α := ZMod (namedPattern k (n + 1) h)) (↑(↑x.val : ℤ) : ZMod (namedPattern k (n + 1) h))
      (↑(↑(namedPattern k (n + 1) h) : ℤ) : ZMod (namedPattern k (n + 1) h)) =
    x
neg₁ :
  HSub.hSub (α := ZMod (namedPattern k (n + 1) h)) (↑x.val : ZMod (namedPattern k (n + 1) h))
      (↑(↑(namedPattern k (n + 1) h) : ℤ) : ZMod (namedPattern k (n + 1) h)) =
    x
neg₂ : x - (↑(↑(namedPattern k (n + 1) h) : ℤ) : ZMod (namedPattern k (n + 1) h)) = x
neg₃ : x - (↑(namedPattern k (n + 1) h) : ZMod (namedPattern k (n + 1) h)) = x
neg₄ : x - 0 = x
neg₅ neg₆ : x = x
⊢ (↑(HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑(namedPattern k (n + 1) h) : ℤ)) : ZMod (namedPattern k (n + 1) h)) = x

Tactic:
rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
        sub_zero]

Premises used: Int.cast_natCast, ZMod.natCast_self, sub_zero, Int.cast_sub, ZMod.natCast_zmod_val
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
⊢ Function.Injective (α := ZMod n) valMinAbs

Tactic:
Function.injective_iff_hasLeftInverse.2 ⟨_, coe_valMinAbs⟩

Premises used: Iff.mpr, ZMod.coe_valMinAbs, Function.injective_iff_hasLeftInverse, Exists.intro
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
⊢ a.valMinAbs = b.valMinAbs ↔ a = b

Tactic:
ZMod.injective_valMinAbs.eq_iff

Premises used: ZMod.injective_valMinAbs, Function.Injective.eq_iff
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
rw : (0 ≤ if x.val ≤ n / 2 then (↑x.val : ℤ) else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ)) ↔ x.val ≤ n / 2
⊢ 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2

Tactic:
rw [valMinAbs_def_pos]

Premises used: ZMod.valMinAbs_def_pos
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
pos : ∀ (h : x.val ≤ n / 2), LE.le (α := ℤ) 0 (↑x.val : ℤ) ↔ x.val ≤ n / 2
neg : ∀ (h : ¬x.val ≤ n / 2), 0 ≤ HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) ↔ x.val ≤ n / 2
⊢ (0 ≤ if x.val ≤ n / 2 then (↑x.val : ℤ) else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ)) ↔ x.val ≤ n / 2

Tactic:
split_ifs with h
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.val ≤ n / 2
⊢ LE.le (α := ℤ) 0 (↑x.val : ℤ) ↔ x.val ≤ n / 2

Tactic:
iff_of_true (Nat.cast_nonneg _) h

Premises used: Nat.cast_nonneg, iff_of_true
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.val ≤ n / 2
⊢ LE.le (α := ℤ) 0 (↑x.val : ℤ) ↔ x.val ≤ n / 2

Tactic:
exact iff_of_true (Nat.cast_nonneg _) h

Premises used: Nat.cast_nonneg, iff_of_true
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : ¬x.val ≤ n / 2
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) ↔ x.val ≤ n / 2

Tactic:
iff_of_false (sub_lt_zero.2 <| Int.ofNat_lt.2 x.val_lt).not_ge h

Premises used: Iff.mpr, sub_lt_zero, Int.ofNat_lt, iff_of_false, LT.lt.not_ge, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : ¬x.val ≤ n / 2
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) ↔ x.val ≤ n / 2

Tactic:
exact iff_of_false (sub_lt_zero.2 <| Int.ofNat_lt.2 x.val_lt).not_ge h

Premises used: Iff.mpr, sub_lt_zero, Int.ofNat_lt, iff_of_false, LT.lt.not_ge, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
zero : ∀ (a : ZMod 0), a.valMinAbs * 2 = (↑0 : ℤ) ↔ 2 * a.val = 0
succ : ∀ (n : ℕ) (a : ZMod (n + 1)), a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1
⊢ a.valMinAbs * 2 = (↑n : ℤ) ↔ 2 * a.val = n

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
a : ZMod 0
⊢ a.valMinAbs * 2 = (↑0 : ℤ) ↔ 2 * a.val = 0

Tactic:
simp
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
pos : ∀ (h : a.val ≤ n.succ / 2), a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1
neg : ∀ (h : ¬a.val ≤ n.succ / 2), a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1
⊢ a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1

Tactic:
by_cases h : a.val ≤ n.succ / 2

Premises used: Nat.succ, ZMod.val
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
pos : HMul.hMul (α := ℤ) (↑a.val : ℤ) 2 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔ 2 * a.val = n + 1
pos₁ : HMul.hMul (α := ℤ) (↑a.val : ℤ) 2 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔ Eq (α := ℤ) (↑(2 * a.val) : ℤ) (↑(n + 1) : ℤ)
pos₂ :
  HMul.hMul (α := ℤ) (↑a.val : ℤ) 2 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    HMul.hMul (α := ℤ) (↑2 : ℤ) (↑a.val : ℤ) = (↑(n + 1) : ℤ)
pos₃ :
  HMul.hMul (α := ℤ) (↑a.val : ℤ) 2 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔ HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = (↑(n + 1) : ℤ)
pos₄ :
  HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔ HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = (↑(n + 1) : ℤ)
pos₅ :
  HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ)
pos₆ pos₇ :
  HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ (if a.val ≤ (n + 1) / 2 then (↑a.val : ℤ) else (↑a.val : ℤ) - HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * 2 =
      HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
    2 * a.val = n + 1

Tactic:
rw [if_pos h, ← Int.natCast_inj, Nat.cast_mul, Nat.cast_two, mul_comm, Int.natCast_add,
      Nat.cast_one]

Premises used: Int.natCast_add, if_pos, Nat.cast_mul, mul_comm, Nat.cast_one, Nat.cast_two, Int.natCast_inj
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
apply : ¬a.valMinAbs * 2 = (↑(n + 1) : ℤ)
apply₁ : 2 * a.val = n + 1 → a.val ≤ n.succ / 2
⊢ a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1

Tactic:
apply iff_of_false _ (mt _ h)

Premises used: mt, iff_of_false
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
he : a.valMinAbs * 2 = (↑(n + 1) : ℤ)
rw : ∀ (h : ¬0 ≤ a.valMinAbs) (h : ¬LE.le (α := ℤ) 0 (↑(n + 1) : ℤ)) (he : a.valMinAbs * 2 = (↑(n + 1) : ℤ)), False
rw₁ : ∀ (h : ¬0 ≤ a.valMinAbs) (he : a.valMinAbs * 2 = (↑(n + 1) : ℤ)), LT.lt (α := ℤ) 0 2
⊢ False

Tactic:
rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h

Premises used: ZMod.valMinAbs_nonneg_iff, mul_nonneg_iff_left_nonneg_of_pos
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
h_1 : ¬0 ≤ a.valMinAbs
h : ¬LE.le (α := ℤ) 0 (↑(n + 1) : ℤ)
he : a.valMinAbs * 2 = (↑(n + 1) : ℤ)
⊢ False

Tactic:
h (Nat.cast_nonneg _)

Premises used: Nat.cast_nonneg
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬0 ≤ a.valMinAbs
he : a.valMinAbs * 2 = (↑(n + 1) : ℤ)
⊢ LT.lt (α := ℤ) 0 2

Tactic:
zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
h_1 : ¬0 ≤ a.valMinAbs
h : ¬LE.le (α := ℤ) 0 (↑(n + 1) : ℤ)
he : a.valMinAbs * 2 = (↑(n + 1) : ℤ)
⊢ False

Tactic:
exacts [h (Nat.cast_nonneg _), zero_lt_two]

Premises used: Nat.cast_nonneg, zero_lt_two
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
rw : a.val * 2 = n + 1 → a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ a.val * 2 = n + 1 → a.val ≤ n.succ / 2

Tactic:
fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le

Premises used: Iff.mpr, Eq.le, Nat.le_div_iff_mul_le, zero_lt_two
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ a.val * 2 = n + 1 → a.val ≤ n.succ / 2

Tactic:
exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le

Premises used: Iff.mpr, Nat.le_div_iff_mul_le, zero_lt_two
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
simp_rw :
  Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ))
    ((if HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ) then (↑x.val : ℤ) else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ)) *
      2)
⊢ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (x.valMinAbs * 2)

Tactic:
simp_rw [valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le]

Premises used: ZMod.valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
pos :
  ∀ (h : HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)),
    Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (HMul.hMul (α := ℤ) (↑x.val : ℤ) 2)
neg :
  ∀ (h : ¬HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)),
    Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2)
⊢ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ))
    ((if HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ) then (↑x.val : ℤ) else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ)) *
      2)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)
⊢ 0 ≤ HMul.hMul (α := ℤ) (↑x.val : ℤ) 2

Tactic:
positivity
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)
⊢ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (HMul.hMul (α := ℤ) (↑x.val : ℤ) 2)

Tactic:
exact ⟨(neg_lt_zero.2 <| mod_cast NeZero.pos n).trans_le (by positivity), h⟩
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : ¬HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)
⊢ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2)

Tactic:
⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩

Premises used: Set.Ioc, mul_nonpos_of_nonpos_of_nonneg, Set.Mem, Nat.cast_nonneg, setOf, And.intro, zero_le_two, le_trans
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : ¬HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)
neg : -(↑n : ℤ) < HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2
neg₁ : HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) ≤ 0
⊢ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2)

Tactic:
refine ⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : ¬HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)
linarith :
  HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2 ≤ -(↑n : ℤ) →
    -1 + (HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2 - -(↑n : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - HMul.hMul (α := ℤ) (↑x.val : ℤ) 2) =
      0
⊢ -(↑n : ℤ) < HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2

Tactic:
linarith only [h]
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : ¬HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)
⊢ HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) ≤ 0

Tactic:
grind
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
⊢ x = (↑x.valMinAbs : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (x.valMinAbs * 2)

Tactic:
⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩

Premises used: ZMod.valMinAbs_mem_Ioc, ZMod.coe_valMinAbs, And.intro, Eq.symm
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
⊢ x = (↑x.valMinAbs : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (x.valMinAbs * 2)

Tactic:
exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
rw : x.valMinAbs - y = 0
⊢ x.valMinAbs = y

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
h1 : (↑n : ℤ) ∣ x.valMinAbs - y
h2 : |x.valMinAbs - y| < (↑n : ℤ)
⊢ x.valMinAbs - y = 0

Tactic:
apply @Int.eq_zero_of_abs_lt_dvd n

Premises used: Int.eq_zero_of_abs_lt_dvd
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
h1 : Eq (α := ZMod n) (↑(x.valMinAbs - y) : ZMod n) 0
h1₁ : HSub.hSub (α := ZMod n) (↑x.valMinAbs : ZMod n) (↑y : ZMod n) = 0
h1₂ : x - (↑y : ZMod n) = 0
h1₃ : HSub.hSub (α := ZMod n) (↑y : ZMod n) (↑y : ZMod n) = 0
h1₄ h1₅ : Eq (α := ZMod n) 0 0
⊢ (↑n : ℤ) ∣ x.valMinAbs - y

Tactic:
rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]

Premises used: sub_self, Int.cast_sub, ZMod.coe_valMinAbs, ZMod.intCast_zmod_eq_zero_iff_dvd, And.left
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
h2 : |x.valMinAbs - y| * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2
⊢ |x.valMinAbs - y| < (↑n : ℤ)

Tactic:
rw [← mul_lt_mul_iff_left₀ (@zero_lt_two ℤ _ _ _ _ _)]

Premises used: zero_lt_two, mul_lt_mul_iff_left₀
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
h2 : -HMul.hMul (α := ℤ) (↑n : ℤ) 2 < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2
⊢ |x.valMinAbs - y| * |2| < HMul.hMul (α := ℤ) (↑n : ℤ) 2

Tactic:
rw [← abs_mul, sub_mul, abs_lt]

Premises used: abs_mul, sub_mul, abs_lt
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
h2 : -HMul.hMul (α := ℤ) (↑n : ℤ) 2 < x.valMinAbs * 2 - y * 2
h2₁ : x.valMinAbs * 2 - y * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2
⊢ -HMul.hMul (α := ℤ) (↑n : ℤ) 2 < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
linarith :
  x.valMinAbs * 2 - y * 2 ≤ -HMul.hMul (α := ℤ) (↑n : ℤ) 2 →
    -1 + (x.valMinAbs * 2 - y * 2 - -HMul.hMul (α := ℤ) (↑n : ℤ) 2) +
          (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - x.valMinAbs * 2) +
        (y * 2 - (↑n : ℤ)) =
      0
⊢ -HMul.hMul (α := ℤ) (↑n : ℤ) 2 < x.valMinAbs * 2 - y * 2

Tactic:
linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]

Premises used: ZMod.valMinAbs_mem_Ioc, And.right, And.left
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
linarith :
  HMul.hMul (α := ℤ) (↑n : ℤ) 2 ≤ x.valMinAbs * 2 - y * 2 →
    -1 + (HMul.hMul (α := ℤ) (↑n : ℤ) 2 - (x.valMinAbs * 2 - y * 2)) + (x.valMinAbs * 2 - (↑n : ℤ)) +
        (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - y * 2) =
      0
⊢ x.valMinAbs * 2 - y * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2

Tactic:
linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]

Premises used: ZMod.valMinAbs_mem_Ioc, And.right, And.left
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
rw : HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
⊢ x.valMinAbs.natAbs ≤ n / 2

Tactic:
rw [Nat.le_div_two_iff_mul_two_le]

Premises used: Nat.le_div_two_iff_mul_two_le
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
inl : ∀ (h : x.valMinAbs = (↑x.valMinAbs.natAbs : ℤ)), HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
inr : ∀ (h : x.valMinAbs = -(↑x.valMinAbs.natAbs : ℤ)), HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
⊢ HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)

Tactic:
rcases x.valMinAbs.natAbs_eq with h | h

Premises used: ZMod.valMinAbs, Int.natAbs_eq
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.valMinAbs = (↑x.valMinAbs.natAbs : ℤ)
inl : x.valMinAbs * 2 ≤ (↑n : ℤ)
⊢ HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)

Tactic:
rw [← h]
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.valMinAbs = (↑x.valMinAbs.natAbs : ℤ)
⊢ x.valMinAbs * 2 ≤ (↑n : ℤ)

Tactic:
x.valMinAbs_mem_Ioc.2

Premises used: ZMod.valMinAbs_mem_Ioc, And.right
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.valMinAbs = (↑x.valMinAbs.natAbs : ℤ)
⊢ x.valMinAbs * 2 ≤ (↑n : ℤ)

Tactic:
exact x.valMinAbs_mem_Ioc.2

Premises used: ZMod.valMinAbs_mem_Ioc, And.right
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.valMinAbs = -(↑x.valMinAbs.natAbs : ℤ)
inr : -(↑n : ℤ) ≤ x.valMinAbs * 2
⊢ HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)

Tactic:
rw [← neg_le_neg_iff, ← neg_mul, ← h]

Premises used: neg_mul, neg_le_neg_iff
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.valMinAbs = -(↑x.valMinAbs.natAbs : ℤ)
⊢ -(↑n : ℤ) ≤ x.valMinAbs * 2

Tactic:
x.valMinAbs_mem_Ioc.1.le

Premises used: ZMod.valMinAbs_mem_Ioc, LT.lt.le, And.left
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.valMinAbs = -(↑x.valMinAbs.natAbs : ℤ)
⊢ -(↑n : ℤ) ≤ x.valMinAbs * 2

Tactic:
exact x.valMinAbs_mem_Ioc.1.le

Premises used: ZMod.valMinAbs_mem_Ioc, LT.lt.le, And.left
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
h : a.valMinAbs = -b.valMinAbs
inl : ∀ {a b : ZMod 0} (h : a.valMinAbs = -b.valMinAbs), a = -b
inr : ∀ (hn : NeZero n), a = -b
⊢ a = -b

Tactic:
rcases eq_zero_or_neZero n with rfl | hn

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
a b : ZMod 0
h : a.valMinAbs = -b.valMinAbs
⊢ a = -b

Tactic:
simp_all [valMinAbs_spec]

Premises used: ZMod.valMinAbs_spec
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
h : a.valMinAbs = -b.valMinAbs
hn : NeZero n
⊢ a = -b

Tactic:
simp_all [valMinAbs_spec]

Premises used: ZMod.valMinAbs_spec
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
⊢ valMinAbs (n := 0) 0 = 0

Tactic:
simp only [valMinAbs_def_zero]

Premises used: ZMod.valMinAbs_def_zero
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
⊢ valMinAbs (n := n + 1) 0 = 0

Tactic:
simp only [valMinAbs_def_pos, if_true, Int.ofNat_zero, zero_le, val_zero]

Premises used: zero_le, if_true, ZMod.valMinAbs_def_pos, ZMod.val_zero, Int.ofNat_zero