awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
rw : x₁ ∈ g ⁻¹' {g x₂}
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)
have rw₁ : x₁ ∈ f ⁻¹' s
Tactic: rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
rw : x₁ ∈ g ⁻¹' {g x₂}
rw₁ : x₁ ∈ f ⁻¹' s
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)
have rw₂ : f x₁ ∈ s
Tactic: rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
rw : x₁ ∈ g ⁻¹' {g x₂}
rw₁ : x₁ ∈ f ⁻¹' s
rw₂ : f x₁ ∈ s
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)
have rw₃ : f x₂ ∈ s
Tactic: rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
rw : x₁ ∈ g ⁻¹' {g x₂}
rw₁ : x₁ ∈ f ⁻¹' s
rw₂ : f x₁ ∈ s
rw₃ : f x₂ ∈ s
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)
have rw₄ : x₂ ∈ f ⁻¹' s
Tactic: rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
rw : x₁ ∈ g ⁻¹' {g x₂}
rw₁ : x₁ ∈ f ⁻¹' s
rw₂ : f x₁ ∈ s
rw₃ : f x₂ ∈ s
rw₄ : x₂ ∈ f ⁻¹' s
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)
have rw₅ : x₂ ∈ g ⁻¹' {g x₂}
Tactic: rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
rw : x₁ ∈ g ⁻¹' {g x₂}
rw₁ : x₁ ∈ f ⁻¹' s
rw₂ : f x₁ ∈ s
rw₃ : f x₂ ∈ s
rw₄ : x₂ ∈ f ⁻¹' s
rw₅ : x₂ ∈ g ⁻¹' {g x₂}
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)
have rw₆ : Membership.mem (γ := Set Z) {g x₂} (g x₂)
Tactic: rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
rw : x₁ ∈ g ⁻¹' {g x₂}
rw₁ : x₁ ∈ f ⁻¹' s
rw₂ : f x₁ ∈ s
rw₃ : f x₂ ∈ s
rw₄ : x₂ ∈ f ⁻¹' s
rw₅ : x₂ ∈ g ⁻¹' {g x₂}
rw₆ : Membership.mem (γ := Set Z) {g x₂} (g x₂)
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)
have rw₇ : g x₂ = g x₂
Tactic: rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : TopologicalSpace Z
inst_1 : PseudoMetrizableSpace Z
inst_2 : T1Space Z
hg : StronglyMeasurable g
⊢ Function.FactorsThrough g f
have this : let this := borel Z;
BorelSpace Z
Tactic: borelize Z
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g₁ g₂ : X → Z
s : Set X
hg₁ : StronglyMeasurable g₁
hg₂ : StronglyMeasurable g₂
hs : MeasurableSet s
h₁ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₁ = h ∘ f
h₂ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₂ = h ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ s.piecewise (β := fun (a : X) ↦ Z) g₁ g₂ = h ∘ f
have pcw : ∀ (t : Set Y) (ht : MeasurableSet t),
  ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) g₁ g₂ = h ∘ f
Tactic: obtain ⟨t, ht, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g₁ g₂ : X → Z
hg₁ : StronglyMeasurable g₁
hg₂ : StronglyMeasurable g₂
h₁ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₁ = h ∘ f
h₂ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₂ = h ∘ f
t : Set Y
ht : MeasurableSet t
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) g₁ g₂ = h ∘ f
have pcw : ∀ (h₁ : Y → Z) (mh₁ : StronglyMeasurable h₁) (hg₁ : StronglyMeasurable (h₁ ∘ f)),
  ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) g₂ = h ∘ f
Tactic: obtain ⟨h₁, mh₁, rfl⟩ := h₁
Cleared hypotheses: g₁, hg₁, h₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g₂ : X → Z
hg₂ : StronglyMeasurable g₂
h₂ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₂ = h ∘ f
t : Set Y
ht : MeasurableSet t
h₁ : Y → Z
mh₁ : StronglyMeasurable h₁
hg₁ : StronglyMeasurable (h₁ ∘ f)
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) g₂ = h ∘ f
have pcw : ∀ (h₂ : Y → Z) (mh₂ : StronglyMeasurable h₂) (hg₂ : StronglyMeasurable (h₂ ∘ f)),
  ∃ (h : Y → Z), StronglyMeasurable h ∧ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f) = h ∘ f
