awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have pos : ∀ (hn : n = 0), HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
pos : ∀ (hn : n = 0), HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have neg : ∀ (hn : ¬n = 0), HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : n = 0
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have h₁ : IsUnit x
Tactic: simp only [hn, Nat.cast_zero, isCoprime_zero_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
x : ℤ
hn : n = 0
h : IsUnit x
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have pos : ∀ (h : x = 1), HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
Tactic: rcases Int.isUnit_eq_one_or h with h | h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
x : ℤ
hn : n = 0
h : IsUnit x
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
have pos₁ : ∀ (h : x = -1), HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
Tactic: rcases Int.isUnit_eq_one_or h with h | h
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (hypothesis)
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : ¬n = 0
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have this : NeZero n
Tactic: haveI : NeZero n := ⟨hn⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : ¬n = 0
this : NeZero n
⊢ HMul.hMul (α := ZMod n) (↑x : ZMod n) (↑x : ZMod n)⁻¹ = 1
have neg : HMul.hMul (α := ZMod n) (↑(val (n := n) (↑x : ZMod n)) : ZMod n) (↑(val (n := n) (↑x : ZMod n)) : ZMod n)⁻¹ = 1
Tactic: rw [← natCast_zmod_val x]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : ¬n = 0
this : NeZero n
⊢ HMul.hMul (α := ZMod n) (↑(val (n := n) (↑x : ZMod n)) : ZMod n) (↑(val (n := n) (↑x : ZMod n)) : ZMod n)⁻¹ = 1
have neg : (val (n := n) (↑x : ZMod n)).Coprime n
Tactic: apply coe_mul_inv_eq_one
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑n : ℤ)
hn : ¬n = 0
this : NeZero n
⊢ (val (n := n) (↑x : ZMod n)).Coprime n
have neg : ∀ (h : x.gcd (↑n : ℤ) = 1) (hn : ¬n = 0) (this : NeZero n), (val (n := n) (↑x : ZMod n)).Coprime n
Tactic: rwa [Int.isCoprime_iff_gcd_eq_one, ← Int.gcd_emod, ← val_intCast] at h
Cleared hypotheses: h, hn, this
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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
⊢ (val (n := n) (↑x : ZMod n)).Coprime n
have neg₁ : ∀ (h : (x % (↑n : ℤ)).gcd (↑n : ℤ) = 1) (hn : ¬n = 0) (this : NeZero n), (val (n := n) (↑x : ZMod n)).Coprime n
Tactic: rwa [Int.isCoprime_iff_gcd_eq_one, ← Int.gcd_emod, ← val_intCast] at h
Cleared hypotheses: h, hn, this
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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
⊢ (val (n := n) (↑x : ZMod n)).Coprime n
have 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
Tactic: rwa [Int.isCoprime_iff_gcd_eq_one, ← Int.gcd_emod, ← val_intCast] at h
Cleared hypotheses: h, hn, this
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑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_int_mul_inv_eq_one h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
x : ℤ
h : IsCoprime x (↑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_int_mul_inv_eq_one h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
inst : NeZero n
m : ℤ
h : IsCoprime m (↑n : ℤ)
⊢ HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑(val (n := n) (↑m : ZMod n)⁻¹) : ZMod n) = 1
have rw : HMul.hMul (α := ZMod n) (↑m : ZMod n) (↑m : ZMod n)⁻¹ = 1
Tactic: rw [natCast_zmod_val, coe_int_mul_inv_eq_one h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
inst : NeZero n
m : ℤ
h : IsCoprime m (↑n : ℤ)
rw : 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 rw₁ : Eq (α := ZMod n) 1 1
Tactic: rw [natCast_zmod_val, coe_int_mul_inv_eq_one h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
n : ℕ
inst : NeZero n
m : ℤ
h : IsCoprime m (↑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, coe_int_mul_val_inv h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
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
⊢ 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, coe_int_mul_val_inv h]
-- Lean 4 proof step from Mathlib.Data.ZMod.Units (goal)
Goal:
m : ℕ
n : ℤ
h : IsUnit (M := ZMod m) (↑n : ZMod m)
⊢ IsUnit (M := ZMod m) (↑n : ZMod m)⁻¹
have rw : ∃ (b : ZMod m), (↑n : ZMod m)⁻¹ * b = 1 ∧ b * (↑n : ZMod m)⁻¹ = 1
Tactic: rw [isUnit_iff_exists]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
k n : ℕ
h : k = n + 1
x : ZMod (namedPattern k (n + 1) h)
⊢ (↑(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
have pos : x.val ≤ namedPattern k (n + 1) h / 2 → (↑(↑x.val : ℤ) : ZMod (namedPattern k (n + 1) h)) = x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑(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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
k n : ℕ
h : k = n + 1
x : ZMod (namedPattern k (n + 1) h)
h_1 : x.val ≤ namedPattern k (n + 1) h / 2
⊢ (↑(↑x.val : ℤ) : ZMod (namedPattern k (n + 1) h)) = x
have pos : (↑x.val : ZMod (namedPattern k (n + 1) h)) = x
Tactic: rw [Int.cast_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑(↑x.val : ℤ) : ZMod (namedPattern k (n + 1) h)) = x
have pos₁ : x = x
Tactic: rw [Int.cast_natCast, natCast_zmod_val]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
k n : ℕ
h : k = n + 1
x : ZMod (namedPattern k (n + 1) h)
h_1 : ¬x.val ≤ namedPattern k (n + 1) h / 2
⊢ (↑(HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑(namedPattern k (n + 1) h) : ℤ)) : ZMod (namedPattern k (n + 1) h)) = x
have 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
Tactic: rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
        sub_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑(HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑(namedPattern k (n + 1) h) : ℤ)) : ZMod (namedPattern k (n + 1) h)) = x
have 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
Tactic: rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
        sub_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑(HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑(namedPattern k (n + 1) h) : ℤ)) : ZMod (namedPattern k (n + 1) h)) = x
