Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Zhouhang Zhou

! This file was ported from Lean 3 source module algebra.indicator_function
! leanprover-community/mathlib commit 2445c98ae4b87eabebdde552593519b9b6dc350c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Support

/-!
# Indicator function

- `indicator (s : Set α) (f : α → β) (a : α)` is `f a` if `a ∈ s` and is `0` otherwise.
- `mulIndicator (s : Set α) (f : α → β) (a : α)` is `f a` if `a ∈ s` and is `1` otherwise.

## Implementation note

In mathematics, an indicator function or a characteristic function is a function
used to indicate membership of an element in a set `s`,
having the value `1` for all elements of `s` and the value `0` otherwise.
But since it is usually used to restrict a function to a certain set `s`,
we let the indicator function take the value `f x` for some function `f`, instead of `1`.
If the usual indicator function is needed, just set `f` to be the constant function `λx, 1`.

The indicator function is implemented non-computably, to avoid having to pass around `Decidable`
arguments. This is in contrast with the design of `Pi.Single` or `Set.Piecewise`.

## Tags
indicator, characteristic
-/

open BigOperators

open Function

variable {α: Type ?u.17α β: Type ?u.68898β ι: Type ?u.12003ι M: Type ?u.64216M N: Type ?u.29N : Type _: Type (?u.43677+1)Type _}

namespace Set

section One

variable [One: Type ?u.8765 → Type ?u.8765One M: Type ?u.26M] [One: Type ?u.8960 → Type ?u.8960One N: Type ?u.29N] {s: Set αs t: Set αt : Set: Type ?u.8963 → Type ?u.8963Set α: Type ?u.234α} {f: α → Mf g: α → Mg : α: Type ?u.10666α → M: Type ?u.10894M} {a: αa : α: Type ?u.17α}

/-- `indicator s f a` is `f a` if `a ∈ s`, `0` otherwise.  -/
noncomputable def indicator: {M : Type ?u.94} → [inst : Zero M] → Set α → (α → M) → α → Mindicator {M: ?m.91M} [Zero: Type ?u.94 → Type ?u.94Zero M: ?m.91M] (s: Set αs : Set: Type ?u.97 → Type ?u.97Set α: Type ?u.54α) (f: α → Mf : α: Type ?u.54α → M: ?m.91M) : α: Type ?u.54α → M: ?m.91M
| x: ?m.115x =>
haveI := Classical.decPred: {α : Sort ?u.119} → (p : α → Prop) → DecidablePred pClassical.decPred (· ∈ s: Set αs)
if x: ?m.115x ∈ s: Set αs then f: α → Mf x: ?m.115x else 0: ?m.1730
#align set.indicator Set.indicator: {α : Type u_1} → {M : Type u_2} → [inst : Zero M] → Set α → (α → M) → α → MSet.indicator

/-- `mulIndicator s f a` is `f a` if `a ∈ s`, `1` otherwise.  -/
@[to_additive: {α : Type u_1} → {M : Type u_2} → [inst : Zero M] → Set α → (α → M) → α → Mto_additive existing]
noncomputable def mulIndicator: {α : Type u_1} → {M : Type u_2} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (s: Set αs : Set: Type ?u.271 → Type ?u.271Set α: Type ?u.234α) (f: α → Mf : α: Type ?u.234α → M: Type ?u.243M) : α: Type ?u.234α → M: Type ?u.243M
| x: ?m.287x =>
haveI := Classical.decPred: {α : Sort ?u.291} → (p : α → Prop) → DecidablePred pClassical.decPred (· ∈ s: Set αs)
if x: ?m.287x ∈ s: Set αs then f: α → Mf x: ?m.287x else 1: ?m.3451
#align set.mul_indicator Set.mulIndicator: {α : Type u_1} → {M : Type u_2} → [inst : One M] → Set α → (α → M) → α → MSet.mulIndicator

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M} [inst_1 : DecidablePred fun x => x ∈ s],
piecewise s f 0 = indicator s fto_additive (attr := simp)]
theorem piecewise_eq_mulIndicator: ∀ [inst : DecidablePred fun x => x ∈ s], piecewise s f 1 = mulIndicator s fpiecewise_eq_mulIndicator [DecidablePred: {α : Sort ?u.478} → (α → Prop) → Sort (max1?u.478)DecidablePred (· ∈ s: Set αs)] : s: Set αs.piecewise: {α : Type ?u.510} →
{β : α → Sort ?u.509} →
(s : Set α) → ((i : α) → β i) → ((i : α) → β i) → [inst : (j : α) → Decidable (j ∈ s)] → (i : α) → β ipiecewise f: α → Mf 1: ?m.5261 = s: Set αs.mulIndicator: {α : Type ?u.620} → {M : Type ?u.619} → [inst : One M] → Set α → (α → M) → α → MmulIndicator f: α → Mf :=
funext: ∀ {α : Sort ?u.654} {β : α → Sort ?u.653} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext fun _: ?m.668_ => @if_congr: ∀ {α : Sort ?u.670} {b c : Prop} [inst : Decidable b] [inst_1 : Decidable c] {x y u v : α},
(b ↔ c) → x = u → y = v → (if b then x else y) = if c then u else vif_congr _: Sort ?u.670_ _: Prop_ _: Prop_ _ (id: {α : Sort ?u.675} → α → αid _: ?m.676_) _: ?m.671_ _: ?m.671_ _: ?m.671_ _: ?m.671_ Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl rfl: ∀ {α : Sort ?u.905} {a : α}, a = arfl rfl: ∀ {α : Sort ?u.908} {a : α}, a = arfl
#align set.piecewise_eq_mul_indicator Set.piecewise_eq_mulIndicator: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : α → M} [inst_1 : DecidablePred fun x => x ∈ s],
piecewise s f 1 = mulIndicator s fSet.piecewise_eq_mulIndicator
#align set.piecewise_eq_indicator Set.piecewise_eq_indicator: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M} [inst_1 : DecidablePred fun x => x ∈ s],
piecewise s f 0 = indicator s fSet.piecewise_eq_indicator

