/-
Copyright (c) 2020 Zhouhang Zhou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.64216
M N: Type ?u.29
N : Type _: Type (?u.43677+1)
Type _}

namespace Set

section One

variable [One: Type ?u.8765 → Type ?u.8765
One M: Type ?u.26
M] [One: Type ?u.8960 → Type ?u.8960
One N: Type ?u.29
N] {s: Set α
s t: Set α
t : Set: Type ?u.8963 → Type ?u.8963
Set α: Type ?u.234
α} {f: α → M
f g: α → M
g : α: Type ?u.10666
α → M: Type ?u.10894
M} {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) → α → M
indicator {M: ?m.91
M} [Zero: Type ?u.94 → Type ?u.94
Zero M: ?m.91
M] (s: Set α
s : Set: Type ?u.97 → Type ?u.97
Set α: Type ?u.54
α) (f: α → M
f : α: Type ?u.54
α → M: ?m.91
M) : α: Type ?u.54
α → M: ?m.91
M
  | x: ?m.115
x =>
    haveI := Classical.decPred: {α : Sort ?u.119} → (p : α → Prop) → DecidablePred p
Classical.decPred (· ∈ s: Set α
s)
    if x: ?m.115
x ∈ s: Set α
s then f: α → M
f x: ?m.115
x else 0: ?m.173
0
#align set.indicator Set.indicator: {α : Type u_1} → {M : Type u_2} → [inst : Zero M] → Set α → (α → M) → α → M
Set.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) → α → M
to_additive existing]
noncomputable def mulIndicator: {α : Type u_1} → {M : Type u_2} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (s: Set α
s : Set: Type ?u.271 → Type ?u.271
Set α: Type ?u.234
α) (f: α → M
f : α: Type ?u.234
α → M: Type ?u.243
M) : α: Type ?u.234
α → M: Type ?u.243
M
  | x: ?m.287
x =>
    haveI := Classical.decPred: {α : Sort ?u.291} → (p : α → Prop) → DecidablePred p
Classical.decPred (· ∈ s: Set α
s)
    if x: ?m.287
x ∈ s: Set α
s then f: α → M
f x: ?m.287
x else 1: ?m.345
1
#align set.mul_indicator Set.mulIndicator: {α : Type u_1} → {M : Type u_2} → [inst : One M] → Set α → (α → M) → α → M
Set.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 f
to_additive (attr := simp)]
theorem piecewise_eq_mulIndicator: ∀ [inst : DecidablePred fun x => x ∈ s], piecewise s f 1 = mulIndicator s f
piecewise_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 : α) → β i
piecewise f: α → M
f 1: ?m.526
1 = s: Set α
s.mulIndicator: {α : Type ?u.620} → {M : Type ?u.619} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator f: α → M
f :=
  funext: ∀ {α : Sort ?u.654} {β : α → Sort ?u.653} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext 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 v
if_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 ↔ a
Iff.rfl rfl: ∀ {α : Sort ?u.905} {a : α}, a = a
rfl rfl: ∀ {α : Sort ?u.908} {a : α}, a = a
rfl
#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 f
Set.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 f
Set.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 0
to_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 1
mulIndicator_apply (s: Set α
s : Set: Type ?u.1081 → Type ?u.1081
Set α: Type ?u.1044
α) (f: α → M
f : α: Type ?u.1044
α → M: Type ?u.1053
M) (a: α
a : α: Type ?u.1044
α) [Decidable: Prop → Type
Decidable (a: α
a ∈ s: Set α
s)] :
    mulIndicator: {α : Type ?u.1110} → {M : Type ?u.1109} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f a: α
a = if a: α
a ∈ s: Set α
s then f: α → M
f a: α
a else 1: ?m.1149
1 := by
Goals accomplished! 🐙
      α: Type u_1

β: Type ?u.1047

ι: Type ?u.1050

M: Type u_2

N: Type ?u.1056

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

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) → α → M
mulIndicatorα: Type u_1

β: Type ?u.1047

ι: Type ?u.1050

M: Type u_2

N: Type ?u.1056

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

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.1050

M: Type u_2

N: Type ?u.1056

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

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.1050

M: Type u_2

N: Type ?u.1056

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

inst✝: Decidable (a ∈ s)

h: a ∈ s

inlf a = f a
α: Type u_1

β: Type ?u.1047

ι: Type ?u.1050

M: Type u_2

N: Type ?u.1056

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

inst✝: Decidable (a ∈ s)

h: ¬a ∈ s

inr1 = 1 α: Type u_1

β: Type ?u.1047

ι: Type ?u.1050

M: Type u_2

N: Type ?u.1056

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

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.1050

M: Type u_2

N: Type ?u.1056

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

inst✝: Decidable (a ∈ s)

h: a ∈ s

inlf a = f a
α: Type u_1

β: Type ?u.1047

ι: Type ?u.1050

M: Type u_2

N: Type ?u.1056

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

inst✝: Decidable (a ∈ s)

h: ¬a ∈ s

inr1 = 1 α: Type u_1

β: Type ?u.1047

ι: Type ?u.1050

M: Type u_2

N: Type ?u.1056

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

inst✝: Decidable (a ∈ s)

(let x := a;
  if x ∈ s then f x else 1) =   if a ∈ s then f a else 1simp
Goals 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 1
Set.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 0
Set.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 a
to_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 a
mulIndicator_of_mem (h: a ∈ s
h : a: α
a ∈ s: Set α
s) (f: α → M
f : α: Type ?u.1793
α → M: Type ?u.1802
M) : mulIndicator: {α : Type ?u.1867} → {M : Type ?u.1866} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f a: α
a = f: α → M
f a: α
a :=
  letI := Classical.dec: (p : Prop) → Decidable p
