-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem induction {α γ} [MeasurableSpace α] [AddMonoid γ] {P : SimpleFunc α γ → Prop}
    (h_ind :
      ∀ (c) {s} (hs : MeasurableSet s),
        P (SimpleFunc.piecewise s hs (SimpleFunc.const _ c) (SimpleFunc.const _ 0)))
    (h_add : ∀ ⦃f g : SimpleFunc α γ⦄, Disjoint (support f) (support g) → P f → P g → P (f + g))
    (f : SimpleFunc α γ) : P f

Proof state:
α : Type u_5
γ : Type u_6
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

Tactic:
generalize h : f.range \ {0} = s

Result:
α : Type u_5
γ : Type u_6
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 : f.range \ {0} = s
⊢ P f

Proof state:
case empty
α : Type u_5
γ : Type u_6
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

Tactic:
convert h_ind 0 MeasurableSet.univ

Result:
case h.e'_1
α : Type u_5
γ : Type u_6
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 ⋯ (const α 0) (const α 0)

Proof state:
case h.e'_1.H
α : Type u_5
γ : Type u_6
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

Tactic:
by_cases hy : y ∈ f ⁻¹' {x}

Result:
case pos
α : Type u_5
γ : Type u_6
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_5
γ : Type u_6
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

Proof state:
case h.e'_4
α : Type u_5
γ : Type u_6
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

Tactic:
exact preimage_const_of_mem (mem_singleton _)

Result:
no goals

Proof state:
case h.e'_1
α : Type u_5
γ : Type u_6
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 ⋯ (const α 0) (const α 0)

Tactic:
ext x

Result:
case h.e'_1.H
α : Type u_5
γ : Type u_6
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 ⋯ (const α 0) (const α 0)) x

Proof state:
case h
α : Type u_5
γ : Type u_6
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}

Tactic:
convert Set.subset_univ _

Result:
case h.e'_4
α : Type u_5
γ : Type u_6
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

Proof state:
case pos
α : Type u_5
γ : Type u_6
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 ∈ ⊥

Tactic:
simp [g, piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]

Result:
no goals

Proof state:
case h
α : Type u_5
γ : Type u_6
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

Tactic:
rwa [Finset.mem_coe]

Result:
no goals