have neg₂ : x - (↑(↑(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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑(HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑(namedPattern k (n + 1) h) : ℤ)) : ZMod (namedPattern k (n + 1) h)) = x
have neg₃ : x - (↑(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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑(HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑(namedPattern k (n + 1) h) : ℤ)) : ZMod (namedPattern k (n + 1) h)) = x
have neg₄ : x - 0 = x
Tactic: rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
        sub_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (↑(HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑(namedPattern k (n + 1) h) : ℤ)) : ZMod (namedPattern k (n + 1) h)) = x
have neg₅ : x = x
Tactic: rw [Int.cast_sub, Int.cast_natCast, natCast_zmod_val, Int.cast_natCast, natCast_self,
        sub_zero]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
⊢ 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2
have rw : (0 ≤ if x.val ≤ n / 2 then (↑x.val : ℤ) else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ)) ↔ x.val ≤ n / 2
Tactic: rw [valMinAbs_def_pos]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
⊢ (0 ≤ if x.val ≤ n / 2 then (↑x.val : ℤ) else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ)) ↔ x.val ≤ n / 2
have pos : ∀ (h : x.val ≤ n / 2), LE.le (α := ℤ) 0 (↑x.val : ℤ) ↔ 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
pos : ∀ (h : x.val ≤ n / 2), LE.le (α := ℤ) 0 (↑x.val : ℤ) ↔ x.val ≤ n / 2
⊢ (0 ≤ if x.val ≤ n / 2 then (↑x.val : ℤ) else HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ)) ↔ x.val ≤ n / 2
have neg : ∀ (h : ¬x.val ≤ n / 2), 0 ≤ HSub.hSub (α := ℤ) (↑x.val : ℤ) (↑n : ℤ) ↔ x.val ≤ n / 2
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
⊢ a.valMinAbs * 2 = (↑n : ℤ) ↔ 2 * a.val = n
have zero : ∀ (a : ZMod 0), a.valMinAbs * 2 = (↑0 : ℤ) ↔ 2 * a.val = 0
Tactic: rcases n with - | n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod n
zero : ∀ (a : ZMod 0), a.valMinAbs * 2 = (↑0 : ℤ) ↔ 2 * a.val = 0
⊢ a.valMinAbs * 2 = (↑n : ℤ) ↔ 2 * a.val = n
have succ : ∀ (n : ℕ) (a : ZMod (n + 1)), a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1
Tactic: rcases n with - | n
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
⊢ a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1
have pos : ∀ (h : a.val ≤ n.succ / 2), a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1
Tactic: by_cases h : a.val ≤ n.succ / 2
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
pos : ∀ (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
have neg : ∀ (h : ¬a.val ≤ n.succ / 2), a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1
Tactic: by_cases h : a.val ≤ n.succ / 2
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ (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
have pos : HMul.hMul (α := ℤ) (↑a.val : ℤ) 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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ (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
have pos₁ : HMul.hMul (α := ℤ) (↑a.val : ℤ) 2 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔ Eq (α := ℤ) (↑(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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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) : ℤ)
⊢ (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
have pos₂ : HMul.hMul (α := ℤ) (↑a.val : ℤ) 2 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
  HMul.hMul (α := ℤ) (↑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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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) : ℤ)
⊢ (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
have pos₃ : HMul.hMul (α := ℤ) (↑a.val : ℤ) 2 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔ HMul.hMul (α := ℤ) 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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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) : ℤ)
⊢ (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
have pos₄ : HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔ HMul.hMul (α := ℤ) 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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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) : ℤ)
⊢ (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
have pos₅ : HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
  HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ)
Tactic: rw [if_pos h, ← Int.natCast_inj, Nat.cast_mul, Nat.cast_two, mul_comm, Int.natCast_add,
      Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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 : ℤ)
⊢ (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
have pos₆ : HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
  HMul.hMul (α := ℤ) 2 (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
Tactic: rw [if_pos h, ← Int.natCast_inj, Nat.cast_mul, Nat.cast_two, mul_comm, Int.natCast_add,
      Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1
have apply : ¬a.valMinAbs * 2 = (↑(n + 1) : ℤ)
Tactic: apply iff_of_false _ (mt _ h)
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
apply : ¬a.valMinAbs * 2 = (↑(n + 1) : ℤ)
⊢ a.valMinAbs * 2 = (↑(n + 1) : ℤ) ↔ 2 * a.val = n + 1
have apply₁ : 2 * a.val = n + 1 → a.val ≤ n.succ / 2
Tactic: apply iff_of_false _ (mt _ h)
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
he : a.valMinAbs * 2 = (↑(n + 1) : ℤ)
⊢ False
have rw : ∀ (h : ¬0 ≤ a.valMinAbs) (h : ¬LE.le (α := ℤ) 0 (↑(n + 1) : ℤ)) (he : a.valMinAbs * 2 = (↑(n + 1) : ℤ)), False
Tactic: rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h
Cleared hypotheses: h, he
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ False
have rw₁ : ∀ (h : ¬0 ≤ a.valMinAbs) (he : a.valMinAbs * 2 = (↑(n + 1) : ℤ)), LT.lt (α := ℤ) 0 2
Tactic: rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h
Cleared hypotheses: h, he
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2
have rw : a.val * 2 = n + 1 → a.val ≤ n.succ / 2
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
x : ZMod n
⊢ Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (x.valMinAbs * 2)
have 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)
Tactic: simp_rw [valMinAbs_def_pos, 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
⊢ 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 pos : ∀ (h : HMul.hMul (α := ℤ) (↑x.val : ℤ) 2 ≤ (↑n : ℤ)),
  Membership.mem (γ := Set ℤ) (Set.Ioc (-(↑n : ℤ)) (↑n : ℤ)) (HMul.hMul (α := ℤ) (↑x.val : ℤ) 2)
Tactic: split_ifs with h