Classical.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) = t
if_pos h: a ∈ s
h
#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 a
Set.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 a
Set.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 = 0
to_additive (attr := simp)]
theorem mulIndicator_of_not_mem: ¬a ∈ s → ∀ (f : α → M), mulIndicator s f a = 1
mulIndicator_of_not_mem (h: ¬a ∈ s
h : a: α
a ∉ s: Set α
s) (f: α → M
f : α: Type ?u.2023
α → M: Type ?u.2032
M) : mulIndicator: {α : Type ?u.2084} → {M : Type ?u.2083} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f a: α
a = 1: ?m.2109
1 :=
  letI := Classical.dec: (p : Prop) → Decidable p
Classical.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) = e
if_neg h: ¬a ∈ s
h
#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 = 1
Set.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 = 0
Set.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 a
to_additive]
theorem mulIndicator_eq_one_or_self: ∀ (s : Set α) (f : α → M) (a : α), mulIndicator s f a = 1 ∨ mulIndicator s f a = f a
mulIndicator_eq_one_or_self (s: Set α
s : Set: Type ?u.2318 → Type ?u.2318
Set α: Type ?u.2281
α) (f: α → M
f : α: Type ?u.2281
α → M: Type ?u.2290
M) (a: α
a : α: Type ?u.2281
α) :
    mulIndicator: {α : Type ?u.2329} → {M : Type ?u.2328} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f a: α
a = 1: ?m.2355
1 ∨ mulIndicator: {α : Type ?u.2395} → {M : Type ?u.2394} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f a: α
a = f: α → M
f a: α
a := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

mulIndicator s f a = 1 ∨ mulIndicator s f a = f aby_cases h: ?m.2435
h : a: α
a ∈ s: Set α
sα: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

h: a ∈ s

posmulIndicator s f a = 1 ∨ mulIndicator s f a = f a
α: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

h: ¬a ∈ s

negmulIndicator s f a = 1 ∨ mulIndicator s f a = f a
  α: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

mulIndicator s f a = 1 ∨ mulIndicator s f a = f a·α: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

h: a ∈ s

posmulIndicator s f a = 1 ∨ mulIndicator s f a = f a α: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

h: a ∈ s

posmulIndicator s f a = 1 ∨ mulIndicator s f a = f a
α: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

h: ¬a ∈ s

negmulIndicator s f a = 1 ∨ mulIndicator s f a = f aexact Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.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 a
mulIndicator_of_mem h: ?m.2435
h f: α → M
f)
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

mulIndicator s f a = 1 ∨ mulIndicator s f a = f a·α: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

h: ¬a ∈ s

negmulIndicator s f a = 1 ∨ mulIndicator s f a = f a α: Type u_1

β: Type ?u.2284

ι: Type ?u.2287

M: Type u_2

N: Type ?u.2293

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a✝: α

s: Set α

f: α → M

a: α

h: ¬a ∈ s

negmulIndicator s f a = 1 ∨ mulIndicator s f a = f aexact Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.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 = 1
mulIndicator_of_not_mem h: ?m.2442
h f: α → M
f)
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 a
Set.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 a
Set.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 = 0
to_additive (attr := simp)]
theorem mulIndicator_apply_eq_self: mulIndicator s f a = f a ↔ ¬a ∈ s → f a = 1
mulIndicator_apply_eq_self : s: Set α
s.mulIndicator: {α : Type ?u.2586} → {M : Type ?u.2585} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator f: α → M
f a: α
a = f: α → M
f a: α
a ↔ a: α
a ∉ s: Set α
s → f: α → M
f a: α
a = 1: ?m.2635
1 :=
  letI := Classical.dec: (p : Prop) → Decidable p
Classical.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 = a
ite_eq_left_iff.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans (by
Goals accomplished! 🐙 α: Type u_2

β: Type ?u.2550

ι: Type ?u.2553

M: Type u_1

N: Type ?u.2559

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

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.2553

M: Type u_1

N: Type ?u.2559

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

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 = a
eq_comm _: Sort ?u.2930
_ (f: α → M
f a: α
a)α: Type u_2

β: Type ?u.2550

ι: Type ?u.2553

M: Type u_1

N: Type ?u.2559

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

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 = 1
Set.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 = 0
Set.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 ⊆ s
to_additive (attr := simp)]
theorem mulIndicator_eq_self: mulIndicator s f = f ↔ mulSupport f ⊆ s
mulIndicator_eq_self : s: Set α
s.mulIndicator: {α : Type ?u.3109} → {M : Type ?u.3108} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator f: α → M
f = f: α → M
f ↔ mulSupport: {α : Type ?u.3146} → {M : Type ?u.3145} → [inst : One M] → (α → M) → Set α
mulSupport f: α → M
f ⊆ s: Set α
s := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.3073

ι: Type ?u.3076

M: Type u_2

N: Type ?u.3082

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

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₂ a
funext_iff, subset_def: ∀ {α : Type ?u.3229} {s t : Set α}, (s ⊆ t) = ∀ (x : α), x ∈ s → x ∈ t
subset_def, mem_mulSupport: ∀ {α : Type ?u.3242} {M : Type ?u.3243} [inst : One M] {f : α → M} {x : α}, x ∈ mulSupport f ↔ f x ≠ 1
mem_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 = 1
mulIndicator_apply_eq_self, not_imp_comm: ∀ {a b : Prop}, ¬a → b ↔ ¬b → a
not_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 ⊆ s
Set.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 ⊆ s
Set.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 = f
to_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 = f
mulIndicator_eq_self_of_superset (h1: mulIndicator s f = f
h1 : s: Set α
s.mulIndicator: {α : Type ?u.3845} → {M : Type ?u.3844} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator f: α → M
f = f: α → M
f) (h2: s ⊆ t
h2 : s: Set α
s ⊆ t: Set α
t) :
    t: Set α
t.mulIndicator: {α : Type ?u.3902} → {M : Type ?u.3901} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator f: α → M
f = f: α → M
f := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.3809

