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
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
inst_4 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x = setToSimpleFunc T f
have refine : ∀ x ∈ f.range,
  ∀ (hx0 : x = 0),
    Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F') (0 : F')
Tactic: refine sum_filter_of_ne fun x _ => mt fun hx0 => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
inst_4 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
h : x ∈ f.range
hx0 : x = 0
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F') (0 : F')
have rw : Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {0}) : (a : F) → F') 0 : F') (0 : F')
Tactic: rw [hx0]
-- 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
⊢ setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have T_empty : T ∅ = 0
Tactic: have T_empty : T ∅ = 0 := h_add.map_empty_eq_zero
-- 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
⊢ setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have hfp : ∀ x ∈ f.range,
  x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' {x}) ≠ ∞ := fun x _ hx0 =>
    (measure_preimage_lt_top_of_integrable f hf hx0).ne
-- 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∞)
⊢ setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x)
have 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))
Tactic: simp only [setToSimpleFunc, range_map]
-- 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∞)
⊢ 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))
have 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')
Tactic: refine Finset.sum_image' _ fun b hb => ?_
-- 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∞)
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')
have 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')
Tactic: rcases mem_range.1 hb with ⟨a, rfl⟩
Cleared hypotheses: b, hb
-- 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)
⊢ 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')
have 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')
Tactic: by_cases h0 : g (f a) = 0
-- 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)
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')
⊢ 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')
have 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')
Tactic: by_cases h0 : g (f a) = 0
-- 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
⊢ 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')
have 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')
Tactic: simp_rw [h0]
-- 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
⊢ 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')
have 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')
Tactic: rw [map_zero, Finset.sum_eq_zero 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
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')
have hx₁ : x ∈ f.range ∧ g x = 0
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
x : G
hx : 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')
have rw : Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') 0 : F') (0 : F')
Tactic: rw [hx.2, map_zero]
-- 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
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')
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : (a : F) → F') (g x) : F') (0 : F')
have rw₁ : Eq.{u_4 + 1} (α := F') 0 0
Tactic: rw [hx.2, map_zero]
-- 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
⊢ 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')
have 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')
Tactic: rw [map_preimage_singleton]
-- 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
⊢ 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')
have 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')
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]
-- 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')
⊢ 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')
have 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')
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')
⊢ 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')
have 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')
Tactic: rw [← Finset.set_biUnion_preimage_singleton]
-- 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')
⊢ 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 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')
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]