Theorem: exercise5_3 (LeanCourse/Assignments/Assignment5.lean)

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
⊢ (x + y) ^ p = x ^ p + y ^ p
Tactic:
rw [add_pow]
State after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p
Tactic:
have h2 : p.Prime := hp.out
State after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p
Tactic:
have h3 : 0 < p := h2.pos
State after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p
Tactic:
have h4 : range p = insert 0 (Ioo 0 p)
State after:
case h4
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
⊢ range p = insert 0 (Ioo 0 p)

p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
h4 : range p = insert 0 (Ioo 0 p)
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
h4 : range p = insert 0 (Ioo 0 p)
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p
Tactic:
have h5 : ∀ i ∈ Ioo 0 p, p ∣ Nat.choose p i := by sorry
State after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
h4 : range p = insert 0 (Ioo 0 p)
h5 : ∀ i ∈ Ioo 0 p, p ∣ Nat.choose p i
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
h4 : range p = insert 0 (Ioo 0 p)
h5 : ∀ i ∈ Ioo 0 p, p ∣ Nat.choose p i
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p
Tactic:
have h6 : ∑ i in Ioo 0 p, x ^ i * y ^ (p - i) * Nat.choose p i = 0 :=
calc
  _ =  ∑ i in Ioo 0 p, x ^ i * y ^ (p - i) * 0 := by sorry
  _ = 0 := by sorry
State after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
h4 : range p = insert 0 (Ioo 0 p)
h5 : ∀ i ∈ Ioo 0 p, p ∣ Nat.choose p i
h6 : ∑ i in Ioo 0 p, x ^ i * y ^ (p - i) * ↑(Nat.choose p i) = 0
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
h4 : range p = insert 0 (Ioo 0 p)
h5 : ∀ i ∈ Ioo 0 p, p ∣ Nat.choose p i
h6 : ∑ i in Ioo 0 p, x ^ i * y ^ (p - i) * ↑(Nat.choose p i) = 0
⊢ ∑ m in range (p + 1), x ^ m * y ^ (p - m) * ↑(Nat.choose p m) = x ^ p + y ^ p
Tactic:
sorry
State after:
no goals

State before:
case h4
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
⊢ range p = insert 0 (Ioo 0 p)
Tactic:
ext (_|_) <;> simp [h3]
State after:
no goals

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
h4 : range p = insert 0 (Ioo 0 p)
⊢ ∀ i ∈ Ioo 0 p, p ∣ Nat.choose p i
Tactic:
sorry
State after:
no goals

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
h4 : range p = insert 0 (Ioo 0 p)
h5 : ∀ i ∈ Ioo 0 p, p ∣ Nat.choose p i
⊢ ∑ i in Ioo 0 p, x ^ i * y ^ (p - i) * ↑(Nat.choose p i) = ∑ i in Ioo 0 p, x ^ i * y ^ (p - i) * 0
Tactic:
sorry
State after:
no goals

State before:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : CharP K p
x y : K
h2 : Nat.Prime p
h3 : 0 < p
h4 : range p = insert 0 (Ioo 0 p)
h5 : ∀ i ∈ Ioo 0 p, p ∣ Nat.choose p i
⊢ ∑ i in Ioo 0 p, x ^ i * y ^ (p - i) * 0 = 0
Tactic:
sorry
State after:
no goals