case h.e'_1.h.e'_1
α : Type u_2
β : Type u_1
γ : Type ?u.378311
δ : Type ?u.378314
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s₁ s₂ : β
⊢ s₁ ⊔ s₂ = ⨆ (b : Bool), bif b then s₁ else s₂

case h.e'_2
α : Type u_2
β : Type u_1
γ : Type ?u.378311
δ : Type ?u.378314
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s₁ s₂ : β
⊢ m s₁ + m s₂ = ∑' (b : Bool), m (bif b then s₁ else s₂)
α : Type u_2
β : Type u_1
γ : Type ?u.378311
δ : Type ?u.378314
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s₁ s₂ : β
⊢ R (m (s₁ ⊔ s₂)) (m s₁ + m s₂)
convert rel_iSup_tsum m m0 R m_iSup fun b => cond b s₁ s₂
no goals
case h.e'_1.h.e'_1
α : Type u_2
β : Type u_1
γ : Type ?u.378311
δ : Type ?u.378314
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s₁ s₂ : β
⊢ s₁ ⊔ s₂ = ⨆ (b : Bool), bif b then s₁ else s₂
simp only [iSup_bool_eq, cond]
no goals
case h.e'_2
α : Type u_2
β : Type u_1
γ : Type ?u.378311
δ : Type ?u.378314
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Countable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
R : α → α → Prop
m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))
s₁ s₂ : β
⊢ m s₁ + m s₂ = ∑' (b : Bool), m (bif b then s₁ else s₂)
rw [tsum_fintype, Fintype.sum_bool, cond, cond]