α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∏ k in Ico n m, f k = ∏ k in filter (fun k => n ≤ k) (range m), f k
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ (∏ k in range m, f k) / ∏ k in range n, f k = ∏ k in filter (fun k => n ≤ k) (range m), f k
rw [← prod_Ico_eq_div f hnm]
case e_s
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ Ico n m = filter (fun k => n ≤ k) (range m)
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∏ k in Ico n m, f k = ∏ k in filter (fun k => n ≤ k) (range m), f k
congr
case e_s.a
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ filter (fun k => n ≤ k) (range m)
case e_s
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ Ico n m = filter (fun k => n ≤ k) (range m)
apply Finset.ext
case e_s.a
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
case e_s.a
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ filter (fun k => n ≤ k) (range m)
simp only [mem_Ico, mem_filter, mem_range, *]
no goals
case e_s.a
α✝ : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α✝
a : α✝
g f✝ : α✝ → β
inst✝¹ : CommMonoid β
α : Type u_1
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
tauto