case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d n = disjointed f n
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
⊢ d = disjointed f
ext n
case h.zero
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
⊢ d Nat.zero = disjointed f Nat.zero

case h.succ
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d (Nat.succ n) = disjointed f (Nat.succ n)
case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d n = disjointed f n
cases' n with n
case h.succ
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
h : d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
⊢ d (Nat.succ n) = disjointed f (Nat.succ n)

case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
case h.succ
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d (Nat.succ n) = disjointed f (Nat.succ n)
suffices h : d n.succ = partialSups d n.succ \ partialSups d n
case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ Disjoint (↑(partialSups d) n) (d (n + 1))
case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
rw [partialSups_succ, sup_sdiff, sdiff_self, bot_sup_eq, eq_comm, sdiff_eq_self_iff_disjoint]
case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
h : ∀ (m : ℕ), m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
⊢ Disjoint (↑(partialSups d) n) (d (n + 1))

case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ ∀ (m : ℕ), m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ Disjoint (↑(partialSups d) n) (d (n + 1))
suffices h : ∀ m ≤ n, Disjoint (partialSups d m) (d n.succ)
case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m : ℕ
hm : m ≤ n
⊢ Disjoint (↑(partialSups d) m) (d (Nat.succ n))
case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ ∀ (m : ℕ), m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
rintro m hm
case h.zero
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m : ℕ
hm✝ : m ≤ n
hm : Nat.zero ≤ n
⊢ Disjoint (↑(partialSups d) Nat.zero) (d (Nat.succ n))

case h.succ
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m✝ : ℕ
hm✝ : m✝ ≤ n
m : ℕ
ih : m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
hm : Nat.succ m ≤ n
⊢ Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m : ℕ
hm : m ≤ n
⊢ Disjoint (↑(partialSups d) m) (d (Nat.succ n))
induction' m with m ih
case h.succ
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m✝ : ℕ
hm✝ : m✝ ≤ n
m : ℕ
ih : m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
hm : Nat.succ m ≤ n
⊢ Disjoint (↑(partialSups d) m) (d (Nat.succ n)) ∧ Disjoint (d (m + 1)) (d (Nat.succ n))
case h.succ
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m✝ : ℕ
hm✝ : m✝ ≤ n
m : ℕ
ih : m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
hm : Nat.succ m ≤ n
⊢ Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
rw [partialSups_succ, disjoint_iff, inf_sup_right, sup_eq_bot_iff, ← disjoint_iff, ← disjoint_iff]
no goals
case h.succ
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m✝ : ℕ
hm✝ : m✝ ≤ n
m : ℕ
ih : m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
hm : Nat.succ m ≤ n
⊢ Disjoint (↑(partialSups d) m) (d (Nat.succ n)) ∧ Disjoint (d (m + 1)) (d (Nat.succ n))
exact ⟨ih (Nat.le_of_succ_le hm), hdisj (Nat.lt_succ_of_le hm).ne⟩
no goals
case h.zero
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
⊢ d Nat.zero = disjointed f Nat.zero
rw [← partialSups_zero d, hsups, partialSups_zero, disjointed_zero]
no goals
case h.succ
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
h : d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
⊢ d (Nat.succ n) = disjointed f (Nat.succ n)
rw [h, hsups, partialSups_succ, disjointed_succ, sup_sdiff, sdiff_self, bot_sup_eq]
no goals
case h
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
h : ∀ (m : ℕ), m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
⊢ Disjoint (↑(partialSups d) n) (d (n + 1))
exact h n le_rfl
no goals
case h.zero
α : Type u_1
β : Type ?u.7993
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m : ℕ
hm✝ : m ≤ n
hm : Nat.zero ≤ n
⊢ Disjoint (↑(partialSups d) Nat.zero) (d (Nat.succ n))
exact hdisj (Nat.succ_ne_zero _).symm