awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = b ∨ a.valMinAbs = -b.valMinAbs → a = b ∨ a = -b
Tactic: rw [Int.natAbs_eq_natAbs_iff, valMinAbs_inj]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
b : ZMod n
⊢ (-b).valMinAbs.natAbs = b.valMinAbs.natAbs
have mpr : b.valMinAbs.natAbs = b.valMinAbs.natAbs
Tactic: rw [natAbs_valMinAbs_neg]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod n
⊢ |a.valMinAbs| = |b.valMinAbs| ↔ a = b ∨ a = -b
have rw : Eq (α := ℤ) (↑a.valMinAbs.natAbs : ℤ) (↑b.valMinAbs.natAbs : ℤ) ↔ a.valMinAbs.natAbs = b.valMinAbs.natAbs
Tactic: rw [← natAbs_valMinAbs_eq_natAbs_valMinAbs, Int.abs_eq_natAbs, Int.abs_eq_natAbs]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod n
⊢ Eq (α := ℤ) (↑a.valMinAbs.natAbs : ℤ) (↑b.valMinAbs.natAbs : ℤ) ↔ a.valMinAbs.natAbs = b.valMinAbs.natAbs
have norm_cast : a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a.valMinAbs.natAbs = b.valMinAbs.natAbs
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ (↑a.val : ℤ) = a.valMinAbs + (↑(if a.val ≤ n / 2 then 0 else n) : ℤ)
have 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) : ℤ)
Tactic: rw [valMinAbs_def_pos]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod 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) : ℤ)
have pos : a.val ≤ n / 2 → (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑a.val : ℤ) (↑0 : ℤ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
pos : a.val ≤ n / 2 → (↑a.val : ℤ) = HAdd.hAdd (α := ℤ) (↑a.val : ℤ) (↑0 : ℤ)
⊢ (↑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) : ℤ)
have neg : ¬a.val ≤ n / 2 → (↑a.val : ℤ) = HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ) + (↑n : ℤ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
hpq : p ≠ q
⊢ Ne (α := ZMod p) (↑q : ZMod p) 0
have rwa : Ne (α := ZMod p) (↑q : ZMod p) (↑0 : ZMod p)
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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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)
⊢ Ne (α := ZMod p) (↑q : ZMod p) 0
have rwa₁ : ¬Eq (α := ZMod p) (↑q : ZMod p) (↑0 : ZMod p)
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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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)
⊢ Ne (α := ZMod p) (↑q : ZMod p) 0
have rwa₂ : ¬q ≡ 0 [MOD p]
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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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]
⊢ Ne (α := ZMod p) (↑q : ZMod p) 0
have rwa₃ : ¬p ∣ q
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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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
⊢ Ne (α := ZMod p) (↑q : ZMod p) 0
have rwa₄ : p.Coprime q
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]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
hpos : NeZero n
a : ZMod n
⊢ a.valMinAbs.natAbs = min a.val (n - a.val)
have rw : (if a.val ≤ n / 2 then (↑a.val : ℤ) else HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs = min a.val (n - a.val)
Tactic: rw [valMinAbs_def_pos]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (hypothesis)
Goal:
n : ℕ
hpos : NeZero n
a : ZMod n
⊢ (if a.val ≤ n / 2 then (↑a.val : ℤ) else HSub.hSub (α := ℤ) (↑a.val : ℤ) (↑n : ℤ)).natAbs = min a.val (n - a.val)
have this : a.val < n
Tactic: have := a.val_lt
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n a : ℕ
ha : a ≤ n / 2
⊢ valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ)
have zero : ∀ (ha : a ≤ 0 / 2), valMinAbs (n := 0) (↑a : ZMod 0) = (↑a : ℤ)
Tactic: cases n
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n a : ℕ
ha : a ≤ n / 2
zero : ∀ (ha : a ≤ 0 / 2), valMinAbs (n := 0) (↑a : ZMod 0) = (↑a : ℤ)
⊢ valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ)
have succ : ∀ (n : ℕ) (ha : a ≤ (n + 1) / 2), valMinAbs (n := n + 1) (↑a : ZMod (n + 1)) = (↑a : ℤ)
Tactic: cases n
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n a : ℕ
ha : n / 2 < a
ha' : a < n
⊢ valMinAbs (n := n) (↑a : ZMod n) = HSub.hSub (α := ℤ) (↑a : ℤ) (↑n : ℤ)
have zero : ∀ (ha : 0 / 2 < a) (ha' : a < 0), valMinAbs (n := 0) (↑a : ZMod 0) = HSub.hSub (α := ℤ) (↑a : ℤ) (↑0 : ℤ)
Tactic: cases n
Cleared hypotheses: n, ha, ha'
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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 : ℤ)
⊢ valMinAbs (n := n) (↑a : ZMod n) = HSub.hSub (α := ℤ) (↑a : ℤ) (↑n : ℤ)
have succ : ∀ (n : ℕ) (ha : (n + 1) / 2 < a) (ha' : a < n + 1),
  valMinAbs (n := n + 1) (↑a : ZMod (n + 1)) = HSub.hSub (α := ℤ) (↑a : ℤ) (↑(n + 1) : ℤ)
Tactic: cases n
Cleared hypotheses: n, ha, ha'
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n a : ℕ
inst : NeZero n
⊢ valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ) ↔ a ≤ n / 2
have refine : ∀ (ha : valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ)), a ≤ n / 2
Tactic: refine ⟨fun ha => ?_, valMinAbs_natCast_of_le_half⟩
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n a : ℕ
inst : NeZero n
ha : valMinAbs (n := n) (↑a : ZMod n) = (↑a : ℤ)
⊢ a ≤ n / 2
have rw : (valMinAbs (n := n) (↑a : ZMod n)).natAbs ≤ n / 2
Tactic: rw [← Int.natAbs_natCast a, ← ha]
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod n
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
have zero : ∀ (a b : ZMod 0), (a + b).valMinAbs.natAbs ≤ (a + b).valMinAbs.natAbs
Tactic: rcases n with - | n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod n
zero : ∀ (a b : ZMod 0), (a + b).valMinAbs.natAbs ≤ (a + b).valMinAbs.natAbs
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
have succ : ∀ (n : ℕ) (a b : ZMod (n + 1)), (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
Tactic: rcases n with - | n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
have succ : Eq (α := ZMod n.succ) (↑(a + b).valMinAbs : ZMod n.succ) (↑(a.valMinAbs + b.valMinAbs) : ZMod n.succ)
Tactic: apply natAbs_min_of_le_div_two n.succ
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
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)
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
have succ₁ : (a + b).valMinAbs.natAbs ≤ n.succ / 2
Tactic: apply natAbs_min_of_le_div_two n.succ
-- Lean 4 proof step from Mathlib.Data.ZMod.ValMinAbs (goal)
Goal:
n : ℕ
a b : ZMod (n + 1)
⊢ Eq (α := ZMod n.succ) (↑(a + b).valMinAbs : ZMod n.succ) (↑(a.valMinAbs + b.valMinAbs) : ZMod n.succ)
have succ : (↑(a + b).valMinAbs : ZMod n.succ) =
  HAdd.hAdd (α := ZMod n.succ) (↑a.valMinAbs : ZMod n.succ) (↑b.valMinAbs : ZMod n.succ)
