awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
x : ZMod n
⊢ x.valMinAbs = 0 ↔ x = 0

Tactic:
injective_valMinAbs.eq_iff' <| valMinAbs_zero _

Premises used: ZMod.injective_valMinAbs, ZMod.valMinAbs_zero, Function.Injective.eq_iff'
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
rw : a.val ≤ n
⊢ HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0

Tactic:
rw [sub_nonpos, Int.ofNat_le]

Premises used: sub_nonpos, Int.ofNat_le
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ a.val ≤ n

Tactic:
a.val_le

Premises used: ZMod.val_le
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ a.val ≤ n

Tactic:
exact a.val_le

Premises used: ZMod.val_le
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0

Tactic:
have : (a.val : ℤ) - n ≤ 0 := by
    rw [sub_nonpos, Int.ofNat_le]
    exact a.val_le
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
this : HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) ≤ 0
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
⊢ (↑a.valMinAbs.natAbs : ZMod n) = if a.val ≤ n / 2 then a else -a

Tactic:
rw [valMinAbs_def_pos]

Premises used: ZMod.valMinAbs_def_pos
-- Module: Mathlib.Data.ZMod.ValMinAbs
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
neg : ¬a.val ≤ n / 2 → (↑(HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs : 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

Tactic:
split_ifs
-- Module: Mathlib.Data.ZMod.ValMinAbs
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
pos₁ pos₂ : a = a
⊢ (↑(Int.natAbs (↑a.val : ℤ)) : ZMod n) = a

Tactic:
rw [Int.natAbs_natCast, natCast_zmod_val]

Premises used: ZMod.natCast_zmod_val, Int.natAbs_natCast
-- Module: Mathlib.Data.ZMod.ValMinAbs
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
neg₈ neg₉ : -a = -a
⊢ (↑(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]

Premises used: Int.cast_neg, Int.cast_natCast, ZMod.natCast_self, sub_zero, Int.cast_sub, ZMod.natCast_zmod_val, Int.ofNat_natAbs_of_nonpos
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
inl : ∀ {a : ZMod 0} (ha : 2 * a.val ≠ 0), (-a).valMinAbs = -a.valMinAbs
inr : ∀ (h : NeZero n), (-a).valMinAbs = -a.valMinAbs
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
rcases eq_zero_or_neZero n with rfl | h

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
a : ZMod 0
ha : 2 * a.val ≠ 0
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
(valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩

Premises used: Iff.mpr, And.intro, ZMod.valMinAbs_spec
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
inr : -a = (↑(-a.valMinAbs) : ZMod n)
inr₁ : -(↑n : ℤ) < -a.valMinAbs * 2
inr₂ : -a.valMinAbs * 2 ≤ (↑n : ℤ)
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩

Premises used: Iff.mpr, And.intro, ZMod.valMinAbs_spec
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
inr : -a = -(↑a.valMinAbs : ZMod n)
inr₁ inr₂ : -a = -a
⊢ -a = (↑(-a.valMinAbs) : ZMod n)

Tactic:
rw [Int.cast_neg, coe_valMinAbs]

Premises used: Int.cast_neg, ZMod.coe_valMinAbs
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
inr : a.valMinAbs * 2 < (↑n : ℤ)
⊢ -(↑n : ℤ) < -a.valMinAbs * 2

Tactic:
rw [neg_mul, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, neg_mul
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ a.valMinAbs * 2 < (↑n : ℤ)

Tactic:
a.valMinAbs_mem_Ioc.2.lt_of_ne (mt a.valMinAbs_mul_two_eq_iff.1 ha)

Premises used: ZMod.valMinAbs_mem_Ioc, mt, ZMod.valMinAbs_mul_two_eq_iff, LE.le.lt_of_ne, And.right, Iff.mp
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ a.valMinAbs * 2 < (↑n : ℤ)

Tactic:
exact a.valMinAbs_mem_Ioc.2.lt_of_ne (mt a.valMinAbs_mul_two_eq_iff.1 ha)

Premises used: ZMod.valMinAbs_mem_Ioc, mt, ZMod.valMinAbs_mul_two_eq_iff, LE.le.lt_of_ne, And.right, Iff.mp
-- Module: Mathlib.Data.ZMod.ValMinAbs
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
linarith₁ : (↑n : ℤ) < -a.valMinAbs * 2 → GT.gt (α := ℤ) 2 0
⊢ -a.valMinAbs * 2 ≤ (↑n : ℤ)

Tactic:
linarith only [a.valMinAbs_mem_Ioc.1]

Premises used: ZMod.valMinAbs_mem_Ioc, And.left
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
pos : ∀ (h2a : 2 * a.val = n), (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
neg : ∀ (h2a : ¬2 * a.val = n), (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
by_cases h2a : 2 * a.val = n

Premises used: ZMod.val
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
pos pos₁ : a.valMinAbs.natAbs = a.valMinAbs.natAbs
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
rw [a.neg_eq_self_iff.2 (Or.inr h2a)]

Premises used: Iff.mpr, ZMod.neg_eq_self_iff, Or.inr
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
h2a : ¬2 * a.val = n
neg : (-a.valMinAbs).natAbs = a.valMinAbs.natAbs
neg₁ neg₂ : a.valMinAbs.natAbs = a.valMinAbs.natAbs
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]

Premises used: ZMod.valMinAbs_neg_of_ne_half, Int.natAbs_neg
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
mp : a.valMinAbs.natAbs = b.valMinAbs.natAbs → a = b ∨ a = -b
mpr : a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a = b ∨ a = -b

Tactic:
constructor
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
mp : a = b ∨ a.valMinAbs = -b.valMinAbs → a = b ∨ a = -b
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs → a = b ∨ a = -b

Tactic:
rw [Int.natAbs_eq_natAbs_iff, valMinAbs_inj]

Premises used: Int.natAbs_eq_natAbs_iff, ZMod.valMinAbs_inj
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
⊢ a = b ∨ a.valMinAbs = -b.valMinAbs → a = b ∨ a = -b

Tactic:
Or.imp_right eq_neg_of_valMinAbs_eq_neg_valMinAbs

Premises used: ZMod.eq_neg_of_valMinAbs_eq_neg_valMinAbs, Or.imp_right
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
⊢ a = b ∨ a.valMinAbs = -b.valMinAbs → a = b ∨ a = -b

Tactic:
exact Or.imp_right eq_neg_of_valMinAbs_eq_neg_valMinAbs

Premises used: ZMod.eq_neg_of_valMinAbs_eq_neg_valMinAbs, Or.imp_right
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a : ZMod n
⊢ a.valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
b : ZMod n
mpr mpr₁ : b.valMinAbs.natAbs = b.valMinAbs.natAbs
⊢ (-b).valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
rw [natAbs_valMinAbs_neg]

Premises used: ZMod.natAbs_valMinAbs_neg
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
rw : Eq (α := ℤ) (↑a.valMinAbs.natAbs : ℤ) (↑b.valMinAbs.natAbs : ℤ) ↔ a.valMinAbs.natAbs = b.valMinAbs.natAbs
⊢ |a.valMinAbs| = |b.valMinAbs| ↔ a = b ∨ a = -b

Tactic:
rw [← natAbs_valMinAbs_eq_natAbs_valMinAbs, Int.abs_eq_natAbs, Int.abs_eq_natAbs]

Premises used: ZMod.natAbs_valMinAbs_eq_natAbs_valMinAbs, Int.abs_eq_natAbs
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a.valMinAbs.natAbs = b.valMinAbs.natAbs
⊢ Eq (α := ℤ) (↑a.valMinAbs.natAbs : ℤ) (↑b.valMinAbs.natAbs : ℤ) ↔ a.valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
norm_cast
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
rw :
  (↑a.val : ℤ) =
    (if a.val ≤ n / 2 then (↑a.val : ℤ) else HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) +
      (↑(if a.val ≤ n / 2 then 0 else n) : ℤ)
⊢ (↑a.val : ℤ) = a.valMinAbs + (↑(if a.val ≤ n / 2 then 0 else n) : ℤ)

Tactic:
rw [valMinAbs_def_pos]

Premises used: ZMod.valMinAbs_def_pos
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
pos : a.val ≤ n / 2 → (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑a.val : ℤ) (↑0 : ℤ)
neg : ¬a.val ≤ n / 2 → (↑a.val : ℤ) = HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) + (↑n : ℤ)
⊢ (↑a.val : ℤ) =
    (if a.val ≤ n / 2 then (↑a.val : ℤ) else HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)) +
      (↑(if a.val ≤ n / 2 then 0 else n) : ℤ)

Tactic:
split_ifs
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : a.val ≤ n / 2
⊢ (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑a.val : ℤ) (↑0 : ℤ)

Tactic:
simp [add_zero, sub_add_cancel]

Premises used: add_zero, sub_add_cancel
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
h : ¬a.val ≤ n / 2
⊢ (↑a.val : ℤ) = HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) + (↑n : ℤ)

Tactic:
simp [add_zero, sub_add_cancel]

Premises used: add_zero, sub_add_cancel
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
hpq : p ≠ q
rwa : Ne (α := ZMod p) (↑q : ZMod p) (↑0 : ZMod p)
rwa₁ : ¬Eq (α := ZMod p) (↑q : ZMod p) (↑0 : ZMod p)
rwa₂ : ¬q ≡ 0 [MOD p]
rwa₃ : ¬p ∣ q
rwa₄ : p.Coprime q
rwa₅ rwa₆ rwa₇ rwa₈ : p ≠ q
⊢ Ne (α := ZMod p) (↑q : ZMod p) 0

Tactic:
rwa [← Nat.cast_zero, Ne, natCast_eq_natCast_iff, Nat.modEq_zero_iff_dvd,
    ← hp.1.coprime_iff_not_dvd, Nat.coprime_primes hp.1 hq.1]

Premises used: Ne, ZMod.natCast_eq_natCast_iff, Nat.cast_zero, Nat.modEq_zero_iff_dvd, Nat.Prime.coprime_iff_not_dvd, Fact.out, Nat.coprime_primes
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
hpos : NeZero n
a : ZMod n
rw : (if a.val ≤ n / 2 then (↑a.val : ℤ) else HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs = min a.val (n - a.val)
⊢ a.valMinAbs.natAbs = min a.val (n - a.val)

Tactic:
rw [valMinAbs_def_pos]

Premises used: ZMod.valMinAbs_def_pos
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
hpos : NeZero n
a : ZMod n
⊢ a.val < n

Tactic:
have := a.val_lt
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
hpos : NeZero n
a : ZMod n
this : a.val < n
⊢ (if a.val ≤ n / 2 then (↑a.val : ℤ) else HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs = min a.val (n - a.val)

Tactic:
omega
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n a : ℕ
ha : a ≤ n / 2
zero : ∀ (ha : a ≤ 0 / 2), valMinAbs (n := 0) (↑a : ZMod 0) = (↑a : ℤ)
succ : ∀ (n : ℕ) (ha : a ≤ (n + 1) / 2), valMinAbs (n := n + 1) (↑a : ZMod (n + 1)) = (↑a : ℤ)
⊢ valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ)

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
a : ℕ
ha : a ≤ 0 / 2
⊢ valMinAbs (n := 0) (↑a : ZMod 0) = (↑a : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
a n : ℕ
ha : a ≤ (n + 1) / 2
⊢ valMinAbs (n := n + 1) (↑a : ZMod (n + 1)) = (↑a : ℤ)

Tactic:
simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
      ha]

Premises used: ZMod.valMinAbs_def_pos, Nat.mod_eq_of_lt, Nat.div_lt_self', ZMod.val_natCast, OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n a : ℕ
ha : n / 2 < a
ha' : a < n
zero : ∀ (ha : 0 / 2 < a) (ha' : a < 0), valMinAbs (n := 0) (↑a : ZMod 0) = HSub.hSub (α := ℤ) (↑a : ℤ) (↑0 : ℤ)
succ :
  ∀ (n : ℕ) (ha : (n + 1) / 2 < a) (ha' : a < n + 1),
    valMinAbs (n := n + 1) (↑a : ZMod (n + 1)) = HSub.hSub (α := ℤ) (↑a : ℤ) (↑(n + 1) : ℤ)
⊢ valMinAbs (n := n) (↑a : ZMod n) = HSub.hSub (α := ℤ) (↑a : ℤ) (↑n : ℤ)

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
a : ℕ
ha : 0 / 2 < a
ha' : a < 0
⊢ valMinAbs (n := 0) (↑a : ZMod 0) = HSub.hSub (α := ℤ) (↑a : ℤ) (↑0 : ℤ)

Tactic:
cases not_lt_bot ha'

Premises used: not_lt_bot
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
a n : ℕ
ha : (n + 1) / 2 < a
ha' : a < n + 1
⊢ valMinAbs (n := n + 1) (↑a : ZMod (n + 1)) = HSub.hSub (α := ℤ) (↑a : ℤ) (↑(n + 1) : ℤ)

Tactic:
simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt ha', ha.not_ge]

Premises used: ZMod.valMinAbs_def_pos, Nat.mod_eq_of_lt, ZMod.val_natCast, LT.lt.not_ge
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n a : ℕ
inst : NeZero n
⊢ valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ) ↔ a ≤ n / 2

Tactic:
⟨fun ha => ?_, valMinAbs_natCast_of_le_half⟩

Premises used: ZMod.valMinAbs_natCast_of_le_half, Iff.intro
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n a : ℕ
inst : NeZero n
refine : ∀ (ha : valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ)), a ≤ n / 2
⊢ valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ) ↔ a ≤ n / 2

Tactic:
refine ⟨fun ha => ?_, valMinAbs_natCast_of_le_half⟩
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n a : ℕ
inst : NeZero n
ha : valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ)
rw : (valMinAbs (n := n) (↑a : ZMod n)).natAbs ≤ n / 2
⊢ a ≤ n / 2

Tactic:
rw [← Int.natAbs_natCast a, ← ha]

Premises used: Int.natAbs_natCast
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n a : ℕ
inst : NeZero n
ha : valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ)
⊢ (valMinAbs (n := n) (↑a : ZMod n)).natAbs ≤ n / 2

Tactic:
natAbs_valMinAbs_le (n := n) a

Premises used: Nat.cast, ZMod.natAbs_valMinAbs_le
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n a : ℕ
inst : NeZero n
ha : valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ)
⊢ (valMinAbs (n := n) (↑a : ZMod n)).natAbs ≤ n / 2

