awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C
⊢ ⋃ (i : ℕ), ⋃ (_ : i ≤ n + 1), s i ∈ C
have succ : (⋃ (k : ℕ), ⋃ (_ : k ≤ n), s k) ∪ s (n + 1) ∈ C
Tactic: rw [biUnion_le_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
⊢ ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C
have zero : ⋃ (i : ℕ), ⋃ (_ : i ≤ 0), s i ∈ C
Tactic: induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [biUnion_le_succ]; exact hC.union_mem hn (hs _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
zero : ⋃ (i : ℕ), ⋃ (_ : i ≤ 0), s i ∈ C
⊢ ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C
have succ : ∀ (n : ℕ) (hn : ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C), ⋃ (i : ℕ), ⋃ (_ : i ≤ n + 1), s i ∈ C
Tactic: induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [biUnion_le_succ]; exact hC.union_mem hn (hs _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C
⊢ ⋂ (i : ℕ), ⋂ (_ : i ≤ n + 1), s i ∈ C
have succ : (⋂ (k : ℕ), ⋂ (_ : k ≤ n), s k) ∩ s (n + 1) ∈ C
Tactic: rw [biInter_le_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
⊢ ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C
have zero : ⋂ (i : ℕ), ⋂ (_ : i ≤ 0), s i ∈ C
Tactic: induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [biInter_le_succ]; exact hC.inter_mem hn (hs _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
zero : ⋂ (i : ℕ), ⋂ (_ : i ≤ 0), s i ∈ C
⊢ ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C
have succ : ∀ (n : ℕ) (hn : ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C), ⋂ (i : ℕ), ⋂ (_ : i ≤ n + 1), s i ∈ C
Tactic: induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [biInter_le_succ]; exact hC.inter_mem hn (hs _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : accumulate s n ∈ C
⊢ accumulate s (n + 1) ∈ C
have succ : accumulate s n ∪ s (n + 1) ∈ C
Tactic: rw [accumulate_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
⊢ accumulate s n ∈ C
have zero : accumulate s 0 ∈ C
Tactic: induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [accumulate_succ]; exact hC.union_mem hn (hs _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.SetSemiring (goal)
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
zero : accumulate s 0 ∈ C
⊢ accumulate s n ∈ C
have succ : ∀ (n : ℕ) (hn : accumulate s n ∈ C), accumulate s (n + 1) ∈ C
Tactic: induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [accumulate_succ]; exact hC.union_mem hn (hs _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
⊢ HasFiniteIntegral f μ
have inl : ∀ (h : IsEmpty Y), HasFiniteIntegral f μ
Tactic: rcases isEmpty_or_nonempty Y with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
inl : ∀ (h : IsEmpty Y), HasFiniteIntegral f μ
⊢ HasFiniteIntegral f μ
have inr : ∀ (h : Nonempty Y), HasFiniteIntegral f μ
Tactic: rcases isEmpty_or_nonempty Y with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
⊢ 0 ≤ᶠ[ae μ] bound
have h₁ : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X |
      Membership.mem (γ := Set X)
          {x : X | (fun (x : X) ↦ ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x) x} x →
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ 0 x ≤ bound x) x} x}
    a
Tactic: filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x h.some)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
h₁ :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X)
            {x : X | (fun (x : X) ↦ ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ 0 x ≤ bound x) x} x}
      a
⊢ 0 ≤ᶠ[ae μ] bound
have h₂ : ∀ (a : X), (∀ (y : Y), norm.{u_3} (E := E) ((f a : (a : Y) → E) y : E) ≤ bound a) → 0 a ≤ bound a
Tactic: filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x h.some)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
⊢ HasFiniteIntegral f μ
have bound_nonneg : 0 ≤ᶠ[ae μ] bound
Tactic: have bound_nonneg : 0 ≤ᵐ[μ] bound := by
      filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x h.some)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᶠ[ae μ] bound
⊢ HasFiniteIntegral f μ
have inr : ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a
Tactic: refine .mono' bound_int ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h : Nonempty Y
bound_nonneg : 0 ≤ᶠ[ae μ] bound
⊢ ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a
have h₁ : ∀ (x : X) (bound_ge_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x)
  (bound_nonneg_x : 0 x ≤ bound x), ‖f x‖ ≤ bound x
Tactic: filter_upwards [bound_ge, bound_nonneg] with x bound_ge_x bound_nonneg_x
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (ε := C(Y, E)) (fun (x : X) ↦ mkD (f x) g) μ
have refine : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
Tactic: refine hasFiniteIntegral_of_bound _ bound bound_int ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
f : X → Y → E
g : C(Y, E)
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
have h : ∀ (x : X) (bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x) (cont_x : Continuous (f x)) (y : Y),
  norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
Tactic: filter_upwards [bound_ge, f_ae_cont] with x bound_ge_x cont_x
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set Y
inst_3 : CompactSpace.{u_2} (↑s : Type u_2)
f : X → Y → E
g : ContinuousMap.{u_2, u_3} (↑s : Type u_2) E
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (ε := ContinuousMap.{u_2, u_3} (↑s : Type u_2) E)
    (fun (x : X) ↦ mkD (s.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ
have refine_1 : ∀ᵐ (x : X) ∂μ, Continuous (s.restrict (π := fun (a : Y) ↦ E) (f x))
Tactic: refine hasFiniteIntegral_mkD_of_bound _ _ ?_ bound bound_int ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set Y
inst_3 : CompactSpace.{u_2} (↑s : Type u_2)
f : X → Y → E
g : ContinuousMap.{u_2, u_3} (↑s : Type u_2) E
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
refine_1 : ∀ᵐ (x : X) ∂μ, Continuous (s.restrict (π := fun (a : Y) ↦ E) (f x))
⊢ HasFiniteIntegral (ε := ContinuousMap.{u_2, u_3} (↑s : Type u_2) E)
    (fun (x : X) ↦ mkD (s.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ
have refine_2 : ∀ᵐ (x : X) ∂μ, ∀ (y : (↑s : Type u_2)), ‖s.restrict (π := fun (a : Y) ↦ E) (f x) y‖ ≤ bound x
Tactic: refine hasFiniteIntegral_mkD_of_bound _ _ ?_ bound bound_int ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
⊢ 0 ≤ᶠ[ae μ] bound
have h : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X |
      Membership.mem (γ := Set X)
          {x : X | (fun (x : X) ↦ ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x) x} x →
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ 0 x ≤ bound x) x} x}
    a
Tactic: filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X)
            {x : X | (fun (x : X) ↦ ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ 0 x ≤ bound x) x} x}
      a