Tactic: obtain ⟨h₂, mh₂, rfl⟩ := h₂
Cleared hypotheses: g₂, hg₂, h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
t : Set Y
ht : MeasurableSet t
h₁ : Y → Z
mh₁ : StronglyMeasurable h₁
hg₁ : StronglyMeasurable (h₁ ∘ f)
h₂ : Y → Z
mh₂ : StronglyMeasurable h₂
hg₂ : StronglyMeasurable (h₂ ∘ f)
⊢ (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f) = t.piecewise (β := fun (a : Y) ↦ Z) h₁ h₂ ∘ f
have rw : (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f) =
  (f ⁻¹' t).piecewise (β := fun (a : X) ↦ Z) (h₁ ∘ f) (h₂ ∘ f)
Tactic: rw [piecewise_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₁ : ∀ (n : ℕ), ∃ (h : Y → Z), StronglyMeasurable h ∧ g n = h ∘ f
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ i = h ∘ f
have lim : ∀ (h : (n : ℕ) → Y → Z) (mh : ∀ (n : ℕ), StronglyMeasurable (h n)) (hh : ∀ (n : ℕ), g n = h n ∘ f),
  ∃ (h : Y → Z), StronglyMeasurable h ∧ i = h ∘ f
Tactic: choose h mh hh using h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
h : (n : ℕ) → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ i = h ∘ f
have lim : i = (fun (y : Y) ↦ limUnder atTop fun (x : ℕ) ↦ h x y) ∘ f
Tactic: refine ⟨fun y ↦ limUnder atTop (h · y), StronglyMeasurable.limUnder mh, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
h : (n : ℕ) → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
⊢ i = (fun (y : Y) ↦ limUnder atTop fun (x : ℕ) ↦ h x y) ∘ f
have lim : ∀ (x : X), i x = ((fun (y : Y) ↦ limUnder atTop fun (x : ℕ) ↦ h x y) ∘ f) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g_1 : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))
h : (n : ℕ) → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
⊢ i x = ((fun (y : Y) ↦ limUnder atTop fun (x : ℕ) ↦ h x y) ∘ f) x
have lim : Tendsto (fun (x_1 : ℕ) ↦ h x_1 (f x)) atTop (𝓝 (i x))
Tactic: rw [Function.comp_apply, Tendsto.limUnder_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
hg : StronglyMeasurable g
mX : MeasurableSpace X := MeasurableSpace.comap f mY
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ g = h ∘ f
have const : ∀ (z : Z), ∃ (h : Y → Z), StronglyMeasurable h ∧ (fun (x : X) ↦ z) = h ∘ f
Tactic: induction g, hg using StronglyMeasurable.induction' with
  | const z => exact ⟨fun _ ↦ z, stronglyMeasurable_const, rfl⟩
  | @pcw g₁ g₂ s hg₁ hg₂ hs h₁ h₂ =>
    obtain ⟨t, ht, rfl⟩ := hs
    obtain ⟨h₁, mh₁, rfl⟩ := h₁
    obtain ⟨h₂, mh₂, rfl⟩ := h₂
    classical
    exact ⟨t.piecewise h₁ h₂, mh₁.piecewise ht mh₂, by rw [piecewise_comp]⟩
  | @lim g i hg hi h₁ h₂ =>
    choose h mh hh using h₁
    refine ⟨fun y ↦ limUnder atTop (h · y), StronglyMeasurable.limUnder mh, ?_⟩
    ext x
    rw [Function.comp_apply, Tendsto.limUnder_eq]
    simp_all
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
hg : StronglyMeasurable g
mX : MeasurableSpace X := MeasurableSpace.comap f mY
const : ∀ (z : Z), ∃ (h : Y → Z), StronglyMeasurable h ∧ (fun (x : X) ↦ z) = h ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ g = h ∘ f
have pcw : ∀ ⦃g₁ g₂ : X → Z⦄ {s : Set X} (hg₁ : StronglyMeasurable g₁) (hg₂ : StronglyMeasurable g₂) (hs : MeasurableSet s)
  (h₁ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₁ = h ∘ f) (h₂ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₂ = h ∘ f),
  ∃ (h : Y → Z), StronglyMeasurable h ∧ s.piecewise (β := fun (a : X) ↦ Z) g₁ g₂ = h ∘ f
Tactic: induction g, hg using StronglyMeasurable.induction' with
  | const z => exact ⟨fun _ ↦ z, stronglyMeasurable_const, rfl⟩
  | @pcw g₁ g₂ s hg₁ hg₂ hs h₁ h₂ =>
    obtain ⟨t, ht, rfl⟩ := hs
    obtain ⟨h₁, mh₁, rfl⟩ := h₁
    obtain ⟨h₂, mh₂, rfl⟩ := h₂
    classical
    exact ⟨t.piecewise h₁ h₂, mh₁.piecewise ht mh₂, by rw [piecewise_comp]⟩
  | @lim g i hg hi h₁ h₂ =>
    choose h mh hh using h₁
    refine ⟨fun y ↦ limUnder atTop (h · y), StronglyMeasurable.limUnder mh, ?_⟩
    ext x
    rw [Function.comp_apply, Tendsto.limUnder_eq]
    simp_all
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : TopologicalSpace Z
inst_2 : IsCompletelyMetrizableSpace Z
hg : StronglyMeasurable g
mX : MeasurableSpace X := MeasurableSpace.comap f mY
const : ∀ (z : Z), ∃ (h : Y → Z), StronglyMeasurable h ∧ (fun (x : X) ↦ z) = h ∘ f
pcw :
  ∀ ⦃g₁ g₂ : X → Z⦄ {s : Set X} (hg₁ : StronglyMeasurable g₁) (hg₂ : StronglyMeasurable g₂) (hs : MeasurableSet s)
    (h₁ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₁ = h ∘ f) (h₂ : ∃ (h : Y → Z), StronglyMeasurable h ∧ g₂ = h ∘ f),
    ∃ (h : Y → Z), StronglyMeasurable h ∧ s.piecewise (β := fun (a : X) ↦ Z) g₁ g₂ = h ∘ f
⊢ ∃ (h : Y → Z), StronglyMeasurable h ∧ g = h ∘ f
have lim : ∀ ⦃g : ℕ → X → Z⦄ ⦃i : X → Z⦄ (hg : ∀ (n : ℕ), StronglyMeasurable (g n)) (hi : StronglyMeasurable i)
  (h₁ : ∀ (n : ℕ), ∃ (h : Y → Z), StronglyMeasurable h ∧ g n = h ∘ f)
  (h₂ : ∀ (x : X), Tendsto (fun (x_1 : ℕ) ↦ g x_1 x) atTop (𝓝 (i x))), ∃ (h : Y → Z), StronglyMeasurable h ∧ i = h ∘ f
Tactic: induction g, hg using StronglyMeasurable.induction' with
  | const z => exact ⟨fun _ ↦ z, stronglyMeasurable_const, rfl⟩
  | @pcw g₁ g₂ s hg₁ hg₂ hs h₁ h₂ =>
    obtain ⟨t, ht, rfl⟩ := hs
    obtain ⟨h₁, mh₁, rfl⟩ := h₁
    obtain ⟨h₂, mh₂, rfl⟩ := h₂
    classical
    exact ⟨t.piecewise h₁ h₂, mh₁.piecewise ht mh₂, by rw [piecewise_comp]⟩
  | @lim g i hg hi h₁ h₂ =>
    choose h mh hh using h₁
    refine ⟨fun y ↦ limUnder atTop (h · y), StronglyMeasurable.limUnder mh, ?_⟩
    ext x
    rw [Function.comp_apply, Tendsto.limUnder_eq]
    simp_all
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : Nonempty Z
inst_1 : MeasurableSpace Z
inst_2 : StandardBorelSpace Z
hg : Measurable g
this : UpgradedStandardBorel Z := upgradeStandardBorel Z
⊢ ∃ (h : Y → Z), Measurable h ∧ g = h ∘ f
have obtain : ∀ (h : Y → Z) (mh : StronglyMeasurable h) (hh : g = h ∘ f), ∃ (h : Y → Z), Measurable h ∧ g = h ∘ f
Tactic: obtain ⟨h, mh, hh⟩ := hg.stronglyMeasurable.exists_eq_measurable_comp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Floor (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : IsStrictOrderedRing R
inst_7 : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (Int.fract ⁻¹' s)
have rw : MeasurableSet.{u_2} (α := R) (⋃ (m : ℤ), (fun (x : R) ↦ x - (↑m : R)) ⁻¹' (s ∩ Ico 0 1))
Tactic: rw [Int.preimage_fract]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Floor (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : IsStrictOrderedRing R
inst_7 : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (Int.fract '' s)
have simp : MeasurableSet.{u_2} (α := R) (⋃ (m : ℤ), (fun (x : R) ↦ x + (↑m : R)) ⁻¹' s ∩ Ico 0 1)
Tactic: simp only [Int.image_fract, sub_eq_add_neg, image_add_right']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Floor (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
inst_7 : IsStrictOrderedRing R
n : R
⊢ MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})
have inl : ∀ (h : ⌊n⌋₊ = 0), MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})
Tactic: rcases eq_or_ne ⌊n⌋₊ 0 with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Floor (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
inst_7 : IsStrictOrderedRing R
n : R
inl : ∀ (h : ⌊n⌋₊ = 0), MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})
⊢ MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})
have inr : ∀ (h : ⌊n⌋₊ ≠ 0), MeasurableSet.{u_2} (α := R) (floor ⁻¹' {⌊n⌋₊})
Tactic: rcases eq_or_ne ⌊n⌋₊ 0 with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Floor (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
n : R
⊢ MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})
have inl : ∀ (h : ⌈n⌉₊ = 0), MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})
Tactic: rcases eq_or_ne ⌈n⌉₊ 0 with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Floor (goal)
Goal:
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : TopologicalSpace R
inst_4 : OrderTopology R
inst_5 : MeasurableSpace R
inst_6 : OpensMeasurableSpace R
n : R
inl : ∀ (h : ⌈n⌉₊ = 0), MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})
⊢ MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})
have inr : ∀ (h : ⌈n⌉₊ ≠ 0), MeasurableSet.{u_2} (α := R) (ceil ⁻¹' {⌈n⌉₊})
Tactic: rcases eq_or_ne ⌈n⌉₊ 0 with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ (↑(↑(holder r B f g) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] fun (x : α) ↦
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑g : α →ₘ[μ] F) : α → F) x)
have rw : (↑(↑(MemLp.toLp
            (fun (x : α) ↦
              (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
                ((↑(↑g : α →ₘ[μ] F) : α → F) x))
            sorry) :
        α →ₘ[μ] G) :
    α → G) =ᶠ[ae μ]
  fun (x : α) ↦
  (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
    ((↑(↑g : α →ₘ[μ] F) : α → F) x)
Tactic: rw [holder]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ ‖holder r B f g‖₊ ≤ ‖B‖₊ * ‖f‖₊ * ‖g‖₊
have simp_rw : eLpNorm (↑(↑(holder r B f g) : α →ₘ[μ] G) : α → G) r μ ≤
  ‖B‖ₑ * eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ * eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) q μ
Tactic: simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_mul, ← enorm_eq_nnnorm, Lp.enorm_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ eLpNorm (↑(↑(holder r B f g) : α →ₘ[μ] G) : α → G) r μ ≤
    ‖B‖ₑ * eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ * eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) q μ
