-- Mathlib/Algebra/Order/Group/Indicator.lean
@[to_additive]
lemma iSup_mulIndicator {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f : ι → α → M}
    {s : ι → Set α} (h1 : (⊥ : M) = 1) (hf : Monotone f) (hs : Monotone s) :
    ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i)

Proof state:
case neg
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ i, s i
⊢ ⊥ ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
exact bot_le

Result:
no goals

Proof state:
case pos.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
rw [mulIndicator_of_mem ha, iSup_apply, iSup_apply]

Result:
case pos.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
⊢ ⨆ i, f i a ≤ ⨆ i, (s i).mulIndicator (f i) a

Proof state:
case pos.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
⊢ ⨆ i, f i a ≤ ⨆ i, (s i).mulIndicator (f i) a

Tactic:
refine iSup_le fun j ↦ ?_

Result:
case pos.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
j : ι
⊢ f j a ≤ ⨆ i, (s i).mulIndicator (f i) a

Proof state:
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
⊢ ∃ i, a ∈ s i

Tactic:
simpa using ha

Result:
no goals

Proof state:
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
⊢ (∀ (i : ι), (s i).mulIndicator (f i) ≤ (⋃ i, s i).mulIndicator (⨆ i, f i)) ∧
    (⋃ i, s i).mulIndicator (⨆ i, f i) ≤ ⨆ i, (s i).mulIndicator (f i)

Tactic:
refine ⟨fun i ↦ (mulIndicator_mono (le_iSup _ _)).trans (mulIndicator_le_mulIndicator_of_subset
  (subset_iUnion _ _) (fun _ ↦ by simp [← h1])), fun a ↦ ?_⟩

Result:
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Proof state:
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
by_cases ha : a ∈ ⋃ i, s i

Result:
case pos
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

case neg
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Proof state:
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
⊢ ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i)

Tactic:
simp only [le_antisymm_iff, iSup_le_iff]

Result:
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
⊢ (∀ (i : ι), (s i).mulIndicator (f i) ≤ (⋃ i, s i).mulIndicator (⨆ i, f i)) ∧
    (⋃ i, s i).mulIndicator (⨆ i, f i) ≤ ⨆ i, (s i).mulIndicator (f i)

Proof state:
case neg
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
rw [mulIndicator_of_not_mem ha, ← h1]

Result:
case neg
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ i, s i
⊢ ⊥ ≤ (⨆ i, (s i).mulIndicator (f i)) a

Proof state:
case pos.intro.intro.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
j k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ f j a ≤ ⨆ i, (s i).mulIndicator (f i) a

Tactic:
refine le_iSup_of_le k <| (hf hjk _).trans_eq ?_

Result:
case pos.intro.intro.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
j k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ f k a = (s k).mulIndicator (f k) a

Proof state:
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
i : ι
x✝ : α
⊢ 1 x✝ ≤ (⨆ i, f i) x✝

Tactic:
simp [← h1]

Result:
no goals

Proof state:
case pos
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
obtain ⟨i, hi⟩ : ∃ i, a ∈ s i := by simpa using ha

Result:
case pos.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Proof state:
case pos.intro.intro.intro
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
j k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ f k a = (s k).mulIndicator (f k) a

Tactic:
rw [mulIndicator_of_mem (hs hik hi)]

Result:
no goals