case intro
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
m : ℕ
hn : N ≤ N + m
⊢ ∏ k in range (N + m + 1), u k = ∏ k in range (N + 1), u k
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
n : ℕ
hn : N ≤ n
⊢ ∏ k in range (n + 1), u k = ∏ k in range (N + 1), u k
obtain ⟨m, rfl : n = N + m⟩ := le_iff_exists_add.mp hn
case intro
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
m : ℕ
⊢ ∏ k in range (N + m + 1), u k = ∏ k in range (N + 1), u k
case intro
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
m : ℕ
hn : N ≤ N + m
⊢ ∏ k in range (N + m + 1), u k = ∏ k in range (N + 1), u k
clear hn
case intro.zero
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
⊢ ∏ k in range (N + Nat.zero + 1), u k = ∏ k in range (N + 1), u k

case intro.succ
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
m : ℕ
hm : ∏ k in range (N + m + 1), u k = ∏ k in range (N + 1), u k
⊢ ∏ k in range (N + Nat.succ m + 1), u k = ∏ k in range (N + 1), u k
case intro
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
m : ℕ
⊢ ∏ k in range (N + m + 1), u k = ∏ k in range (N + 1), u k
induction' m with m hm
case intro.succ
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
m : ℕ
hm : ∏ k in range (N + m + 1), u k = ∏ k in range (N + 1), u k
⊢ (∏ k in range (N + 1), u k) * u (N + Nat.succ m) = ∏ k in range (N + 1), u k
case intro.succ
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
m : ℕ
hm : ∏ k in range (N + m + 1), u k = ∏ k in range (N + 1), u k
⊢ ∏ k in range (N + Nat.succ m + 1), u k = ∏ k in range (N + 1), u k
erw [prod_range_succ, hm]
no goals
case intro.succ
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
m : ℕ
hm : ∏ k in range (N + m + 1), u k = ∏ k in range (N + 1), u k
⊢ (∏ k in range (N + 1), u k) * u (N + Nat.succ m) = ∏ k in range (N + 1), u k
simp [hu, @zero_le' ℕ]
no goals
case intro.zero
ι : Type ?u.436010
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
u : ℕ → β
N : ℕ
hu : ∀ (n : ℕ), n ≥ N → u n = 1
⊢ ∏ k in range (N + Nat.zero + 1), u k = ∏ k in range (N + 1), u k
simp