have apply : eLpNorm.{u_1, u_5} (ε := G)
    (fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x))
    r μ ≤
  ‖B‖ₑ * eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) p μ * eLpNorm (↑(↑g : α →ₘ[μ] F) : α → F) q μ
Tactic: apply eLpNorm_congr_ae (coeFn_holder B f g) |>.trans_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ holder r B (f₁ + f₂) g = holder r B f₁ g + holder r B f₂ g
have simp : MemLp.toLp
    (fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑(f₁ + f₂) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x))
    sorry =
  MemLp.toLp
    (HAdd.hAdd (α := α → G)
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₁ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₂ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x))
    sorry
Tactic: simp only [holder, ← MemLp.toLp_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Holder (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ MemLp.toLp
      (fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑(f₁ + f₂) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      ⋯ =
    MemLp.toLp
      (HAdd.hAdd (α := α → G)
        (fun (x : α) ↦
          (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₁ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
            ((↑(↑g : α →ₘ[μ] F) : α → F) x))
        fun (x : α) ↦
        (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₂ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
          ((↑(↑g : α →ₘ[μ] F) : α → F) x))
      ⋯
have hfg : (fun (x : α) ↦
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑(f₁ + f₂) : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑g : α →ₘ[μ] F) : α → F) x)) =ᶠ[ae μ]
  HAdd.hAdd (α := α → G)
    (fun (x : α) ↦
      (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₁ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
        ((↑(↑g : α →ₘ[μ] F) : α → F) x))
    fun (x : α) ↦
    (((B : (a : E) → F →L[𝕜] G) ((↑(↑f₂ : α →ₘ[μ] E) : α → E) x) : F →L[𝕜] G) : (a : F) → G)
      ((↑(↑g : α →ₘ[μ] F) : α → F) x)
Tactic: apply MemLp.toLp_congr