α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ Disjoint (Ioc m n) (Ioc n k)
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ (∏ i in Ioc m n, f i) * ∏ i in Ioc n k, f i = ∏ i in Ioc m k, f i
rw [← Ioc_union_Ioc_eq_Ioc hmn hnk, prod_union]
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ ∀ (x : ℕ), x ∈ Ioc m n → x ∈ Ioc n k → False
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ Disjoint (Ioc m n) (Ioc n k)
apply disjoint_left.2 fun x hx h'x => _
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
h'x : x ∈ Ioc n k
⊢ False
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ ∀ (x : ℕ), x ∈ Ioc m n → x ∈ Ioc n k → False
intros x hx h'x
no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
h'x : x ∈ Ioc n k
⊢ False
exact lt_irrefl _ ((mem_Ioc.1 h'x).1.trans_le (mem_Ioc.1 hx).2)