-- Porting note: needed unfold for mulIndicator
@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : α → M) (a : α) [inst_1 : Decidable (a ∈ s)],
indicator s f a = if a ∈ s then f a else 0to_additive]
theorem mulIndicator_apply: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : α → M) (a : α) [inst_1 : Decidable (a ∈ s)],
mulIndicator s f a = if a ∈ s then f a else 1mulIndicator_apply (s: Set αs : Set: Type ?u.1081 → Type ?u.1081Set α: Type ?u.1044α) (f: α → Mf : α: Type ?u.1044α → M: Type ?u.1053M) (a: αa : α: Type ?u.1044α) [Decidable: Prop → TypeDecidable (a: αa ∈ s: Set αs)] :
mulIndicator: {α : Type ?u.1110} → {M : Type ?u.1109} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf a: αa = if a: αa ∈ s: Set αs then f: α → Mf a: αa else 1: ?m.11491 := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.1047ι: Type ?u.1050M: Type u_2N: Type ?u.1056inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αinst✝: Decidable (a ∈ s)mulIndicator s f a = if a ∈ s then f a else 1unfold mulIndicator: {α : Type u_1} → {M : Type u_2} → [inst : One M] → Set α → (α → M) → α → MmulIndicatorα: Type u_1β: Type ?u.1047ι: Type ?u.1050M: Type u_2N: Type ?u.1056inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αinst✝: Decidable (a ∈ s)(let x := a;
if x ∈ s then f x else 1) =   if a ∈ s then f a else 1
α: Type u_1β: Type ?u.1047ι: Type ?u.1050M: Type u_2N: Type ?u.1056inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αinst✝: Decidable (a ∈ s)mulIndicator s f a = if a ∈ s then f a else 1split_ifs with hα: Type u_1β: Type ?u.1047ι: Type ?u.1050M: Type u_2N: Type ?u.1056inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αinst✝: Decidable (a ∈ s)h: a ∈ sinlf a = f aα: Type u_1β: Type ?u.1047ι: Type ?u.1050M: Type u_2N: Type ?u.1056inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αinst✝: Decidable (a ∈ s)h: ¬a ∈ sinr1 = 1 α: Type u_1β: Type ?u.1047ι: Type ?u.1050M: Type u_2N: Type ?u.1056inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αinst✝: Decidable (a ∈ s)(let x := a;
if x ∈ s then f x else 1) =   if a ∈ s then f a else 1<;>α: Type u_1β: Type ?u.1047ι: Type ?u.1050M: Type u_2N: Type ?u.1056inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αinst✝: Decidable (a ∈ s)h: a ∈ sinlf a = f aα: Type u_1β: Type ?u.1047ι: Type ?u.1050M: Type u_2N: Type ?u.1056inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αinst✝: Decidable (a ∈ s)h: ¬a ∈ sinr1 = 1 α: Type u_1β: Type ?u.1047ι: Type ?u.1050M: Type u_2N: Type ?u.1056inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αinst✝: Decidable (a ∈ s)(let x := a;
if x ∈ s then f x else 1) =   if a ∈ s then f a else 1simpGoals accomplished! 🐙
#align set.mul_indicator_apply Set.mulIndicator_apply: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : α → M) (a : α) [inst_1 : Decidable (a ∈ s)],
mulIndicator s f a = if a ∈ s then f a else 1Set.mulIndicator_apply
#align set.indicator_apply Set.indicator_apply: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : α → M) (a : α) [inst_1 : Decidable (a ∈ s)],
indicator s f a = if a ∈ s then f a else 0Set.indicator_apply

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {a : α}, a ∈ s → ∀ (f : α → M), indicator s f a = f ato_additive (attr := simp)]
theorem mulIndicator_of_mem: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {a : α}, a ∈ s → ∀ (f : α → M), mulIndicator s f a = f amulIndicator_of_mem (h: a ∈ sh : a: αa ∈ s: Set αs) (f: α → Mf : α: Type ?u.1793α → M: Type ?u.1802M) : mulIndicator: {α : Type ?u.1867} → {M : Type ?u.1866} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf a: αa = f: α → Mf a: αa :=
letI := Classical.dec: (p : Prop) → Decidable pClassical.dec (a: αa ∈ s: Set αs)
if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.1915} {t e : α}, (if c then t else e) = tif_pos h: a ∈ sh
#align set.mul_indicator_of_mem Set.mulIndicator_of_mem: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {a : α}, a ∈ s → ∀ (f : α → M), mulIndicator s f a = f aSet.mulIndicator_of_mem
#align set.indicator_of_mem Set.indicator_of_mem: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {a : α}, a ∈ s → ∀ (f : α → M), indicator s f a = f aSet.indicator_of_mem

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {a : α}, ¬a ∈ s → ∀ (f : α → M), indicator s f a = 0to_additive (attr := simp)]
theorem mulIndicator_of_not_mem: ¬a ∈ s → ∀ (f : α → M), mulIndicator s f a = 1mulIndicator_of_not_mem (h: ¬a ∈ sh : a: αa ∉ s: Set αs) (f: α → Mf : α: Type ?u.2023α → M: Type ?u.2032M) : mulIndicator: {α : Type ?u.2084} → {M : Type ?u.2083} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf a: αa = 1: ?m.21091 :=
letI := Classical.dec: (p : Prop) → Decidable pClassical.dec (a: αa ∈ s: Set αs)
if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.2170} {t e : α}, (if c then t else e) = eif_neg h: ¬a ∈ sh
#align set.mul_indicator_of_not_mem Set.mulIndicator_of_not_mem: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {a : α}, ¬a ∈ s → ∀ (f : α → M), mulIndicator s f a = 1Set.mulIndicator_of_not_mem
#align set.indicator_of_not_mem Set.indicator_of_not_mem: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {a : α}, ¬a ∈ s → ∀ (f : α → M), indicator s f a = 0Set.indicator_of_not_mem

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : α → M) (a : α),
indicator s f a = 0 ∨ indicator s f a = f ato_additive]
theorem mulIndicator_eq_one_or_self: ∀ (s : Set α) (f : α → M) (a : α), mulIndicator s f a = 1 ∨ mulIndicator s f a = f amulIndicator_eq_one_or_self (s: Set αs : Set: Type ?u.2318 → Type ?u.2318Set α: Type ?u.2281α) (f: α → Mf : α: Type ?u.2281α → M: Type ?u.2290M) (a: αa : α: Type ?u.2281α) :
mulIndicator: {α : Type ?u.2329} → {M : Type ?u.2328} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf a: αa = 1: ?m.23551 ∨ mulIndicator: {α : Type ?u.2395} → {M : Type ?u.2394} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf a: αa = f: α → Mf a: αa := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αmulIndicator s f a = 1 ∨ mulIndicator s f a = f aby_cases h: ?m.2435h : a: αa ∈ s: Set αsα: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αh: a ∈ sposmulIndicator s f a = 1 ∨ mulIndicator s f a = f aα: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αh: ¬a ∈ snegmulIndicator s f a = 1 ∨ mulIndicator s f a = f a
α: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αmulIndicator s f a = 1 ∨ mulIndicator s f a = f a·α: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αh: a ∈ sposmulIndicator s f a = 1 ∨ mulIndicator s f a = f a α: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αh: a ∈ sposmulIndicator s f a = 1 ∨ mulIndicator s f a = f aα: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αh: ¬a ∈ snegmulIndicator s f a = 1 ∨ mulIndicator s f a = f aexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr (mulIndicator_of_mem: ∀ {α : Type ?u.2453} {M : Type ?u.2454} [inst : One M] {s : Set α} {a : α},
a ∈ s → ∀ (f : α → M), mulIndicator s f a = f amulIndicator_of_mem h: ?m.2435h f: α → Mf)Goals accomplished! 🐙
α: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αmulIndicator s f a = 1 ∨ mulIndicator s f a = f a·α: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αh: ¬a ∈ snegmulIndicator s f a = 1 ∨ mulIndicator s f a = f a α: Type u_1β: Type ?u.2284ι: Type ?u.2287M: Type u_2N: Type ?u.2293inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma✝: αs: Set αf: α → Ma: αh: ¬a ∈ snegmulIndicator s f a = 1 ∨ mulIndicator s f a = f aexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl (mulIndicator_of_not_mem: ∀ {α : Type ?u.2490} {M : Type ?u.2491} [inst : One M] {s : Set α} {a : α},
¬a ∈ s → ∀ (f : α → M), mulIndicator s f a = 1mulIndicator_of_not_mem h: ?m.2442h f: α → Mf)Goals accomplished! 🐙
#align set.mul_indicator_eq_one_or_self Set.mulIndicator_eq_one_or_self: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : α → M) (a : α),
mulIndicator s f a = 1 ∨ mulIndicator s f a = f aSet.mulIndicator_eq_one_or_self
#align set.indicator_eq_zero_or_self Set.indicator_eq_zero_or_self: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : α → M) (a : α),
indicator s f a = 0 ∨ indicator s f a = f aSet.indicator_eq_zero_or_self

@[to_additive: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : α → M} {a : α},
indicator s f a = f a ↔ ¬a ∈ s → f a = 0to_additive (attr := simp)]
theorem mulIndicator_apply_eq_self: mulIndicator s f a = f a ↔ ¬a ∈ s → f a = 1mulIndicator_apply_eq_self : s: Set αs.mulIndicator: {α : Type ?u.2586} → {M : Type ?u.2585} → [inst : One M] → Set α → (α → M) → α → MmulIndicator f: α → Mf a: αa = f: α → Mf a: αa ↔ a: αa ∉ s: Set αs → f: α → Mf a: αa = 1: ?m.26351 :=
letI := Classical.dec: (p : Prop) → Decidable pClassical.dec (a: αa ∈ s: Set αs)
ite_eq_left_iff: ∀ {α : Sort ?u.2695} {P : Prop} [inst : Decidable P] {a b : α}, (if P then a else b) = a ↔ ¬P → b = aite_eq_left_iff.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans (byGoals accomplished! 🐙 α: Type u_2β: Type ?u.2550ι: Type ?u.2553M: Type u_1N: Type ?u.2559inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αthis:= Classical.dec (a ∈ s): Decidable (a ∈ s)¬a ∈ s → 1 = f a ↔ ¬a ∈ s → f a = 1rw [α: Type u_2β: Type ?u.2550ι: Type ?u.2553M: Type u_1N: Type ?u.2559inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αthis:= Classical.dec (a ∈ s): Decidable (a ∈ s)¬a ∈ s → 1 = f a ↔ ¬a ∈ s → f a = 1@eq_comm: ∀ {α : Sort ?u.2930} {a b : α}, a = b ↔ b = aeq_comm _: Sort ?u.2930_ (f: α → Mf a: αa)α: Type u_2β: Type ?u.2550ι: Type ?u.2553M: Type u_1N: Type ?u.2559inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αthis:= Classical.dec (a ∈ s): Decidable (a ∈ s)¬a ∈ s → 1 = f a ↔ ¬a ∈ s → 1 = f a]Goals accomplished! 🐙)
#align set.mul_indicator_apply_eq_self Set.mulIndicator_apply_eq_self: ∀ {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : α → M} {a : α},
mulIndicator s f a = f a ↔ ¬a ∈ s → f a = 1Set.mulIndicator_apply_eq_self
#align set.indicator_apply_eq_self Set.indicator_apply_eq_self: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : α → M} {a : α},
indicator s f a = f a ↔ ¬a ∈ s → f a = 0Set.indicator_apply_eq_self

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, indicator s f = f ↔ support f ⊆ sto_additive (attr := simp)]
theorem mulIndicator_eq_self: mulIndicator s f = f ↔ mulSupport f ⊆ smulIndicator_eq_self : s: Set αs.mulIndicator: {α : Type ?u.3109} → {M : Type ?u.3108} → [inst : One M] → Set α → (α → M) → α → MmulIndicator f: α → Mf = f: α → Mf ↔ mulSupport: {α : Type ?u.3146} → {M : Type ?u.3145} → [inst : One M] → (α → M) → Set αmulSupport f: α → Mf ⊆ s: Set αs := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.3073ι: Type ?u.3076M: Type u_2N: Type ?u.3082inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αmulIndicator s f = f ↔ mulSupport f ⊆ ssimp only [funext_iff: ∀ {α : Sort ?u.3209} {β : α → Sort ?u.3208} {f₁ f₂ : (x : α) → β x}, f₁ = f₂ ↔ ∀ (a : α), f₁ a = f₂ afunext_iff, subset_def: ∀ {α : Type ?u.3229} {s t : Set α}, (s ⊆ t) = ∀ (x : α), x ∈ s → x ∈ tsubset_def, mem_mulSupport: ∀ {α : Type ?u.3242} {M : Type ?u.3243} [inst : One M] {f : α → M} {x : α}, x ∈ mulSupport f ↔ f x ≠ 1mem_mulSupport, mulIndicator_apply_eq_self: ∀ {α : Type ?u.3276} {M : Type ?u.3275} [inst : One M] {s : Set α} {f : α → M} {a : α},
mulIndicator s f a = f a ↔ ¬a ∈ s → f a = 1mulIndicator_apply_eq_self, not_imp_comm: ∀ {a b : Prop}, ¬a → b ↔ ¬b → anot_imp_comm]Goals accomplished! 🐙
#align set.mul_indicator_eq_self Set.mulIndicator_eq_self: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : α → M}, mulIndicator s f = f ↔ mulSupport f ⊆ sSet.mulIndicator_eq_self
#align set.indicator_eq_self Set.indicator_eq_self: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, indicator s f = f ↔ support f ⊆ sSet.indicator_eq_self

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s t : Set α} {f : α → M}, indicator s f = f → s ⊆ t → indicator t f = fto_additive]
theorem mulIndicator_eq_self_of_superset: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s t : Set α} {f : α → M},
mulIndicator s f = f → s ⊆ t → mulIndicator t f = fmulIndicator_eq_self_of_superset (h1: mulIndicator s f = fh1 : s: Set αs.mulIndicator: {α : Type ?u.3845} → {M : Type ?u.3844} → [inst : One M] → Set α → (α → M) → α → MmulIndicator f: α → Mf = f: α → Mf) (h2: s ⊆ th2 : s: Set αs ⊆ t: Set αt) :
t: Set αt.mulIndicator: {α : Type ?u.3902} → {M : Type ?u.3901} → [inst : One M] → Set α → (α → M) → α → MmulIndicator f: α → Mf = f: α → Mf := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.3809ι: Type ?u.3812M: Type u_2N: Type ?u.3818inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh1: mulIndicator s f = fh2: s ⊆ tmulIndicator t f = frw [α: Type u_1β: Type ?u.3809ι: Type ?u.3812M: Type u_2N: Type ?u.3818inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh1: mulIndicator s f = fh2: s ⊆ tmulIndicator t f = fmulIndicator_eq_self: ∀ {α : Type ?u.3924} {M : Type ?u.3925} [inst : One M] {s : Set α} {f : α → M}, mulIndicator s f = f ↔ mulSupport f ⊆ smulIndicator_eq_selfα: Type u_1β: Type ?u.3809ι: Type ?u.3812M: Type u_2N: Type ?u.3818inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh1: mulSupport f ⊆ sh2: s ⊆ tmulSupport f ⊆ t]α: Type u_1β: Type ?u.3809ι: Type ?u.3812M: Type u_2N: Type ?u.3818inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh1: mulSupport f ⊆ sh2: s ⊆ tmulSupport f ⊆ t at h1: mulIndicator s f = fh1⊢α: Type u_1β: Type ?u.3809ι: Type ?u.3812M: Type u_2N: Type ?u.3818inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh1: mulSupport f ⊆ sh2: s ⊆ tmulSupport f ⊆ t
α: Type u_1β: Type ?u.3809ι: Type ?u.3812M: Type u_2N: Type ?u.3818inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh1: mulIndicator s f = fh2: s ⊆ tmulIndicator t f = fexact Subset.trans: ∀ {α : Type ?u.4188} {a b c : Set α}, a ⊆ b → b ⊆ c → a ⊆ cSubset.trans h1: mulSupport f ⊆ sh1 h2: s ⊆ th2Goals accomplished! 🐙
#align set.mul_indicator_eq_self_of_superset Set.mulIndicator_eq_self_of_superset: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s t : Set α} {f : α → M},
mulIndicator s f = f → s ⊆ t → mulIndicator t f = fSet.mulIndicator_eq_self_of_superset
#align set.indicator_eq_self_of_superset Set.indicator_eq_self_of_superset: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s t : Set α} {f : α → M}, indicator s f = f → s ⊆ t → indicator t f = fSet.indicator_eq_self_of_superset

