intro hy
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.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)