no goals
R : Type ?u.146799
m i : ℕ
hi : i ∈ range (m + 1)
⊢ i ≤ 2 * m + 1
linarith [mem_range.1 hi]
no goals
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * ∑ i in range (m + 1), choose (2 * m + 1) i =
    ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i)
rw [two_mul, this]
case e_a.e_s.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ ∑ i in Ico 0 (m + 1), choose (2 * m + 1) i +
      ∑ j in Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), choose (2 * m + 1) j =
    ∑ i in Ico 0 (m + 1), choose (2 * m + 1) i + ∑ i in Ico (m + 1) (2 * m + 2), choose (2 * m + 1) i
congr
case e_a.e_s.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1
case e_a.e_s.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1
have A : m + 1 ≤ 2 * m + 1 := by linarith
case e_a.e_s.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 - (m + 1) + 1 = m + 1
case e_a.e_s.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1
rw [add_comm, add_tsub_assoc_of_le A, ← add_comm]
case e_a.e_s.e_a.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 - (m + 1) = m
case e_a.e_s.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 - (m + 1) + 1 = m + 1
congr
case e_a.e_s.e_a.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 = m + (m + 1)
case e_a.e_s.e_a.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 - (m + 1) = m
rw [tsub_eq_iff_eq_add_of_le A]
no goals
case e_a.e_s.e_a.e_a
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 = m + (m + 1)
ring
no goals
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ m + 1 ≤ 2 * m + 1
linarith
no goals
case h
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ m + 1 ≤ 2 * m + 1 + 1
linarith
no goals
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ m + 1 ≤ 2 * m + 2
linarith
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * (2 ^ 2) ^ m = 2 * 4 ^ m
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 ^ (2 * m + 1) = 2 * 4 ^ m
rw [pow_succ, pow_mul, mul_comm]
no goals
R : Type ?u.146799
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * (2 ^ 2) ^ m = 2 * 4 ^ m
rfl