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

State before:
case zero
f : ℕ → ℝ
⊢ ∏ i ∈ Finset.range (0 + 1), ∏ j ∈ (Finset.range (0 + 1)).erase i, f j = ∏ i ∈ Finset.range (0 + 1), f i ^ ↑0
Tactic:
simp
State after:
no goals

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ∏ i ∈ Finset.range (n + 1 + 1), f i ^ ↑(n + 1)
Tactic:
have h1 : ∏ i ∈ Finset.range (Nat.succ n + 1), f i ^ ((Nat.succ n):ℝ) =
        (∏ i ∈ Finset.range (n + 1), f i ^ ((Nat.succ n):ℝ)) * f (n + 1) ^ ((Nat.succ n):ℝ) :=
 by rw [Finset.prod_range_succ]
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h1 : ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ∏ i ∈ Finset.range (n + 1 + 1), f i ^ ↑(n + 1)

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h1 : ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ∏ i ∈ Finset.range (n + 1 + 1), f i ^ ↑(n + 1)
Tactic:
rw [h1]
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h1 : ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h1 : ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
Tactic:
clear h1
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
Tactic:
have h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ((Nat.succ n):ℝ) =
          ∏ i ∈ Finset.range (n + 1), (f i ^ (n:ℝ) * f i) := by
   congr; funext x
   norm_cast
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
Tactic:
rw [h2]
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i) * f (n + 1) ^ ↑n.succ
Tactic:
clear h2
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i) * f (n + 1) ^ ↑n.succ
Tactic:
rw [Finset.prod_mul_distrib]
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
Tactic:
rw [Finset.prod_range_succ, lemma2']
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase x, f j) * ∏ j ∈ Finset.range (n + 1), f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
⊢ (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase x, f j) * ∏ j ∈ Finset.range (n + 1), f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
Tactic:
rw [h3]
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
⊢ (∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)) *
      ∏ j ∈ Finset.range (n + 1), f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
⊢ (∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)) *
      ∏ j ∈ Finset.range (n + 1), f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
Tactic:
have h4 :
    ∏ x ∈ Finset.range (n + 1),
      ((∏ j ∈ Finset.erase (Finset.range (n + 1)) x, f j) * f (n + 1)) =
     (∏ x ∈ Finset.range (n + 1),
        ∏ j ∈ Finset.erase (Finset.range (n + 1)) x, f j) * f (n + 1) ^ (n+1) := by
  rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
h4 :
  ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
⊢ (∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)) *
      ∏ j ∈ Finset.range (n + 1), f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
h4 :
  ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
⊢ (∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)) *
      ∏ j ∈ Finset.range (n + 1), f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
Tactic:
rw [h4, ih, mul_right_comm]
State after:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
h4 :
  ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
⊢ ((∏ i ∈ Finset.range (n + 1), f i ^ ↑n) * ∏ j ∈ Finset.range (n + 1), f j) * f (n + 1) ^ (n + 1) =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ

State before:
case succ
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
h4 :
  ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
⊢ ((∏ i ∈ Finset.range (n + 1), f i ^ ↑n) * ∏ j ∈ Finset.range (n + 1), f j) * f (n + 1) ^ (n + 1) =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
Tactic:
norm_cast
State after:
no goals

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
Tactic:
rw [Finset.prod_range_succ]
State after:
no goals

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
Tactic:
congr
State after:
case e_f
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ (fun i => f i ^ ↑n.succ) = fun i => f i ^ ↑n * f i

State before:
case e_f
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ (fun i => f i ^ ↑n.succ) = fun i => f i ^ ↑n * f i
Tactic:
funext x
State after:
case e_f.h
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
⊢ f x ^ ↑n.succ = f x ^ ↑n * f x

State before:
case e_f.h
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
⊢ f x ^ ↑n.succ = f x ^ ↑n * f x
Tactic:
norm_cast
State after:
no goals

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
apply Finset.prod_congr rfl
State after:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∀ x ∈ Finset.range (n + 1),
    ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
⊢ ∀ x ∈ Finset.range (n + 1),
    ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
intro x hx
State after:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
have h7' : (n + 1) ∉ (Finset.erase (Finset.range (n + 1)) x) := by simp_all
State after:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
⊢ ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
h7 : (Finset.range (n.succ + 1)).erase x = insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
rw [h7, Finset.prod_insert h7']
State after:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
h7 : (Finset.range (n.succ + 1)).erase x = insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ f (n + 1) * ∏ x ∈ (Finset.range (n + 1)).erase x, f x = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
h7 : (Finset.range (n.succ + 1)).erase x = insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ f (n + 1) * ∏ x ∈ (Finset.range (n + 1)).erase x, f x = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
Tactic:
ring
State after:
no goals

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ n + 1 ∉ (Finset.range (n + 1)).erase x
Tactic:
simp_all
State after:
no goals

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
⊢ (Finset.range (n.succ + 1)).erase x = insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
ext y
State after:
case a
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ (Finset.range (n.succ + 1)).erase x ↔ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)

State before:
case a
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ (Finset.range (n.succ + 1)).erase x ↔ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
constructor
State after:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ (Finset.range (n.succ + 1)).erase x → y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)

case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x) → y ∈ (Finset.range (n.succ + 1)).erase x

State before:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ (Finset.range (n.succ + 1)).erase x → y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
intro hy
State after:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ∈ (Finset.range (n.succ + 1)).erase x
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)

State before:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ∈ (Finset.range (n.succ + 1)).erase x
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
rw [Finset.mem_erase, Finset.mem_range] at hy
State after:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ≠ x ∧ y < n.succ + 1
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)

State before:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ≠ x ∧ y < n.succ + 1
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
Tactic:
rw [Finset.mem_insert, Finset.mem_erase, Finset.mem_range]
State after:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ≠ x ∧ y < n.succ + 1
⊢ y = n + 1 ∨ y ≠ x ∧ y < n + 1

State before:
case a.mp
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ≠ x ∧ y < n.succ + 1
⊢ y = n + 1 ∨ y ≠ x ∧ y < n + 1
Tactic:
omega
State after:
no goals

State before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
⊢ y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x) → y ∈ (Finset.range (n.succ + 1)).erase x
Tactic:
intro hy
State after:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ y ∈ (Finset.range (n.succ + 1)).erase x

State before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y ∈ insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ y ∈ (Finset.range (n.succ + 1)).erase x
Tactic:
rw [Finset.mem_insert, Finset.mem_erase, Finset.mem_range] at hy
State after:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ∈ (Finset.range (n.succ + 1)).erase x

State before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ∈ (Finset.range (n.succ + 1)).erase x
Tactic:
rw [Finset.mem_range] at hx
State after:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x < n + 1
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ∈ (Finset.range (n.succ + 1)).erase x

State before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x < n + 1
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ∈ (Finset.range (n.succ + 1)).erase x
Tactic:
rw [Finset.mem_erase, Finset.mem_range]
State after:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x < n + 1
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ≠ x ∧ y < n.succ + 1

State before:
case a.mpr
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x < n + 1
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
y : ℕ
hy : y = n + 1 ∨ y ≠ x ∧ y < n + 1
⊢ y ≠ x ∧ y < n.succ + 1
Tactic:
omega
State after:
no goals

State before:
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
⊢ ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
Tactic:
rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
State after:
no goals