awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑g : α → β) a ≤ (↑(f ⊔ g) : α → β) a
have h : (↑g : α → β) a ≤ (↑f : α → β) a ⊔ (↑g : α → β) a
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : f ≤ f'
hg : g ≤ f'
⊢ f ⊔ g ≤ f'
have rw : ∀ (hf : (↑f : α → β) ≤ᶠ[ae μ] (↑f' : α → β)) (hg : (↑g : α → β) ≤ᶠ[ae μ] (↑f' : α → β)),
  (↑(f ⊔ g) : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
Tactic: rw [← coeFn_le] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : (↑f : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
hg : (↑g : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
⊢ (↑(f ⊔ g) : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
have h : ∀ (a : α) (haf : (↑f : α → β) a ≤ (↑f' : α → β) a) (hag : (↑g : α → β) a ≤ (↑f' : α → β) a)
  (ha_sup : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a), (↑(f ⊔ g) : α → β) a ≤ (↑f' : α → β) a
Tactic: filter_upwards [hf, hg, coeFn_sup f g] with _ haf hag ha_sup
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : (↑f : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
hg : (↑g : α → β) ≤ᶠ[ae μ] (↑f' : α → β)
a : α
haf : (↑f : α → β) a ≤ (↑f' : α → β) a
hag : (↑g : α → β) a ≤ (↑f' : α → β) a
ha_sup : (↑(f ⊔ g) : α → β) a = (↑f : α → β) a ⊔ (↑g : α → β) a
⊢ (↑(f ⊔ g) : α → β) a ≤ (↑f' : α → β) a
have h : (↑f : α → β) a ⊔ (↑g : α → β) a ≤ (↑f' : α → β) a
Tactic: rw [ha_sup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
⊢ f ⊓ g ≤ f
have rw : (↑(f ⊓ g) : α → β) ≤ᶠ[ae μ] (↑f : α → β)
Tactic: rw [← coeFn_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
⊢ (↑(f ⊓ g) : α → β) ≤ᶠ[ae μ] (↑f : α → β)
have h : ∀ (a : α) (ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a), (↑(f ⊓ g) : α → β) a ≤ (↑f : α → β) a
Tactic: filter_upwards [coeFn_inf f g] with _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑(f ⊓ g) : α → β) a ≤ (↑f : α → β) a
have h : (↑f : α → β) a ⊓ (↑g : α → β) a ≤ (↑f : α → β) a
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
⊢ f ⊓ g ≤ g
have rw : (↑(f ⊓ g) : α → β) ≤ᶠ[ae μ] (↑g : α → β)
Tactic: rw [← coeFn_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
⊢ (↑(f ⊓ g) : α → β) ≤ᶠ[ae μ] (↑g : α → β)
have h : ∀ (a : α) (ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a), (↑(f ⊓ g) : α → β) a ≤ (↑g : α → β) a
Tactic: filter_upwards [coeFn_inf f g] with _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : α →ₘ[μ] β
a : α
ha : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑(f ⊓ g) : α → β) a ≤ (↑g : α → β) a
have h : (↑f : α → β) a ⊓ (↑g : α → β) a ≤ (↑g : α → β) a
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : f' ≤ f
hg : f' ≤ g
⊢ f' ≤ f ⊓ g
have rw : ∀ (hf : (↑f' : α → β) ≤ᶠ[ae μ] (↑f : α → β)) (hg : (↑f' : α → β) ≤ᶠ[ae μ] (↑g : α → β)),
  (↑f' : α → β) ≤ᶠ[ae μ] (↑(f ⊓ g) : α → β)
Tactic: rw [← coeFn_le] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : (↑f' : α → β) ≤ᶠ[ae μ] (↑f : α → β)
hg : (↑f' : α → β) ≤ᶠ[ae μ] (↑g : α → β)
⊢ (↑f' : α → β) ≤ᶠ[ae μ] (↑(f ⊓ g) : α → β)
have h : ∀ (a : α) (haf : (↑f' : α → β) a ≤ (↑f : α → β) a) (hag : (↑f' : α → β) a ≤ (↑g : α → β) a)
  (ha_inf : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a), (↑f' : α → β) a ≤ (↑(f ⊓ g) : α → β) a
Tactic: filter_upwards [hf, hg, coeFn_inf f g] with _ haf hag ha_inf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : (↑f' : α → β) ≤ᶠ[ae μ] (↑f : α → β)
hg : (↑f' : α → β) ≤ᶠ[ae μ] (↑g : α → β)
a : α
haf : (↑f' : α → β) a ≤ (↑f : α → β) a
hag : (↑f' : α → β) a ≤ (↑g : α → β) a
ha_inf : (↑(f ⊓ g) : α → β) a = (↑f : α → β) a ⊓ (↑g : α → β) a
⊢ (↑f' : α → β) a ≤ (↑(f ⊓ g) : α → β) a
have h : (↑f' : α → β) a ≤ (↑f : α → β) a ⊓ (↑g : α → β) a
Tactic: rw [ha_inf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
⊢ (↑(const α b) : α → β) x = b
have simp : (if h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) sorry) then
      Function.const α
        (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) sorry)) h)
    else AEStronglyMeasurable.mk (m := inst) (μ := μ) (↑(Quotient.out (const α b)) : α → β) sorry)
    x =
  b
Tactic: simp only [cast]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
⊢ (if h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯) then
        Function.const α
          (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h)
      else AEStronglyMeasurable.mk (m := inst) (μ := μ) (↑(Quotient.out (const α b)) : α → β) ⋯)
      x =
    b
have pos : ∀ (h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) sorry)),
  Function.const α (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) sorry)) h)
      x =
    b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
pos :
  ∀ (h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)),
    Function.const α
        (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h) x =
      b
⊢ (if h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯) then
        Function.const α
          (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h)
      else AEStronglyMeasurable.mk (m := inst) (μ := μ) (↑(Quotient.out (const α b)) : α → β) ⋯)
      x =
    b
have split_ifs : ∀ (h : ¬∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) sorry)),
  AEStronglyMeasurable.mk (↑(Quotient.out (const α b)) : α → β) sorry x = b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
⊢ Function.const α (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h)
      x =
    b
have this : Eq (α := α →ₘ[μ] β) (const α b)
  (mk
    (Function.const α
      (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) sorry)) h))
    sorry)
Tactic: have := Classical.choose_spec h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
this :
  Eq (α := α →ₘ[μ] β) (const α b)
    (mk
      (Function.const α
        (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h))
      ⋯)
⊢ Function.const α (Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h)
      x =
    b
have pos : let b' := Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) sorry)) h;
∀ (this : Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b') sorry)), Function.const α b' x = b
Tactic: set b' := Classical.choose h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
b' : β := Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h
this : Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b') ⋯)
⊢ Function.const α b' x = b
have this₁ : b = b'
Tactic: simp_rw [const, mk_eq_mk, EventuallyEq, ← const_def, eventually_const] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
b' : β := Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h
this : b = b'
⊢ Function.const α b' x = b
have pos : b' = b
Tactic: rw [Function.const, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
inst_2 : NeZero μ
b : β
x : α
h : ∃ (b_1 : β), Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α b_1) ⋯)
b' : β := Classical.choose (p := fun (x : β) ↦ Eq (α := α →ₘ[μ] β) (const α b) (mk (Function.const α x) ⋯)) h
this : b = b'
pos : b' = b
⊢ Function.const α b' x = b
have pos₁ : b' = b'
Tactic: rw [Function.const, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst_4 : SMul 𝕜 γ
inst_5 : ContinuousConstSMul 𝕜 γ
inst_6 : SMul 𝕜' γ
inst_7 : ContinuousConstSMul 𝕜' γ
inst_8 : SMulCommClass 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f_1 : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ a • b • mk f hf = b • a • mk f hf
have simp_rw : mk (a • b • f) sorry = mk (b • a • f) sorry
Tactic: simp_rw [smul_mk, smul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst_4 : SMul 𝕜 γ
inst_5 : ContinuousConstSMul 𝕜 γ
inst_6 : SMul 𝕜' γ
inst_7 : ContinuousConstSMul 𝕜' γ
inst_8 : SMul 𝕜 𝕜'
inst_9 : IsScalarTower 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f_1 : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ (a • b) • mk f hf = a • b • mk f hf
have simp_rw : mk ((a • b) • f) sorry = mk (a • b • f) sorry
Tactic: simp_rw [smul_mk, smul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
μ ν : Measure α
inst_1 : TopologicalSpace δ
inst_2 : TopologicalSpace β
inst_3 : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst_4 : SMul 𝕜 γ
inst_5 : ContinuousConstSMul 𝕜 γ
inst_6 : SMul 𝕜' γ
inst_7 : ContinuousConstSMul 𝕜' γ
inst_8 : SMul.{u_5, u_3} 𝕜ᵐᵒᵖ γ
inst_9 : IsCentralScalar 𝕜 γ
a : 𝕜
f_1 : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ MulOpposite.op a • mk f hf = a • mk f hf
have simp_rw : mk (MulOpposite.op a • f) sorry = mk (a • f) sorry
Tactic: simp_rw [smul_mk, op_smul_eq_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α →ₘ[μ] ℝ≥0∞
⊢ ∫⁻ (a : α), (↑f : α → ℝ≥0∞) a ∂μ = f.lintegral
have rw : (mk (↑f : α → ℝ≥0∞) sorry).lintegral = f.lintegral
Tactic: rw [← lintegral_mk (hf := f.aestronglyMeasurable), mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α →ₘ[μ] ℝ≥0∞
rw : (mk (↑f : α → ℝ≥0∞) ⋯).lintegral = f.lintegral
⊢ ∫⁻ (a : α), (↑f : α → ℝ≥0∞) a ∂μ = f.lintegral
have rw₁ : f.lintegral = f.lintegral
Tactic: rw [← lintegral_mk (hf := f.aestronglyMeasurable), mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Lattice β
inst_3 : TopologicalLattice β
inst_4 : AddGroup β
inst_5 : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ (↑|f| : α → β) =ᶠ[ae μ] fun (x : α) ↦ |(↑f : α → β) x|
have simp_rw : (↑(f ⊔ -f) : α → β) =ᶠ[ae μ] fun (x : α) ↦ (↑f : α → β) x ⊔ -(↑f : α → β) x
Tactic: simp_rw [abs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Lattice β
inst_3 : TopologicalLattice β
inst_4 : AddGroup β
inst_5 : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ (↑(f ⊔ -f) : α → β) =ᶠ[ae μ] fun (x : α) ↦ (↑f : α → β) x ⊔ -(↑f : α → β) x
have h : ∀ (x : α) (hx_sup : (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ (↑(-f) : α → β) x)
  (hx_neg : (↑(-f) : α → β) x = (-(↑f : α → β)) x), (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
Tactic: filter_upwards [AEEqFun.coeFn_sup f (-f), AEEqFun.coeFn_neg f] with x hx_sup hx_neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Lattice β
inst_3 : TopologicalLattice β
inst_4 : AddGroup β
inst_5 : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ (↑(-f) : α → β) x
hx_neg : (↑(-f) : α → β) x = (-(↑f : α → β)) x
⊢ (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
have h : (↑f : α → β) x ⊔ (↑(-f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
Tactic: rw [hx_sup, hx_neg, Pi.neg_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Lattice β
inst_3 : TopologicalLattice β
inst_4 : AddGroup β
inst_5 : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ (↑(-f) : α → β) x
hx_neg : (↑(-f) : α → β) x = (-(↑f : α → β)) x
h : (↑f : α → β) x ⊔ (↑(-f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
⊢ (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
have h₁ : (↑f : α → β) x ⊔ (-(↑f : α → β)) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
Tactic: rw [hx_sup, hx_neg, Pi.neg_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Lattice β
inst_3 : TopologicalLattice β
inst_4 : AddGroup β
inst_5 : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ (↑(-f) : α → β) x
hx_neg : (↑(-f) : α → β) x = (-(↑f : α → β)) x
h : (↑f : α → β) x ⊔ (↑(-f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
h₁ : (↑f : α → β) x ⊔ (-(↑f : α → β)) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
⊢ (↑(f ⊔ -f) : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
have h₂ : (↑f : α → β) x ⊔ -(↑f : α → β) x = (↑f : α → β) x ⊔ -(↑f : α → β) x
Tactic: rw [hx_sup, hx_neg, Pi.neg_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
ι : Type u_5
inst_2 : T2Space β
g h : α → β
f : ι → α → β
l : Filter ι
inst_3 : l.NeBot
hg : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (g ω))
hh : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (h ω))
⊢ g =ᶠ[ae μ] h
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (g ω))) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (h ω))) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x = h x) x} x}
          x}
    a
Tactic: filter_upwards [hg, hh] with ω hg1 hh1 using tendsto_nhds_unique hg1 hh1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
ι : Type u_5
inst_2 : T2Space β
g h : α → β
f : ι → α → β
l : Filter ι
inst_3 : l.NeBot
hg : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (g ω))
hh : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (h ω))
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (g ω))) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ Tendsto (fun (i : ι) ↦ f i ω) l (𝓝 (h ω))) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x = h x) x} x}
            x}
      a
⊢ g =ᶠ[ae μ] h
have h₂ : ∀ (a : α), Tendsto (fun (i : ι) ↦ f i a) l (𝓝 (g a)) → Tendsto (fun (i : ι) ↦ f i a) l (𝓝 (h a)) → g a = h a
Tactic: filter_upwards [hg, hh] with ω hg1 hh1 using tendsto_nhds_unique hg1 hh1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
⊢ f =ᶠ[ae μ] 0
have hs : DenseRange s
Tactic: have hs : DenseRange s := denseRange_denseSeq E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
⊢ f =ᶠ[ae μ] 0
have hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
Tactic: have hf' : ∀ᵐ x ∂μ, ∀ n : ℕ, ⟪s n, f x⟫_𝕜 = 0 := ae_all_iff.mpr fun n => hf (s n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ f =ᶠ[ae μ] 0
have refine : ∀ (x : α) (hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0), f x = 0 x
Tactic: refine hf'.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ f x = 0 x
have rw : ⟪f x, f x⟫_𝕜 = 0
Tactic: rw [Pi.zero_apply, ← @inner_self_eq_zero 𝕜]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ ⟪c, f x⟫_𝕜) 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ ⟪f x, f x⟫_𝕜 = 0
have h_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {c : E | ⟪c, f x⟫_𝕜 = 0}
Tactic: have h_closed : IsClosed {c : E | ⟪c, f x⟫_𝕜 = 0} :=
    isClosed_eq (by fun_prop) (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
t : Set E
ht : IsSeparable t
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ f =ᶠ[ae μ] 0
have rcases : ∀ (d : Set E) (d_count : d.Countable) (hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d),
  f =ᶠ[ae μ] 0
Tactic: rcases ht with ⟨d, d_count, hd⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
⊢ f =ᶠ[ae μ] 0
have haveI : ∀ (this : Encodable (↑d : Type u_2)), f =ᶠ[ae μ] 0
Tactic: haveI : Encodable d := d_count.toEncodable