⊢ 0 ≤ᶠ[ae μ] bound
have h₁ : ∀ (a : X), (∀ (y : Y), norm.{u_3} (E := E) ((f a : (a : Y) → E) y : E) ≤ bound a) → 0 a ≤ bound a
Tactic: filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
⊢ HasFiniteIntegral f μ
have bound_nonneg : 0 ≤ᶠ[ae μ] bound
Tactic: have bound_nonneg : 0 ≤ᵐ[μ] bound := by
    filter_upwards [bound_ge] with x bound_x using le_trans (norm_nonneg _) (bound_x 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg : 0 ≤ᶠ[ae μ] bound
⊢ HasFiniteIntegral f μ
have refine : ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a
Tactic: refine .mono' bound_int ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x
bound_nonneg : 0 ≤ᶠ[ae μ] bound
⊢ ∀ᵐ (a : X) ∂μ, ‖f a‖ ≤ bound a
have h : ∀ (x : X) (bound_ge_x : ∀ (y : Y), norm.{u_3} (E := E) ((f x : (a : Y) → E) y : E) ≤ bound x)
  (bound_nonneg_x : 0 x ≤ bound x), ‖f x‖ ≤ bound x
Tactic: filter_upwards [bound_ge, bound_nonneg] with x bound_ge_x bound_nonneg_x
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (ε := C(Y, E)₀) (fun (x : X) ↦ mkD (f x) g) μ
have refine : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
Tactic: refine hasFiniteIntegral_of_bound _ bound bound_int ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
f : X → Y → E
g : C(Y, E)₀
f_ae_cont : ∀ᵐ (x : X) ∂μ, Continuous (f x)
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x
⊢ ∀ᵐ (x : X) ∂μ, ∀ (y : Y), norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
have h : ∀ (x : X) (bound_ge_x : ∀ (y : Y), ‖f x y‖ ≤ bound x) (cont_x : Continuous (f x)) (zero_x : f x 0 = 0) (y : Y),
  norm.{u_3} (E := E) ((mkD (f x) g : (a : Y) → E) y : E) ≤ bound x
Tactic: filter_upwards [bound_ge, f_ae_cont, f_ae_zero] with x bound_ge_x cont_x zero_x
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set Y
inst_3 : CompactSpace.{u_2} (↑s : Type u_2)
inst_4 : Zero (↑s : Type u_2)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑s : Type u_2) E
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
⊢ HasFiniteIntegral (ε := ContinuousMapZero.{u_2, u_3} (↑s : Type u_2) E)
    (fun (x : X) ↦ mkD (s.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ
have refine_1 : ∀ᵐ (x : X) ∂μ, Continuous (s.restrict (π := fun (a : Y) ↦ E) (f x))
Tactic: refine hasFiniteIntegral_mkD_of_bound _ _ ?_ f_ae_zero bound bound_int ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
s : Set Y
inst_3 : CompactSpace.{u_2} (↑s : Type u_2)
inst_4 : Zero (↑s : Type u_2)
f : X → Y → E
g : ContinuousMapZero.{u_2, u_3} (↑s : Type u_2) E
f_ae_contOn : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s
f_ae_zero : ∀ᵐ (x : X) ∂μ, f x (↑0 : Y) = 0
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x
refine_1 : ∀ᵐ (x : X) ∂μ, Continuous (s.restrict (π := fun (a : Y) ↦ E) (f x))
⊢ HasFiniteIntegral (ε := ContinuousMapZero.{u_2, u_3} (↑s : Type u_2) E)
    (fun (x : X) ↦ mkD (s.restrict (π := fun (a : Y) ↦ E) (f x)) g) μ
have refine_2 : ∀ᵐ (x : X) ∂μ, ∀ (y : (↑s : Type u_2)), ‖s.restrict (π := fun (a : Y) ↦ E) (f x) y‖ ≤ bound x
Tactic: refine hasFiniteIntegral_mkD_of_bound _ _ ?_ f_ae_zero bound bound_int ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
⊢ AEStronglyMeasurable (β := C(Y, E)₀) (fun (x : X) ↦ mkD (f x) g) μ
have rw : AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) μ
Tactic: rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
⊢ AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) μ
have refine : (ae μ).EventuallyEq (β := C(Y, E)) (fun (x : X) ↦ ContinuousMap.mkD (f x) (↑g : C(Y, E))) fun (x : X) ↦
  (↑(mkD (f x) g) : C(Y, E))