@[to_additive: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, indicator s f a = 0 ↔ a ∈ s → f a = 0to_additive (attr := simp)]
theorem mulIndicator_apply_eq_one: ∀ {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : α → M} {a : α}, mulIndicator s f a = 1 ↔ a ∈ s → f a = 1mulIndicator_apply_eq_one : mulIndicator: {α : Type ?u.4296} → {M : Type ?u.4295} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf a: αa = 1: ?m.43221 ↔ a: αa ∈ s: Set αs → f: α → Mf a: αa = 1: ?m.43921 :=
letI := Classical.dec: (p : Prop) → Decidable pClassical.dec (a: αa ∈ s: Set αs)
ite_eq_right_iff: ∀ {α : Sort ?u.4430} {P : Prop} [inst : Decidable P] {a b : α}, (if P then a else b) = b ↔ P → a = bite_eq_right_iff
#align set.mul_indicator_apply_eq_one Set.mulIndicator_apply_eq_one: ∀ {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : α → M} {a : α}, mulIndicator s f a = 1 ↔ a ∈ s → f a = 1Set.mulIndicator_apply_eq_one
#align set.indicator_apply_eq_zero Set.indicator_apply_eq_zero: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, indicator s f a = 0 ↔ a ∈ s → f a = 0Set.indicator_apply_eq_zero

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M},
(indicator s f = fun x => 0) ↔ Disjoint (support f) sto_additive (attr := simp)]
theorem mulIndicator_eq_one: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : α → M},
(mulIndicator s f = fun x => 1) ↔ Disjoint (mulSupport f) smulIndicator_eq_one : (mulIndicator: {α : Type ?u.4806} → {M : Type ?u.4805} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf = fun x: ?m.4833x => 1: ?m.48361) ↔ Disjoint: {α : Type ?u.4918} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (mulSupport: {α : Type ?u.4923} → {M : Type ?u.4922} → [inst : One M] → (α → M) → Set αmulSupport f: α → Mf) s: Set αs := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.4770ι: Type ?u.4773M: Type u_2N: Type ?u.4779inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: α(mulIndicator s f = fun x => 1) ↔ Disjoint (mulSupport f) ssimp only [funext_iff: ∀ {α : Sort ?u.5311} {β : α → Sort ?u.5310} {f₁ f₂ : (x : α) → β x}, f₁ = f₂ ↔ ∀ (a : α), f₁ a = f₂ afunext_iff, mulIndicator_apply_eq_one: ∀ {α : Type ?u.5332} {M : Type ?u.5331} [inst : One M] {s : Set α} {f : α → M} {a : α},
mulIndicator s f a = 1 ↔ a ∈ s → f a = 1mulIndicator_apply_eq_one, Set.disjoint_left: ∀ {α : Type ?u.5369} {s t : Set α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ tSet.disjoint_left, mem_mulSupport: ∀ {α : Type ?u.5390} {M : Type ?u.5391} [inst : One M] {f : α → M} {x : α}, x ∈ mulSupport f ↔ f x ≠ 1mem_mulSupport,
not_imp_not: ∀ {a b : Prop}, ¬a → ¬b ↔ b → anot_imp_not]Goals accomplished! 🐙
#align set.mul_indicator_eq_one Set.mulIndicator_eq_one: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : α → M},
(mulIndicator s f = fun x => 1) ↔ Disjoint (mulSupport f) sSet.mulIndicator_eq_one
#align set.indicator_eq_zero Set.indicator_eq_zero: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M},
(indicator s f = fun x => 0) ↔ Disjoint (support f) sSet.indicator_eq_zero

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, indicator s f = 0 ↔ Disjoint (support f) sto_additive (attr := simp)]
theorem mulIndicator_eq_one': mulIndicator s f = 1 ↔ Disjoint (mulSupport f) smulIndicator_eq_one' : mulIndicator: {α : Type ?u.5957} → {M : Type ?u.5956} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf = 1: ?m.59841 ↔ Disjoint: {α : Type ?u.6064} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint (mulSupport: {α : Type ?u.6069} → {M : Type ?u.6068} → [inst : One M] → (α → M) → Set αmulSupport f: α → Mf) s: Set αs :=
mulIndicator_eq_one: ∀ {α : Type ?u.6444} {M : Type ?u.6445} [inst : One M] {s : Set α} {f : α → M},
(mulIndicator s f = fun x => 1) ↔ Disjoint (mulSupport f) smulIndicator_eq_one
#align set.mul_indicator_eq_one' Set.mulIndicator_eq_one': ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : α → M}, mulIndicator s f = 1 ↔ Disjoint (mulSupport f) sSet.mulIndicator_eq_one'
#align set.indicator_eq_zero' Set.indicator_eq_zero': ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, indicator s f = 0 ↔ Disjoint (support f) sSet.indicator_eq_zero'

@[to_additive: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, indicator s f a ≠ 0 ↔ a ∈ s ∩ support fto_additive]
theorem mulIndicator_apply_ne_one: ∀ {a : α}, mulIndicator s f a ≠ 1 ↔ a ∈ s ∩ mulSupport fmulIndicator_apply_ne_one {a: αa : α: Type ?u.6620α} : s: Set αs.mulIndicator: {α : Type ?u.6662} → {M : Type ?u.6661} → [inst : One M] → Set α → (α → M) → α → MmulIndicator f: α → Mf a: αa ≠ 1: ?m.67251 ↔ a: αa ∈ s: Set αs ∩ mulSupport: {α : Type ?u.6766} → {M : Type ?u.6765} → [inst : One M] → (α → M) → Set αmulSupport f: α → Mf := byGoals accomplished! 🐙
α: Type u_2β: Type ?u.6623ι: Type ?u.6626M: Type u_1N: Type ?u.6632inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma✝, a: αmulIndicator s f a ≠ 1 ↔ a ∈ s ∩ mulSupport fsimp only [Ne.def: ∀ {α : Sort ?u.6838} (a b : α), (a ≠ b) = ¬a = bNe.def, mulIndicator_apply_eq_one: ∀ {α : Type ?u.6851} {M : Type ?u.6850} [inst : One M] {s : Set α} {f : α → M} {a : α},
mulIndicator s f a = 1 ↔ a ∈ s → f a = 1mulIndicator_apply_eq_one, not_imp: ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬bnot_imp, mem_inter_iff: ∀ {α : Type ?u.6898} (x : α) (a b : Set α), x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ bmem_inter_iff, mem_mulSupport: ∀ {α : Type ?u.6926} {M : Type ?u.6927} [inst : One M] {f : α → M} {x : α}, x ∈ mulSupport f ↔ f x ≠ 1mem_mulSupport]Goals accomplished! 🐙
#align set.mul_indicator_apply_ne_one Set.mulIndicator_apply_ne_one: ∀ {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : α → M} {a : α},
mulIndicator s f a ≠ 1 ↔ a ∈ s ∩ mulSupport fSet.mulIndicator_apply_ne_one
#align set.indicator_apply_ne_zero Set.indicator_apply_ne_zero: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, indicator s f a ≠ 0 ↔ a ∈ s ∩ support fSet.indicator_apply_ne_zero

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, support (indicator s f) = s ∩ support fto_additive (attr := simp)]
theorem mulSupport_mulIndicator: mulSupport (mulIndicator s f) = s ∩ mulSupport fmulSupport_mulIndicator :
Function.mulSupport: {α : Type ?u.7278} → {M : Type ?u.7277} → [inst : One M] → (α → M) → Set αFunction.mulSupport (s: Set αs.mulIndicator: {α : Type ?u.7283} → {M : Type ?u.7282} → [inst : One M] → Set α → (α → M) → α → MmulIndicator f: α → Mf) = s: Set αs ∩ Function.mulSupport: {α : Type ?u.7356} → {M : Type ?u.7355} → [inst : One M] → (α → M) → Set αFunction.mulSupport f: α → Mf :=
ext: ∀ {α : Type ?u.7407} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = bext fun x: ?m.7416x => byGoals accomplished! 🐙 α: Type u_1β: Type ?u.7242ι: Type ?u.7245M: Type u_2N: Type ?u.7251inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma, x: αx ∈ mulSupport (mulIndicator s f) ↔ x ∈ s ∩ mulSupport fsimp [Function.mem_mulSupport: ∀ {α : Type ?u.7424} {M : Type ?u.7425} [inst : One M] {f : α → M} {x : α}, x ∈ mulSupport f ↔ f x ≠ 1Function.mem_mulSupport, mulIndicator_apply_eq_one: ∀ {α : Type ?u.7458} {M : Type ?u.7457} [inst : One M] {s : Set α} {f : α → M} {a : α},
mulIndicator s f a = 1 ↔ a ∈ s → f a = 1mulIndicator_apply_eq_one]Goals accomplished! 🐙
#align set.mul_support_mul_indicator Set.mulSupport_mulIndicator: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : α → M}, mulSupport (mulIndicator s f) = s ∩ mulSupport fSet.mulSupport_mulIndicator
#align set.support_indicator Set.support_indicator: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, support (indicator s f) = s ∩ support fSet.support_indicator

