α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
have : ∀ i < m, i ≤ n := by
  intro i hi
  exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j

case inr
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
cases' lt_or_le k m with hkm hkm
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
i : ℕ
hi : i < m
⊢ i ≤ n
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
⊢ ∀ (i : ℕ), i < m → i ≤ n
intro i hi
no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
i : ℕ
hi : i < m
⊢ i ≤ n
exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in image (fun x => n - x) (Ico k m), f j
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∀ (x : ℕ), x ∈ Ico k m → ∀ (y : ℕ), y ∈ Ico k m → n - x = n - y → x = y
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in image (fun x => n - x) (Ico k m), f j
refine' (prod_image _).symm
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∀ (x : ℕ), k ≤ x ∧ x < m → ∀ (y : ℕ), k ≤ y ∧ y < m → n - x = n - y → x = y
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∀ (x : ℕ), x ∈ Ico k m → ∀ (y : ℕ), y ∈ Ico k m → n - x = n - y → x = y
simp only [mem_Ico]
case inl.intro.intro
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ i = j
case inl
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
⊢ ∀ (x : ℕ), k ≤ x ∧ x < m → ∀ (y : ℕ), k ≤ y ∧ y < m → n - x = n - y → x = y
rintro i ⟨_, im⟩ j ⟨_, jm⟩ Hij
no goals
case inl.intro.intro
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ i = j
rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]
case inr
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this✝ : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
this : n + 1 - k ≤ n + 1 - m
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
case inr
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
have : n + 1 - k ≤ n + 1 - m := by
  rw [tsub_le_tsub_iff_left h]
  exact hkm
no goals
case inr
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this✝ : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
this : n + 1 - k ≤ n + 1 - m
⊢ ∏ j in Ico k m, f (n - j) = ∏ j in Ico (n + 1 - m) (n + 1 - k), f j
simp only [ge_iff_le, hkm, Ico_eq_empty_of_le, prod_empty, tsub_le_iff_right, Ico_eq_empty_of_le
  this]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
⊢ m ≤ k
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
⊢ n + 1 - k ≤ n + 1 - m
rw [tsub_le_tsub_iff_left h]
no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
k m n : ℕ
h : m ≤ n + 1
this : ∀ (i : ℕ), i < m → i ≤ n
hkm : m ≤ k
⊢ m ≤ k
exact hkm