awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
inst_4 : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable.{u_5, u_1} (ε := G) (⇑f : (a : α) → G) μ
g : G → F
hg : g 0 = 0
have have₁ have₂ :
  ∀ (T_empty : T ∅ = 0),
    setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have₃ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
⊢ setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have have₄ : ∀ (T_empty : T ∅ = 0)
  (hfp :
    ∀ x ∈ f.range,
      x ≠ 0 →
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Eq.{u_4 + 1} (α := F')
    (∑ x ∈ Finset.image g f.range, (T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {x}) : (a : F) → F') x)
    (∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x))
Tactic: classical
  have T_empty : T ∅ = 0 := h_add.map_empty_eq_zero
  have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' {x}) ≠ ∞ := fun x _ hx0 =>
    (measure_preimage_lt_top_of_integrable f hf hx0).ne
  simp only [setToSimpleFunc, range_map]
  refine Finset.sum_image' _ fun b hb => ?_
  rcases mem_range.1 hb with ⟨a, rfl⟩
  by_cases h0 : g (f a) = 0
  · simp_rw [h0]
    rw [map_zero, Finset.sum_eq_zero fun x hx => ?_]
    rw [mem_filter] at hx
    rw [hx.2, map_zero]
  have h_left_eq :
    T (map g f ⁻¹' {g (f a)}) (g (f a))
      = T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a)) := by
    rw [map_preimage_singleton]
  rw [h_left_eq]
  have h_left_eq' :
    T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a))
      = T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, f ⁻¹' {y}) (g (f a)) := by
    rw [← Finset.set_biUnion_preimage_singleton]
  rw [h_left_eq']
  rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
  · simp only [sum_apply, ContinuousLinearMap.coe_sum']
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [mem_filter] at hx
    rw [hx.2]
  · exact fun i => measurableSet_fiber _ _
  · grind
  · grind [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
inst_4 : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable.{u_5, u_1} (ε := G) (⇑f : (a : α) → G) μ
g : G → F
hg : g 0 = 0
have have₁ have₂ :
  ∀ (T_empty : T ∅ = 0),
    setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have₃ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have₄ :
  ∀ (T_empty : T ∅ = 0)
    (hfp :
      ∀ x ∈ f.range,
        x ≠ 0 →
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq.{u_4 + 1} (α := F')
      (∑ x ∈ Finset.image g f.range, (T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {x}) : (a : F) → F') x)
      (∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x))
⊢ setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have have₅ : ∀ (T_empty : T ∅ = 0)
  (hfp :
    ∀ x ∈ f.range,
      x ≠ 0 →
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (b : G) (hb : b ∈ f.range),
  Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g b}) : (a : F) → F') (g b) : F')
    (∑ j ∈ f.range with g j = g b, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) : F')
Tactic: classical
  have T_empty : T ∅ = 0 := h_add.map_empty_eq_zero
  have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' {x}) ≠ ∞ := fun x _ hx0 =>
    (measure_preimage_lt_top_of_integrable f hf hx0).ne
  simp only [setToSimpleFunc, range_map]
  refine Finset.sum_image' _ fun b hb => ?_
  rcases mem_range.1 hb with ⟨a, rfl⟩
  by_cases h0 : g (f a) = 0
  · simp_rw [h0]
    rw [map_zero, Finset.sum_eq_zero fun x hx => ?_]
    rw [mem_filter] at hx
    rw [hx.2, map_zero]
  have h_left_eq :
    T (map g f ⁻¹' {g (f a)}) (g (f a))
      = T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a)) := by
    rw [map_preimage_singleton]
  rw [h_left_eq]
  have h_left_eq' :
    T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a))
      = T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, f ⁻¹' {y}) (g (f a)) := by
    rw [← Finset.set_biUnion_preimage_singleton]
  rw [h_left_eq']
  rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
  · simp only [sum_apply, ContinuousLinearMap.coe_sum']
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [mem_filter] at hx
    rw [hx.2]
  · exact fun i => measurableSet_fiber _ _
  · grind
  · grind [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
⊢ setToSimpleFunc T (map Prod.fst (f.pair g)) = setToSimpleFunc T (map Prod.snd (f.pair g))
have h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
Tactic: have h_pair : Integrable (f.pair g) μ := integrable_pair hf hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
⊢ setToSimpleFunc T (map Prod.fst (f.pair g)) = setToSimpleFunc T (map Prod.snd (f.pair g))
have rw : ∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1 =
  setToSimpleFunc T (map Prod.snd (f.pair g))
Tactic: rw [map_setToSimpleFunc T h_add h_pair Prod.fst_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
⊢ ∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1 =
    setToSimpleFunc T (map Prod.snd (f.pair g))
have rw : Eq.{u_3 + 1} (α := F)
  (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
  (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2)
Tactic: rw [map_setToSimpleFunc T h_add h_pair Prod.snd_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
⊢ Eq.{u_3 + 1} (α := F)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.1)
    (∑ x ∈ (f.pair g).range, (T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {x}) : (a : E) → F) x.2)
have refine : ∀ (p : E × E) (hp : p ∈ (f.pair g).range),
  Eq.{u_3 + 1} (α := F) ((T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {p}) : (a : E) → F) p.1 : F)
    ((T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {p}) : (a : E) → F) p.2 : F)
Tactic: refine Finset.sum_congr rfl fun p hp => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
p : E × E
hp : p ∈ (f.pair g).range
⊢ Eq.{u_3 + 1} (α := F) ((T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {p}) : (a : E) → F) p.1 : F)
    ((T (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E) {p}) : (a : E) → F) p.2 : F)