ι: Type ?u.3812

M: Type u_2

N: Type ?u.3818

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h1: mulIndicator s f = f

h2: s ⊆ t

mulIndicator t f = frw [α: Type u_1

β: Type ?u.3809

ι: Type ?u.3812

M: Type u_2

N: Type ?u.3818

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h1: mulIndicator s f = f

h2: s ⊆ t

mulIndicator 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 ⊆ s
mulIndicator_eq_selfα: Type u_1

β: Type ?u.3809

ι: Type ?u.3812

M: Type u_2

N: Type ?u.3818

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h1: mulSupport f ⊆ s

h2: s ⊆ t

mulSupport f ⊆ t]α: Type u_1

β: Type ?u.3809

ι: Type ?u.3812

M: Type u_2

N: Type ?u.3818

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h1: mulSupport f ⊆ s

h2: s ⊆ t

mulSupport f ⊆ t at h1: mulIndicator s f = f
h1⊢α: Type u_1

β: Type ?u.3809

ι: Type ?u.3812

M: Type u_2

N: Type ?u.3818

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h1: mulSupport f ⊆ s

h2: s ⊆ t

mulSupport f ⊆ t
  α: Type u_1

β: Type ?u.3809

ι: Type ?u.3812

M: Type u_2

N: Type ?u.3818

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h1: mulIndicator s f = f

h2: s ⊆ t

mulIndicator t f = fexact Subset.trans: ∀ {α : Type ?u.4188} {a b c : Set α}, a ⊆ b → b ⊆ c → a ⊆ c
Subset.trans h1: mulSupport f ⊆ s
h1 h2: s ⊆ t
h2
Goals 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 = f
Set.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 = f
Set.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 = 0
to_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 = 1
mulIndicator_apply_eq_one : mulIndicator: {α : Type ?u.4296} → {M : Type ?u.4295} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f a: α
a = 1: ?m.4322
1 ↔ a: α
a ∈ s: Set α
s → f: α → M
f a: α
a = 1: ?m.4392
1 :=
  letI := Classical.dec: (p : Prop) → Decidable p
Classical.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 = b
ite_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 = 1
Set.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 = 0
Set.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) s
to_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) s
mulIndicator_eq_one : (mulIndicator: {α : Type ?u.4806} → {M : Type ?u.4805} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f = fun x: ?m.4833
x => 1: ?m.4836
1) ↔ Disjoint: {α : Type ?u.4918} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (mulSupport: {α : Type ?u.4923} → {M : Type ?u.4922} → [inst : One M] → (α → M) → Set α
mulSupport f: α → M
f) s: Set α
s := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.4770

ι: Type ?u.4773

M: Type u_2

N: Type ?u.4779

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

(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₂ a
funext_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 = 1
mulIndicator_apply_eq_one, Set.disjoint_left: ∀ {α : Type ?u.5369} {s t : Set α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ t
Set.disjoint_left, mem_mulSupport: ∀ {α : Type ?u.5390} {M : Type ?u.5391} [inst : One M] {f : α → M} {x : α}, x ∈ mulSupport f ↔ f x ≠ 1
mem_mulSupport,
    not_imp_not: ∀ {a b : Prop}, ¬a → ¬b ↔ b → a
not_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) s
Set.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) s
Set.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) s
to_additive (attr := simp)]
theorem mulIndicator_eq_one': mulIndicator s f = 1 ↔ Disjoint (mulSupport f) s
mulIndicator_eq_one' : mulIndicator: {α : Type ?u.5957} → {M : Type ?u.5956} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f = 1: ?m.5984
1 ↔ Disjoint: {α : Type ?u.6064} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint (mulSupport: {α : Type ?u.6069} → {M : Type ?u.6068} → [inst : One M] → (α → M) → Set α
mulSupport f: α → M
f) 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) s
mulIndicator_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) s
Set.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) s
Set.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 f
to_additive]
theorem mulIndicator_apply_ne_one: ∀ {a : α}, mulIndicator s f a ≠ 1 ↔ a ∈ s ∩ mulSupport f
mulIndicator_apply_ne_one {a: α
a : α: Type ?u.6620
α} : s: Set α
s.mulIndicator: {α : Type ?u.6662} → {M : Type ?u.6661} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator f: α → M
f a: α
a ≠ 1: ?m.6725
1 ↔ a: α
a ∈ s: Set α
s ∩ mulSupport: {α : Type ?u.6766} → {M : Type ?u.6765} → [inst : One M] → (α → M) → Set α
mulSupport f: α → M
f := by
Goals accomplished! 🐙
  α: Type u_2

β: Type ?u.6623

ι: Type ?u.6626

M: Type u_1

N: Type ?u.6632

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a✝, a: α

mulIndicator s f a ≠ 1 ↔ a ∈ s ∩ mulSupport fsimp only [Ne.def: ∀ {α : Sort ?u.6838} (a b : α), (a ≠ b) = ¬a = b
Ne.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 = 1
mulIndicator_apply_eq_one, not_imp: ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
not_imp, mem_inter_iff: ∀ {α : Type ?u.6898} (x : α) (a b : Set α), x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b
mem_inter_iff, mem_mulSupport: ∀ {α : Type ?u.6926} {M : Type ?u.6927} [inst : One M] {f : α → M} {x : α}, x ∈ mulSupport f ↔ f x ≠ 1
mem_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 f
Set.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 f
Set.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 f
to_additive (attr := simp)]
theorem mulSupport_mulIndicator: mulSupport (mulIndicator s f) = s ∩ mulSupport f
mulSupport_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) → α → M
mulIndicator f: α → M
f) = s: Set α
s ∩ Function.mulSupport: {α : Type ?u.7356} → {M : Type ?u.7355} → [inst : One M] → (α → M) → Set α
Function.mulSupport f: α → M
f :=
  ext: ∀ {α : Type ?u.7407} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b