Tactic:
exact natAbs_valMinAbs_le (n := n) a

Premises used: Nat.cast, ZMod.natAbs_valMinAbs_le
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod n
zero : ∀ (a b : ZMod 0), (a + b).valMinAbs.natAbs ≤ (a + b).valMinAbs.natAbs
succ : ∀ (n : ℕ) (a b : ZMod (n + 1)), (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
a b : ZMod 0
⊢ (a + b).valMinAbs.natAbs ≤ (a + b).valMinAbs.natAbs

Tactic:
rfl
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod (n + 1)
succ : Eq (α := ZMod n.succ) (↑(a + b).valMinAbs : ZMod n.succ) (↑(a.valMinAbs + b.valMinAbs) : ZMod n.succ)
succ₁ : (a + b).valMinAbs.natAbs ≤ n.succ / 2
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Tactic:
apply natAbs_min_of_le_div_two n.succ

Premises used: ZMod.natAbs_min_of_le_div_two, Nat.succ
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod (n + 1)
succ :
  (↑(a + b).valMinAbs : ZMod n.succ) =
    HAdd.hAdd (α := ZMod n.succ) (↑a.valMinAbs : ZMod n.succ) (↑b.valMinAbs : ZMod n.succ)
⊢ Eq (α := ZMod n.succ) (↑(a + b).valMinAbs : ZMod n.succ) (↑(a.valMinAbs + b.valMinAbs) : ZMod n.succ)

Tactic:
simp_rw [Int.cast_add, coe_valMinAbs]

Premises used: Int.cast_add, ZMod.coe_valMinAbs
-- Module: Mathlib.Data.ZMod.ValMinAbs
Goal:
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ n.succ / 2

Tactic:
apply natAbs_valMinAbs_le

Premises used: ZMod.natAbs_valMinAbs_le
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g : α → M
x : α
⊢ birkhoffAverage R f g 0 x = 0

Tactic:
simp [birkhoffAverage]

Premises used: birkhoffAverage
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g : α → M
⊢ birkhoffAverage R f g 0 = 0

Tactic:
funext <| birkhoffAverage_zero _ _ _

Premises used: birkhoffAverage_zero, funext
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g : α → M
x : α
⊢ birkhoffAverage R f g 1 x = g x

Tactic:
simp [birkhoffAverage]

Premises used: birkhoffAverage
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g : α → M
⊢ birkhoffAverage R f g 1 = g

Tactic:
funext <| birkhoffAverage_one R f g

Premises used: funext, birkhoffAverage_one
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
F : Type u_5
N : Type u_6
inst_3 : DivisionSemiring S
inst_4 : AddCommMonoid N
inst_5 : Module S N
inst_6 : FunLike F M N
inst_7 : AddMonoidHomClass F M N
g' : F
f : α → α
g : α → M
n : ℕ
x : α
⊢ Eq.{u_6 + 1} (α := N) ((g' : (a : M) → N) (birkhoffAverage R f g n x) : N)
    (birkhoffAverage S f ((⇑g' : (a : M) → N) ∘ g) n x : N)

Tactic:
simp only [birkhoffAverage, map_inv_natCast_smul g' R S, map_birkhoffSum]

Premises used: map_birkhoffSum, map_inv_natCast_smul, birkhoffAverage
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : DivisionSemiring S
inst_4 : Module S M
f : α → α
g : α → M
n : ℕ
x : α
⊢ birkhoffAverage R f g n x = birkhoffAverage S f g n x

Tactic:
map_birkhoffAverage R S (AddMonoidHom.id M) f g n x

Premises used: map_birkhoffAverage, AddMonoidHom.id, birkhoffAverage
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : DivisionSemiring S
inst_4 : Module S M
h : ∀ (x : α → α) (x_1 : α → M) (x_2 : ℕ) (x_3 : α), birkhoffAverage R x x_1 x_2 x_3 = birkhoffAverage S x x_1 x_2 x_3
⊢ Eq (α := (f : α → α) → (g : α → M) → (n : ℕ) → (x : α) → M) (birkhoffAverage R) (birkhoffAverage S)

Tactic:
ext
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : DivisionSemiring S
inst_4 : Module S M
x : α → α
x_1 : α → M
x_2 : ℕ
x_3 : α
⊢ birkhoffAverage R x x_1 x_2 x_3 = birkhoffAverage S x x_1 x_2 x_3

Tactic:
apply birkhoffAverage_congr_ring

Premises used: birkhoffAverage_congr_ring
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : Ne.{u_1 + 1} (α := R) (↑n : R) 0
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (birkhoffSum f g n x) = g x
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x
rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) (g x)) = g x
rw₃ rw₄ : g x = g x
⊢ birkhoffAverage R f g n x = g x

Tactic:
rw [birkhoffAverage, h.birkhoffSum_eq, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀ hn]

Premises used: inv_smul_smul₀, birkhoffAverage, Nat.cast_smul_eq_nsmul, Function.IsFixedPt.birkhoffSum_eq
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g g' : α → M
h : ∀ (x : ℕ) (x_1 : α), birkhoffAverage R f (g + g') x x_1 = (birkhoffAverage R f g + birkhoffAverage R f g') x x_1
⊢ birkhoffAverage R f (g + g') = birkhoffAverage R f g + birkhoffAverage R f g'

Tactic:
funext _ x
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g g' : α → M
x_1 : ℕ
x : α
⊢ birkhoffAverage R f (g + g') x_1 x = (birkhoffAverage R f g + birkhoffAverage R f g') x_1 x

Tactic:
simp [birkhoffAverage, birkhoffSum, sum_add_distrib, smul_add]

Premises used: Finset.sum_add_distrib, birkhoffAverage, birkhoffSum, smul_add
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g : α → M
h : g ∘ f = g
n : ℕ
hn : Ne.{u_1 + 1} (α := R) (↑n : R) 0
h₁ : ∀ (x : α), birkhoffAverage R f g n x = g x
⊢ birkhoffAverage R f g n = g

Tactic:
funext x
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g : α → M
h : g ∘ f = g
n : ℕ
hn : Ne.{u_1 + 1} (α := R) (↑n : R) 0
x : α
this : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x
⊢ birkhoffAverage R f g n x = g x

Tactic:
simpa [birkhoffAverage, birkhoffSum_of_comp_eq h]

Premises used: birkhoffSum_of_comp_eq, birkhoffAverage
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g : α → M
h : g ∘ f = g
n : ℕ
hn : Ne.{u_1 + 1} (α := R) (↑n : R) 0
x : α
h₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x
⊢ birkhoffAverage R f g n x = g x

Tactic:
suffices (n : R)⁻¹ • n • g x = g x by simpa [birkhoffAverage, birkhoffSum_of_comp_eq h]
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α → α
g : α → M
h : g ∘ f = g
n : ℕ
hn : Ne.{u_1 + 1} (α := R) (↑n : R) 0
x : α
h₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) (g x)) = g x
h₂ : HMul.hMul (α := R) (↑n : R)⁻¹ (↑n : R) • g x = g x
h₃ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (g x) = g x
h₄ h₅ : g x = g x
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x

Tactic:
rw [← Nat.cast_smul_eq_nsmul (R := R), ← mul_smul, inv_mul_cancel₀ hn, one_smul]

Premises used: one_smul, Nat.cast_smul_eq_nsmul, inv_mul_cancel₀, SemigroupAction.mul_smul
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : α → α
g : α → M
h : ∀ (x : ℕ) (x_1 : α), birkhoffAverage R f (-g) x x_1 = (-birkhoffAverage R f g) x x_1
⊢ birkhoffAverage R f (-g) = -birkhoffAverage R f g

Tactic:
funext _ x
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : α → α
g : α → M
x_1 : ℕ
x : α
⊢ birkhoffAverage R f (-g) x_1 x = (-birkhoffAverage R f g) x_1 x

Tactic:
simp [birkhoffAverage, birkhoffSum]

Premises used: birkhoffAverage, birkhoffSum
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : α → α
g g' : α → M
h : ∀ (x : ℕ) (x_1 : α), birkhoffAverage R f (g - g') x x_1 = (birkhoffAverage R f g - birkhoffAverage R f g') x x_1
⊢ birkhoffAverage R f (g - g') = birkhoffAverage R f g - birkhoffAverage R f g'

Tactic:
funext _ x
-- Module: Mathlib.Dynamics.BirkhoffSum.Average
Goal:
R : Type u_1
α : Type u_2
M : Type u_3
inst : DivisionSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : α → α
g g' : α → M
x_1 : ℕ
x : α
⊢ birkhoffAverage R f (g - g') x_1 x = (birkhoffAverage R f g - birkhoffAverage R f g') x_1 x

Tactic:
simp [birkhoffAverage, birkhoffSum, smul_sub]

Premises used: birkhoffAverage, birkhoffSum, smul_sub