Tactic: simp_rw [Int.cast_add, coe_valMinAbs]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ Eq (α := (f : α → α) → (g : α → M) → (n : ℕ) → (x : α) → M) (birkhoffAverage R) (birkhoffAverage S)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ birkhoffAverage R f g n x = g x
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (birkhoffSum f g n x) = g x
Tactic: rw [birkhoffAverage, h.birkhoffSum_eq, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀ hn]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ birkhoffAverage R f g n x = g x
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x
Tactic: rw [birkhoffAverage, h.birkhoffSum_eq, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀ hn]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ birkhoffAverage R f g n x = g x
have 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
Tactic: rw [birkhoffAverage, h.birkhoffSum_eq, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀ hn]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ birkhoffAverage R f g n x = g x
have rw₃ : g x = g x
Tactic: rw [birkhoffAverage, h.birkhoffSum_eq, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀ hn]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ birkhoffAverage R f (g + g') = birkhoffAverage R f g + birkhoffAverage R f g'
have h : ∀ (x : ℕ) (x_1 : α), birkhoffAverage R f (g + g') x x_1 = (birkhoffAverage R f g + birkhoffAverage R f g') x x_1
Tactic: funext _ x
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ birkhoffAverage R f g n = g
have h₁ : ∀ (x : α), birkhoffAverage R f g n x = g x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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 : α
⊢ birkhoffAverage R f g n x = g x
have h₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x
Tactic: suffices (n : R)⁻¹ • n • g x = g x by simpa [birkhoffAverage, birkhoffSum_of_comp_eq h]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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 : α
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x
have 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
Tactic: rw [← Nat.cast_smul_eq_nsmul (R := R), ← mul_smul, inv_mul_cancel₀ hn, one_smul]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x
have h₂ : HMul.hMul (α := R) (↑n : R)⁻¹ (↑n : R) • g x = g x
Tactic: rw [← Nat.cast_smul_eq_nsmul (R := R), ← mul_smul, inv_mul_cancel₀ hn, one_smul]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x
have h₃ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (g x) = g x
Tactic: rw [← Nat.cast_smul_eq_nsmul (R := R), ← mul_smul, inv_mul_cancel₀ hn, one_smul]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R)⁻¹ (n • g x) = g x
have h₄ : g x = g x
Tactic: rw [← Nat.cast_smul_eq_nsmul (R := R), ← mul_smul, inv_mul_cancel₀ hn, one_smul]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ birkhoffAverage R f (-g) = -birkhoffAverage R f g
have h : ∀ (x : ℕ) (x_1 : α), birkhoffAverage R f (-g) x x_1 = (-birkhoffAverage R f g) x x_1
Tactic: funext _ x
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Average (goal)
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
⊢ birkhoffAverage R f (g - g') = birkhoffAverage R f g - birkhoffAverage R f g'
have h : ∀ (x : ℕ) (x_1 : α), birkhoffAverage R f (g - g') x x_1 = (birkhoffAverage R f g - birkhoffAverage R f g') x x_1
Tactic: funext _ x
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
⊢ birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)
have simp_rw : ∑ k ∈ range (m + n), g (f^[k] x) = HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ k ∈ range n, g (f^[k] (f^[m] x)))
Tactic: simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
simp_rw :
  ∑ k ∈ range (m + n), g (f^[k] x) =
    HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ k ∈ range n, g (f^[k] (f^[m] x)))