ext fun x: ?m.7416
x => by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.7242

ι: Type ?u.7245

M: Type u_2

N: Type ?u.7251

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a, 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 ≠ 1
Function.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 = 1
mulIndicator_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 f
Set.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 f
Set.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 ∈ s
to_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 ∈ s
mem_of_mulIndicator_ne_one (h: mulIndicator s f a ≠ 1
h : mulIndicator: {α : Type ?u.8533} → {M : Type ?u.8532} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f a: α
a ≠ 1: ?m.8592
1) : a: α
a ∈ s: Set α
s :=
  not_imp_comm: ∀ {a b : Prop}, ¬a → b ↔ ¬b → a
not_imp_comm.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 (fun hn: ?m.8658
hn => 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 = 1
mulIndicator_of_not_mem hn: ?m.8658
hn f: α → M
f) h: mulIndicator s f a ≠ 1
h
#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 ∈ s
Set.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 ∈ s
Set.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 s
to_additive]
theorem eqOn_mulIndicator: EqOn (mulIndicator s f) f s
eqOn_mulIndicator : EqOn: {α : Type ?u.8788} → {β : Type ?u.8787} → (α → β) → (α → β) → Set α → Prop
EqOn (mulIndicator: {α : Type ?u.8792} → {M : Type ?u.8791} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f) f: α → M
f s: Set α
s := fun _: ?m.8861
_ hx: ?m.8864
hx => 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 a
mulIndicator_of_mem hx: ?m.8864
hx f: α → M
f
#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 s
Set.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 s
Set.eqOn_indicator

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α → M}, support (indicator s f) ⊆ s
to_additive]
theorem mulSupport_mulIndicator_subset: mulSupport (mulIndicator s f) ⊆ s
mulSupport_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) → α → M
mulIndicator f: α → M
f) ⊆ s: Set α
s := fun _: ?m.9106
_ hx: ?m.9109
hx =>
  hx: ?m.9109
hx.imp_symm: ∀ {a b : Prop}, (¬a → b) → ¬b → a
imp_symm fun h: ?m.9118
h => 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 = 1
mulIndicator_of_not_mem h: ?m.9118
h f: α → M
f
#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) ⊆ s
Set.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) ⊆ s
Set.support_indicator_subset

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α → M}, indicator (support f) f = f
to_additive (attr := simp)]
theorem mulIndicator_mulSupport: mulIndicator (mulSupport f) f = f
mulIndicator_mulSupport : mulIndicator: {α : Type ?u.9242} → {M : Type ?u.9241} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (mulSupport: {α : Type ?u.9247} → {M : Type ?u.9246} → [inst : One M] → (α → M) → Set α
mulSupport f: α → M
f) f: α → M
f = f: α → M
f :=
  mulIndicator_eq_self: ∀ {α : Type ?u.9314} {M : Type ?u.9315} [inst : One M] {s : Set α} {f : α → M}, mulIndicator s f = f ↔ mulSupport f ⊆ s
mulIndicator_eq_self.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 Subset.rfl: ∀ {α : Type ?u.9372} {s : Set α}, s ⊆ s
Subset.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 = f
Set.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 = f
Set.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 ∘ f
to_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 ∘ f
mulIndicator_range_comp {ι: Sort ?u.9500
ι : Sort _: Type ?u.9500
SortSort _: Type ?u.9500
 _} (f: ι → α
f : ι: Sort ?u.9500
ι → α: Type ?u.9463
α) (g: α → M
g : α: Type ?u.9463
α → M: Type ?u.9472
M) :
    mulIndicator: {α : Type ?u.9519} → {M : Type ?u.9518} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (range: {α : Type ?u.9559} → {ι : Sort ?u.9558} → (ι → α) → Set α
range f: ι → α
f) g: α → M
g ∘ f: ι → α
f = g: α → M
g ∘ f: ι → α
f :=
  letI := Classical.decPred: {α : Sort ?u.9616} → (p : α → Prop) → DecidablePred p
Classical.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₁ ∘ f
piecewise_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 ∘ f
Set.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 ∘ f
Set.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 g
to_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 g
mulIndicator_congr (h: EqOn f g s
h : EqOn: {α : Type ?u.9899} → {β : Type ?u.9898} → (α → β) → (α → β) → Set α → Prop
EqOn f: α → M
f g: α → M
g s: Set α
s) : mulIndicator: {α : Type ?u.9914} → {M : Type ?u.9913} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f = mulIndicator: {α : Type ?u.9940} → {M : Type ?u.9939} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s g: α → M
g :=
  funext: ∀ {α : Sort ?u.9956} {β : α → Sort ?u.9955} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun x: ?m.9970
x => by
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

mulIndicator s f x = mulIndicator s g xsimp only [mulIndicator: {α : Type ?u.9992} → {M : Type ?u.9991} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator]α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

(if x ∈ s then f x else 1) = if x ∈ s then g x else 1
    α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

mulIndicator s f x = mulIndicator s g xsplit_ifs with h_1α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

h_1: x ∈ s

inlf x = g x
α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

h_1: ¬x ∈ s

inr1 = 1
    α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

mulIndicator s f x = mulIndicator s g x·α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

h_1: x ∈ s

inlf x = g x α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

h_1: x ∈ s

inlf x = g x
α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

h_1: ¬x ∈ s

inr1 = 1exact h: EqOn f g s
h h_1: x ∈ s
h_1
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.9864

ι: Type ?u.9867

M: Type u_2

N: Type ?u.9873

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g: α → M

a: α

h: EqOn f g s

x: α