have rcases : ∀ (a : α) (hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)),
  Eq.{u_3 + 1} (α := F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).1 :
      F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).2 :
      F)
Tactic: rcases mem_range.1 hp with ⟨a, rfl⟩
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
a : α
hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)
⊢ Eq.{u_3 + 1} (α := F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).1 :
      F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).2 :
      F)
have pos : ∀ (eq : Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)),
  Eq.{u_3 + 1} (α := F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).1 :
      F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).2 :
      F)
Tactic: by_cases eq : f a = g a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
a : α
hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)
pos :
  ∀ (eq : Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)),
    Eq.{u_3 + 1} (α := F)
      ((T
              (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
                (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
            (a : E) → F)
          ((f.pair g : (a : α) → E × E) a).1 :
        F)
      ((T
              (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
                (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
            (a : E) → F)
          ((f.pair g : (a : α) → E × E) a).2 :
        F)
⊢ Eq.{u_3 + 1} (α := F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).1 :
      F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).2 :
      F)
have neg : ∀ (eq : ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)),
  Eq.{u_3 + 1} (α := F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).1 :
      F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).2 :
      F)
Tactic: by_cases eq : f a = g a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
a : α
hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)
eq : Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)
⊢ Eq.{u_3 + 1} (α := F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).1 :
      F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) ((f.pair g : (a : α) → E × E) a : E × E))) :
          (a : E) → F)
        ((f.pair g : (a : α) → E × E) a).2 :
      F)
have pos : Eq.{u_3 + 1} (α := F)
  ((T
          (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
            (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) :
        (a : E) → F)
      ((f : (a : α) → E) a : E) :
    F)
  ((T
          (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
            (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) :
        (a : E) → F)
      ((g : (a : α) → E) a : E) :
    F)
Tactic: dsimp only [pair_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
a : α
hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)
eq : Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)
⊢ Eq.{u_3 + 1} (α := F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) :
          (a : E) → F)
        ((f : (a : α) → E) a : E) :
      F)
    ((T
            (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
              (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) :
          (a : E) → F)
        ((g : (a : α) → E) a : E) :
      F)
have pos : Eq.{u_3 + 1} (α := F)
  ((T
          (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
            (singleton (α := E × E) (((g : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) :
        (a : E) → F)
      ((g : (a : α) → E) a : E) :
    F)
  ((T
          (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
            (singleton (α := E × E) (((g : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) :
        (a : E) → F)
      ((g : (a : α) → E) a : E) :
    F)
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
a : α
hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)
eq : ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)
⊢ T
      (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
        (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) =
    T
      (Set.preimage (β := E) (⇑f : (a : α) → E) (singleton (α := E) ((f : (a : α) → E) a : E)) ∩
        Set.preimage (β := E) (⇑g : (a : α) → E) (singleton (α := E) ((g : (a : α) → E) a : E)))
have e_a : Eq.{u_1 + 1} (α := Set α)
  (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
    (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E)))
  (Set.preimage (β := E) (⇑f : (a : α) → E) (singleton (α := E) ((f : (a : α) → E) a : E)) ∩
    Set.preimage (β := E) (⇑g : (a : α) → E) (singleton (α := E) ((g : (a : α) → E) a : E)))
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
a : α
hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)
eq : ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)
⊢ Eq.{u_1 + 1} (α := Set α)
    (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
      (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E)))
    (Set.preimage (β := E) (⇑f : (a : α) → E) (singleton (α := E) ((f : (a : α) → E) a : E)) ∩
      Set.preimage (β := E) (⇑g : (a : α) → E) (singleton (α := E) ((g : (a : α) → E) a : E)))
have e_a : Eq.{u_1 + 1} (α := Set α)
  (Set.preimage (β := E) (⇑f : (a : α) → E) (singleton (α := E) ((f : (a : α) → E) a : E)) ∩
    Set.preimage (β := E) (⇑g : (a : α) → E) (singleton (α := E) ((g : (a : α) → E) a : E)))
  (Set.preimage (β := E) (⇑f : (a : α) → E) (singleton (α := E) ((f : (a : α) → E) a : E)) ∩
    Set.preimage (β := E) (⇑g : (a : α) → E) (singleton (α := E) ((g : (a : α) → E) a : E)))
Tactic: rw [pair_preimage_singleton f g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
h :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
h_pair : Integrable.{u_2, u_1} (ε := E × E) (⇑(f.pair g) : (a : α) → E × E) μ
a : α
hp : Membership.mem (α := E × E) (f.pair g).range ((f.pair g : (a : α) → E × E) a : E × E)
eq : ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)
⊢ T
      (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
        (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) =
    0
have h_eq : T
    (Set.preimage (β := E × E) (⇑(f.pair g) : (a : α) → E × E)
      (singleton (α := E × E) (((f : (a : α) → E) a, (g : (a : α) → E) a) : E × E))) =
  T
    (Set.preimage (β := E) (⇑f : (a : α) → E) (singleton (α := E) ((f : (a : α) → E) a : E)) ∩
      Set.preimage (β := E) (⇑g : (a : α) → E) (singleton (α := E) ((g : (a : α) → E) a : E)))
Tactic: have h_eq : T ((⇑(f.pair g)) ⁻¹' {(f a, g a)}) = T (f ⁻¹' {f a} ∩ g ⁻¹' {g a}) := by
          congr; rw [pair_preimage_singleton f g]