⊢ birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)
have simp_rw₁ : HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ x_1 ∈ range n, g (f^[m + x_1] x)) =
  HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ k ∈ range n, g (f^[k] (f^[m] x)))
Tactic: simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
simp_rw :
  ∑ k ∈ range (m + n), g (f^[k] x) =
    HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ k ∈ range n, g (f^[k] (f^[m] x)))
simp_rw₁ :
  HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ x_1 ∈ range n, g (f^[m + x_1] x)) =
    HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ k ∈ range n, g (f^[k] (f^[m] x)))
⊢ birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)
have simp_rw₂ : HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ x_1 ∈ range n, g (f^[x_1 + m] x)) =
  HAdd.hAdd (α := M) (∑ k ∈ range m, g (f^[k] x)) (∑ k ∈ range n, g (f^[k] (f^[m] x)))
Tactic: simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
⊢ birkhoffSum f φ n = n • φ
have h₁ : ∀ (x : α), birkhoffSum f φ n x = (n • φ) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
x : α
⊢ birkhoffSum f φ n x = (n • φ) x
have h₁ : ∀ (k : ℕ), φ (f^[k] x) = φ x
Tactic: suffices ∀ k, φ (f^[k] x) = φ x by simp [birkhoffSum, this]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
G : Type u_2
inst : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
have rw : birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) = g (f^[n] x) - g x
Tactic: rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x),
    ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x),
    ← sub_add, ← sub_add, sub_add_comm]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
G : Type u_2
inst : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
rw : birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) = g (f^[n] x) - g x
⊢ birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
have rw₁ : birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) =
  g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
Tactic: rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x),
    ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x),
    ← sub_add, ← sub_add, sub_add_comm]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
G : Type u_2
inst : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
rw : birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) = g (f^[n] x) - g x
rw₁ :
  birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
⊢ birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
have rw₂ : birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
  g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
Tactic: rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x),
    ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x),
    ← sub_add, ← sub_add, sub_add_comm]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
G : Type u_2
inst : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
rw : birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) = g (f^[n] x) - g x
rw₁ :
  birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
rw₂ :
  birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
⊢ birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
have rw₃ : birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
  g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x)
Tactic: rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x),
    ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x),
    ← sub_add, ← sub_add, sub_add_comm]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.Basic (goal)
Goal:
α : Type u_1
G : Type u_2
inst : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
rw : birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) = g (f^[n] x) - g x
rw₁ :
  birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
rw₂ :
  birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
rw₃ :
  birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
    g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x)
⊢ birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
have rw₄ : g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x) =
  g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x)
Tactic: rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x),
    ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x),
    ← sub_add, ← sub_add, sub_add_comm]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffSum f g n x) (birkhoffSum f g n y) / (↑n : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) (↑n : ℝ)
have hab : dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)
have rcases : ∀ (C : ℝ) (hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C),
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)
Tactic: rcases Metric.isBounded_range_iff.1 h with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)
have this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
Tactic: have : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) :=
    tendsto_const_nhds.div_atTop tendsto_natCast_atTop_atTop