mulIndicator s f x = mulIndicator s g xrfl
Goals 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 g
Set.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 g
Set.indicator_congr

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), indicator univ f = f
to_additive (attr := simp)]
theorem mulIndicator_univ: ∀ (f : α → M), mulIndicator univ f = f
mulIndicator_univ (f: α → M
f : α: Type ?u.10666
α → M: Type ?u.10675
M) : mulIndicator: {α : Type ?u.10709} → {M : Type ?u.10708} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (univ: {α : Type ?u.10715} → Set α
univ : Set: Type ?u.10714 → Type ?u.10714
Set α: Type ?u.10666
α) f: α → M
f = f: α → M
f :=
  mulIndicator_eq_self: ∀ {α : Type ?u.10743} {M : Type ?u.10744} [inst : One M] {s : Set α} {f : α → M},
  mulIndicator s f = f ↔ mulSupport f ⊆ s
mulIndicator_eq_self.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| subset_univ: ∀ {α : Type ?u.10801} (s : Set α), s ⊆ univ
subset_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 = f
Set.mulIndicator_univ
#align set.indicator_univ Set.indicator_univ: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), indicator univ f = f
Set.indicator_univ

@[to_additive: ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α → M), indicator ∅ f = fun x => 0
to_additive (attr := simp)]
theorem mulIndicator_empty: ∀ {α : Type u_1} {M : Type u_2} [inst : One M] (f : α → M), mulIndicator ∅ f = fun x => 1
mulIndicator_empty (f: α → M
f : α: Type ?u.10885
α → M: Type ?u.10894
M) : mulIndicator: {α : Type ?u.10928} → {M : Type ?u.10927} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (∅: ?m.10935
∅ : Set: Type ?u.10933 → Type ?u.10933
Set α: Type ?u.10885
α) f: α → M
f = fun _: ?m.11001
_ => 1: ?m.11004
1 :=
  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) s
mulIndicator_eq_one.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| 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 => 1
Set.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 => 0
Set.indicator_empty

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

variable (M: ?m.11540
M)

@[to_additive: ∀ {α : Type u_1} (M : Type u_2) [inst : Zero M] (s : Set α), (indicator s fun x => 0) = fun x => 0
to_additive (attr := simp)]
theorem mulIndicator_one: ∀ (s : Set α), (mulIndicator s fun x => 1) = fun x => 1
mulIndicator_one (s: Set α
s : Set: Type ?u.11580 → Type ?u.11580
Set α: Type ?u.11543
α) : (mulIndicator: {α : Type ?u.11585} → {M : Type ?u.11584} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s fun _: ?m.11593
_ => (1: ?m.11597
1 : M: Type ?u.11552
M)) = fun _: ?m.11640
_ => (1: ?m.11644
1 : M: Type ?u.11552
M) :=
  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) s
mulIndicator_eq_one.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.11546

ι: Type ?u.11549

M: Type u_2

N: Type ?u.11555

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

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 ∅ s
empty_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 => 1
Set.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 => 0
Set.indicator_zero

@[to_additive: ∀ {α : Type u_1} (M : Type u_2) [inst : Zero M] {s : Set α}, indicator s 0 = 0
to_additive (attr := simp)]
theorem mulIndicator_one': ∀ {s : Set α}, mulIndicator s 1 = 1
mulIndicator_one' {s: Set α
s : Set: Type ?u.12034 → Type ?u.12034
Set α: Type ?u.11997
α} : s: Set α
s.mulIndicator: {α : Type ?u.12039} → {M : Type ?u.12038} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (1: ?m.12054
1 : α: Type ?u.11997
α → M: Type ?u.12006
M) = 1: ?m.12137
1 :=
  mulIndicator_one: ∀ {α : Type ?u.12157} (M : Type ?u.12158) [inst : One M] (s : Set α), (mulIndicator s fun x => 1) = fun x => 1
mulIndicator_one M: Type ?u.12006
M 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 = 1
Set.mulIndicator_one'
#align set.indicator_zero' Set.indicator_zero': ∀ {α : Type u_1} (M : Type u_2) [inst : Zero M] {s : Set α}, indicator s 0 = 0
Set.indicator_zero'

variable {M: ?m.12292
M}

@[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) f
to_additive]
theorem mulIndicator_mulIndicator: ∀ (s t : Set α) (f : α → M), mulIndicator s (mulIndicator t f) = mulIndicator (s ∩ t) f
mulIndicator_mulIndicator (s: Set α
s t: Set α
t : Set: Type ?u.12335 → Type ?u.12335
Set α: Type ?u.12295
α) (f: α → M
f : α: Type ?u.12295
α → M: Type ?u.12304
M) :
    mulIndicator: {α : Type ?u.12344} → {M : Type ?u.12343} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s (mulIndicator: {α : Type ?u.12352} → {M : Type ?u.12351} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator t: Set α
t f: α → M
f) = mulIndicator: {α : Type ?u.12415} → {M : Type ?u.12414} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (s: Set α
s ∩ t: Set α
t) f: α → M
f :=
  funext: ∀ {α : Sort ?u.12451} {β : α → Sort ?u.12450} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun x: ?m.12465
x => by
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

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) → α → M
mulIndicator]α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

