awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
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)
⊢ 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

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
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)
⊢ 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:
dsimp only [pair_apply]

Premises used: MeasureTheory.SimpleFunc.pair_apply
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
pos 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)
⊢ 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:
rw [eq]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
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)))
⊢ 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:
congr
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
e_a 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)))
⊢ 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:
rw [pair_preimage_singleton f g]

Premises used: MeasureTheory.SimpleFunc.pair_preimage_singleton
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)))

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]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
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)))
rw :
  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))) =
    0
⊢ 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

Tactic:
rw [h_eq]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
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)))
⊢ 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))) =
    0

Tactic:
h eq
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
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)))
⊢ 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))) =
    0

Tactic:
exact h eq
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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

Tactic:
have : T (pair f g ⁻¹' {(f a, g a)}) = 0 := by
        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]
        rw [h_eq]
        exact h eq
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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)
this :
  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
⊢ 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:
simp only [this, ContinuousLinearMap.zero_apply, pair_apply]

Premises used: MeasureTheory.SimpleFunc.pair_apply, ContinuousLinearMap.zero_apply
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
⊢ setToSimpleFunc T f = setToSimpleFunc T g

Tactic:
setToSimpleFunc_congr' T h_add hf ((integrable_congr h).mp hf) ?_

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_congr', MeasureTheory.integrable_congr, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
refine :
  Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0
⊢ setToSimpleFunc T f = setToSimpleFunc T g

Tactic:
refine setToSimpleFunc_congr' T h_add hf ((integrable_congr h).mp hf) ?_

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_congr', MeasureTheory.integrable_congr, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
⊢ Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0

Tactic:
fun x y hxy => h_zero _ ((measurableSet_fiber f x).inter (measurableSet_fiber g y)) ?_

Premises used: Inter.inter, Set.preimage, Pairwise, MeasureTheory.SimpleFunc.measurableSet_fiber, Singleton.singleton, DFunLike.coe, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
refine :
  ∀ (x y : E) (hxy : x ≠ y),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Pairwise fun (x y : E) ↦
    T (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) = 0

Tactic:
refine fun x y hxy => h_zero _ ((measurableSet_fiber f x).inter (measurableSet_fiber g y)) ?_

Premises used: Inter.inter, Set.preimage, MeasureTheory.SimpleFunc.measurableSet_fiber, Singleton.singleton, DFunLike.coe, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
x y : E
hxy : x ≠ y
rw :
  ∀
    (h :
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} :
          ℝ≥0∞)
        (0 : ℝ≥0∞))
    (x y : E) (hxy : x ≠ y),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [EventuallyEq, ae_iff] at h

Premises used: Filter.EventuallyEq, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬Eq.{u_2 + 1} (α := E) ((f : (a : α) → E) a : E) ((g : (a : α) → E) a : E)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
x y : E
hxy : x ≠ y
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := E) (⇑f : (a : α) → E) {x} ∩ Set.preimage (β := E) (⇑g : (a : α) → E) {y}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
measure_mono_null (fun z => ?_) h

Premises used: MeasureTheory.measure_mono_null