awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
T_empty : T ∅ = 0
hfp :
  ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)
h0 : ¬g ((f : (a : α) → G) a) = 0
h_left_eq :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
h_left_eq' :
  Eq.{u_4 + 1} (α := F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
neg :
  Eq.{u_4 + 1} (α := F')
    (∑ c ∈ f.range with g c = g ((f : (a : α) → G) a),
      (T (Set.preimage (β := G) (⇑f : (a : α) → G) {c}) : (a : F) → F') (g ((f : (a : α) → G) a)))
    (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
      (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j))
⊢ Eq.{u_4 + 1} (α := F')
    ((∑ i ∈ f.range with g i = g ((f : (a : α) → G) a), T (Set.preimage (β := G) (⇑f : (a : α) → G) {i}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
        (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j) :
      F')

Tactic:
simp only [sum_apply, ContinuousLinearMap.coe_sum']

Premises used: Finset.sum_apply, ContinuousLinearMap.coe_sum'
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
T_empty : T ∅ = 0
hfp :
  ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)
h0 : ¬g ((f : (a : α) → G) a) = 0
h_left_eq :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
h_left_eq' :
  Eq.{u_4 + 1} (α := F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
⊢ Eq.{u_4 + 1} (α := F')
    (∑ c ∈ f.range with g c = g ((f : (a : α) → G) a),
      (T (Set.preimage (β := G) (⇑f : (a : α) → G) {c}) : (a : F) → F') (g ((f : (a : α) → G) a)))
    (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
      (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j))

Tactic:
Finset.sum_congr rfl fun x hx => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
T_empty : T ∅ = 0
hfp :
  ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)
h0 : ¬g ((f : (a : α) → G) a) = 0
h_left_eq :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
h_left_eq' :
  Eq.{u_4 + 1} (α := F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
neg :
  ∀ (x : G) (hx : x ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}),
    Eq.{u_4 + 1} (α := F')
      ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g ((f : (a : α) → G) a)) : F')
      ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x) : F')
⊢ Eq.{u_4 + 1} (α := F')
    (∑ c ∈ f.range with g c = g ((f : (a : α) → G) a),
      (T (Set.preimage (β := G) (⇑f : (a : α) → G) {c}) : (a : F) → F') (g ((f : (a : α) → G) a)))
    (∑ j ∈ f.range with g j = g ((f : (a : α) → G) a),
      (T (Set.preimage (β := G) (⇑f : (a : α) → G) {j}) : (a : F) → F') (g j))

Tactic:
refine Finset.sum_congr rfl fun x hx => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
T_empty : T ∅ = 0
hfp :
  ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)
h0 : ¬g ((f : (a : α) → G) a) = 0
h_left_eq :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
h_left_eq' :
  Eq.{u_4 + 1} (α := F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
x : G
hx : x ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}
⊢ x ∈ f.range ∧ g x = g ((f : (a : α) → G) a)

Tactic:
rw [mem_filter] at hx

Premises used: Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
T_empty : T ∅ = 0
hfp :
  ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)
h0 : ¬g ((f : (a : α) → G) a) = 0
h_left_eq :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
h_left_eq' :
  Eq.{u_4 + 1} (α := F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
x : G
hx : x ∈ f.range ∧ g x = g ((f : (a : α) → G) a)
neg neg₁ :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g ((f : (a : α) → G) a)) : F')
    ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g ((f : (a : α) → G) a)) : F')
⊢ Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g ((f : (a : α) → G) a)) : F')
    ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x) : F')

Tactic:
rw [hx.2]

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
T_empty : T ∅ = 0
hfp :
  ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)
h0 : ¬g ((f : (a : α) → G) a) = 0
h_left_eq :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
h_left_eq' :
  Eq.{u_4 + 1} (α := F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
⊢ ∀ (i : G), MeasurableSet.{u_1} (α := α) (Set.preimage (β := G) (⇑f : (a : α) → G) {i})

Tactic:
fun i => measurableSet_fiber _ _

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
T_empty : T ∅ = 0
hfp :
  ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)
h0 : ¬g ((f : (a : α) → G) a) = 0
h_left_eq :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
h_left_eq' :
  Eq.{u_4 + 1} (α := F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
⊢ ∀ (i : G), MeasurableSet.{u_1} (α := α) (Set.preimage (β := G) (⇑f : (a : α) → G) {i})

Tactic:
exact fun i => measurableSet_fiber _ _

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
T_empty : T ∅ = 0
hfp :
  ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)
h0 : ¬g ((f : (a : α) → G) a) = 0
h_left_eq :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
h_left_eq' :
  Eq.{u_4 + 1} (α := F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
⊢ ∀ i ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {i}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
T_empty : T ∅ = 0
hfp :
  ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)
h0 : ¬g ((f : (a : α) → G) a) = 0
h_left_eq :
  Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {g ((f : (a : α) → G) a)}) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
h_left_eq' :
  Eq.{u_4 + 1} (α := F')
    ((T ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
    ((T (⋃ y ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)}, Set.preimage (β := G) (⇑f : (a : α) → G) {y}) :
          (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
⊢ ∀ i ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)},
    ∀ j ∈ {b ∈ f.range | g b = g ((f : (a : α) → G) a)},
      i ≠ j →
        Disjoint.{u_1} (α := Set α) (Set.preimage (β := G) (⇑f : (a : α) → G) {i})
          (Set.preimage (β := G) (⇑f : (a : α) → G) {j})

Tactic:
grind [Set.disjoint_iff]

Premises used: Set.disjoint_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_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
⊢ 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
-- 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) μ
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))
⊢ setToSimpleFunc T (map Prod.fst (f.pair g)) = setToSimpleFunc T (map Prod.snd (f.pair g))

Tactic:
rw [map_setToSimpleFunc T h_add h_pair Prod.fst_zero]

Premises used: Prod.fst_zero, MeasureTheory.SimpleFunc.map_setToSimpleFunc
-- 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) μ
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)
⊢ ∑ 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.snd_zero]

Premises used: MeasureTheory.SimpleFunc.map_setToSimpleFunc, Prod.snd_zero
-- 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) μ
⊢ 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:
Finset.sum_congr rfl fun p hp => ?_

Premises used: Finset.sum_congr, rfl
-- 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) μ
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)
⊢ 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:
refine Finset.sum_congr rfl fun p hp => ?_

Premises used: Finset.sum_congr, rfl
-- 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) μ
p : E × E
hp : p ∈ (f.pair g).range
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)
⊢ 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:
rcases mem_range.1 hp with ⟨a, rfl⟩

Premises used: MeasureTheory.SimpleFunc.mem_range, Iff.mp, rfl