(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.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

mulIndicator s (mulIndicator t f) x = mulIndicator (s ∩ t) f xsplit_ifsα: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝²: x ∈ s

h✝¹: x ∈ t

h✝: x ∈ s ∩ t

inl.inl.inlf x = f x
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝²: x ∈ s

h✝¹: x ∈ t

h✝: ¬x ∈ s ∩ t

inl.inl.inrf x = 1
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝²: x ∈ s

h✝¹: ¬x ∈ t

h✝: x ∈ s ∩ t

inl.inr.inl1 = f x
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝²: x ∈ s

h✝¹: ¬x ∈ t

h✝: ¬x ∈ s ∩ t

inl.inr.inr1 = 1
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝¹: ¬x ∈ s

h✝: x ∈ s ∩ t

inr.inl1 = f x
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝¹: ¬x ∈ s

h✝: ¬x ∈ s ∩ t

inr.inr1 = 1
    α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

mulIndicator s (mulIndicator t f) x = mulIndicator (s ∩ t) f xrepeat' α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝²: x ∈ s

h✝¹: x ∈ t

h✝: x ∈ s ∩ t

inl.inl.inlf x = f x
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝²: x ∈ s

h✝¹: x ∈ t

h✝: ¬x ∈ s ∩ t

inl.inl.inrf x = 1
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝²: x ∈ s

h✝¹: ¬x ∈ t

h✝: x ∈ s ∩ t

inl.inr.inl1 = f x
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝²: x ∈ s

h✝¹: ¬x ∈ t

h✝: ¬x ∈ s ∩ t

inl.inr.inr1 = 1
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝¹: ¬x ∈ s

h✝: x ∈ s ∩ t

inr.inl1 = f x
α: Type u_1

β: Type ?u.12298

ι: Type ?u.12301

M: Type u_2

N: Type ?u.12307

inst✝¹: One M

inst✝: One N

s✝, t✝: Set α

f✝, g: α → M

a: α

s, t: Set α

f: α → M

x: α

h✝¹: ¬x ∈ s

h✝: ¬x ∈ s ∩ t

inr.inr1 = 1simp_all (config := { contextual := true: Bool
true })
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) f
Set.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) f
Set.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 f
to_additive (attr := simp)]
theorem mulIndicator_inter_mulSupport: ∀ (s : Set α) (f : α → M), mulIndicator (s ∩ mulSupport f) f = mulIndicator s f
mulIndicator_inter_mulSupport (s: Set α
s : Set: Type ?u.15927 → Type ?u.15927
Set α: Type ?u.15890
α) (f: α → M
f : α: Type ?u.15890
α → M: Type ?u.15899
M) :
    mulIndicator: {α : Type ?u.15936} → {M : Type ?u.15935} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (s: Set α
s ∩ mulSupport: {α : Type ?u.15954} → {M : Type ?u.15953} → [inst : One M] → (α → M) → Set α
mulSupport f: α → M
f) f: α → M
f = mulIndicator: {α : Type ?u.16023} → {M : Type ?u.16022} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.15893

ι: Type ?u.15896

M: Type u_2

N: Type ?u.15902

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a: α

s: Set α

f: α → M

mulIndicator (s ∩ mulSupport f) f = mulIndicator s frw [α: Type u_1

β: Type ?u.15893

ι: Type ?u.15896

M: Type u_2

N: Type ?u.15902

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a: α

s: Set α

f: α → M

mulIndicator (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) f
mulIndicator_mulIndicator,α: Type u_1

β: Type ?u.15893

ι: Type ?u.15896

M: Type u_2

N: Type ?u.15902

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a: α

s: Set α

f: α → M

mulIndicator s (mulIndicator (mulSupport f) f) = mulIndicator s f α: Type u_1

β: Type ?u.15893

ι: Type ?u.15896

M: Type u_2

N: Type ?u.15902

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a: α

s: Set α

f: α → M

mulIndicator (s ∩ mulSupport f) f = mulIndicator s fmulIndicator_mulSupport: ∀ {α : Type ?u.16156} {M : Type ?u.16157} [inst : One M] {f : α → M}, mulIndicator (mulSupport f) f = f
mulIndicator_mulSupportα: Type u_1

β: Type ?u.15893

ι: Type ?u.15896

M: Type u_2

N: Type ?u.15902

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g: α → M

a: α

s: Set α

f: α → M

mulIndicator 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 f
Set.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 f
Set.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)) x
to_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)) x
comp_mulIndicator (h: M → β
h : M: Type ?u.16346
M → β: Type ?u.16340
β) (f: α → M
f : α: Type ?u.16337
α → M: Type ?u.16346
M) {s: Set α
s : Set: Type ?u.16382 → Type ?u.16382
Set α: 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) → α → M
mulIndicator f: α → M
f x: α
x) = s: Set α
s.piecewise: {α : Type ?u.16481} →
  {β : α → Sort ?u.16480} →
    (s : Set α) → ((i : α) → β i) → ((i : α) → β i) → [inst : (j : α) → Decidable (j ∈ s)] → (i : α) → β i
piecewise (h: M → β
h ∘ f: α → M
f) (const: {α : Sort ?u.16513} → (β : Sort ?u.16512) → α → β → α
const α: Type ?u.16337
α (h: M → β
h 1: ?m.16518
1)) x: α
x := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

ι: Type ?u.16343

M: Type u_3

N: Type ?u.16349

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a: α

h: M → β

f: α → M

s: Set α

x: α

inst✝: DecidablePred fun x => x ∈ s

h (mulIndicator s f x) = piecewise s (h ∘ f) (const α (h 1)) xletI := Classical.decPred: {α : Sort ?u.16581} → (p : α → Prop) → DecidablePred p
Classical.decPred (· ∈ s: Set α
s)α: Type u_1

β: Type u_2

ι: Type ?u.16343

M: Type u_3

N: Type ?u.16349

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a: α

h: M → β

f: α → M

s: Set α

x: α

inst✝: DecidablePred fun x => x ∈ s

this:= Classical.decPred fun x => x ∈ s: DecidablePred fun x => x ∈ s

h (mulIndicator s f x) = piecewise s (h ∘ f) (const α (h 1)) x
  α: Type u_1

β: Type u_2

ι: Type ?u.16343

M: Type u_3

N: Type ?u.16349

inst✝²: One M

inst✝¹: One N

s✝, t: Set α

f✝, g: α → M

a: α

h: M → β

f: α → M

s: Set α

x: α

inst✝: DecidablePred fun x => x ∈ s