/-- If a multiplicative indicator function is not equal to `1` at a point, then that point is in the
set. -/
@[to_additive: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, indicator s f a ≠ 0 → a ∈ sto_additive
"If an additive indicator function is not equal to `0` at a point, then that point is
in the set."]
theorem mem_of_mulIndicator_ne_one: mulIndicator s f a ≠ 1 → a ∈ smem_of_mulIndicator_ne_one (h: mulIndicator s f a ≠ 1h : mulIndicator: {α : Type ?u.8533} → {M : Type ?u.8532} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf a: αa ≠ 1: ?m.85921) : a: αa ∈ s: Set αs :=
not_imp_comm: ∀ {a b : Prop}, ¬a → b ↔ ¬b → anot_imp_comm.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 (fun hn: ?m.8658hn => mulIndicator_of_not_mem: ∀ {α : Type ?u.8660} {M : Type ?u.8661} [inst : One M] {s : Set α} {a : α},
¬a ∈ s → ∀ (f : α → M), mulIndicator s f a = 1mulIndicator_of_not_mem hn: ?m.8658hn f: α → Mf) h: mulIndicator s f a ≠ 1h
#align set.mem_of_mul_indicator_ne_one Set.mem_of_mulIndicator_ne_one: ∀ {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : α → M} {a : α}, mulIndicator s f a ≠ 1 → a ∈ sSet.mem_of_mulIndicator_ne_one
#align set.mem_of_indicator_ne_zero Set.mem_of_indicator_ne_zero: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, indicator s f a ≠ 0 → a ∈ sSet.mem_of_indicator_ne_zero

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, EqOn (indicator s f) f sto_additive]
theorem eqOn_mulIndicator: EqOn (mulIndicator s f) f seqOn_mulIndicator : EqOn: {α : Type ?u.8788} → {β : Type ?u.8787} → (α → β) → (α → β) → Set α → PropEqOn (mulIndicator: {α : Type ?u.8792} → {M : Type ?u.8791} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf) f: α → Mf s: Set αs := fun _: ?m.8861_ hx: ?m.8864hx => mulIndicator_of_mem: ∀ {α : Type ?u.8866} {M : Type ?u.8867} [inst : One M] {s : Set α} {a : α},
a ∈ s → ∀ (f : α → M), mulIndicator s f a = f amulIndicator_of_mem hx: ?m.8864hx f: α → Mf
#align set.eq_on_mul_indicator Set.eqOn_mulIndicator: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : α → M}, EqOn (mulIndicator s f) f sSet.eqOn_mulIndicator
#align set.eq_on_indicator Set.eqOn_indicator: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, EqOn (indicator s f) f sSet.eqOn_indicator

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, support (indicator s f) ⊆ sto_additive]
theorem mulSupport_mulIndicator_subset: mulSupport (mulIndicator s f) ⊆ smulSupport_mulIndicator_subset : mulSupport: {α : Type ?u.8990} → {M : Type ?u.8989} → [inst : One M] → (α → M) → Set αmulSupport (s: Set αs.mulIndicator: {α : Type ?u.9029} → {M : Type ?u.9028} → [inst : One M] → Set α → (α → M) → α → MmulIndicator f: α → Mf) ⊆ s: Set αs := fun _: ?m.9106_ hx: ?m.9109hx =>
hx: ?m.9109hx.imp_symm: ∀ {a b : Prop}, (¬a → b) → ¬b → aimp_symm fun h: ?m.9118h => mulIndicator_of_not_mem: ∀ {α : Type ?u.9120} {M : Type ?u.9121} [inst : One M] {s : Set α} {a : α},
¬a ∈ s → ∀ (f : α → M), mulIndicator s f a = 1mulIndicator_of_not_mem h: ?m.9118h f: α → Mf
#align set.mul_support_mul_indicator_subset Set.mulSupport_mulIndicator_subset: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : α → M}, mulSupport (mulIndicator s f) ⊆ sSet.mulSupport_mulIndicator_subset
#align set.support_indicator_subset Set.support_indicator_subset: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, support (indicator s f) ⊆ sSet.support_indicator_subset

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M}, indicator (support f) f = fto_additive (attr := simp)]
theorem mulIndicator_mulSupport: mulIndicator (mulSupport f) f = fmulIndicator_mulSupport : mulIndicator: {α : Type ?u.9242} → {M : Type ?u.9241} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (mulSupport: {α : Type ?u.9247} → {M : Type ?u.9246} → [inst : One M] → (α → M) → Set αmulSupport f: α → Mf) f: α → Mf = f: α → Mf :=
mulIndicator_eq_self: ∀ {α : Type ?u.9314} {M : Type ?u.9315} [inst : One M] {s : Set α} {f : α → M}, mulIndicator s f = f ↔ mulSupport f ⊆ smulIndicator_eq_self.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 Subset.rfl: ∀ {α : Type ?u.9372} {s : Set α}, s ⊆ sSubset.rfl
#align set.mul_indicator_mul_support Set.mulIndicator_mulSupport: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {f : α → M}, mulIndicator (mulSupport f) f = fSet.mulIndicator_mulSupport
#align set.indicator_support Set.indicator_support: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M}, indicator (support f) f = fSet.indicator_support

