awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
neg neg₁ neg₂ : StronglyMeasurable (hs.piecewise (s := s) f)
neg₃ :
  let g : (n : ℕ) → (i : ι) → Fin (n + 1) := fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n;
  ∀ (sg : ∀ (n : ℕ), Function.Surjective (g n)), StronglyMeasurable (hs.piecewise (s := s) f)
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have neg₄ : let g : (n : ℕ) → (i : ι) → Fin (n + 1) := fun (n : ℕ) (i : ι) ↦
  if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), sorry⟩
  else Fin.last n;
∀ (sg : ∀ (n : ℕ), Function.Surjective (g n))
  (G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i),
  StronglyMeasurable (hs.piecewise (s := s) f)
Tactic: classical
  let g (n : ℕ) (i : ι) : Fin (n + 1) :=
    if hi : ∃ m < n, i = e m then ⟨hi.choose, by grind⟩ else Fin.last n
  have sg (n : ℕ) : (g n).Surjective := by
    intro b
    unfold g
    refine ⟨e b, ?_⟩
    by_cases hb : b < n
    · have : ∃ m < n, e b = e m := ⟨b, ⟨hb, rfl⟩⟩
      simpa only [this, Fin.ext_iff] using e.injective this.choose_spec.2.symm
    · simp [hb]
      grind
  have G (n : ℕ) := hs.coarserPartition (g n) (sg n)
  refine ⟨fun n => (G n).simpleFunc_piecewise (fun i => ?_) (fun i => (hf (e i)).approx n),
    fun x => ?_⟩
  · exact .biUnion (to_countable _) fun _ _ ↦ hm _
  simp only [simpleFunc_piecewise, SimpleFunc.coe_mk, piecewise_apply]
  have : ∀ᶠ n in atTop, e ((G n).index x) = hs.index x := by
    obtain ⟨y, hy⟩ := e.bijective.2 (hs.index x)
    refine eventually_atTop.mpr ⟨y + 1, fun b hb => ?_⟩
    have : y = (⟨y, by lia⟩ : Fin (b + 1)).1 := rfl
    rw [← hy, EmbeddingLike.apply_eq_iff_eq, this, ← Fin.ext_iff, ← (G b).mem_iff_index_eq]
    have : ∃ m < b, hs.index x = e m := ⟨y, ⟨by lia, hy.symm⟩⟩
    simpa [g, hs.mem_iff_index_eq, this] using e.injective (hy.trans this.choose_spec.2).symm
  have : ∀ᶠ n in atTop, (hf (hs.index x)).approx n x = (hf (e ((G n).index x))).approx n x := by
    filter_upwards [this] with n hn using by rw [hn]
  exact (Filter.tendsto_congr' this).mp (by simp [StronglyMeasurable.tendsto_approx])
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
neg neg₁ neg₂ : StronglyMeasurable (hs.piecewise (s := s) f)
neg₃ :
  let g : (n : ℕ) → (i : ι) → Fin (n + 1) := fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n;
  ∀ (sg : ∀ (n : ℕ), Function.Surjective (g n)), StronglyMeasurable (hs.piecewise (s := s) f)
neg₄ :
  let g : (n : ℕ) → (i : ι) → Fin (n + 1) := fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n;
  ∀ (sg : ∀ (n : ℕ), Function.Surjective (g n))
    (G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i),
    StronglyMeasurable (hs.piecewise (s := s) f)
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have neg₅ : let g : (n : ℕ) → (i : ι) → Fin (n + 1) := fun (n : ℕ) (i : ι) ↦
  if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), sorry⟩
  else Fin.last n;
