α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ (∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)) = ∑' (b : γ), m (s b)
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
⊢ (∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)) = ∑' (b : γ), m (s b)
have H : ∀ n, m (⨆ b ∈ decode₂ γ n, s b) ≠ 0 → (decode₂ γ n).isSome :=by
  intro n h
  generalize decode₂ γ n = foo at *
  cases' foo with b
  . refine' (h <| by simp [m0]).elim
  . exact rfl
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ (∑' (b : γ), m (s b)) = ∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ (∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)) = ∑' (b : γ), m (s b)
symm
case refine'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∀ ⦃x y : ↑(support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))⦄,
    (fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) x =
        (fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) y →
      ↑x = ↑y

case refine'_2
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ (support fun b => m (s b)) ⊆ Set.range fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)

case refine'_3
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∀ (x : ↑(support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))),
    m (s ((fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) x)) =
      m (⨆ (b : γ) (_ : b ∈ decode₂ γ ↑x), s b)
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ (∑' (b : γ), m (s b)) = ∑' (i : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
refine' tsum_eq_tsum_of_ne_zero_bij (fun a => Option.get _ (H a.1 a.2)) _ _ _
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
h : m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0
⊢ Option.isSome (decode₂ γ n) = true
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
⊢ ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
intro n h
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
foo : Option γ
h : m (⨆ (b : γ) (_ : b ∈ foo), s b) ≠ 0
⊢ Option.isSome foo = true
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
h : m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0
⊢ Option.isSome (decode₂ γ n) = true
generalize decode₂ γ n = foo at *
case none
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
h : m (⨆ (b : γ) (_ : b ∈ none), s b) ≠ 0
⊢ Option.isSome none = true

case some
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
b : γ
h : m (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) ≠ 0
⊢ Option.isSome (some b) = true
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
foo : Option γ
h : m (⨆ (b : γ) (_ : b ∈ foo), s b) ≠ 0
⊢ Option.isSome foo = true
cases' foo with b
case some
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
b : γ
h : m (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) ≠ 0
⊢ Option.isSome (some b) = true
case none
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
h : m (⨆ (b : γ) (_ : b ∈ none), s b) ≠ 0
⊢ Option.isSome none = true

case some
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
b : γ
h : m (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) ≠ 0
⊢ Option.isSome (some b) = true
. refine' (h <| by simp [m0]).elim
no goals
case some
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
b : γ
h : m (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) ≠ 0
⊢ Option.isSome (some b) = true
. exact rfl
no goals
case none
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
h : m (⨆ (b : γ) (_ : b ∈ none), s b) ≠ 0
⊢ Option.isSome none = true
refine' (h <| by simp [m0]).elim
no goals
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
h : m (⨆ (b : γ) (_ : b ∈ none), s b) ≠ 0
⊢ m (⨆ (b : γ) (_ : b ∈ none), s b) = 0
simp [m0]
no goals
case some
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
n : ℕ
b : γ
h : m (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) ≠ 0
⊢ Option.isSome (some b) = true
exact rfl
case refine'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∀ ⦃x y : ↑(support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))⦄,
    Option.get (decode₂ γ ↑x) (_ : Option.isSome (decode₂ γ ↑x) = true) =
        Option.get (decode₂ γ ↑y) (_ : Option.isSome (decode₂ γ ↑y) = true) →
      ↑x = ↑y
case refine'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∀ ⦃x y : ↑(support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))⦄,
    (fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) x =
        (fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) y →
      ↑x = ↑y
dsimp only []
case refine'_1.mk.mk
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m✝ : β → α
m0 : m✝ ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
m : ℕ
hm : m ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
n : ℕ
hn : n ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
e :
  Option.get (decode₂ γ ↑{ val := m, property := hm })
      (_ : Option.isSome (decode₂ γ ↑{ val := m, property := hm }) = true) =
    Option.get (decode₂ γ ↑{ val := n, property := hn })
      (_ : Option.isSome (decode₂ γ ↑{ val := n, property := hn }) = true)
⊢ ↑{ val := m, property := hm } = ↑{ val := n, property := hn }
case refine'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∀ ⦃x y : ↑(support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))⦄,
    Option.get (decode₂ γ ↑x) (_ : Option.isSome (decode₂ γ ↑x) = true) =
        Option.get (decode₂ γ ↑y) (_ : Option.isSome (decode₂ γ ↑y) = true) →
      ↑x = ↑y
rintro ⟨m, hm⟩ ⟨n, hn⟩ e
case refine'_1.mk.mk
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m✝ : β → α
m0 : m✝ ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
m : ℕ
hm : m ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
n : ℕ
hn : n ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
e :
  Option.get (decode₂ γ ↑{ val := m, property := hm })
      (_ : Option.isSome (decode₂ γ ↑{ val := m, property := hm }) = true) =
    Option.get (decode₂ γ ↑{ val := n, property := hn })
      (_ : Option.isSome (decode₂ γ ↑{ val := n, property := hn }) = true)
this : encode (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true)) = n
⊢ ↑{ val := m, property := hm } = ↑{ val := n, property := hn }
case refine'_1.mk.mk
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m✝ : β → α
m0 : m✝ ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
m : ℕ
hm : m ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
n : ℕ
hn : n ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
e :
  Option.get (decode₂ γ ↑{ val := m, property := hm })
      (_ : Option.isSome (decode₂ γ ↑{ val := m, property := hm }) = true) =
    Option.get (decode₂ γ ↑{ val := n, property := hn })
      (_ : Option.isSome (decode₂ γ ↑{ val := n, property := hn }) = true)
⊢ ↑{ val := m, property := hm } = ↑{ val := n, property := hn }
have := mem_decode₂.1 (Option.get_mem (H n hn))
no goals
case refine'_1.mk.mk
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m✝ : β → α
m0 : m✝ ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
m : ℕ
hm : m ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
n : ℕ
hn : n ∈ support fun i => m✝ (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
e :
  Option.get (decode₂ γ ↑{ val := m, property := hm })
      (_ : Option.isSome (decode₂ γ ↑{ val := m, property := hm }) = true) =
    Option.get (decode₂ γ ↑{ val := n, property := hn })
      (_ : Option.isSome (decode₂ γ ↑{ val := n, property := hn }) = true)
this : encode (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true)) = n
⊢ ↑{ val := m, property := hm } = ↑{ val := n, property := hn }
rwa [← e, mem_decode₂.1 (Option.get_mem (H m hm))] at this
case refine'_2
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : b ∈ support fun b => m (s b)
⊢ b ∈ Set.range fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)
case refine'_2
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ (support fun b => m (s b)) ⊆ Set.range fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)
intro b h
case refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : b ∈ support fun b => m (s b)
⊢ encode b ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)

case refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : b ∈ support fun b => m (s b)
⊢ (fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true))
      { val := encode b, property := ?refine'_2.refine'_1 } =
    b
case refine'_2
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : b ∈ support fun b => m (s b)
⊢ b ∈ Set.range fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)
refine' ⟨⟨encode b, _⟩, _⟩
case refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : m (s b) ≠ 0
⊢ m (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) ≠ 0
case refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : b ∈ support fun b => m (s b)
⊢ encode b ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
simp only [mem_support, encodek₂] at h⊢
case h.e'_2.h.e'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : m (s b) ≠ 0
⊢ (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) = s b
case refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : m (s b) ≠ 0
⊢ m (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) ≠ 0
convert h
no goals
case h.e'_2.h.e'_1
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : m (s b) ≠ 0
⊢ (⨆ (b_1 : γ) (_ : b_1 ∈ some b), s b_1) = s b
simp [Set.ext_iff, encodek₂]
no goals
case refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
b : γ
h : b ∈ support fun b => m (s b)
⊢ (fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true))
      { val := encode b, property := (_ : encode b ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)) } =
    b
exact Option.get_of_mem _ (encodek₂ _)
case refine'_3.mk
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s ((fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) { val := n, property := h })) =
    m (⨆ (b : γ) (_ : b ∈ decode₂ γ ↑{ val := n, property := h }), s b)
case refine'_3
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
⊢ ∀ (x : ↑(support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b))),
    m (s ((fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) x)) =
      m (⨆ (b : γ) (_ : b ∈ decode₂ γ ↑x), s b)
rintro ⟨n, h⟩
case refine'_3.mk
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) = m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b)
case refine'_3.mk
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s ((fun a => Option.get (decode₂ γ ↑a) (_ : Option.isSome (decode₂ γ ↑a) = true)) { val := n, property := h })) =
    m (⨆ (b : γ) (_ : b ∈ decode₂ γ ↑{ val := n, property := h }), s b)
dsimp only [Subtype.coe_mk]
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) = ?m.371147

α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ ?m.371147 = m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b)

α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ α
case refine'_3.mk
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) = m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b)
trans
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ ?m.371147 = m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b)

α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) = ?m.371147

α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ α
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) = ?m.371147

α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ ?m.371147 = m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b)

α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ α
swap
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) =
    m (⨆ (b : γ) (_ : b ∈ some (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))), s b)
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ ?m.371147 = m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b)

α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) = ?m.371147

α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ α
rw [show decode₂ γ n = _ from Option.get_mem (H n h)]
case e_a
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true)) =
    ⨆ (b : γ) (_ : b ∈ some (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))), s b
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ m (s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))) =
    m (⨆ (b : γ) (_ : b ∈ some (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))), s b)
congr
no goals
case e_a
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.362154
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
f g : β → α
a a₁ a₂ : α
inst✝¹ : Encodable γ
inst✝ : CompleteLattice β
m : β → α
m0 : m ⊥ = 0
s : γ → β
H : ∀ (n : ℕ), m (⨆ (b : γ) (_ : b ∈ decode₂ γ n), s b) ≠ 0 → Option.isSome (decode₂ γ n) = true
n : ℕ
h : n ∈ support fun i => m (⨆ (b : γ) (_ : b ∈ decode₂ γ i), s b)
⊢ s (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true)) =
    ⨆ (b : γ) (_ : b ∈ some (Option.get (decode₂ γ n) (_ : Option.isSome (decode₂ γ n) = true))), s b
simp [ext_iff, -Option.some_get]