@[to_additive: ∀ {α : Type u_3} {M : Type u_2} [inst : Zero M] {ι : Sort u_1} (f : ι → α) (g : α → M),
indicator (range f) g ∘ f = g ∘ fto_additive (attr := simp)]
theorem mulIndicator_range_comp: ∀ {α : Type u_3} {M : Type u_2} [inst : One M] {ι : Sort u_1} (f : ι → α) (g : α → M),
mulIndicator (range f) g ∘ f = g ∘ fmulIndicator_range_comp {ι: Sort ?u.9500ι : Sort _: Type ?u.9500SortSort _: Type ?u.9500 _} (f: ι → αf : ι: Sort ?u.9500ι → α: Type ?u.9463α) (g: α → Mg : α: Type ?u.9463α → M: Type ?u.9472M) :
mulIndicator: {α : Type ?u.9519} → {M : Type ?u.9518} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (range: {α : Type ?u.9559} → {ι : Sort ?u.9558} → (ι → α) → Set αrange f: ι → αf) g: α → Mg ∘ f: ι → αf = g: α → Mg ∘ f: ι → αf :=
letI := Classical.decPred: {α : Sort ?u.9616} → (p : α → Prop) → DecidablePred pClassical.decPred (· ∈ range: {α : Type ?u.9627} → {ι : Sort ?u.9626} → (ι → α) → Set αrange f: ι → αf)
piecewise_range_comp: ∀ {α : Type ?u.9653} {β : Type ?u.9654} {ι : Sort ?u.9652} (f : ι → α) [inst : (j : α) → Decidable (j ∈ range f)]
(g₁ g₂ : α → β), piecewise (range f) g₁ g₂ ∘ f = g₁ ∘ fpiecewise_range_comp _: ?m.9657 → ?m.9655_ _: ?m.9655 → ?m.9656_ _: ?m.9655 → ?m.9656_
#align set.mul_indicator_range_comp Set.mulIndicator_range_comp: ∀ {α : Type u_3} {M : Type u_2} [inst : One M] {ι : Sort u_1} (f : ι → α) (g : α → M),
mulIndicator (range f) g ∘ f = g ∘ fSet.mulIndicator_range_comp
#align set.indicator_range_comp Set.indicator_range_comp: ∀ {α : Type u_3} {M : Type u_2} [inst : Zero M] {ι : Sort u_1} (f : ι → α) (g : α → M),
indicator (range f) g ∘ f = g ∘ fSet.indicator_range_comp

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f g : α → M}, EqOn f g s → indicator s f = indicator s gto_additive]
theorem mulIndicator_congr: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f g : α → M},
EqOn f g s → mulIndicator s f = mulIndicator s gmulIndicator_congr (h: EqOn f g sh : EqOn: {α : Type ?u.9899} → {β : Type ?u.9898} → (α → β) → (α → β) → Set α → PropEqOn f: α → Mf g: α → Mg s: Set αs) : mulIndicator: {α : Type ?u.9914} → {M : Type ?u.9913} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf = mulIndicator: {α : Type ?u.9940} → {M : Type ?u.9939} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs g: α → Mg :=
funext: ∀ {α : Sort ?u.9956} {β : α → Sort ?u.9955} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext fun x: ?m.9970x => byGoals accomplished! 🐙
α: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: αmulIndicator s f x = mulIndicator s g xsimp only [mulIndicator: {α : Type ?u.9992} → {M : Type ?u.9991} → [inst : One M] → Set α → (α → M) → α → MmulIndicator]α: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: α(if x ∈ s then f x else 1) = if x ∈ s then g x else 1
α: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: αmulIndicator s f x = mulIndicator s g xsplit_ifs with h_1α: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: αh_1: x ∈ sinlf x = g xα: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: αh_1: ¬x ∈ sinr1 = 1
α: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: αmulIndicator s f x = mulIndicator s g x·α: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: αh_1: x ∈ sinlf x = g x α: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: αh_1: x ∈ sinlf x = g xα: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: αh_1: ¬x ∈ sinr1 = 1exact h: EqOn f g sh h_1: x ∈ sh_1Goals accomplished! 🐙
α: Type u_1β: Type ?u.9864ι: Type ?u.9867M: Type u_2N: Type ?u.9873inst✝¹: One Minst✝: One Ns, t: Set αf, g: α → Ma: αh: EqOn f g sx: αmulIndicator s f x = mulIndicator s g xrflGoals accomplished! 🐙
#align set.mul_indicator_congr Set.mulIndicator_congr: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f g : α → M},
EqOn f g s → mulIndicator s f = mulIndicator s gSet.mulIndicator_congr
#align set.indicator_congr Set.indicator_congr: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f g : α → M}, EqOn f g s → indicator s f = indicator s gSet.indicator_congr

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), indicator univ f = fto_additive (attr := simp)]
theorem mulIndicator_univ: ∀ (f : α → M), mulIndicator univ f = fmulIndicator_univ (f: α → Mf : α: Type ?u.10666α → M: Type ?u.10675M) : mulIndicator: {α : Type ?u.10709} → {M : Type ?u.10708} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (univ: {α : Type ?u.10715} → Set αuniv : Set: Type ?u.10714 → Type ?u.10714Set α: Type ?u.10666α) f: α → Mf = f: α → Mf :=
mulIndicator_eq_self: ∀ {α : Type ?u.10743} {M : Type ?u.10744} [inst : One M] {s : Set α} {f : α → M},
mulIndicator s f = f ↔ mulSupport f ⊆ smulIndicator_eq_self.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 <| subset_univ: ∀ {α : Type ?u.10801} (s : Set α), s ⊆ univsubset_univ _: Set ?m.10802_
#align set.mul_indicator_univ Set.mulIndicator_univ: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (f : α → M), mulIndicator univ f = fSet.mulIndicator_univ
#align set.indicator_univ Set.indicator_univ: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), indicator univ f = fSet.indicator_univ

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), indicator ∅ f = fun x => 0to_additive (attr := simp)]
theorem mulIndicator_empty: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (f : α → M), mulIndicator ∅ f = fun x => 1mulIndicator_empty (f: α → Mf : α: Type ?u.10885α → M: Type ?u.10894M) : mulIndicator: {α : Type ?u.10928} → {M : Type ?u.10927} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (∅: ?m.10935∅ : Set: Type ?u.10933 → Type ?u.10933Set α: Type ?u.10885α) f: α → Mf = fun _: ?m.11001_ => 1: ?m.110041 :=
mulIndicator_eq_one: ∀ {α : Type ?u.11088} {M : Type ?u.11089} [inst : One M] {s : Set α} {f : α → M},
(mulIndicator s f = fun x => 1) ↔ Disjoint (mulSupport f) smulIndicator_eq_one.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 <| disjoint_empty: ∀ {α : Type ?u.11147} (s : Set α), Disjoint s ∅disjoint_empty _: Set ?m.11148_
#align set.mul_indicator_empty Set.mulIndicator_empty: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (f : α → M), mulIndicator ∅ f = fun x => 1Set.mulIndicator_empty
#align set.indicator_empty Set.indicator_empty: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), indicator ∅ f = fun x => 0Set.indicator_empty

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), indicator ∅ f = 0to_additive]
theorem mulIndicator_empty': ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (f : α → M), mulIndicator ∅ f = 1mulIndicator_empty' (f: α → Mf : α: Type ?u.11248α → M: Type ?u.11257M) : mulIndicator: {α : Type ?u.11291} → {M : Type ?u.11290} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (∅: ?m.11298∅ : Set: Type ?u.11296 → Type ?u.11296Set α: Type ?u.11248α) f: α → Mf = 1: ?m.113641 :=
mulIndicator_empty: ∀ {α : Type ?u.11446} {M : Type ?u.11447} [inst : One M] (f : α → M), mulIndicator ∅ f = fun x => 1mulIndicator_empty f: α → Mf
#align set.mul_indicator_empty' Set.mulIndicator_empty': ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (f : α → M), mulIndicator ∅ f = 1Set.mulIndicator_empty'
#align set.indicator_empty' Set.indicator_empty': ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), indicator ∅ f = 0Set.indicator_empty'

variable (M: ?m.11540M)

@[to_additive: ∀ {α : Type u_1} (M : Type u_2) [inst : Zero M] (s : Set α), (indicator s fun x => 0) = fun x => 0to_additive (attr := simp)]
theorem mulIndicator_one: ∀ (s : Set α), (mulIndicator s fun x => 1) = fun x => 1mulIndicator_one (s: Set αs : Set: Type ?u.11580 → Type ?u.11580Set α: Type ?u.11543α) : (mulIndicator: {α : Type ?u.11585} → {M : Type ?u.11584} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs fun _: ?m.11593_ => (1: ?m.115971 : M: Type ?u.11552M)) = fun _: ?m.11640_ => (1: ?m.116441 : M: Type ?u.11552M) :=
mulIndicator_eq_one: ∀ {α : Type ?u.11687} {M : Type ?u.11688} [inst : One M] {s : Set α} {f : α → M},
(mulIndicator s f = fun x => 1) ↔ Disjoint (mulSupport f) smulIndicator_eq_one.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 <| byGoals accomplished! 🐙 α: Type u_1β: Type ?u.11546ι: Type ?u.11549M: Type u_2N: Type ?u.11555inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set αDisjoint (mulSupport fun x => 1) ssimp only [mulSupport_one: ∀ {α : Type ?u.11774} {M : Type ?u.11775} [inst : One M], (mulSupport fun x => 1) = ∅mulSupport_one, empty_disjoint: ∀ {α : Type ?u.11789} (s : Set α), Disjoint ∅ sempty_disjoint]Goals accomplished! 🐙
#align set.mul_indicator_one Set.mulIndicator_one: ∀ {α : Type u_1} (M : Type u_2) [inst : One M] (s : Set α), (mulIndicator s fun x => 1) = fun x => 1Set.mulIndicator_one
#align set.indicator_zero Set.indicator_zero: ∀ {α : Type u_1} (M : Type u_2) [inst : Zero M] (s : Set α), (indicator s fun x => 0) = fun x => 0Set.indicator_zero

@[to_additive: ∀ {α : Type u_1} (M : Type u_2) [inst : Zero M] {s : Set α}, indicator s 0 = 0to_additive (attr := simp)]
theorem mulIndicator_one': ∀ {s : Set α}, mulIndicator s 1 = 1mulIndicator_one' {s: Set αs : Set: Type ?u.12034 → Type ?u.12034Set α: Type ?u.11997α} : s: Set αs.mulIndicator: {α : Type ?u.12039} → {M : Type ?u.12038} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (1: ?m.120541 : α: Type ?u.11997α → M: Type ?u.12006M) = 1: ?m.121371 :=
mulIndicator_one: ∀ {α : Type ?u.12157} (M : Type ?u.12158) [inst : One M] (s : Set α), (mulIndicator s fun x => 1) = fun x => 1mulIndicator_one M: Type ?u.12006M s: Set αs
#align set.mul_indicator_one' Set.mulIndicator_one': ∀ {α : Type u_1} (M : Type u_2) [inst : One M] {s : Set α}, mulIndicator s 1 = 1Set.mulIndicator_one'
#align set.indicator_zero' Set.indicator_zero': ∀ {α : Type u_1} (M : Type u_2) [inst : Zero M] {s : Set α}, indicator s 0 = 0Set.indicator_zero'