∀ (sg : ∀ (n : ℕ), Function.Surjective (g n))
  (G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) (n : ℕ) (i : Fin (n + 1)),
  MeasurableSet.{u_2} (α := α) (⋃ i_1 ∈ g n ⁻¹' {i}, s i_1)
Tactic: classical
  let g (n : ℕ) (i : ι) : Fin (n + 1) :=
    if hi : ∃ m < n, i = e m then ⟨hi.choose, by grind⟩ else Fin.last n
  have sg (n : ℕ) : (g n).Surjective := by
    intro b
    unfold g
    refine ⟨e b, ?_⟩
    by_cases hb : b < n
    · have : ∃ m < n, e b = e m := ⟨b, ⟨hb, rfl⟩⟩
      simpa only [this, Fin.ext_iff] using e.injective this.choose_spec.2.symm
    · simp [hb]
      grind
  have G (n : ℕ) := hs.coarserPartition (g n) (sg n)
  refine ⟨fun n => (G n).simpleFunc_piecewise (fun i => ?_) (fun i => (hf (e i)).approx n),
    fun x => ?_⟩
  · exact .biUnion (to_countable _) fun _ _ ↦ hm _
  simp only [simpleFunc_piecewise, SimpleFunc.coe_mk, piecewise_apply]
  have : ∀ᶠ n in atTop, e ((G n).index x) = hs.index x := by
    obtain ⟨y, hy⟩ := e.bijective.2 (hs.index x)
    refine eventually_atTop.mpr ⟨y + 1, fun b hb => ?_⟩
    have : y = (⟨y, by lia⟩ : Fin (b + 1)).1 := rfl
    rw [← hy, EmbeddingLike.apply_eq_iff_eq, this, ← Fin.ext_iff, ← (G b).mem_iff_index_eq]
    have : ∃ m < b, hs.index x = e m := ⟨y, ⟨by lia, hy.symm⟩⟩
    simpa [g, hs.mem_iff_index_eq, this] using e.injective (hy.trans this.choose_spec.2).symm
  have : ∀ᶠ n in atTop, (hf (hs.index x)).approx n x = (hf (e ((G n).index x))).approx n x := by
    filter_upwards [this] with n hn using by rw [hn]
  exact (Filter.tendsto_congr' this).mp (by simp [StronglyMeasurable.tendsto_approx])
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ AEStronglyMeasurable (hs.piecewise (s := s) f) μ
have choose : ∀ (p : (i : ι) → α → β) (hp : ∀ (i : ι), StronglyMeasurable (p i)) (hq : ∀ (i : ι), f i =ᶠ[ae μ] p i),
  AEStronglyMeasurable (hs.piecewise (s := s) f) μ
Tactic: choose p hp hq using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
p : (i : ι) → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
⊢ AEStronglyMeasurable (hs.piecewise (s := s) f) μ
have refine : hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p
Tactic: refine ⟨hs.piecewise p, hs.stronglyMeasurable_piecewise hm hp, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
p : (i : ι) → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
⊢ hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ι), f i a = p i a) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ hs.piecewise (s := s) f x = hs.piecewise (s := s) p x) x} x}
    a
Tactic: filter_upwards [ae_all_iff.2 hq] with x hx using hx (hs.index x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
p : (i : ι) → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ι), f i a = p i a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ hs.piecewise (s := s) f x = hs.piecewise (s := s) p x) x}
            x}
      a
