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∞)
simp :
  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)

Tactic:
simp only [setToSimpleFunc, range_map]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc, MeasureTheory.SimpleFunc.range_map
-- 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∞)
⊢ 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:
Finset.sum_image' _ fun b hb => ?_

Premises used: Finset.sum_image'
-- 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∞)
refine :
  ∀ (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')
⊢ 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:
refine Finset.sum_image' _ fun b hb => ?_

Premises used: Finset.sum_image'
-- 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∞)
b : G
hb : b ∈ f.range
rcases :
  ∀ (a : α) (hb : Membership.mem (α := G) f.range ((f : (a : α) → G) a : G)),
    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')
      (∑ 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')
⊢ 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:
rcases mem_range.1 hb with ⟨a, rfl⟩

Premises used: MeasureTheory.SimpleFunc.mem_range, Iff.mp, 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)
pos :
  ∀ (h0 : g ((f : (a : α) → G) a) = 0),
    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')
      (∑ 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')
neg :
  ∀ (h0 : ¬g ((f : (a : α) → G) a) = 0),
    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')
      (∑ 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')
⊢ 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')
    (∑ 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:
by_cases h0 : g (f a) = 0

Premises used: DFunLike.coe
-- 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
pos :
  Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {0}) : (a : F) → F') 0 : F')
    (∑ x ∈ f.range with g x = 0, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x) : F')
⊢ 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')
    (∑ 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_rw [h0]
-- 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
rw :
  ∀ (x : G) (hx : x ∈ {x ∈ f.range | g x = 0}),
    Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x) : F') (0 : F')
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑(map g f) : (a : α) → F) {0}) : (a : F) → F') 0 : F')
    (∑ x ∈ f.range with g x = 0, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x) : F')

Tactic:
rw [map_zero, Finset.sum_eq_zero fun x hx => ?_]

Premises used: Finset.sum_eq_zero, map_zero
-- 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
x : G
hx : x ∈ {x ∈ f.range | g x = 0}
⊢ x ∈ f.range ∧ g x = 0

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
x : G
hx : x ∈ f.range ∧ g x = 0
rw : Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') 0 : F') (0 : F')
rw₁ rw₂ : Eq.{u_4 + 1} (α := F') 0 0
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x) : F') (0 : F')

Tactic:
rw [hx.2, map_zero]

Premises used: map_zero, 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
rw rw₁ :
  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 ((⇑f : (a : α) → G) ⁻¹' (↑({b ∈ f.range | g b = g ((f : (a : α) → G) a)}) : Set G)) : (a : F) → F')
        (g ((f : (a : α) → G) a)) :
      F')
⊢ 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')

Tactic:
rw [map_preimage_singleton]

Premises used: MeasureTheory.SimpleFunc.map_preimage_singleton
-- 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
⊢ 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')

Tactic:
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]
-- 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')
neg :
  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')
    (∑ 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')
⊢ 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')
    (∑ 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:
rw [h_left_eq]
-- 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')
rw rw₁ :
  Eq.{u_4 + 1} (α := 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')
    ((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')
    ((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')

Tactic:
rw [← Finset.set_biUnion_preimage_singleton]

Premises used: Finset.set_biUnion_preimage_singleton
-- 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')
⊢ 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')

Tactic:
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]
-- 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')
    ((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')
    (∑ 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')
⊢ 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')
    (∑ 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:
rw [h_left_eq']
-- 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')
    ((∑ 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')
neg₁ : ∀ (i : G), MeasurableSet.{u_1} (α := α) (Set.preimage (β := G) (⇑f : (a : α) → G) {i})
neg₂ :
  ∀ 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∞)
neg₃ :
  ∀ 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})
⊢ Eq.{u_4 + 1} (α := 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')
    (∑ 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:
rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]

Premises used: MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum