α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
s : Finset γ
h : SimpleFunc.range f \ {0} = s
⊢ P f
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
⊢ P f
generalize h : f.range \ {0} = s
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
s : Finset γ
h : range ↑f \ {0} = ↑s
⊢ P f
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
s : Finset γ
h : SimpleFunc.range f \ {0} = s
⊢ P f
rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h
case empty
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : ↑f = Function.const α 0
⊢ P f
case empty
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : range ↑f \ {0} = ↑∅
⊢ P f
rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h
case h.e'_1
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : ↑f = Function.const α 0
⊢ f = piecewise univ (_ : MeasurableSet univ) (const α 0) (const α 0)
case empty
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : ↑f = Function.const α 0
⊢ P f
convert h_ind 0 MeasurableSet.univ
case h.e'_1.H
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : ↑f = Function.const α 0
x : α
⊢ ↑f x = ↑(piecewise univ (_ : MeasurableSet univ) (const α 0) (const α 0)) x
case h.e'_1
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : ↑f = Function.const α 0
⊢ f = piecewise univ (_ : MeasurableSet univ) (const α 0) (const α 0)
ext x
no goals
case h.e'_1.H
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : ↑f = Function.const α 0
x : α
⊢ ↑f x = ↑(piecewise univ (_ : MeasurableSet univ) (const α 0) (const α 0)) x
simp [h]
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
⊢ P f
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
⊢ P f
have mx := f.measurableSet_preimage {x}
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ P f
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
⊢ P f
let g := SimpleFunc.piecewise (f ⁻¹' {x}) mx 0 f
case h.e'_1
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ f = g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)

case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ Disjoint (support ↑g) (support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)))
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ P f
convert h_add _ Pg (h_ind x mx)
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) ≤ ⊥
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ Disjoint (support ↑g) (support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)))
rw [disjoint_iff_inf_le]
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
⊢ y ∈ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) → y ∈ ⊥
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) ≤ ⊥
rintro y
case pos
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : y ∈ ↑f ⁻¹' {x}
⊢ y ∈ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) → y ∈ ⊥

case neg
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : ¬y ∈ ↑f ⁻¹' {x}
⊢ y ∈ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) → y ∈ ⊥
case insert
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
⊢ y ∈ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) → y ∈ ⊥
by_cases hy : y ∈ f ⁻¹' {x}
case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ range ↑g \ {0} = ↑s
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ P g
apply ih
case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ (↑0 '' (↑f ⁻¹' {x}) ∪ ↑f '' (↑f ⁻¹' {x})ᶜ) \ {0} = ↑s
case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ range ↑g \ {0} = ↑s
simp only [SimpleFunc.coe_piecewise, range_piecewise]
case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ↑0 '' (↑f ⁻¹' {x}) ⊆ {0}

case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ¬x ∈ ↑s
case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ (↑0 '' (↑f ⁻¹' {x}) ∪ ↑f '' (↑f ⁻¹' {x})ᶜ) \ {0} = ↑s
rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert,
  insert_diff_self_of_not_mem, diff_eq_empty.mpr, Set.empty_union]
case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ↑f ⁻¹' {x} ⊆ ↑0 ⁻¹' {0}
case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ↑0 '' (↑f ⁻¹' {x}) ⊆ {0}
rw [Set.image_subset_iff]
case h.e'_4
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ↑0 ⁻¹' {0} = univ
case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ↑f ⁻¹' {x} ⊆ ↑0 ⁻¹' {0}
convert Set.subset_univ _
no goals
case h.e'_4
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ↑0 ⁻¹' {0} = univ
exact preimage_const_of_mem (mem_singleton _)
no goals
case h
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ¬x ∈ ↑s
rwa [Finset.mem_coe]
case h.e'_1.H
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
⊢ ↑f y = ↑(g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) y
case h.e'_1
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ f = g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)
ext1 y
case pos
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : y ∈ ↑f ⁻¹' {x}
⊢ ↑f y = ↑(g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) y

case neg
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : ¬y ∈ ↑f ⁻¹' {x}
⊢ ↑f y = ↑(g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) y
case h.e'_1.H
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
⊢ ↑f y = ↑(g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) y
by_cases hy : y ∈ f ⁻¹' {x}
no goals
case pos
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : y ∈ ↑f ⁻¹' {x}
⊢ ↑f y = ↑(g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) y
simpa [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
no goals
case neg
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : ¬y ∈ ↑f ⁻¹' {x}
⊢ ↑f y = ↑(g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) y
simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
no goals
case pos
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : y ∈ ↑f ⁻¹' {x}
⊢ y ∈ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) → y ∈ ⊥
simp [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
no goals
case neg
α✝ : Type ?u.922804
β : Type ?u.922807
γ✝ : Type ?u.922810
δ : Type ?u.922813
α : Type u_1
γ : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : ¬y ∈ ↑f ⁻¹' {x}
⊢ y ∈ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) → y ∈ ⊥
simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]