Theorem: IntegersInACircle.lemma2 (Compfiles/IntegersInACircle.lean)

State before:
f : ZMod 101 → ℤ
y : ZMod 101
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)
Tactic:
let g := λ (i:ℕ) ↦ y + (i:ZMod 101)
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)
Tactic:
have hg: ∀ (x : ℕ),
    x ∈ Finset.range 101 → ∀ (y : ℕ), y ∈ Finset.range 101 → g x = g y → x = y := by
  intro a ha b hb hgab
  dsimp [g] at hgab
  have h5 : (a : ZMod 101) = (b : ZMod 101) := by linear_combination hgab
  have h8: a % 101 = b % 101 := Iff.mp (ZMod.natCast_eq_natCast_iff' a b 101) h5
  rw [Finset.mem_range] at ha hb
  rwa [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb] at h8
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)
Tactic:
rw[← Finset.sum_image hg]
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∑ z : ZMod 101, f z = ∑ x ∈ Finset.image (fun x => g x) (Finset.range 101), f x

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
h3 : Finset.image g (Finset.range 101) = Finset.univ
⊢ ∑ z : ZMod 101, f z = ∑ x ∈ Finset.image (fun x => g x) (Finset.range 101), f x
Tactic:
rw[h3]
State after:
no goals

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
⊢ ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
Tactic:
intro a ha b hb hgab
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : g a = g b
⊢ a = b

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : g a = g b
⊢ a = b
Tactic:
dsimp [g] at hgab
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
⊢ a = b

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
⊢ a = b
Tactic:
have h5 : (a : ZMod 101) = (b : ZMod 101) := by linear_combination hgab
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
⊢ a = b

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
⊢ a = b
Tactic:
have h8: a % 101 = b % 101 := Iff.mp (ZMod.natCast_eq_natCast_iff' a b 101) h5
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b
Tactic:
rw [Finset.mem_range] at ha hb
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a < 101
b : ℕ
hb : b < 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a < 101
b : ℕ
hb : b < 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b
Tactic:
rwa [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb] at h8
State after:
no goals

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
⊢ ↑a = ↑b
Tactic:
linear_combination hgab
State after:
no goals

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ Finset.image g (Finset.range 101) = Finset.univ
Tactic:
rw [Finset.eq_univ_iff_forall]
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∀ (x : ZMod 101), x ∈ Finset.image g (Finset.range 101)

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∀ (x : ZMod 101), x ∈ Finset.image g (Finset.range 101)
Tactic:
intro a
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ a ∈ Finset.image g (Finset.range 101)

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ a ∈ Finset.image g (Finset.range 101)
Tactic:
rw [Finset.mem_image]
State after:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ ∃ a_1 ∈ Finset.range 101, g a_1 = a

State before:
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ ∃ a_1 ∈ Finset.range 101, g a_1 = a
Tactic:
use (a - y).val
State after:
case h
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101 ∧ g (a - y).val = a

State before:
case h
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101 ∧ g (a - y).val = a
Tactic:
constructor
State after:
case h.left
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101

case h.right
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ g (a - y).val = a

State before:
case h.left
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101
Tactic:
exact Finset.mem_range.mpr (ZMod.val_lt (a - y))
State after:
no goals

State before:
case h.right
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ g (a - y).val = a
Tactic:
simp [g]
State after:
no goals