variable {M: ?m.12292M}

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s t : Set α) (f : α → M),
indicator s (indicator t f) = indicator (s ∩ t) fto_additive]
theorem mulIndicator_mulIndicator: ∀ (s t : Set α) (f : α → M), mulIndicator s (mulIndicator t f) = mulIndicator (s ∩ t) fmulIndicator_mulIndicator (s: Set αs t: Set αt : Set: Type ?u.12335 → Type ?u.12335Set α: Type ?u.12295α) (f: α → Mf : α: Type ?u.12295α → M: Type ?u.12304M) :
mulIndicator: {α : Type ?u.12344} → {M : Type ?u.12343} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs (mulIndicator: {α : Type ?u.12352} → {M : Type ?u.12351} → [inst : One M] → Set α → (α → M) → α → MmulIndicator t: Set αt f: α → Mf) = mulIndicator: {α : Type ?u.12415} → {M : Type ?u.12414} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (s: Set αs ∩ t: Set αt) f: α → Mf :=
funext: ∀ {α : Sort ?u.12451} {β : α → Sort ?u.12450} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext fun x: ?m.12465x => byGoals accomplished! 🐙
α: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αmulIndicator s (mulIndicator t f) x = mulIndicator (s ∩ t) f xsimp only [mulIndicator: {α : Type ?u.12487} → {M : Type ?u.12486} → [inst : One M] → Set α → (α → M) → α → MmulIndicator]α: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: α(if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1
α: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αmulIndicator s (mulIndicator t f) x = mulIndicator (s ∩ t) f xsplit_ifsα: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝²: x ∈ sh✝¹: x ∈ th✝: x ∈ s ∩ tinl.inl.inlf x = f xα: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝²: x ∈ sh✝¹: x ∈ th✝: ¬x ∈ s ∩ tinl.inl.inrf x = 1α: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝²: x ∈ sh✝¹: ¬x ∈ th✝: x ∈ s ∩ tinl.inr.inl1 = f xα: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝²: x ∈ sh✝¹: ¬x ∈ th✝: ¬x ∈ s ∩ tinl.inr.inr1 = 1α: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝¹: ¬x ∈ sh✝: x ∈ s ∩ tinr.inl1 = f xα: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝¹: ¬x ∈ sh✝: ¬x ∈ s ∩ tinr.inr1 = 1
α: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αmulIndicator s (mulIndicator t f) x = mulIndicator (s ∩ t) f xrepeat' α: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝²: x ∈ sh✝¹: x ∈ th✝: x ∈ s ∩ tinl.inl.inlf x = f xα: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝²: x ∈ sh✝¹: x ∈ th✝: ¬x ∈ s ∩ tinl.inl.inrf x = 1α: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝²: x ∈ sh✝¹: ¬x ∈ th✝: x ∈ s ∩ tinl.inr.inl1 = f xα: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝²: x ∈ sh✝¹: ¬x ∈ th✝: ¬x ∈ s ∩ tinl.inr.inr1 = 1α: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝¹: ¬x ∈ sh✝: x ∈ s ∩ tinr.inl1 = f xα: Type u_1β: Type ?u.12298ι: Type ?u.12301M: Type u_2N: Type ?u.12307inst✝¹: One Minst✝: One Ns✝, t✝: Set αf✝, g: α → Ma: αs, t: Set αf: α → Mx: αh✝¹: ¬x ∈ sh✝: ¬x ∈ s ∩ tinr.inr1 = 1simp_all (config := { contextual := true: Booltrue })Goals accomplished! 🐙
#align set.mul_indicator_mul_indicator Set.mulIndicator_mulIndicator: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (s t : Set α) (f : α → M),
mulIndicator s (mulIndicator t f) = mulIndicator (s ∩ t) fSet.mulIndicator_mulIndicator
#align set.indicator_indicator Set.indicator_indicator: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s t : Set α) (f : α → M),
indicator s (indicator t f) = indicator (s ∩ t) fSet.indicator_indicator

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : α → M), indicator (s ∩ support f) f = indicator s fto_additive (attr := simp)]
theorem mulIndicator_inter_mulSupport: ∀ (s : Set α) (f : α → M), mulIndicator (s ∩ mulSupport f) f = mulIndicator s fmulIndicator_inter_mulSupport (s: Set αs : Set: Type ?u.15927 → Type ?u.15927Set α: Type ?u.15890α) (f: α → Mf : α: Type ?u.15890α → M: Type ?u.15899M) :
mulIndicator: {α : Type ?u.15936} → {M : Type ?u.15935} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (s: Set αs ∩ mulSupport: {α : Type ?u.15954} → {M : Type ?u.15953} → [inst : One M] → (α → M) → Set αmulSupport f: α → Mf) f: α → Mf = mulIndicator: {α : Type ?u.16023} → {M : Type ?u.16022} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.15893ι: Type ?u.15896M: Type u_2N: Type ?u.15902inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma: αs: Set αf: α → MmulIndicator (s ∩ mulSupport f) f = mulIndicator s frw [α: Type u_1β: Type ?u.15893ι: Type ?u.15896M: Type u_2N: Type ?u.15902inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma: αs: Set αf: α → MmulIndicator (s ∩ mulSupport f) f = mulIndicator s f← mulIndicator_mulIndicator: ∀ {α : Type ?u.16041} {M : Type ?u.16042} [inst : One M] (s t : Set α) (f : α → M),
mulIndicator s (mulIndicator t f) = mulIndicator (s ∩ t) fmulIndicator_mulIndicator,α: Type u_1β: Type ?u.15893ι: Type ?u.15896M: Type u_2N: Type ?u.15902inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma: αs: Set αf: α → MmulIndicator s (mulIndicator (mulSupport f) f) = mulIndicator s f α: Type u_1β: Type ?u.15893ι: Type ?u.15896M: Type u_2N: Type ?u.15902inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma: αs: Set αf: α → MmulIndicator (s ∩ mulSupport f) f = mulIndicator s fmulIndicator_mulSupport: ∀ {α : Type ?u.16156} {M : Type ?u.16157} [inst : One M] {f : α → M}, mulIndicator (mulSupport f) f = fmulIndicator_mulSupportα: Type u_1β: Type ?u.15893ι: Type ?u.15896M: Type u_2N: Type ?u.15902inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g: α → Ma: αs: Set αf: α → MmulIndicator s f = mulIndicator s f]Goals accomplished! 🐙
#align set.mul_indicator_inter_mul_support Set.mulIndicator_inter_mulSupport: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : α → M),
mulIndicator (s ∩ mulSupport f) f = mulIndicator s fSet.mulIndicator_inter_mulSupport
#align set.indicator_inter_support Set.indicator_inter_support: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : α → M), indicator (s ∩ support f) f = indicator s fSet.indicator_inter_support

@[to_additive: ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] (h : M → β) (f : α → M) {s : Set α} {x : α}
[inst_1 : DecidablePred fun x => x ∈ s], h (indicator s f x) = piecewise s (h ∘ f) (const α (h 0)) xto_additive]
theorem comp_mulIndicator: ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] (h : M → β) (f : α → M) {s : Set α} {x : α}
[inst_1 : DecidablePred fun x => x ∈ s], h (mulIndicator s f x) = piecewise s (h ∘ f) (const α (h 1)) xcomp_mulIndicator (h: M → βh : M: Type ?u.16346M → β: Type ?u.16340β) (f: α → Mf : α: Type ?u.16337α → M: Type ?u.16346M) {s: Set αs : Set: Type ?u.16382 → Type ?u.16382Set α: Type ?u.16337α} {x: αx : α: Type ?u.16337α} [DecidablePred: {α : Sort ?u.16387} → (α → Prop) → Sort (max1?u.16387)DecidablePred (· ∈ s: Set αs)] :
h: M → βh (s: Set αs.mulIndicator: {α : Type ?u.16419} → {M : Type ?u.16418} → [inst : One M] → Set α → (α → M) → α → MmulIndicator f: α → Mf x: αx) = s: Set αs.piecewise: {α : Type ?u.16481} →
{β : α → Sort ?u.16480} →
(s : Set α) → ((i : α) → β i) → ((i : α) → β i) → [inst : (j : α) → Decidable (j ∈ s)] → (i : α) → β ipiecewise (h: M → βh ∘ f: α → Mf) (const: {α : Sort ?u.16513} → (β : Sort ?u.16512) → α → β → αconst α: Type ?u.16337α (h: M → βh 1: ?m.165181)) x: αx := byGoals accomplished! 🐙
α: Type u_1β: Type u_2ι: Type ?u.16343M: Type u_3N: Type ?u.16349inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma: αh: M → βf: α → Ms: Set αx: αinst✝: DecidablePred fun x => x ∈ sh (mulIndicator s f x) = piecewise s (h ∘ f) (const α (h 1)) xletI := Classical.decPred: {α : Sort ?u.16581} → (p : α → Prop) → DecidablePred pClassical.decPred (· ∈ s: Set αs)α: Type u_1β: Type u_2ι: Type ?u.16343M: Type u_3N: Type ?u.16349inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma: αh: M → βf: α → Ms: Set αx: αinst✝: DecidablePred fun x => x ∈ sthis:= Classical.decPred fun x => x ∈ s: DecidablePred fun x => x ∈ sh (mulIndicator s f x) = piecewise s (h ∘ f) (const α (h 1)) x
α: Type u_1β: Type u_2ι: Type ?u.16343M: Type u_3N: Type ?u.16349inst✝²: One Minst✝¹: One Ns✝, t: Set αf✝, g: α → Ma: αh: M → βf: α → Ms: Set αx: αinst✝: DecidablePred fun x => x ∈ sh (mulIndicator s f x) = piecewise s (h ∘ f) (const α (h 1)) xconvert s: Set αs.apply_piecewise: ∀ {α : Type ?u.16612} {δ : α → Sort ?u.16613} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
{δ' : α → Sort ?u.16611} (h : (i : α) → δ i → δ' i) {x : α},
h x (piecewise s f g x) = piecewise s (fun x => h x (f x)) (fun x => h x (g x)) xapply_piecewise f: α → Mf (const: {α : Sort ?u.16650} → (β : Sort ?u.16649) → α → β → αconst α: Type u_1α 1: ?m.166551) (fun _: ?m.16688_ => h: M → βh) (x := x: αx) using 2Goals accomplished! 🐙
#align set.comp_mul_indicator Set.comp_mulIndicator: ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] (h : M → β) (f : α → M) {s : Set α} {x : α}
[inst_1 : DecidablePred fun x => x ∈ s], h (mulIndicator s f x) = piecewise s (h ∘ f) (const α (h 1)) xSet.comp_mulIndicator
#align set.comp_indicator Set.comp_indicator: ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] (h : M → β) (f : α → M) {s : Set α} {x : α}
[inst_1 : DecidablePred fun x => x ∈ s], h (indicator s f x) = piecewise s (h ∘ f) (const α (h 0)) xSet.comp_indicator