h (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)) x
apply_piecewise f: α → M
f (const: {α : Sort ?u.16650} → (β : Sort ?u.16649) → α → β → α
const α: Type u_1
α 1: ?m.16655
1) (fun _: ?m.16688
_ => h: M → β
h) (x := x: α
x) using 2
Goals 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)) x
Set.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)) x
Set.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.20700
Set α: Type ?u.20663
α} (f: β → α
f : β: Type ?u.20666
β → α: Type ?u.20663
α) {g: α → M
g : α: Type ?u.20663
α → M: Type ?u.20672
M} {x: β
x : β: Type ?u.20666
β} :
    mulIndicator: {α : Type ?u.20715} → {M : Type ?u.20714} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (f: β → α
f ⁻¹' s: Set α
s) (g: α → M
g ∘ f: β → α
f) x: β
x = mulIndicator: {α : Type ?u.20765} → {M : Type ?u.20764} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s g: α → M
g (f: β → α
f x: β
x) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

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) → α → M
mulIndicator, Function.comp: {α : Sort ?u.20825} → {β : Sort ?u.20824} → {δ : Sort ?u.20823} → (β → δ) → (α → β) → α → δ
Function.comp]α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

(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.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

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.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: x ∈ f ⁻¹' s

h': f x ∈ s

inl.inlg (f x) = g (f x)
α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: x ∈ f ⁻¹' s

h': ¬f x ∈ s

inl.inrg (f x) = 1
α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: ¬x ∈ f ⁻¹' s

h'': f x ∈ s

inr.inl1 = g (f x)
α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: ¬x ∈ f ⁻¹' s

h'': ¬f x ∈ s

inr.inr1 = 1 α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

(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.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: x ∈ f ⁻¹' s

h': f x ∈ s

inl.inlg (f x) = g (f x)
α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: x ∈ f ⁻¹' s

h': ¬f x ∈ s

inl.inrg (f x) = 1
α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: ¬x ∈ f ⁻¹' s

h'': f x ∈ s

inr.inl1 = g (f x)
α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: ¬x ∈ f ⁻¹' s

h'': ¬f x ∈ s

inr.inr1 = 1 α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

(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.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: x ∈ f ⁻¹' s

h': ¬f x ∈ s

inl.inrg (f x) = 1rflα: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: ¬x ∈ f ⁻¹' s

h'': f x ∈ s

inr.inl1 = g (f x) | α: Type u_1

β: Type u_3

ι: Type ?u.20669

M: Type u_2

N: Type ?u.20675

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → α

g: α → M

x: β

h: x ∈ f ⁻¹' s

h': ¬f x ∈ s

inl.inrg (f x) = 1contradiction
Goals 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) x
to_additive]
theorem mulIndicator_image: ∀ {s : Set α} {f : β → M} {g : α → β}, Injective g → ∀ {x : α}, mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) x
mulIndicator_image {s: Set α
s : Set: Type ?u.22149 → Type ?u.22149
Set α: Type ?u.22112
α} {f: β → M
f : β: Type ?u.22115
β → M: Type ?u.22121
M} {g: α → β
g : α: Type ?u.22112
α → β: Type ?u.22115
β} (hg: Injective g
hg : Injective: {α : Sort ?u.22161} → {β : Sort ?u.22160} → (α → β) → Prop
Injective g: α → β
g) {x: α
x : α: Type ?u.22112
α} :
    mulIndicator: {α : Type ?u.22173} → {M : Type ?u.22172} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (g: α → β
g '' s: Set α
s) f: β → M
f (g: α → β
g x: α
x) = mulIndicator: {α : Type ?u.22209} → {M : Type ?u.22208} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s (f: β → M
f ∘ g: α → β
g) x: α
x := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

ι: Type ?u.22118

M: Type u_3

N: Type ?u.22124

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → M

g: α → β

hg: Injective g

x: α

mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) xrw [α: Type u_1

β: Type u_2

ι: Type ?u.22118

M: Type u_3

N: Type ?u.22124

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → M

g: α → β

hg: Injective g

x: α

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.22118

M: Type u_3

N: Type ?u.22124

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → M

g: α → β

hg: Injective g

x: α

mulIndicator (g ⁻¹' (g '' s)) (f ∘ g) x = mulIndicator s (f ∘ g) x α: Type u_1

β: Type u_2

ι: Type ?u.22118

M: Type u_3

N: Type ?u.22124

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → M

g: α → β

hg: Injective g

x: α

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) = s
preimage_image_eq _: Set ?m.22359
_ hg: Injective g
hgα: Type u_1

β: Type u_2

ι: Type ?u.22118

M: Type u_3

N: Type ?u.22124

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f✝, g✝: α → M

a: α

s: Set α

f: β → M

g: α → β

hg: Injective g

x: α

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) x
Set.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) x
Set.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 f
to_additive]
theorem mulIndicator_comp_of_one: ∀ {g : M → N}, g 1 = 1 → mulIndicator s (g ∘ f) = g ∘ mulIndicator s f
mulIndicator_comp_of_one {g: M → N
g : M: Type ?u.22463
M → N: Type ?u.22466
N} (hg: g 1 = 1
hg : g: M → N
g 1: ?m.22497
1 = 1: ?m.22524
1) :
    mulIndicator: {α : Type ?u.22568} → {M : Type ?u.22567} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s (g: M → N
g ∘ f: α → M
f) = g: M → N
g ∘ mulIndicator: {α : Type ?u.22616} → {M : Type ?u.22615} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f := by
Goals accomplished! 🐙
  α: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

mulIndicator s (g ∘ f) = g ∘ mulIndicator s ffunextα: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

x✝: α

hmulIndicator s (g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝
  α: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

mulIndicator s (g ∘ f) = g ∘ mulIndicator s fsimp only [mulIndicator: {α : Type ?u.22741} → {M : Type ?u.22740} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator]α: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

x✝: α

h(if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ mulIndicator s f) x✝
  α: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

mulIndicator s (g ∘ f) = g ∘ mulIndicator s fsplit_ifsα: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

x✝: α

h✝: x✝ ∈ s

h.inl(g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝
α: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

x✝: α

h✝: ¬x✝ ∈ s

h.inr1 = (g ∘ mulIndicator s f) x✝ α: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

x✝: α

h(if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ mulIndicator s f) x✝<;>α: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

x✝: α

h✝: x✝ ∈ s

h.inl(g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝
α: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

x✝: α

h✝: ¬x✝ ∈ s

h.inr1 = (g ∘ mulIndicator s f) x✝ α: Type u_3

β: Type ?u.22457

ι: Type ?u.22460

M: Type u_2

N: Type u_1

inst✝¹: One M

inst✝: One N

s, t: Set α

f, g✝: α → M

a: α

g: M → N

hg: g 1 = 1

x✝: α

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 f
Set.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 f
Set.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 c
to_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 c
comp_mulIndicator_const (c: M
c : M: Type ?u.23546
M) (f: M → N
f : M: Type ?u.23546
M → N: Type ?u.23549
N) (hf: f 1 = 1
hf : f: M → N
f 1: ?m.23582
1 = 1: ?m.23609
1) :
    (fun x: ?m.23653
x => f: M → N
f (s: Set α
s.mulIndicator: {α : Type ?u.23656} → {M : Type ?u.23655} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator (fun _: ?m.23701
_ => c: M
c) x: ?m.23653
x)) = s: Set α
s.mulIndicator: {α : Type ?u.23719} → {M : Type ?u.23718} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator fun _: ?m.23730
_ => f: M → N
f c: M
c :=
  (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 f
mulIndicator_comp_of_one hf: f 1 = 1
hf).symm: ∀ {α : Sort ?u.23816} {a b : α}, a = b → b = a
symm
#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 c
Set.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 c
Set.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.23954
Set α: Type ?u.23917
α) (f: α → M
f : α: Type ?u.23917
α → M: Type ?u.23926
M) (B: Set M
B : Set: Type ?u.23961 → Type ?u.23961
Set M: Type ?u.23926
M) :
    mulIndicator: {α : Type ?u.23970} → {M : Type ?u.23969} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator s: Set α
s f: α → M
f ⁻¹' B: Set M
B = s: Set α
s.ite: {α : Type ?u.24036} → Set α → Set α → Set α → Set α
ite (f: α → M
f ⁻¹' B: Set M
B) (1: ?m.24059
1 ⁻¹' B: Set M
B) :=
  letI := Classical.decPred: {α : Sort ?u.24203} → (p : α → Prop) → DecidablePred p
Classical.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: α → M
f 1: ?m.24242
1 B: Set M
B
#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 M
s : Set: Type ?u.24453 → Type ?u.24453
Set M: Type ?u.24425
M) :
    t: Set α
t.mulIndicator: {α : Type ?u.24480} → {M : Type ?u.24479} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator 1: ?m.24527
1 ⁻¹' s: Set M
s ∈ ({Set.univ: {α : Type ?u.24686} → Set α
Set.univ, ∅: ?m.24705
∅} : Set: Type ?u.24669 → Type ?u.24669
Set (Set: Type ?u.24670 → Type ?u.24670
Set α: Type ?u.24416
α)) := by
Goals accomplished! 🐙
  α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}classical
    α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}rw [α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}mulIndicator_one': ∀ {α : Type ?u.24904} (M : Type ?u.24905) [inst : One M] {s : Set α}, mulIndicator s 1 = 1
mulIndicator_one',α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

1 ⁻¹' s ∈ {univ, ∅} α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

mulIndicator 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.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

(if 1 ∈ s then univ else ∅) ∈ {univ, ∅}]α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

(if 1 ∈ s then univ else ∅) ∈ {univ, ∅}
    α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}split_ifsα: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

h✝: 1 ∈ s

inluniv ∈ {univ, ∅}
α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

h✝: ¬1 ∈ s

inr∅ ∈ {univ, ∅} α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

(if 1 ∈ s then univ else ∅) ∈ {univ, ∅}<;>α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

h✝: 1 ∈ s

inluniv ∈ {univ, ∅}
α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

h✝: ¬1 ∈ s

inr∅ ∈ {univ, ∅} α: Type u_2

β: Type ?u.24419

ι: Type ?u.24422

M: Type u_1

N: Type ?u.24428

inst✝¹: One M

inst✝: One N

s✝, t: Set α

f, g: α → M

a: α

s: Set M

(if 1 ∈ s then univ else ∅) ∈ {univ, ∅}simp
Goals 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.27025
Set α: Type ?u.26988
α) (s: Set M
s : Set: Type ?u.27028 → Type ?u.27028
Set M: Type ?u.26997
M) (a: M
a : M: Type ?u.26997
M) [Decidable: Prop → Type
Decidable (a: M
a ∈ s: Set M
s)]
    [Decidable: Prop → Type
Decidable ((1: ?m.27058
1 : M: Type ?u.26997
M) ∈ s: Set M
s)] : (U: Set α
U.mulIndicator: {α : Type ?u.27097} → {M : Type ?u.27096} → [inst : One M] → Set α → (α → M) → α → M
mulIndicator fun _: ?m.27144
_ => a: M
a) ⁻¹' s: Set M
s =
      (if a: M
a ∈ s: Set M
s then U: Set α
U else ∅: ?m.27197
∅) ∪ if (1: ?m.27250
1 : M: Type ?u.26997
M) ∈ s: Set M
s then U: Set α
Uᶜ else ∅: ?m.27305
∅ := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.26991

ι: Type ?u.26994

M: Type u_2

N: Type ?u.27000

inst✝³: One M

inst✝²: One N

s✝, t: Set α

f, g: α → M

a✝: α

U: Set α

s: Set M

a: M

inst✝¹: 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.26994

M: Type u_2

N: Type ?u.27000

inst✝³: One M

inst✝²: One N

s✝, t: Set α

f, g: α → M

a✝: α

U: Set α

s: Set M

a: M

inst✝¹: 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 ∅