Tactic: refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry f g f_cont
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
⊢ (ae μ).EventuallyEq (β := C(Y, E)) (fun (x : X) ↦ ContinuousMap.mkD (f x) (↑g : C(Y, E))) fun (x : X) ↦
    (↑(mkD (f x) g) : C(Y, E))
have h : ∀ (x : X) (zero_x : f x 0 = 0), Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (↑(mkD (f x) g) : C(Y, E))
Tactic: filter_upwards [f_zero] with x zero_x
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
f : X → Y → E
g : C(Y, E)₀
f_cont : Continuous (Function.uncurry f)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
x : X
zero_x : f x 0 = 0
⊢ Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (↑(mkD (f x) g) : C(Y, E))
have h : Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (ContinuousMap.mkD (f x) (↑g : C(Y, E)))
Tactic: rw [mkD_eq_mkD_of_map_zero _ _ zero_x]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
s : Set X
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set Y) s univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
⊢ AEStronglyMeasurable (β := C(Y, E)₀) (fun (x : X) ↦ mkD (f x) g) (μ.restrict s)
have rw : AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) (μ.restrict s)
Tactic: rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
s : Set X
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set Y) s univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
⊢ AEStronglyMeasurable (β := C(Y, E)) (fun (x : X) ↦ (↑(mkD (f x) g) : C(Y, E))) (μ.restrict s)
have refine : (ae (μ.restrict s)).EventuallyEq (β := C(Y, E)) (fun (x : X) ↦ ContinuousMap.mkD (f x) (↑g : C(Y, E))) fun (x : X) ↦
  (↑(mkD (f x) g) : C(Y, E))
Tactic: refine aestronglyMeasurable_congr ?_ |>.mp <|
    ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry hs f g f_cont
-- Lean 4 proof step from Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : TopologicalSpace Y
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : CompactSpace Y
inst_4 : Zero Y
s : Set X
inst_5 : TopologicalSpace X
inst_6 : OpensMeasurableSpace X
inst_7 : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set Y) s univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
⊢ (ae (μ.restrict s)).EventuallyEq (β := C(Y, E)) (fun (x : X) ↦ ContinuousMap.mkD (f x) (↑g : C(Y, E))) fun (x : X) ↦
    (↑(mkD (f x) g) : C(Y, E))
have h : ∀ (x : X) (zero_x : f x 0 = 0), Eq (α := C(Y, E)) (ContinuousMap.mkD (f x) (↑g : C(Y, E))) (↑(mkD (f x) g) : C(Y, E))
Tactic: filter_upwards [f_zero] with x zero_x