@[to_additive: ∀ {α : Type u_1} {β : Type u_3} {M : Type u_2} [inst : Zero M] {s : Set α} (f : β → α) {g : α → M} {x : β},
indicator (f ⁻¹' s) (g ∘ f) x = indicator s g (f x)to_additive]
theorem mulIndicator_comp_right: ∀ {α : Type u_1} {β : Type u_3} {M : Type u_2} [inst : One M] {s : Set α} (f : β → α) {g : α → M} {x : β},
mulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x)mulIndicator_comp_right {s: Set αs : Set: Type ?u.20700 → Type ?u.20700Set α: Type ?u.20663α} (f: β → αf : β: Type ?u.20666β → α: Type ?u.20663α) {g: α → Mg : α: Type ?u.20663α → M: Type ?u.20672M} {x: βx : β: Type ?u.20666β} :
mulIndicator: {α : Type ?u.20715} → {M : Type ?u.20714} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (f: β → αf ⁻¹' s: Set αs) (g: α → Mg ∘ f: β → αf) x: βx = mulIndicator: {α : Type ?u.20765} → {M : Type ?u.20764} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs g: α → Mg (f: β → αf x: βx) := byGoals accomplished! 🐙
α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βmulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x)simp only [mulIndicator: {α : Type ?u.20794} → {M : Type ?u.20793} → [inst : One M] → Set α → (α → M) → α → MmulIndicator, Function.comp: {α : Sort ?u.20825} → {β : Sort ?u.20824} → {δ : Sort ?u.20823} → (β → δ) → (α → β) → α → δFunction.comp]α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: β(if x ∈ f ⁻¹' s then g (f x) else 1) = if f x ∈ s then g (f x) else 1
α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βmulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x)split_ifs with h h' h''α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: x ∈ f ⁻¹' sh': f x ∈ sinl.inlg (f x) = g (f x)α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: x ∈ f ⁻¹' sh': ¬f x ∈ sinl.inrg (f x) = 1α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: ¬x ∈ f ⁻¹' sh'': f x ∈ sinr.inl1 = g (f x)α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: ¬x ∈ f ⁻¹' sh'': ¬f x ∈ sinr.inr1 = 1 α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: β(if x ∈ f ⁻¹' s then g (f x) else 1) = if f x ∈ s then g (f x) else 1<;>α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: x ∈ f ⁻¹' sh': f x ∈ sinl.inlg (f x) = g (f x)α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: x ∈ f ⁻¹' sh': ¬f x ∈ sinl.inrg (f x) = 1α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: ¬x ∈ f ⁻¹' sh'': f x ∈ sinr.inl1 = g (f x)α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: ¬x ∈ f ⁻¹' sh'': ¬f x ∈ sinr.inr1 = 1 α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: β(if x ∈ f ⁻¹' s then g (f x) else 1) = if f x ∈ s then g (f x) else 1first | α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: x ∈ f ⁻¹' sh': ¬f x ∈ sinl.inrg (f x) = 1rflα: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: ¬x ∈ f ⁻¹' sh'': f x ∈ sinr.inl1 = g (f x) | α: Type u_1β: Type u_3ι: Type ?u.20669M: Type u_2N: Type ?u.20675inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → αg: α → Mx: βh: x ∈ f ⁻¹' sh': ¬f x ∈ sinl.inrg (f x) = 1contradictionGoals accomplished! 🐙
#align set.mul_indicator_comp_right Set.mulIndicator_comp_right: ∀ {α : Type u_1} {β : Type u_3} {M : Type u_2} [inst : One M] {s : Set α} (f : β → α) {g : α → M} {x : β},
mulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x)Set.mulIndicator_comp_right
#align set.indicator_comp_right Set.indicator_comp_right: ∀ {α : Type u_1} {β : Type u_3} {M : Type u_2} [inst : Zero M] {s : Set α} (f : β → α) {g : α → M} {x : β},
indicator (f ⁻¹' s) (g ∘ f) x = indicator s g (f x)Set.indicator_comp_right

@[to_additive: ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {s : Set α} {f : β → M} {g : α → β},
Injective g → ∀ {x : α}, indicator (g '' s) f (g x) = indicator s (f ∘ g) xto_additive]
theorem mulIndicator_image: ∀ {s : Set α} {f : β → M} {g : α → β}, Injective g → ∀ {x : α}, mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) xmulIndicator_image {s: Set αs : Set: Type ?u.22149 → Type ?u.22149Set α: Type ?u.22112α} {f: β → Mf : β: Type ?u.22115β → M: Type ?u.22121M} {g: α → βg : α: Type ?u.22112α → β: Type ?u.22115β} (hg: Injective ghg : Injective: {α : Sort ?u.22161} → {β : Sort ?u.22160} → (α → β) → PropInjective g: α → βg) {x: αx : α: Type ?u.22112α} :
mulIndicator: {α : Type ?u.22173} → {M : Type ?u.22172} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (g: α → βg '' s: Set αs) f: β → Mf (g: α → βg x: αx) = mulIndicator: {α : Type ?u.22209} → {M : Type ?u.22208} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs (f: β → Mf ∘ g: α → βg) x: αx := byGoals accomplished! 🐙
α: Type u_1β: Type u_2ι: Type ?u.22118M: Type u_3N: Type ?u.22124inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → Mg: α → βhg: Injective gx: αmulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) xrw [α: Type u_1β: Type u_2ι: Type ?u.22118M: Type u_3N: Type ?u.22124inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → Mg: α → βhg: Injective gx: αmulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) x← mulIndicator_comp_right: ∀ {α : Type ?u.22241} {β : Type ?u.22243} {M : Type ?u.22242} [inst : One M] {s : Set α} (f : β → α) {g : α → M}
{x : β}, mulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x)mulIndicator_comp_right,α: Type u_1β: Type u_2ι: Type ?u.22118M: Type u_3N: Type ?u.22124inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → Mg: α → βhg: Injective gx: αmulIndicator (g ⁻¹' (g '' s)) (f ∘ g) x = mulIndicator s (f ∘ g) x α: Type u_1β: Type u_2ι: Type ?u.22118M: Type u_3N: Type ?u.22124inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → Mg: α → βhg: Injective gx: αmulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) xpreimage_image_eq: ∀ {α : Type ?u.22357} {β : Type ?u.22358} {f : α → β} (s : Set α), Injective f → f ⁻¹' (f '' s) = spreimage_image_eq _: Set ?m.22359_ hg: Injective ghgα: Type u_1β: Type u_2ι: Type ?u.22118M: Type u_3N: Type ?u.22124inst✝¹: One Minst✝: One Ns✝, t: Set αf✝, g✝: α → Ma: αs: Set αf: β → Mg: α → βhg: Injective gx: αmulIndicator s (f ∘ g) x = mulIndicator s (f ∘ g) x]Goals accomplished! 🐙
#align set.mul_indicator_image Set.mulIndicator_image: ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] {s : Set α} {f : β → M} {g : α → β},
Injective g → ∀ {x : α}, mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) xSet.mulIndicator_image
#align set.indicator_image Set.indicator_image: ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {s : Set α} {f : β → M} {g : α → β},
Injective g → ∀ {x : α}, indicator (g '' s) f (g x) = indicator s (f ∘ g) xSet.indicator_image

@[to_additive: ∀ {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst_1 : Zero N] {s : Set α} {f : α → M} {g : M → N},
g 0 = 0 → indicator s (g ∘ f) = g ∘ indicator s fto_additive]
theorem mulIndicator_comp_of_one: ∀ {g : M → N}, g 1 = 1 → mulIndicator s (g ∘ f) = g ∘ mulIndicator s fmulIndicator_comp_of_one {g: M → Ng : M: Type ?u.22463M → N: Type ?u.22466N} (hg: g 1 = 1hg : g: M → Ng 1: ?m.224971 = 1: ?m.225241) :
mulIndicator: {α : Type ?u.22568} → {M : Type ?u.22567} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs (g: M → Ng ∘ f: α → Mf) = g: M → Ng ∘ mulIndicator: {α : Type ?u.22616} → {M : Type ?u.22615} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf := byGoals accomplished! 🐙
α: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1mulIndicator s (g ∘ f) = g ∘ mulIndicator s ffunextα: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1x✝: αhmulIndicator s (g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝
α: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1mulIndicator s (g ∘ f) = g ∘ mulIndicator s fsimp only [mulIndicator: {α : Type ?u.22741} → {M : Type ?u.22740} → [inst : One M] → Set α → (α → M) → α → MmulIndicator]α: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1x✝: αh(if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ mulIndicator s f) x✝
α: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1mulIndicator s (g ∘ f) = g ∘ mulIndicator s fsplit_ifsα: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1x✝: αh✝: x✝ ∈ sh.inl(g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝α: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1x✝: αh✝: ¬x✝ ∈ sh.inr1 = (g ∘ mulIndicator s f) x✝ α: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1x✝: αh(if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ mulIndicator s f) x✝<;>α: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1x✝: αh✝: x✝ ∈ sh.inl(g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝α: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1x✝: αh✝: ¬x✝ ∈ sh.inr1 = (g ∘ mulIndicator s f) x✝ α: Type u_3β: Type ?u.22457ι: Type ?u.22460M: Type u_2N: Type u_1inst✝¹: One Minst✝: One Ns, t: Set αf, g✝: α → Ma: αg: M → Nhg: g 1 = 1x✝: αh(if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ mulIndicator s f) x✝simp [*]Goals accomplished! 🐙
#align set.mul_indicator_comp_of_one Set.mulIndicator_comp_of_one: ∀ {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : One M] [inst_1 : One N] {s : Set α} {f : α → M} {g : M → N},
g 1 = 1 → mulIndicator s (g ∘ f) = g ∘ mulIndicator s fSet.mulIndicator_comp_of_one
#align set.indicator_comp_of_zero Set.indicator_comp_of_zero: ∀ {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst_1 : Zero N] {s : Set α} {f : α → M} {g : M → N},
g 0 = 0 → indicator s (g ∘ f) = g ∘ indicator s fSet.indicator_comp_of_zero

@[to_additive: ∀ {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst_1 : Zero N] {s : Set α} (c : M) (f : M → N),
f 0 = 0 → (fun x => f (indicator s (fun x => c) x)) = indicator s fun x => f cto_additive]
theorem comp_mulIndicator_const: ∀ (c : M) (f : M → N), f 1 = 1 → (fun x => f (mulIndicator s (fun x => c) x)) = mulIndicator s fun x => f ccomp_mulIndicator_const (c: Mc : M: Type ?u.23546M) (f: M → Nf : M: Type ?u.23546M → N: Type ?u.23549N) (hf: f 1 = 1hf : f: M → Nf 1: ?m.235821 = 1: ?m.236091) :
(fun x: ?m.23653x => f: M → Nf (s: Set αs.mulIndicator: {α : Type ?u.23656} → {M : Type ?u.23655} → [inst : One M] → Set α → (α → M) → α → MmulIndicator (fun _: ?m.23701_ => c: Mc) x: ?m.23653x)) = s: Set αs.mulIndicator: {α : Type ?u.23719} → {M : Type ?u.23718} → [inst : One M] → Set α → (α → M) → α → MmulIndicator fun _: ?m.23730_ => f: M → Nf c: Mc :=
(mulIndicator_comp_of_one: ∀ {α : Type ?u.23760} {M : Type ?u.23759} {N : Type ?u.23758} [inst : One M] [inst_1 : One N] {s : Set α} {f : α → M}
{g : M → N}, g 1 = 1 → mulIndicator s (g ∘ f) = g ∘ mulIndicator s fmulIndicator_comp_of_one hf: f 1 = 1hf).symm: ∀ {α : Sort ?u.23816} {a b : α}, a = b → b = asymm
#align set.comp_mul_indicator_const Set.comp_mulIndicator_const: ∀ {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : One M] [inst_1 : One N] {s : Set α} (c : M) (f : M → N),
f 1 = 1 → (fun x => f (mulIndicator s (fun x => c) x)) = mulIndicator s fun x => f cSet.comp_mulIndicator_const
#align set.comp_indicator_const Set.comp_indicator_const: ∀ {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst_1 : Zero N] {s : Set α} (c : M) (f : M → N),
f 0 = 0 → (fun x => f (indicator s (fun x => c) x)) = indicator s fun x => f cSet.comp_indicator_const

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : α → M) (B : Set M),
indicator s f ⁻¹' B = Set.ite s (f ⁻¹' B) (0 ⁻¹' B)to_additive]
theorem mulIndicator_preimage: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : α → M) (B : Set M),
mulIndicator s f ⁻¹' B = Set.ite s (f ⁻¹' B) (1 ⁻¹' B)mulIndicator_preimage (s: Set αs : Set: Type ?u.23954 → Type ?u.23954Set α: Type ?u.23917α) (f: α → Mf : α: Type ?u.23917α → M: Type ?u.23926M) (B: Set MB : Set: Type ?u.23961 → Type ?u.23961Set M: Type ?u.23926M) :
mulIndicator: {α : Type ?u.23970} → {M : Type ?u.23969} → [inst : One M] → Set α → (α → M) → α → MmulIndicator s: Set αs f: α → Mf ⁻¹' B: Set MB = s: Set αs.ite: {α : Type ?u.24036} → Set α → Set α → Set α → Set αite (f: α → Mf ⁻¹' B: Set MB) (1: ?m.240591 ⁻¹' B: Set MB) :=
letI := Classical.decPred: {α : Sort ?u.24203} → (p : α → Prop) → DecidablePred pClassical.decPred (· ∈ s: Set αs)
piecewise_preimage: ∀ {α : Type ?u.24231} {β : Type ?u.24230} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → β) (t : Set β),
piecewise s f g ⁻¹' t = Set.ite s (f ⁻¹' t) (g ⁻¹' t)piecewise_preimage s: Set αs f: α → Mf 1: ?m.242421 B: Set MB
#align set.mul_indicator_preimage Set.mulIndicator_preimage: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : α → M) (B : Set M),
mulIndicator s f ⁻¹' B = Set.ite s (f ⁻¹' B) (1 ⁻¹' B)Set.mulIndicator_preimage
#align set.indicator_preimage Set.indicator_preimage: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : α → M) (B : Set M),
indicator s f ⁻¹' B = Set.ite s (f ⁻¹' B) (0 ⁻¹' B)Set.indicator_preimage

@[to_additive: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {t : Set α} (s : Set M), indicator t 0 ⁻¹' s ∈ {univ, ∅}to_additive]
theorem mulIndicator_one_preimage: ∀ {α : Type u_2} {M : Type u_1} [inst : One M] {t : Set α} (s : Set M), mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}mulIndicator_one_preimage (s: Set Ms : Set: Type ?u.24453 → Type ?u.24453Set M: Type ?u.24425M) :
t: Set αt.mulIndicator: {α : Type ?u.24480} → {M : Type ?u.24479} → [inst : One M] → Set α → (α → M) → α → MmulIndicator 1: ?m.245271 ⁻¹' s: Set Ms ∈ ({Set.univ: {α : Type ?u.24686} → Set αSet.univ, ∅: ?m.24705∅} : Set: Type ?u.24669 → Type ?u.24669Set (Set: Type ?u.24670 → Type ?u.24670Set α: Type ?u.24416α)) := byGoals accomplished! 🐙
α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set MmulIndicator t 1 ⁻¹' s ∈ {univ, ∅}classical
α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set MmulIndicator t 1 ⁻¹' s ∈ {univ, ∅}rw [α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set MmulIndicator t 1 ⁻¹' s ∈ {univ, ∅}mulIndicator_one': ∀ {α : Type ?u.24904} (M : Type ?u.24905) [inst : One M] {s : Set α}, mulIndicator s 1 = 1mulIndicator_one',α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set M1 ⁻¹' s ∈ {univ, ∅} α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set MmulIndicator t 1 ⁻¹' s ∈ {univ, ∅}preimage_one: ∀ {α : Type ?u.24952} {β : Type ?u.24953} [inst : One β] (s : Set β) [inst_1 : Decidable (1 ∈ s)],
1 ⁻¹' s = if 1 ∈ s then univ else ∅preimage_oneα: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set M(if 1 ∈ s then univ else ∅) ∈ {univ, ∅}]α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set M(if 1 ∈ s then univ else ∅) ∈ {univ, ∅}
α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set MmulIndicator t 1 ⁻¹' s ∈ {univ, ∅}split_ifsα: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set Mh✝: 1 ∈ sinluniv ∈ {univ, ∅}α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set Mh✝: ¬1 ∈ sinr∅ ∈ {univ, ∅} α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set M(if 1 ∈ s then univ else ∅) ∈ {univ, ∅}<;>α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set Mh✝: 1 ∈ sinluniv ∈ {univ, ∅}α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set Mh✝: ¬1 ∈ sinr∅ ∈ {univ, ∅} α: Type u_2β: Type ?u.24419ι: Type ?u.24422M: Type u_1N: Type ?u.24428inst✝¹: One Minst✝: One Ns✝, t: Set αf, g: α → Ma: αs: Set M(if 1 ∈ s then univ else ∅) ∈ {univ, ∅}simpGoals accomplished! 🐙
#align set.mul_indicator_one_preimage Set.mulIndicator_one_preimage: ∀ {α : Type u_2} {M : Type u_1} [inst : One M] {t : Set α} (s : Set M), mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}Set.mulIndicator_one_preimage
#align set.indicator_zero_preimage Set.indicator_zero_preimage: ∀ {α : Type u_2} {M : Type u_1} [inst : Zero M] {t : Set α} (s : Set M), indicator t 0 ⁻¹' s ∈ {univ, ∅}Set.indicator_zero_preimage

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (U : Set α) (s : Set M) (a : M) [inst_1 : Decidable (a ∈ s)]
[inst_2 : Decidable (0 ∈ s)], (indicator U fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 0 ∈ s then Uᶜ else ∅to_additive]
theorem mulIndicator_const_preimage_eq_union: ∀ (U : Set α) (s : Set M) (a : M) [inst : Decidable (a ∈ s)] [inst_1 : Decidable (1 ∈ s)],
(mulIndicator U fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅mulIndicator_const_preimage_eq_union (U: Set αU : Set: Type ?u.27025 → Type ?u.27025Set α: Type ?u.26988α) (s: Set Ms : Set: Type ?u.27028 → Type ?u.27028Set M: Type ?u.26997M) (a: Ma : M: Type ?u.26997M) [Decidable: Prop → TypeDecidable (a: Ma ∈ s: Set Ms)]
[Decidable: Prop → TypeDecidable ((1: ?m.270581 : M: Type ?u.26997M) ∈ s: Set Ms)] : (U: Set αU.mulIndicator: {α : Type ?u.27097} → {M : Type ?u.27096} → [inst : One M] → Set α → (α → M) → α → MmulIndicator fun _: ?m.27144_ => a: Ma) ⁻¹' s: Set Ms =
(if a: Ma ∈ s: Set Ms then U: Set αU else ∅: ?m.27197∅) ∪ if (1: ?m.272501 : M: Type ?u.26997M) ∈ s: Set Ms then U: Set αUᶜ else ∅: ?m.27305∅ := byGoals accomplished! 🐙
α: Type u_1β: Type ?u.26991ι: Type ?u.26994M: Type u_2N: Type ?u.27000inst✝³: One Minst✝²: One Ns✝, t: Set αf, g: α → Ma✝: αU: Set αs: Set Ma: Minst✝¹: Decidable (a ∈ s)inst✝: Decidable (1 ∈ s)(mulIndicator U fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅rw [α: Type u_1β: Type ?u.26991ι: Type ?u.26994M: Type u_2N: Type ?u.27000inst✝³: One Minst✝²: One Ns✝, t: Set αf, g: α → Ma✝: αU: Set αs: Set Ma: Minst✝¹: Decidable (a ∈ s)inst✝: Decidable (1 ∈ s)(mulIndicator U fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅```