[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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 1
[PROOFSTEP]
unfold mulIndicator
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝² : One M
inst✝¹ : One N
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
inst✝ : Decidable (a ∈ s)
⊢ (if a ∈ s then f a else 1) = if a ∈ s then f a else 1
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ mulIndicator s f a = 1 ∨ mulIndicator s f a = f a
[PROOFSTEP]
exact Or.inr (mulIndicator_of_mem h f)
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ mulIndicator s f a = 1 ∨ mulIndicator s f a = f a
[PROOFSTEP]
exact Or.inl (mulIndicator_of_not_mem h f)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
this : Decidable (a ∈ s) := Classical.dec (a ∈ s)
⊢ ¬a ∈ s → 1 = f a ↔ ¬a ∈ s → f a = 1
[PROOFSTEP]
rw [@eq_comm _ (f a)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
⊢ mulIndicator s f = f ↔ mulSupport f ⊆ s
[PROOFSTEP]
simp only [funext_iff, subset_def, mem_mulSupport, mulIndicator_apply_eq_self, not_imp_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h1 : mulIndicator s f = f
h2 : s ⊆ t
⊢ mulIndicator t f = f
[PROOFSTEP]
rw [mulIndicator_eq_self] at h1 ⊢
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h1 : mulSupport f ⊆ s
h2 : s ⊆ t
⊢ mulSupport f ⊆ t
[PROOFSTEP]
exact Subset.trans h1 h2
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
⊢ (mulIndicator s f = fun x => 1) ↔ Disjoint (mulSupport f) s
[PROOFSTEP]
simp only [funext_iff, mulIndicator_apply_eq_one, Set.disjoint_left, mem_mulSupport, not_imp_not]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a✝ a : α
⊢ mulIndicator s f a ≠ 1 ↔ a ∈ s ∩ mulSupport f
[PROOFSTEP]
simp only [Ne.def, mulIndicator_apply_eq_one, not_imp, mem_inter_iff, mem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a x : α
⊢ x ∈ mulSupport (mulIndicator s f) ↔ x ∈ s ∩ mulSupport f
[PROOFSTEP]
simp [Function.mem_mulSupport, mulIndicator_apply_eq_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
[PROOFSTEP]
simp only [mulIndicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
[PROOFSTEP]
split_ifs with h_1
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x
[PROOFSTEP]
exact h h_1
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
h : EqOn f g s
x : α
h_1 : ¬x ∈ s
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set α
⊢ Disjoint (mulSupport fun x => 1) s
[PROOFSTEP]
simp only [mulSupport_one, empty_disjoint]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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 x
[PROOFSTEP]
simp only [mulIndicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ f x = f x
[PROOFSTEP]
simp_all (config := { contextual := true })
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ f x = 1
[PROOFSTEP]
simp_all (config := { contextual := true })
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ 1 = f x
[PROOFSTEP]
simp_all (config := { contextual := true })
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ 1 = 1
[PROOFSTEP]
simp_all (config := { contextual := true })
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ 1 = f x
[PROOFSTEP]
simp_all (config := { contextual := true })
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ 1 = 1
[PROOFSTEP]
simp_all (config := { contextual := true })
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
[PROOFSTEP]
rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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)) x
[PROOFSTEP]
letI := Classical.decPred (· ∈ s)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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 : DecidablePred fun x => x ∈ s := Classical.decPred fun x => x ∈ s
⊢ h (mulIndicator s f x) = piecewise s (h ∘ f) (const α (h 1)) x
[PROOFSTEP]
convert s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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)
[PROOFSTEP]
simp only [mulIndicator, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
[PROOFSTEP]
split_ifs with h h' h''
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ g (f x) = g (f x)
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ g (f x) = g (f x)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ g (f x) = 1
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ g (f x) = 1
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ g (f x) = 1
[PROOFSTEP]
contradiction
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ 1 = g (f x)
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ 1 = g (f x)
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ 1 = g (f x)
[PROOFSTEP]
contradiction
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ 1 = 1
[PROOFSTEP]
first
| rfl
| contradiction
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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
[PROOFSTEP]
rw [← mulIndicator_comp_right, preimage_image_eq _ hg]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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 f
[PROOFSTEP]
funext
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g✝ : α → M
a : α
g : M → N
hg : g 1 = 1
x✝ : α
⊢ mulIndicator s (g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝
[PROOFSTEP]
simp only [mulIndicator]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g✝ : α → M
a : α
g : M → N
hg : g 1 = 1
x✝ : α
⊢ (if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ mulIndicator s f) x✝
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g✝ : α → M
a : α
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : x✝ ∈ s
⊢ (g ∘ f) x✝ = (g ∘ mulIndicator s f) x✝
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g✝ : α → M
a : α
g : M → N
hg : g 1 = 1
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = (g ∘ mulIndicator s f) x✝
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set M
⊢ mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}
[PROOFSTEP]
classical
rw [mulIndicator_one', preimage_one]
split_ifs <;> simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set M
⊢ mulIndicator t 1 ⁻¹' s ∈ {univ, ∅}
[PROOFSTEP]
rw [mulIndicator_one', preimage_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set M
⊢ (if 1 ∈ s then univ else ∅) ∈ {univ, ∅}
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set M
h✝ : 1 ∈ s
⊢ univ ∈ {univ, ∅}
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a : α
s : Set M
h✝ : ¬1 ∈ s
⊢ ∅ ∈ {univ, ∅}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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 ∅
[PROOFSTEP]
rw [mulIndicator_preimage, preimage_one, preimage_const]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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)
⊢ Set.ite U (if a ∈ s then univ else ∅) (if 1 ∈ s then univ else ∅) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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)
h✝¹ : a ∈ s
h✝ : 1 ∈ s
⊢ Set.ite U univ univ = U ∪ Uᶜ
[PROOFSTEP]
simp [← compl_eq_univ_diff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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)
h✝¹ : a ∈ s
h✝ : ¬1 ∈ s
⊢ Set.ite U univ ∅ = U ∪ ∅
[PROOFSTEP]
simp [← compl_eq_univ_diff]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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)
h✝¹ : ¬a ∈ s
h✝ : 1 ∈ s
⊢ Set.ite U ∅ univ = ∅ ∪ Uᶜ
[PROOFSTEP]
simp [← compl_eq_univ_diff]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
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)
h✝¹ : ¬a ∈ s
h✝ : ¬1 ∈ s
⊢ Set.ite U ∅ ∅ = ∅ ∪ ∅
[PROOFSTEP]
simp [← compl_eq_univ_diff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
⊢ (mulIndicator U fun x => a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}
[PROOFSTEP]
classical
rw [mulIndicator_const_preimage_eq_union]
split_ifs <;> simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
⊢ (mulIndicator U fun x => a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}
[PROOFSTEP]
rw [mulIndicator_const_preimage_eq_union]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
⊢ ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅) ∈ {univ, U, Uᶜ, ∅}
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : 1 ∈ s
⊢ U ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
h✝¹ : a ∈ s
h✝ : ¬1 ∈ s
⊢ U ∪ ∅ ∈ {univ, U, Uᶜ, ∅}
[PROOFSTEP]
simp
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : 1 ∈ s
⊢ ∅ ∪ Uᶜ ∈ {univ, U, Uᶜ, ∅}
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f g : α → M
a✝ : α
U : Set α
s : Set M
a : M
h✝¹ : ¬a ∈ s
h✝ : ¬1 ∈ s
⊢ ∅ ∪ ∅ ∈ {univ, U, Uᶜ, ∅}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t✝ : Set α
f✝ g : α → M
a : α
s : Set α
f : α → M
t : Set M
ht : ¬1 ∈ t
⊢ mulIndicator s f ⁻¹' t = f ⁻¹' t ∩ s
[PROOFSTEP]
simp [mulIndicator_preimage, Pi.one_def, Set.preimage_const_of_not_mem ht]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ r ∈ range (mulIndicator s f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s
[PROOFSTEP]
simp only [mem_range, mulIndicator, ne_eq, mem_image]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ (∃ y, (if y ∈ s then f y else 1) = r) ↔ r = 1 ∧ ¬s = univ ∨ ∃ x, x ∈ s ∧ f x = r
[PROOFSTEP]
rw [eq_univ_iff_forall, not_forall]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ (∃ y, (if y ∈ s then f y else 1) = r) ↔ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
[PROOFSTEP]
refine ⟨?_, ?_⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ (∃ y, (if y ∈ s then f y else 1) = r) → (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case refine_1.intro
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hy : (if y ∈ s then f y else 1) = r
⊢ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
[PROOFSTEP]
split_ifs at hy  with hys
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hys : y ∈ s
hy : f y = r
⊢ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
[PROOFSTEP]
tauto
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hys : ¬y ∈ s
hy : 1 = r
⊢ (r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r
[PROOFSTEP]
left
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
y : α
hys : ¬y ∈ s
hy : 1 = r
⊢ r = 1 ∧ ∃ x, ¬x ∈ s
[PROOFSTEP]
tauto
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
⊢ ((r = 1 ∧ ∃ x, ¬x ∈ s) ∨ ∃ x, x ∈ s ∧ f x = r) → ∃ y, (if y ∈ s then f y else 1) = r
[PROOFSTEP]
rintro (⟨hr, ⟨x, hx⟩⟩ | ⟨x, ⟨hx, hxs⟩⟩)
[GOAL]
case refine_2.inl.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
hr : r = 1
x : α
hx : ¬x ∈ s
⊢ ∃ y, (if y ∈ s then f y else 1) = r
[PROOFSTEP]
use x
[GOAL]
case refine_2.inr.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
x : α
hx : x ∈ s
hxs : f x = r
⊢ ∃ y, (if y ∈ s then f y else 1) = r
[PROOFSTEP]
use x
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
hr : r = 1
x : α
hx : ¬x ∈ s
⊢ (if x ∈ s then f x else 1) = r
[PROOFSTEP]
split_ifs
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
x : α
hx : x ∈ s
hxs : f x = r
⊢ (if x ∈ s then f x else 1) = r
[PROOFSTEP]
split_ifs
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
hr : r = 1
x : α
hx : ¬x ∈ s
⊢ 1 = r
[PROOFSTEP]
tauto
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
r : M
s : Set α
f : α → M
x : α
hx : x ∈ s
hxs : f x = r
⊢ f x = r
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (mulIndicator s f a) (mulIndicator s g a)
[PROOFSTEP]
simp only [mulIndicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)
[PROOFSTEP]
split_ifs with has
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∈ s
⊢ r (f a) (g a)
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : ¬a ∈ s
⊢ r 1 1
[PROOFSTEP]
exacts [ha has, h1]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t✝ : Set α
f✝ g : α → M
a✝ : α
f : α → M
s t : Set α
a : α
⊢ mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a
[PROOFSTEP]
by_cases hs : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t✝ : Set α
f✝ g : α → M
a✝ : α
f : α → M
s t : Set α
a : α
hs : a ∈ s
⊢ mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a
[PROOFSTEP]
by_cases ht : a ∈ t
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t✝ : Set α
f✝ g : α → M
a✝ : α
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
⊢ mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a
[PROOFSTEP]
by_cases ht : a ∈ t
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t✝ : Set α
f✝ g : α → M
a✝ : α
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : a ∈ t
⊢ mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t✝ : Set α
f✝ g : α → M
a✝ : α
f : α → M
s t : Set α
a : α
hs : a ∈ s
ht : ¬a ∈ t
⊢ mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t✝ : Set α
f✝ g : α → M
a✝ : α
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : a ∈ t
⊢ mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t✝ : Set α
f✝ g : α → M
a✝ : α
f : α → M
s t : Set α
a : α
hs : ¬a ∈ s
ht : ¬a ∈ t
⊢ mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s t : Set α
f✝ g : α → M
a : α
h : ¬a ∈ s ∩ t
f : α → M
⊢ mulIndicator (s ∪ t) f a = mulIndicator s f a * mulIndicator t f a
[PROOFSTEP]
rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_not_mem h, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ (mulIndicator s fun a => f a * g a) = fun a => mulIndicator s f a * mulIndicator s g a
[PROOFSTEP]
funext
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
⊢ mulIndicator s (fun a => f a * g a) x✝ = mulIndicator s f x✝ * mulIndicator s g x✝
[PROOFSTEP]
simp only [mulIndicator]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 1) = (if x✝ ∈ s then f x✝ else 1) * if x✝ ∈ s then g x✝ else 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = 1 * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
ha : a ∈ s
⊢ mulIndicator sᶜ f a * mulIndicator s f a = f a
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
ha : ¬a ∈ s
⊢ mulIndicator sᶜ f a * mulIndicator s f a = f a
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
ha : a ∈ s
⊢ mulIndicator s f a * mulIndicator sᶜ f a = f a
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s✝ t : Set α
f✝ g : α → M
a✝ : α
s : Set α
f : α → M
a : α
ha : ¬a ∈ s
⊢ mulIndicator s f a * mulIndicator sᶜ f a = f a
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ mulIndicator (mulSupport f) (f * g) = f
[PROOFSTEP]
refine' (mulIndicator_congr fun x hx => _).trans mulIndicator_mulSupport
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
⊢ (f * g) x = f x
[PROOFSTEP]
have : g x = 1 := nmem_mulSupport.1 (disjoint_left.1 h hx)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
⊢ (f * g) x = f x
[PROOFSTEP]
rw [Pi.mul_apply, this, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ mulIndicator (mulSupport g) (f * g) = g
[PROOFSTEP]
refine' (mulIndicator_congr fun x hx => _).trans mulIndicator_mulSupport
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
⊢ (f * g) x = g x
[PROOFSTEP]
have : f x = 1 := nmem_mulSupport.1 (disjoint_right.1 h hx)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ (f * g) x = g x
[PROOFSTEP]
rw [Pi.mul_apply, this, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
⊢ mulIndicator s f * mulIndicator sᶜ g = piecewise s f g
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
⊢ (mulIndicator s f * mulIndicator sᶜ g) x = piecewise s f g x
[PROOFSTEP]
by_cases h : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : x ∈ s
⊢ (mulIndicator s f * mulIndicator sᶜ g) x = piecewise s f g x
[PROOFSTEP]
rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
  Set.mulIndicator_of_not_mem (Set.not_mem_compl_iff.2 h), mul_one]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ (mulIndicator s f * mulIndicator sᶜ g) x = piecewise s f g x
[PROOFSTEP]
rw [piecewise_eq_of_not_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_not_mem h,
  Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
A : Type u_6
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : DistribMulAction M A
s : Set α
r : α → M
f : α → A
x : α
⊢ indicator s (fun x => r x • f x) x = r x • indicator s f x
[PROOFSTEP]
dsimp only [indicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
A : Type u_6
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : DistribMulAction M A
s : Set α
r : α → M
f : α → A
x : α
⊢ (if x ∈ s then r x • f x else 0) = r x • if x ∈ s then f x else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
A : Type u_6
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : DistribMulAction M A
s : Set α
r : α → M
f : α → A
x : α
h✝ : x ∈ s
⊢ r x • f x = r x • f x
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
A : Type u_6
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : DistribMulAction M A
s : Set α
r : α → M
f : α → A
x : α
h✝ : ¬x ∈ s
⊢ 0 = r x • 0
[PROOFSTEP]
exacts [rfl, (smul_zero (r x)).symm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
A : Type u_6
inst✝² : Zero A
inst✝¹ : Zero M
inst✝ : SMulWithZero M A
s : Set α
r : α → M
f : α → A
x : α
⊢ indicator s (fun x => r x • f x) x = indicator s r x • f x
[PROOFSTEP]
dsimp only [indicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
A : Type u_6
inst✝² : Zero A
inst✝¹ : Zero M
inst✝ : SMulWithZero M A
s : Set α
r : α → M
f : α → A
x : α
⊢ (if x ∈ s then r x • f x else 0) = (if x ∈ s then r x else 0) • f x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
A : Type u_6
inst✝² : Zero A
inst✝¹ : Zero M
inst✝ : SMulWithZero M A
s : Set α
r : α → M
f : α → A
x : α
h✝ : x ∈ s
⊢ r x • f x = r x • f x
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
A : Type u_6
inst✝² : Zero A
inst✝¹ : Zero M
inst✝ : SMulWithZero M A
s : Set α
r : α → M
f : α → A
x : α
h✝ : ¬x ∈ s
⊢ 0 = 0 • f x
[PROOFSTEP]
exacts [rfl, (zero_smul _ (f x)).symm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
inst✝ : Group G
s✝ t : Set α
f✝ g : α → G
a : α
s : Set α
f : α → G
⊢ mulIndicator sᶜ f = f / mulIndicator s f
[PROOFSTEP]
rw [div_eq_mul_inv, mulIndicator_compl]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
inst✝ : Group G
s t : Set α
f✝ g : α → G
a : α
h : s ⊆ t
f : α → G
⊢ mulIndicator (t \ s) f * mulIndicator s f = mulIndicator t f
[PROOFSTEP]
rw [Pi.mul_def, ← mulIndicator_union_of_disjoint, diff_union_self, union_eq_self_of_subset_right h]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
inst✝ : Group G
s t : Set α
f✝ g : α → G
a : α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s
[PROOFSTEP]
exact disjoint_sdiff_self_left
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
inst✝ : Group G
s t : Set α
f✝ g : α → G
a : α
h : s ⊆ t
f : α → G
⊢ mulIndicator (t \ s) f = mulIndicator t f / mulIndicator s f
[PROOFSTEP]
rw [mulIndicator_diff h, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∏ i in s, g i (f i) = ∏ i in t, g i (mulIndicator (↑s) f i)
[PROOFSTEP]
rw [← Finset.prod_subset h _]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∏ i in s, g i (f i) = ∏ x in s, g x (mulIndicator (↑s) f x)
[PROOFSTEP]
apply Finset.prod_congr rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∀ (x : α), x ∈ s → g x (f x) = g x (mulIndicator (↑s) f x)
[PROOFSTEP]
intro i hi
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
hi : i ∈ s
⊢ g i (f i) = g i (mulIndicator (↑s) f i)
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
hi : i ∈ s
⊢ f i = mulIndicator (↑s) f i
[PROOFSTEP]
symm
  -- Porting note: This did not use to need the implicit argument
[GOAL]
case e_a
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
hi : i ∈ s
⊢ mulIndicator (↑s) f i = f i
[PROOFSTEP]
exact mulIndicator_of_mem (α := α) hi f
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∀ (x : α), x ∈ t → ¬x ∈ s → g x (mulIndicator (↑s) f x) = 1
[PROOFSTEP]
refine' fun i _ hn => _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
x✝ : i ∈ t
hn : ¬i ∈ s
⊢ g i (mulIndicator (↑s) f i) = 1
[PROOFSTEP]
convert hg i
[GOAL]
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
x✝ : i ∈ t
hn : ¬i ∈ s
⊢ mulIndicator (↑s) f i = 1
[PROOFSTEP]
exact mulIndicator_of_not_mem (α := α) hn f
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
s : Finset ι
f : ι → α → M
t : ι → Set α
g : ι → α
inst✝ : DecidablePred fun i => g i ∈ t i
⊢ ∏ i in s, mulIndicator (t i) (f i) (g i) = ∏ i in Finset.filter (fun i => g i ∈ t i) s, f i (g i)
[PROOFSTEP]
refine' (Finset.prod_filter_mul_prod_filter_not s (fun i => g i ∈ t i) _).symm.trans _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
s : Finset ι
f : ι → α → M
t : ι → Set α
g : ι → α
inst✝ : DecidablePred fun i => g i ∈ t i
⊢ (∏ x in Finset.filter (fun i => g i ∈ t i) s, mulIndicator (t x) (f x) (g x)) *
      ∏ x in Finset.filter (fun x => ¬g x ∈ t x) s, mulIndicator (t x) (f x) (g x) =
    ∏ i in Finset.filter (fun i => g i ∈ t i) s, f i (g i)
[PROOFSTEP]
refine' Eq.trans _ (mul_one _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
s : Finset ι
f : ι → α → M
t : ι → Set α
g : ι → α
inst✝ : DecidablePred fun i => g i ∈ t i
⊢ (∏ x in Finset.filter (fun i => g i ∈ t i) s, mulIndicator (t x) (f x) (g x)) *
      ∏ x in Finset.filter (fun x => ¬g x ∈ t x) s, mulIndicator (t x) (f x) (g x) =
    (∏ i in Finset.filter (fun i => g i ∈ t i) s, f i (g i)) * 1
[PROOFSTEP]
exact
  congr_arg₂ (· * ·) (Finset.prod_congr rfl fun x hx => mulIndicator_of_mem (Finset.mem_filter.1 hx).2 _)
    (Finset.prod_eq_one fun x hx => mulIndicator_of_not_mem (Finset.mem_filter.1 hx).2 _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I : Finset ι
s : ι → Set α
f : α → M
⊢ (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
[PROOFSTEP]
classical
refine' Finset.induction_on I _ _
· intro
  funext
  simp
intro a I haI ih hI
funext
rw [Finset.prod_insert haI, Finset.set_biUnion_insert, mulIndicator_union_of_not_mem_inter, ih _]
· intro i hi j hj hij
  exact hI i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
simp only [not_exists, exists_prop, mem_iUnion, mem_inter_iff, not_and]
intro hx a' ha'
refine' disjoint_left.1 (hI a (Finset.mem_insert_self _ _) a' (Finset.mem_insert_of_mem ha') _) hx
exact (ne_of_mem_of_not_mem ha' haI).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I : Finset ι
s : ι → Set α
f : α → M
⊢ (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
[PROOFSTEP]
refine' Finset.induction_on I _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I : Finset ι
s : ι → Set α
f : α → M
⊢ (∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ ∅), s i) f = fun a => ∏ i in ∅, mulIndicator (s i) f a
[PROOFSTEP]
intro
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I : Finset ι
s : ι → Set α
f : α → M
a✝ : ∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (s i) (s j)
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ ∅), s i) f = fun a => ∏ i in ∅, mulIndicator (s i) f a
[PROOFSTEP]
funext
[GOAL]
case refine'_1.h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I : Finset ι
s : ι → Set α
f : α → M
a✝ : ∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ ∅), s i) f x✝ = ∏ i in ∅, mulIndicator (s i) f x✝
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I : Finset ι
s : ι → Set α
f : α → M
⊢ ∀ ⦃a : ι⦄ {s_1 : Finset ι},
    ¬a ∈ s_1 →
      ((∀ (i : ι), i ∈ s_1 → ∀ (j : ι), j ∈ s_1 → i ≠ j → Disjoint (s i) (s j)) →
          mulIndicator (⋃ (i : ι) (_ : i ∈ s_1), s i) f = fun a => ∏ i in s_1, mulIndicator (s i) f a) →
        (∀ (i : ι), i ∈ insert a s_1 → ∀ (j : ι), j ∈ insert a s_1 → i ≠ j → Disjoint (s i) (s j)) →
          mulIndicator (⋃ (i : ι) (_ : i ∈ insert a s_1), s i) f = fun a_4 =>
            ∏ i in insert a s_1, mulIndicator (s i) f a_4
[PROOFSTEP]
intro a I haI ih hI
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ insert a I), s i) f = fun a_1 => ∏ i in insert a I, mulIndicator (s i) f a_1
[PROOFSTEP]
funext
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ insert a I), s i) f x✝ = ∏ i in insert a I, mulIndicator (s i) f x✝
[PROOFSTEP]
rw [Finset.prod_insert haI, Finset.set_biUnion_insert, mulIndicator_union_of_not_mem_inter, ih _]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)
[PROOFSTEP]
intro i hi j hj hij
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
i : ι
hi : i ∈ I
j : ι
hj : j ∈ I
hij : i ≠ j
⊢ Disjoint (s i) (s j)
[PROOFSTEP]
exact hI i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
[GOAL]
case refine'_2.h.h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ ¬x✝ ∈ s a ∩ ⋃ (x : ι) (_ : x ∈ I), s x
[PROOFSTEP]
simp only [not_exists, exists_prop, mem_iUnion, mem_inter_iff, not_and]
[GOAL]
case refine'_2.h.h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ x✝ ∈ s a → ∀ (x : ι), x ∈ I → ¬x✝ ∈ s x
[PROOFSTEP]
intro hx a' ha'
[GOAL]
case refine'_2.h.h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
hx : x✝ ∈ s a
a' : ι
ha' : a' ∈ I
⊢ ¬x✝ ∈ s a'
[PROOFSTEP]
refine' disjoint_left.1 (hI a (Finset.mem_insert_self _ _) a' (Finset.mem_insert_of_mem ha') _) hx
[GOAL]
case refine'_2.h.h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
hx : x✝ ∈ s a
a' : ι
ha' : a' ∈ I
⊢ a ≠ a'
[PROOFSTEP]
exact (ne_of_mem_of_not_mem ha' haI).symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : CommMonoid M
I : Finset ι
s : ι → Set α
f : α → M
h : ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)
x : α
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f x = ∏ i in I, mulIndicator (s i) f x
[PROOFSTEP]
rw [Set.mulIndicator_finset_biUnion I s h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ (indicator s fun a => f a * g a) = fun a => indicator s f a * indicator s g a
[PROOFSTEP]
funext
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
⊢ indicator s (fun a => f a * g a) x✝ = indicator s f x✝ * indicator s g x✝
[PROOFSTEP]
simp only [indicator]
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 0) = (if x✝ ∈ s then f x✝ else 0) * if x✝ ∈ s then g x✝ else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 0 = 0 * 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ indicator s (fun a => f a * g a) a = indicator s f a * g a
[PROOFSTEP]
simp only [indicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ (if a ∈ s then f a * g a else 0) = (if a ∈ s then f a else 0) * g a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
h✝ : a ∈ s
⊢ f a * g a = f a * g a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
h✝ : ¬a ∈ s
⊢ 0 = 0 * g a
[PROOFSTEP]
rw [zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ indicator s (fun a => f a * g a) a = f a * indicator s g a
[PROOFSTEP]
simp only [indicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ (if a ∈ s then f a * g a else 0) = f a * if a ∈ s then g a else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
h✝ : a ∈ s
⊢ f a * g a = f a * g a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
h✝ : ¬a ∈ s
⊢ 0 = f a * 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
⊢ indicator (t1 ∩ t2) (fun x => f x * g x) x = indicator t1 f x * indicator t2 g x
[PROOFSTEP]
rw [← Set.indicator_indicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
⊢ indicator t1 (indicator t2 fun x => f x * g x) x = indicator t1 f x * indicator t2 g x
[PROOFSTEP]
simp_rw [indicator]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
⊢ (if x ∈ t1 then if x ∈ t2 then f x * g x else 0 else 0) = (if x ∈ t1 then f x else 0) * if x ∈ t2 then g x else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
h✝¹ : x ∈ t1
h✝ : x ∈ t2
⊢ f x * g x = f x * g x
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
h✝¹ : x ∈ t1
h✝ : ¬x ∈ t2
⊢ 0 = f x * 0
[PROOFSTEP]
simp
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
h✝¹ : ¬x ∈ t1
h✝ : x ∈ t2
⊢ 0 = 0 * g x
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
h✝¹ : ¬x ∈ t1
h✝ : ¬x ∈ t2
⊢ 0 = 0 * 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s t : Set α
x✝ : α
⊢ indicator (s ∩ t) 1 x✝ = (indicator s 1 * indicator t 1) x✝
[PROOFSTEP]
simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s t : Set α
x✝ : α
⊢ indicator (s ∩ t) 1 x✝ = indicator (s ∩ t) (fun x => 1) x✝
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
⊢ indicator (s ×ˢ t) 1 (x, y) = indicator s 1 x * indicator t 1 y
[PROOFSTEP]
simp_rw [indicator, mem_prod_eq]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
⊢ (if x ∈ s ∧ y ∈ t then OfNat.ofNat 1 (x, y) else 0) =
    (if x ∈ s then OfNat.ofNat 1 x else 0) * if y ∈ t then OfNat.ofNat 1 y else 0
[PROOFSTEP]
split_ifs with h₀
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : x ∈ s ∧ y ∈ t
h✝¹ : x ∈ s
h✝ : y ∈ t
⊢ OfNat.ofNat 1 (x, y) = OfNat.ofNat 1 x * OfNat.ofNat 1 y
[PROOFSTEP]
simp only [Pi.one_apply, mul_one, mul_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : x ∈ s ∧ y ∈ t
h✝¹ : x ∈ s
h✝ : ¬y ∈ t
⊢ OfNat.ofNat 1 (x, y) = OfNat.ofNat 1 x * 0
[PROOFSTEP]
simp only [Pi.one_apply, mul_one, mul_zero]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : x ∈ s ∧ y ∈ t
h✝¹ : ¬x ∈ s
h✝ : y ∈ t
⊢ OfNat.ofNat 1 (x, y) = 0 * OfNat.ofNat 1 y
[PROOFSTEP]
simp only [Pi.one_apply, mul_one, mul_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : x ∈ s ∧ y ∈ t
h✝¹ : ¬x ∈ s
h✝ : ¬y ∈ t
⊢ OfNat.ofNat 1 (x, y) = 0 * 0
[PROOFSTEP]
simp only [Pi.one_apply, mul_one, mul_zero]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : ¬(x ∈ s ∧ y ∈ t)
h✝¹ : x ∈ s
h✝ : y ∈ t
⊢ 0 = OfNat.ofNat 1 x * OfNat.ofNat 1 y
[PROOFSTEP]
simp only [Pi.one_apply, mul_one, mul_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : ¬(x ∈ s ∧ y ∈ t)
h✝¹ : x ∈ s
h✝ : ¬y ∈ t
⊢ 0 = OfNat.ofNat 1 x * 0
[PROOFSTEP]
simp only [Pi.one_apply, mul_one, mul_zero]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : ¬(x ∈ s ∧ y ∈ t)
h✝¹ : ¬x ∈ s
h✝ : y ∈ t
⊢ 0 = 0 * OfNat.ofNat 1 y
[PROOFSTEP]
simp only [Pi.one_apply, mul_one, mul_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : ¬(x ∈ s ∧ y ∈ t)
h✝¹ : ¬x ∈ s
h✝ : ¬y ∈ t
⊢ 0 = 0 * 0
[PROOFSTEP]
simp only [Pi.one_apply, mul_one, mul_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : x ∈ s ∧ y ∈ t
h✝¹ : x ∈ s
h✝ : ¬y ∈ t
⊢ 1 = 0
[PROOFSTEP]
tauto
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : x ∈ s ∧ y ∈ t
h✝¹ : ¬x ∈ s
h✝ : y ∈ t
⊢ 1 = 0
[PROOFSTEP]
tauto
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : x ∈ s ∧ y ∈ t
h✝¹ : ¬x ∈ s
h✝ : ¬y ∈ t
⊢ 1 = 0
[PROOFSTEP]
tauto
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝ : MulZeroOneClass M
s : Set α
t : Set β
x : α
y : β
h₀ : ¬(x ∈ s ∧ y ∈ t)
h✝¹ : x ∈ s
h✝ : y ∈ t
⊢ 0 = 1
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulZeroOneClass M
inst✝ : Nontrivial M
U : Set α
x : α
⊢ indicator U 1 x = 0 ↔ ¬x ∈ U
[PROOFSTEP]
classical simp [indicator_apply, imp_false]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulZeroOneClass M
inst✝ : Nontrivial M
U : Set α
x : α
⊢ indicator U 1 x = 0 ↔ ¬x ∈ U
[PROOFSTEP]
simp [indicator_apply, imp_false]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulZeroOneClass M
inst✝ : Nontrivial M
U : Set α
x : α
⊢ indicator U 1 x = 1 ↔ x ∈ U
[PROOFSTEP]
classical simp [indicator_apply, imp_false]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulZeroOneClass M
inst✝ : Nontrivial M
U : Set α
x : α
⊢ indicator U 1 x = 1 ↔ x ∈ U
[PROOFSTEP]
simp [indicator_apply, imp_false]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulZeroOneClass M
inst✝ : Nontrivial M
U V : Set α
h : indicator U 1 = indicator V 1
⊢ U = V
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : MulZeroOneClass M
inst✝ : Nontrivial M
U V : Set α
h : indicator U 1 = indicator V 1
x✝ : α
⊢ x✝ ∈ U ↔ x✝ ∈ V
[PROOFSTEP]
simp_rw [← indicator_eq_one_iff_mem M, h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
s t : Set α
f g : α → M
a : α
y : M
inst✝ : LE M
hfg : a ∈ s → f a ≤ y
hg : ¬a ∈ s → 1 ≤ y
⊢ mulIndicator s f a ≤ y
[PROOFSTEP]
by_cases ha : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
s t : Set α
f g : α → M
a : α
y : M
inst✝ : LE M
hfg : a ∈ s → f a ≤ y
hg : ¬a ∈ s → 1 ≤ y
ha : a ∈ s
⊢ mulIndicator s f a ≤ y
[PROOFSTEP]
simpa [ha] using hfg ha
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
inst✝¹ : One M
s t : Set α
f g : α → M
a : α
y : M
inst✝ : LE M
hfg : a ∈ s → f a ≤ y
hg : ¬a ∈ s → 1 ≤ y
ha : ¬a ∈ s
⊢ mulIndicator s f a ≤ y
[PROOFSTEP]
simpa [ha] using hg ha
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
by_cases hx : x ∈ ⋃ i, s i
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ (i : ι), s i
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
rw [mulIndicator_of_mem hx]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ (i : ι), s i
⊢ f x = ⨆ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
rw [mem_iUnion] at hx
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ i, x ∈ s i
⊢ f x = ⨆ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
refine' le_antisymm _ (iSup_le fun i => mulIndicator_le_self' (fun x _ => h1 ▸ bot_le) x)
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ i, x ∈ s i
⊢ f x ≤ ⨆ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
rcases hx with ⟨i, hi⟩
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
i : ι
hi : x ∈ s i
⊢ f x ≤ ⨆ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
exact le_iSup_of_le i (ge_of_eq <| mulIndicator_of_mem hi _)
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ¬x ∈ ⋃ (i : ι), s i
⊢ mulIndicator (⋃ (i : ι), s i) f x = ⨆ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
rw [mulIndicator_of_not_mem hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ¬x ∈ ⋃ (i : ι), s i
⊢ 1 = ⨆ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
simp only [mem_iUnion, not_exists] at hx
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝³ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝² : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (x_1 : ι), ¬x ∈ s x_1
⊢ 1 = ⨆ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
simp [hx, ← h1]
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
⊢ mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
by_cases hx : x ∈ ⋂ i, s i
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋂ (i : ι), s i
⊢ mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
rw [mulIndicator_of_mem hx]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋂ (i : ι), s i
⊢ f x = ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
rw [mem_iInter] at hx
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
⊢ f x = ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
refine le_antisymm ?_ (by simp only [mulIndicator_of_mem (hx _), ciInf_const, le_refl])
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
⊢ ⨅ (i : ι), mulIndicator (s i) f x ≤ f x
[PROOFSTEP]
simp only [mulIndicator_of_mem (hx _), ciInf_const, le_refl]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
⊢ f x ≤ ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
exact le_iInf (fun j ↦ by simp only [mulIndicator_of_mem (hx j), le_refl])
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∀ (i : ι), x ∈ s i
j : ι
⊢ f x ≤ mulIndicator (s j) f x
[PROOFSTEP]
simp only [mulIndicator_of_mem (hx j), le_refl]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ¬x ∈ ⋂ (i : ι), s i
⊢ mulIndicator (⋂ (i : ι), s i) f x = ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
rw [mulIndicator_of_not_mem hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ¬x ∈ ⋂ (i : ι), s i
⊢ 1 = ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
simp only [mem_iInter, not_exists, not_forall] at hx
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ x_1, ¬x ∈ s x_1
⊢ 1 = ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
rcases hx with ⟨j, hj⟩
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : ¬x ∈ s j
⊢ 1 = ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
refine le_antisymm (by simp only [← h1, le_iInf_iff, bot_le, forall_const]) ?_
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : ¬x ∈ s j
⊢ 1 ≤ ⨅ (i : ι), mulIndicator (s i) f x
[PROOFSTEP]
simp only [← h1, le_iInf_iff, bot_le, forall_const]
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
M✝ : Type u_4
N : Type u_5
inst✝⁴ : One M✝
s✝ t : Set α
f✝ g : α → M✝
a : α
y : M✝
inst✝³ : Preorder M✝
ι : Sort u_6
M : Type u_7
inst✝² : Nonempty ι
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : ¬x ∈ s j
⊢ ⨅ (i : ι), mulIndicator (s i) f x ≤ 1
[PROOFSTEP]
simpa [mulIndicator_of_not_mem hj] using (iInf_le (fun i ↦ (s i).mulIndicator f) j) x
[GOAL]
α : Type u_1
β✝ : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
β : Type u_6
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
⊢ indicator s f ≤ indicator {x | 0 ≤ f x} f
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β✝ : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
β : Type u_6
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
⊢ indicator s f x ≤ indicator {x | 0 ≤ f x} f x
[PROOFSTEP]
classical
simp_rw [indicator_apply]
split_ifs with h_1 h_2 h_3
· exact le_rfl
· exact (not_le.mp h_2).le
· exact h_3
· exact le_rfl
[GOAL]
α : Type u_1
β✝ : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
β : Type u_6
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
⊢ indicator s f x ≤ indicator {x | 0 ≤ f x} f x
[PROOFSTEP]
simp_rw [indicator_apply]
[GOAL]
α : Type u_1
β✝ : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
β : Type u_6
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
⊢ (if x ∈ s then f x else 0) ≤ if x ∈ {x | 0 ≤ f x} then f x else 0
[PROOFSTEP]
split_ifs with h_1 h_2 h_3
[GOAL]
case pos
α : Type u_1
β✝ : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
β : Type u_6
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : x ∈ s
h_2 : x ∈ {x | 0 ≤ f x}
⊢ f x ≤ f x
[PROOFSTEP]
exact le_rfl
[GOAL]
case neg
α : Type u_1
β✝ : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
β : Type u_6
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : x ∈ s
h_2 : ¬x ∈ {x | 0 ≤ f x}
⊢ f x ≤ 0
[PROOFSTEP]
exact (not_le.mp h_2).le
[GOAL]
case pos
α : Type u_1
β✝ : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
β : Type u_6
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : ¬x ∈ s
h_3 : x ∈ {x | 0 ≤ f x}
⊢ 0 ≤ f x
[PROOFSTEP]
exact h_3
[GOAL]
case neg
α : Type u_1
β✝ : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
β : Type u_6
inst✝¹ : LinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
x : α
h_1 : ¬x ∈ s
h_3 : ¬x ∈ {x | 0 ≤ f x}
⊢ 0 ≤ 0
[PROOFSTEP]
exact le_rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
M✝ : Type u_4
N✝ : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
s : Set α
g : α → M
x : α
⊢ ↑f (Set.mulIndicator s g x) = Set.mulIndicator s (↑f ∘ g) x
[PROOFSTEP]
simp [Set.mulIndicator_comp_of_one]


[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a✝ a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
a : α
⊢ a - a = 0 • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ (∃ b_1, b - a = ↑(Equiv.neg ℤ).symm b_1 • p) ↔ b ≡ a [PMOD p]
[PROOFSTEP]
simp [ModEq, ← neg_eq_iff_eq_neg]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n✝ : ℕ
z : ℤ
x✝¹ : a ≡ b [PMOD p]
x✝ : b ≡ c [PMOD p]
m : ℤ
hm : b - a = m • p
n : ℤ
hn : c - b = n • p
⊢ c - a = (m + n) • p
[PROOFSTEP]
simp [add_smul, ← hm, ← hn]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ -b ≡ -a [PMOD p] ↔ a ≡ b [PMOD p]
[PROOFSTEP]
simp [ModEq, neg_add_eq_sub]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ b ≡ a [PMOD -p] ↔ a ≡ b [PMOD p]
[PROOFSTEP]
simp [ModEq, ← neg_eq_iff_eq_neg]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a ≡ b [PMOD 0] ↔ a = b
[PROOFSTEP]
simp [ModEq, sub_eq_zero, eq_comm]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ 0 - p = -1 • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z✝ z : ℤ
⊢ 0 - z • p = -z • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z✝ z : ℤ
⊢ a - (a + z • p) = -z • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z✝ z : ℤ
⊢ a - (z • p + a) = -z • p
[PROOFSTEP]
simp [← sub_sub]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n✝ : ℕ
z : ℤ
n : ℕ
⊢ a - (a + n • p) = -↑n • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n✝ : ℕ
z : ℤ
n : ℕ
⊢ a - (n • p + a) = -↑n • p
[PROOFSTEP]
simp [← sub_sub]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a ≡ b [PMOD z • p]
m : ℤ
hm : b - a = m • z • p
⊢ b - a = (m * z) • p
[PROOFSTEP]
rwa [mul_smul]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a ≡ b [PMOD n • p]
m : ℤ
hm : b - a = m • n • p
⊢ b - a = (m * ↑n) • p
[PROOFSTEP]
rwa [mul_smul, coe_nat_zsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z m : ℤ
hm : b - a = m • p
⊢ z • b - z • a = m • z • p
[PROOFSTEP]
rw [← smul_sub, hm, smul_comm]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z m : ℤ
hm : b - a = m • p
⊢ n • b - n • a = m • n • p
[PROOFSTEP]
rw [← smul_sub, hm, smul_comm]
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
inst✝ : NoZeroSMulDivisors ℤ α
hn : z ≠ 0
m : ℤ
⊢ z • b - z • a = m • z • p ↔ b - a = m • p
[PROOFSTEP]
rw [← smul_sub, smul_comm, smul_right_inj hn]
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
inst✝ : NoZeroSMulDivisors ℕ α
hn : n ≠ 0
m : ℤ
⊢ n • b - n • a = m • n • p ↔ b - a = m • p
[PROOFSTEP]
rw [← smul_sub, smul_comm, smul_right_inj hn]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a₁ ≡ b₁ [PMOD p]
m : ℤ
hm : b₁ - a₁ = m • p
⊢ (∃ b, b₁ + b₂ - (a₁ + a₂) = ↑(Equiv.addLeft m).symm.symm b • p) ↔ a₂ ≡ b₂ [PMOD p]
[PROOFSTEP]
simp [add_sub_add_comm, hm, add_smul, ModEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a₂ ≡ b₂ [PMOD p]
m : ℤ
hm : b₂ - a₂ = m • p
⊢ (∃ b, b₁ + b₂ - (a₁ + a₂) = ↑(Equiv.addRight m).symm.symm b • p) ↔ a₁ ≡ b₁ [PMOD p]
[PROOFSTEP]
simp [add_sub_add_comm, hm, add_smul, ModEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a₁ ≡ b₁ [PMOD p]
m : ℤ
hm : b₁ - a₁ = m • p
⊢ (∃ b, b₁ - b₂ - (a₁ - a₂) = ↑(Equiv.subLeft m).symm.symm b • p) ↔ a₂ ≡ b₂ [PMOD p]
[PROOFSTEP]
simp [sub_sub_sub_comm, hm, sub_smul, ModEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a₂ ≡ b₂ [PMOD p]
m : ℤ
hm : b₂ - a₂ = m • p
⊢ (∃ b, b₁ - b₂ - (a₁ - a₂) = ↑(Equiv.subRight m).symm.symm b • p) ↔ a₁ ≡ b₁ [PMOD p]
[PROOFSTEP]
simp [sub_sub_sub_comm, hm, sub_smul, ModEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]
[PROOFSTEP]
simp [ModEq, sub_sub]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ c + a ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]
[PROOFSTEP]
simp [sub_modEq_iff_modEq_add]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]
[PROOFSTEP]
simp [← modEq_sub_iff_add_modEq']
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]
[PROOFSTEP]
simp [← modEq_sub_iff_add_modEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p
[PROOFSTEP]
simp_rw [ModEq, sub_eq_iff_eq_add']
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p
[PROOFSTEP]
rw [modEq_iff_eq_add_zsmul, not_exists]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a ≡ b [PMOD p] ↔ ↑b = ↑a
[PROOFSTEP]
simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff, eq_sub_iff_add_eq',
  eq_comm]
[GOAL]
α : Type u_1
a b z : ℤ
⊢ a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]
[PROOFSTEP]
simp [ModEq, dvd_iff_exists_eq_mul_left, Int.modEq_iff_dvd]
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ ↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]
[PROOFSTEP]
simp_rw [ModEq, ← Int.cast_mul_eq_zsmul_cast]
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ (∃ z_1, ↑b - ↑a = ↑(z_1 * z)) ↔ ∃ z_1, b - a = z_1 • z
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b n : ℕ
⊢ ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]
[PROOFSTEP]
simp_rw [← Int.coe_nat_modEq_iff, ← modEq_iff_int_modEq, ← @int_cast_modEq_int_cast α, Int.cast_ofNat]


[GOAL]
R : Type u_1
inst✝ : Zero R
n : R
⊢ ¬NeZero n ↔ n = 0
[PROOFSTEP]
simp [neZero_iff]