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
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')
    ((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')
have 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')
Tactic: rw [h_left_eq']
-- 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
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')
    ((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')
have 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')
Tactic: rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
-- 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
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')
⊢ 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')
have neg₁ : ∀ (i : G), MeasurableSet.{u_1} (α := α) (Set.preimage (β := G) (⇑f : (a : α) → G) {i})
Tactic: rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
-- 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
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})
⊢ 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')
have 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∞)
Tactic: rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
-- 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
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∞)
⊢ 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')
have 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})
Tactic: rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
-- 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
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')
    ((∑ 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')
have 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))
Tactic: simp only [sum_apply, ContinuousLinearMap.coe_sum']
-- 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
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))
have 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')
Tactic: refine Finset.sum_congr rfl fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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)}
⊢ 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')
have hx₁ : x ∈ f.range ∧ g x = g ((f : (a : α) → G) a)
Tactic: rw [mem_filter] at hx
Cleared hypotheses: hx
-- 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
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)
⊢ 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')
have 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')
Tactic: rw [hx.2]
-- 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
⊢ 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),
  setToSimpleFunc T (map g f) = ∑ 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)
⊢ 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∞)),
  setToSimpleFunc T (map g f) = ∑ 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]