awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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)
⊢ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ))
    ((if HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ) then (↑x.val : ℤ) else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ)) *
      2)
have neg : ∀ (h : ¬HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)),
  Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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)
have neg : -(↑n : ℤ) < HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2
Tactic: refine ⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : ¬HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)
neg : -(↑n : ℤ) < HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2
⊢ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2)
have neg₁ : HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) ≤ 0
Tactic: refine ⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : ¬HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)
⊢ -(↑n : ℤ) < HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) * 2
have 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
Tactic: linarith only [h]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
⊢ x.valMinAbs = y
have rw : x.valMinAbs - y = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
⊢ x.valMinAbs - y = 0
have h1 : (↑n : ℤ) ∣ x.valMinAbs - y
Tactic: apply @Int.eq_zero_of_abs_lt_dvd n
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ x.valMinAbs - y = 0
have h2 : |x.valMinAbs - y| < (↑n : ℤ)
Tactic: apply @Int.eq_zero_of_abs_lt_dvd n
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
⊢ (↑n : ℤ) ∣ x.valMinAbs - y
have h1 : Eq (α := ZMod n) (↑(x.valMinAbs - y) : ZMod n) 0
Tactic: rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑n : ℤ) ∣ x.valMinAbs - y
have h1₁ : HSub.hSub (α := ZMod n) (↑x.valMinAbs : ZMod n) (↑y : ZMod n) = 0
Tactic: rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑n : ℤ) ∣ x.valMinAbs - y
have h1₂ : x - (↑y : ZMod n) = 0
Tactic: rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑n : ℤ) ∣ x.valMinAbs - y
have h1₃ : HSub.hSub (α := ZMod n) (↑y : ZMod n) (↑y : ZMod n) = 0
Tactic: rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑n : ℤ) ∣ x.valMinAbs - y
have h1₄ : Eq (α := ZMod n) 0 0
Tactic: rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
⊢ |x.valMinAbs - y| < (↑n : ℤ)
have h2 : |x.valMinAbs - y| * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2
Tactic: rw [← mul_lt_mul_iff_left₀ (@zero_lt_two ℤ _ _ _ _ _)]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
⊢ |x.valMinAbs - y| * |2| < HMul.hMul (α := ℤ) (↑n : ℤ) 2
have h2 : -HMul.hMul (α := ℤ) (↑n : ℤ) 2 < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2
Tactic: rw [← abs_mul, sub_mul, abs_lt]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
⊢ -HMul.hMul (α := ℤ) (↑n : ℤ) 2 < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2
have h2 : -HMul.hMul (α := ℤ) (↑n : ℤ) 2 < x.valMinAbs * 2 - y * 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ -HMul.hMul (α := ℤ) (↑n : ℤ) 2 < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2
have h2₁ : x.valMinAbs * 2 - y * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
⊢ -HMul.hMul (α := ℤ) (↑n : ℤ) 2 < x.valMinAbs * 2 - y * 2
have 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
Tactic: linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
y : ℤ
h : x = (↑y : ZMod n) ∧ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (y * 2)
⊢ x.valMinAbs * 2 - y * 2 < HMul.hMul (α := ℤ) (↑n : ℤ) 2
have 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
Tactic: linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
⊢ x.valMinAbs.natAbs ≤ n / 2
have rw : HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
Tactic: rw [Nat.le_div_two_iff_mul_two_le]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
⊢ HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
have inl : ∀ (h : x.valMinAbs = (↑x.valMinAbs.natAbs : ℤ)), HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
Tactic: rcases x.valMinAbs.natAbs_eq with h | h
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
inl : ∀ (h : x.valMinAbs = (↑x.valMinAbs.natAbs : ℤ)), HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
⊢ HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
have inr : ∀ (h : x.valMinAbs = -(↑x.valMinAbs.natAbs : ℤ)), HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
Tactic: rcases x.valMinAbs.natAbs_eq with h | h
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.valMinAbs = (↑x.valMinAbs.natAbs : ℤ)
⊢ HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
have inl : x.valMinAbs * 2 ≤ (↑n : ℤ)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
h : x.valMinAbs = -(↑x.valMinAbs.natAbs : ℤ)
⊢ HMul.hMul (α := ℤ) (↑x.valMinAbs.natAbs : ℤ) 2 ≤ (↑n : ℤ)
have inr : -(↑n : ℤ) ≤ x.valMinAbs * 2
Tactic: rw [← neg_le_neg_iff, ← neg_mul, ← h]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod n
h : a.valMinAbs = -b.valMinAbs
⊢ a = -b
have inl : ∀ {a b : ZMod 0} (h : a.valMinAbs = -b.valMinAbs), a = -b
Tactic: rcases eq_zero_or_neZero n with rfl | hn
Cleared hypotheses: n, a, b, h
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod n
h : a.valMinAbs = -b.valMinAbs
inl : ∀ {a b : ZMod 0} (h : a.valMinAbs = -b.valMinAbs), a = -b
⊢ a = -b
have inr : ∀ (hn : NeZero n), a = -b
Tactic: rcases eq_zero_or_neZero n with rfl | hn
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
have rw : a.val ≤ n
Tactic: rw [sub_nonpos, Int.ofNat_le]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (hypothesis)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ (↑a.valMinAbs.natAbs : ZMod n) = if a.val ≤ n / 2 then a else -a
have this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
Tactic: have : (a.val : ℤ) - n ≤ 0 := by
    rw [sub_nonpos, Int.ofNat_le]
    exact a.val_le
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
⊢ (↑a.valMinAbs.natAbs : ZMod n) = if a.val ≤ n / 2 then a else -a
have rw : (↑(if a.val ≤ n / 2 then (↑a.val : ℤ) else HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) =
  if a.val ≤ n / 2 then a else -a
Tactic: rw [valMinAbs_def_pos]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
⊢ (↑(if a.val ≤ n / 2 then (↑a.val : ℤ) else HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) =
    if a.val ≤ n / 2 then a else -a
have pos : a.val ≤ n / 2 → (↑(Int.natAbs (↑a.val : ℤ)) : ZMod n) = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
pos : a.val ≤ n / 2 → (↑(Int.natAbs (↑a.val : ℤ)) : ZMod n) = a
⊢ (↑(if a.val ≤ n / 2 then (↑a.val : ℤ) else HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) =
    if a.val ≤ n / 2 then a else -a
have neg : ¬a.val ≤ n / 2 → (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : a.val ≤ n / 2
⊢ (↑(Int.natAbs (↑a.val : ℤ)) : ZMod n) = a
have pos : (↑a.val : ZMod n) = a
Tactic: rw [Int.natAbs_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : a.val ≤ n / 2
pos : (↑a.val : ZMod n) = a
⊢ (↑(Int.natAbs (↑a.val : ℤ)) : ZMod n) = a
have pos₁ : a = a
Tactic: rw [Int.natAbs_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : ¬a.val ≤ n / 2
⊢ (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
have neg : (↑(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ℤ) : ZMod n) = -a
Tactic: rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : ¬a.val ≤ n / 2
neg : (↑(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ℤ) : ZMod n) = -a
⊢ (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
have neg₁ : (↑(-HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
Tactic: rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : ¬a.val ≤ n / 2
neg : (↑(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ℤ) : ZMod n) = -a
neg₁ : (↑(-HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
⊢ (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
have neg₂ : -(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
Tactic: rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : ¬a.val ≤ n / 2
neg : (↑(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ℤ) : ZMod n) = -a
neg₁ : (↑(-HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₂ : -(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
⊢ (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
have neg₃ : -HSub.hSub (α := ZMod n) (↑(↑a.val : ℤ) : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
Tactic: rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : ¬a.val ≤ n / 2
neg : (↑(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ℤ) : ZMod n) = -a
neg₁ : (↑(-HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₂ : -(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₃ : -HSub.hSub (α := ZMod n) (↑(↑a.val : ℤ) : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
⊢ (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
have neg₄ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
Tactic: rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : ¬a.val ≤ n / 2
neg : (↑(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ℤ) : ZMod n) = -a
neg₁ : (↑(-HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₂ : -(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₃ : -HSub.hSub (α := ZMod n) (↑(↑a.val : ℤ) : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
neg₄ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
⊢ (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
have neg₅ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) (↑n : ZMod n) = -a
Tactic: rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : ¬a.val ≤ n / 2
neg : (↑(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ℤ) : ZMod n) = -a
neg₁ : (↑(-HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₂ : -(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₃ : -HSub.hSub (α := ZMod n) (↑(↑a.val : ℤ) : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
neg₄ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
neg₅ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) (↑n : ZMod n) = -a
⊢ (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
have neg₆ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) 0 = -a
Tactic: rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : ¬a.val ≤ n / 2
neg : (↑(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ℤ) : ZMod n) = -a
neg₁ : (↑(-HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₂ : -(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₃ : -HSub.hSub (α := ZMod n) (↑(↑a.val : ℤ) : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
neg₄ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
neg₅ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) (↑n : ZMod n) = -a
neg₆ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) 0 = -a
⊢ (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
have neg₇ : -(↑a.val : ZMod n) = -a
Tactic: rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
h : ¬a.val ≤ n / 2
neg : (↑(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ℤ) : ZMod n) = -a
neg₁ : (↑(-HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₂ : -(↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) : ZMod n) = -a
neg₃ : -HSub.hSub (α := ZMod n) (↑(↑a.val : ℤ) : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
neg₄ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) (↑(↑n : ℤ) : ZMod n) = -a
neg₅ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) (↑n : ZMod n) = -a
neg₆ : -HSub.hSub (α := ZMod n) (↑a.val : ZMod n) 0 = -a
neg₇ : -(↑a.val : ZMod n) = -a
⊢ (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : ZMod n) = -a
have neg₈ : -a = -a
Tactic: rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
⊢ (-a).valMinAbs = -a.valMinAbs
have inl : ∀ {a : ZMod 0} (ha : 2 * a.val ≠ 0), (-a).valMinAbs = -a.valMinAbs
Tactic: rcases eq_zero_or_neZero n with rfl | h
Cleared hypotheses: n, a, ha
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
inl : ∀ {a : ZMod 0} (ha : 2 * a.val ≠ 0), (-a).valMinAbs = -a.valMinAbs
⊢ (-a).valMinAbs = -a.valMinAbs
have inr : ∀ (h : NeZero n), (-a).valMinAbs = -a.valMinAbs
Tactic: rcases eq_zero_or_neZero n with rfl | h
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ (-a).valMinAbs = -a.valMinAbs
have inr : -a = (↑(-a.valMinAbs) : ZMod n)
Tactic: refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
inr : -a = (↑(-a.valMinAbs) : ZMod n)
⊢ (-a).valMinAbs = -a.valMinAbs
have inr₁ : -(↑n : ℤ) < -a.valMinAbs * 2
Tactic: refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
inr : -a = (↑(-a.valMinAbs) : ZMod n)
inr₁ : -(↑n : ℤ) < -a.valMinAbs * 2
⊢ (-a).valMinAbs = -a.valMinAbs
have inr₂ : -a.valMinAbs * 2 ≤ (↑n : ℤ)
Tactic: refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a = (↑(-a.valMinAbs) : ZMod n)
have inr : -a = -(↑a.valMinAbs : ZMod n)
Tactic: rw [Int.cast_neg, coe_valMinAbs]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
inr : -a = -(↑a.valMinAbs : ZMod n)
⊢ -a = (↑(-a.valMinAbs) : ZMod n)
have inr₁ : -a = -a
Tactic: rw [Int.cast_neg, coe_valMinAbs]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -(↑n : ℤ) < -a.valMinAbs * 2
have inr : a.valMinAbs * 2 < (↑n : ℤ)
Tactic: rw [neg_mul, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ (↑n : ℤ)
have linarith : (↑n : ℤ) < -a.valMinAbs * 2 →
  HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - -a.valMinAbs * 2) +
      (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - a.valMinAbs * 2) =
    0
Tactic: linarith only [a.valMinAbs_mem_Ioc.1]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
linarith :
  (↑n : ℤ) < -a.valMinAbs * 2 →
    HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - -a.valMinAbs * 2) +
        (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - a.valMinAbs * 2) =
      0
⊢ -a.valMinAbs * 2 ≤ (↑n : ℤ)
have linarith₁ : (↑n : ℤ) < -a.valMinAbs * 2 → GT.gt (α := ℤ) 2 0
Tactic: linarith only [a.valMinAbs_mem_Ioc.1]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
have pos : ∀ (h2a : 2 * a.val = n), (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
Tactic: by_cases h2a : 2 * a.val = n
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
pos : ∀ (h2a : 2 * a.val = n), (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
have neg : ∀ (h2a : ¬2 * a.val = n), (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
Tactic: by_cases h2a : 2 * a.val = n
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
have pos : a.valMinAbs.natAbs = a.valMinAbs.natAbs
Tactic: rw [a.neg_eq_self_iff.2 (Or.inr h2a)]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
h2a : ¬2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
have neg : (-a.valMinAbs).natAbs = a.valMinAbs.natAbs
Tactic: rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
h2a : ¬2 * a.val = n
neg : (-a.valMinAbs).natAbs = a.valMinAbs.natAbs
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
have neg₁ : a.valMinAbs.natAbs = a.valMinAbs.natAbs
Tactic: rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod n
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a = b ∨ a = -b
have mp : a.valMinAbs.natAbs = b.valMinAbs.natAbs → a = b ∨ a = -b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod n
mp : a.valMinAbs.natAbs = b.valMinAbs.natAbs → a = b ∨ a = -b
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a = b ∨ a = -b
have mpr : a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs
Tactic: constructor