⊢ hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p
have h₁ : ∀ (a : α), (∀ (i : ι), f i a = p i a) → hs.piecewise (s := s) f a = hs.piecewise (s := s) p a
Tactic: filter_upwards [ae_all_iff.2 hq] with x hx using hx (hs.index x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst : Nonempty β
⊢ ∃ (c : β), ∀ (x : α), (f : (a : α) → β) x = c
have hf_meas : ∀ (x : β), MeasurableSet.{u_5} (α := α) (preimage (β := β) (⇑f : (a : α) → β) {x})
Tactic: have hf_meas := @SimpleFunc.measurableSet_fiber α _ ⊥ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst : Nonempty β
hf_meas : ∀ (x : β), MeasurableSet.{u_5} (α := α) (preimage (β := β) (⇑f : (a : α) → β) {x})
⊢ ∃ (c : β), ∀ (x : α), (f : (a : α) → β) x = c
have hf_meas₁ : ∀ (x : β),
  Eq.{u_5 + 1} (α := Set α) (preimage (β := β) (⇑f : (a : α) → β) {x}) ∅ ∨
    Eq.{u_5 + 1} (α := Set α) (preimage (β := β) (⇑f : (a : α) → β) {x}) univ
Tactic: simp_rw [MeasurableSpace.measurableSet_bot_iff] at hf_meas
Cleared hypotheses: hf_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
⊢ Eq.{u_1 + 1} (α := Set α) {a : α | r a ((f : (a : α) → β) a)}
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α) {a : α | r a ((f : (a : α) → β) a)} a ↔
    Membership.mem (γ := Set α)
      (⋃ (b : β),
        ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
          {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
      a
Tactic: ext a
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
a : α
⊢ Membership.mem (γ := Set α) {a : α | r a ((f : (a : α) → β) a)} a ↔
    Membership.mem (γ := Set α)
      (⋃ (b : β),
        ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
          {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
      a
have h₁ : r a ((f : (a : α) → β) a) ↔
  ∃ (i : α), r a ((f : (a : α) → β) i) ∧ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) i : β)
Tactic: suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
⊢ MeasurableSet.{u_1} (α := α) {a : α | r a ((f : (a : α) → β) a)}
have this : Eq.{u_1 + 1} (α := Set α) {a : α | r a ((f : (a : α) → β) a)}
  (⋃ (b : β),
    ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
      {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
Tactic: have : { a | r a (f a) } = ⋃ b ∈ range f, { a | r a b } ∩ f ⁻¹' {b} := by
    ext a
    suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
    exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet.{u_1} (α := α) {a : α | r a b}
this :
  Eq.{u_1 + 1} (α := Set α) {a : α | r a ((f : (a : α) → β) a)}
    (⋃ (b : β),
      ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
        {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
⊢ MeasurableSet.{u_1} (α := α) {a : α | r a ((f : (a : α) → β) a)}
have rw : MeasurableSet.{u_1} (α := α)
  (⋃ (b : β),
    ⋃ (_ : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
      {a : α | r a b} ∩ preimage (β := β) (⇑f : (a : α) → β) {b})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
μ : Measure α
⊢ Eq (α := ℝ≥0∞) (∑ y ∈ f.range, (μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' (↑f.range : Set β)) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
μ : Measure α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' (↑f.range : Set β)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ y ∈ f.range, (μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞)
      (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))) :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
μ : Measure α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' (↑f.range : Set β)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ y ∈ f.range, (μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑(map g f) : (a : α) → γ) ⁻¹' s)
    ((⇑f : (a : α) → β) ⁻¹' (↑({b ∈ f.range | g b ∈ s}) : Set β))
have simp : Eq.{u_1 + 1} (α := Set α) (g ∘ (⇑f : (a : α) → β) ⁻¹' s) ((⇑f : (a : α) → β) ⁻¹' g ⁻¹' s)
Tactic: simp only [coe_range, sep_mem_eq, coe_map, Finset.coe_filter,
    ← mem_preimage, inter_comm, preimage_inter_range, ← Finset.mem_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f₁ : α →ₛ γ
g : α → β
hg : MeasurableEmbedding g
f₂ : β →ₛ γ
this : MeasurableSpace γ := ⊤
⊢ ∀ (x : γ), MeasurableSet (preimage (β := γ) (Function.extend g (⇑f₁ : (a : α) → γ) (⇑f₂ : (a : β) → γ)) {x})
have this₁ : MeasurableSingletonClass γ
Tactic: haveI : MeasurableSingletonClass γ := ⟨fun _ => trivial⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ Eq.{u_1 + 1} (α := Set α) (preimage (β := β × γ) (⇑(f.pair g) : (a : α) → β × γ) {(b, c)})
    (preimage (β := β) (⇑f : (a : α) → β) {b} ∩ preimage (β := γ) (⇑g : (a : α) → γ) {c})
have rw : Eq.{u_1 + 1} (α := Set α) ((⇑(f.pair g) : (a : α) → β × γ) ⁻¹' SProd.sprod (α := Set β) (β := Set γ) {b} {c})
  (preimage (β := β) (⇑f : (a : α) → β) {b} ∩ preimage (β := γ) (⇑g : (a : α) → γ) {c})
Tactic: rw [← singleton_prod_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
⊢ f.bind (const α) = f
have H : ∀ (a : α), Eq.{u_2 + 1} (α := β) ((f.bind (const α) : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
⊢ f.range = ∅
have h : ∀ (a : β), a ∈ f.range ↔ Membership.mem (γ := Finset β) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)
have refine : ∀ (a_1 : γ) (s : Finset γ),
  a_1 ∉ s →
    Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a : β) →
      Eq.{u_2 + 1} (α := β) (((insert a_1 s).sup f : (a : α) → β) a : β)
        ((insert a_1 s).sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)
Tactic: refine Finset.induction_on s rfl ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s_1 : Finset γ
a_1 : α
a : γ
s : Finset γ
h : a ∉ s
ih : Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a_1 : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
⊢ Eq.{u_2 + 1} (α := β) (((insert a s).sup f : (a : α) → β) a_1 : β)
    ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
have rw : Eq.{u_2 + 1} (α := β) ((f a ⊔ s.sup f : (a : α) → β) a_1 : β)
  ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
Tactic: rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s_1 : Finset γ
a_1 : α
a : γ
s : Finset γ
h : a ∉ s
ih : Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a_1 : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw :
  Eq.{u_2 + 1} (α := β) ((f a ⊔ s.sup f : (a : α) → β) a_1 : β)
    ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
⊢ Eq.{u_2 + 1} (α := β) (((insert a s).sup f : (a : α) → β) a_1 : β)
    ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
have rw₁ : Eq.{u_2 + 1} (α := β) ((f a ⊔ s.sup f : (a : α) → β) a_1 : β)
  ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
Tactic: rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s_1 : Finset γ
a_1 : α
a : γ
s : Finset γ
h : a ∉ s
ih : Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a_1 : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw :
  Eq.{u_2 + 1} (α := β) ((f a ⊔ s.sup f : (a : α) → β) a_1 : β)
    ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw₁ :
  Eq.{u_2 + 1} (α := β) ((f a ⊔ s.sup f : (a : α) → β) a_1 : β)
    ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
⊢ Eq.{u_2 + 1} (α := β) (((insert a s).sup f : (a : α) → β) a_1 : β)
    ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
have rw₂ : Eq.{u_2 + 1} (α := β) ((f a : (a : α) → β) a_1 ⊔ (s.sup f : (a : α) → β) a_1 : β)
  ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
Tactic: rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s_1 : Finset γ
a_1 : α
a : γ
s : Finset γ
h : a ∉ s
ih : Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a_1 : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw :
  Eq.{u_2 + 1} (α := β) ((f a ⊔ s.sup f : (a : α) → β) a_1 : β)
    ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw₁ :
  Eq.{u_2 + 1} (α := β) ((f a ⊔ s.sup f : (a : α) → β) a_1 : β)
    ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
rw₂ :
  Eq.{u_2 + 1} (α := β) ((f a : (a : α) → β) a_1 ⊔ (s.sup f : (a : α) → β) a_1 : β)
    ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
⊢ Eq.{u_2 + 1} (α := β) (((insert a s).sup f : (a : α) → β) a_1 : β)
    ((insert a s).sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
have rw₃ : Eq.{u_2 + 1} (α := β) ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
  ((f a : (a : α) → β) a_1 ⊔ s.sup fun (c : γ) ↦ (f c : (a : α) → β) a_1 : β)
Tactic: rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : SemilatticeSup β
inst_2 : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)
have refine : ∀ (a_1 : γ) (s : Finset γ),
  a_1 ∉ s →
    Eq.{u_2 + 1} (α := β) ((s.sup f : (a : α) → β) a : β) (s.sup fun (c : γ) ↦ (f c : (a : α) → β) a : β) →
      Eq.{u_2 + 1} (α := β) (((insert a_1 s).sup f : (a : α) → β) a : β)
        ((insert a_1 s).sup fun (c : γ) ↦ (f c : (a : α) → β) a : β)
Tactic: classical
  refine Finset.induction_on s rfl ?_
  intro a s _ ih
  rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw : Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
  (s.indicator (⇑f : (a : α) → β))
Tactic: rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
Tactic: rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := (a : α) → β) (⇑(if hs : MeasurableSet s then piecewise s hs f 0 else 0) : (a : α) → β)
    (s.indicator (⇑f : (a : α) → β))
rw₁ : Eq (α := (a : α) → β) (⇑(piecewise s hs f 0) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
⊢ Eq (α := (a : α) → β) (⇑(f.restrict s) : (a : α) → β) (s.indicator (⇑f : (a : α) → β))
have rw₂ : Eq (α := (a : α) → β) (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑0 : (a : α) → β))
  (s.indicator (⇑f : (a : α) → β))
Tactic: rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]