case zero
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m n : ℕ
hmn✝ : m < n
hmn : Nat.zero < n
⊢ Disjoint (↑(partialSups f) Nat.zero) (f n)

case succ
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m✝ n : ℕ
hmn✝ : m✝ < n
m : ℕ
ih : m < n → Disjoint (↑(partialSups f) m) (f n)
hmn : Nat.succ m < n
⊢ Disjoint (↑(partialSups f) (Nat.succ m)) (f n)
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m n : ℕ
hmn : m < n
⊢ Disjoint (↑(partialSups f) m) (f n)
induction' m with m ih
no goals
case zero
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m n : ℕ
hmn✝ : m < n
hmn : Nat.zero < n
⊢ Disjoint (↑(partialSups f) Nat.zero) (f n)
exact h hmn.ne
case succ
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m✝ n : ℕ
hmn✝ : m✝ < n
m : ℕ
ih : m < n → Disjoint (↑(partialSups f) m) (f n)
hmn : Nat.succ m < n
⊢ Disjoint (↑(partialSups f) m) (f n) ∧ Disjoint (f (m + 1)) (f n)
case succ
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m✝ n : ℕ
hmn✝ : m✝ < n
m : ℕ
ih : m < n → Disjoint (↑(partialSups f) m) (f n)
hmn : Nat.succ m < n
⊢ Disjoint (↑(partialSups f) (Nat.succ m)) (f n)
rw [partialSups_succ, disjoint_sup_left]
no goals
case succ
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m✝ n : ℕ
hmn✝ : m✝ < n
m : ℕ
ih : m < n → Disjoint (↑(partialSups f) m) (f n)
hmn : Nat.succ m < n
⊢ Disjoint (↑(partialSups f) m) (f n) ∧ Disjoint (f (m + 1)) (f n)
exact ⟨ih (Nat.lt_of_succ_lt hmn), h hmn.ne⟩