-- Mathlib/Algebra/Order/Group/Indicator.lean
@[to_additive]
lemma mulIndicator_iInter_apply (h1 : (⊥ : M) = 1) (s : ι → Set α) (f : α → M) (x : α) :
    mulIndicator (⋂ i, s i) f x = ⨅ i, mulIndicator (s i) f x

Proof state:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ i, s i
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Tactic:
simp only [mem_iInter, not_exists, not_forall] at hx

Result:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ x_1, x ∉ s x_1
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Proof state:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
⊢ f x ≤ ⨅ i, (s i).mulIndicator f x

Tactic:
exact le_iInf (fun j ↦ by simp only [mulIndicator_of_mem (hx j), le_refl])

Result:
no goals

Proof state:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ x_1, x ∉ s x_1
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Tactic:
rcases hx with ⟨j, hj⟩

Result:
case neg.intro
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Proof state:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ 1 ≤ ⨅ i, (s i).mulIndicator f x

Tactic:
simp only [← h1, le_iInf_iff, bot_le, forall_const]

Result:
no goals

Proof state:
case neg.intro
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Tactic:
refine le_antisymm (by simp only [← h1, le_iInf_iff, bot_le, forall_const]) ?_

Result:
case neg.intro
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ ⨅ i, (s i).mulIndicator f x ≤ 1

Proof state:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋂ i, s i
⊢ f x = ⨅ i, (s i).mulIndicator f x

Tactic:
rw [mem_iInter] at hx

Result:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
⊢ f x = ⨅ i, (s i).mulIndicator f x

Proof state:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
j : ι
⊢ f x ≤ (s j).mulIndicator f x

Tactic:
simp only [mulIndicator_of_mem (hx j), le_refl]

Result:
no goals

Proof state:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋂ i, s i
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x

Tactic:
rw [mulIndicator_of_mem hx]

Result:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋂ i, s i
⊢ f x = ⨅ i, (s i).mulIndicator f x

Proof state:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
⊢ ⨅ i, (s i).mulIndicator f x ≤ f x

Tactic:
simp only [mulIndicator_of_mem (hx _), ciInf_const, le_refl]

Result:
no goals

Proof state:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
⊢ f x = ⨅ i, (s i).mulIndicator f x

Tactic:
refine le_antisymm ?_ (by simp only [mulIndicator_of_mem (hx _), ciInf_const, le_refl])

Result:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
⊢ f x ≤ ⨅ i, (s i).mulIndicator f x

Proof state:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ i, s i
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x

Tactic:
rw [mulIndicator_of_not_mem hx]

Result:
case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ i, s i
⊢ 1 = ⨅ i, (s i).mulIndicator f x

Proof state:
case neg.intro
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ ⨅ i, (s i).mulIndicator f x ≤ 1

Tactic:
simpa [mulIndicator_of_not_mem hj] using (iInf_le (fun i ↦ (s i).mulIndicator f) j) x

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x

Tactic:
by_cases hx : x ∈ ⋂ i, s i

Result:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋂ i, s i
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x

case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : CompleteLattice M
inst✝¹ : One M
inst✝ : Nonempty ι
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ i, s i
⊢ (⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x