awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
this : Encodable (↑d : Type u_2)
⊢ f =ᶠ[ae μ] 0
have this₁ : ∀ (x : (↑d : Type u_2)),
  ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
Tactic: have : ∀ x : d, ∃ g : StrongDual 𝕜 E, ‖g‖ ≤ 1 ∧ g x = ‖(x : E)‖ :=
    fun x => exists_dual_vector'' 𝕜 (x : E)
-- 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
this_1 : Encodable (↑d : Type u_2)
this :
  ∀ (x : (↑d : Type u_2)),
    ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
⊢ f =ᶠ[ae μ] 0
have choose : ∀ (s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E)
  (hs :
    ∀ (x : (↑d : Type u_2)),
      ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)),
  f =ᶠ[ae μ] 0
Tactic: choose s hs using this
Cleared hypotheses: this
-- 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : ∀ (x : (↑d : Type u_2)), Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
⊢ a = 0
have contrapose! : ∀ (ha : a ≠ 0), ∃ (x : (↑d : Type u_2)), Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
Tactic: contrapose! ha
Cleared hypotheses: ha
-- 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 : 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
⊢ ∃ (x : (↑d : Type u_2)), Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
have a_pos : 0 < ‖a‖
Tactic: have a_pos : 0 < ‖a‖ := by simp only [ha, norm_pos_iff, Ne, not_false_iff]
-- 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 : 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
⊢ ∃ (x : (↑d : Type u_2)), Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
have a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
Tactic: have a_mem : a ∈ closure d := hd hat
-- 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
⊢ ∃ (x : (↑d : Type u_2)), dist a (↑x : E) < ‖a‖ / 2
have rcases : ∀ (x : E) (h'x : x ∈ d) (hx : dist a x < ‖a‖ / 2), ∃ (x : (↑d : Type u_2)), dist a (↑x : E) < ‖a‖ / 2
Tactic: rcases Metric.mem_closure_iff.1 a_mem (‖a‖ / 2) (half_pos a_pos) with ⟨x, h'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 : 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
⊢ ∃ (x : (↑d : Type u_2)), Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
have obtain : ∀ (x : (↑d : Type u_2)) (hx : dist a (↑x : E) < ‖a‖ / 2),
  ∃ (x : (↑d : Type u_2)), Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
Tactic: obtain ⟨x, hx⟩ : ∃ x : d, dist a x < ‖a‖ / 2 := by
      rcases Metric.mem_closure_iff.1 a_mem (‖a‖ / 2) (half_pos a_pos) with ⟨x, h'x, hx⟩
      exact ⟨⟨x, h'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 : 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
⊢ ∃ (x : (↑d : Type u_2)), Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
have h : Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
Tactic: use x
-- 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 : 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
⊢ ‖a‖ / 2 < ‖(↑x : E)‖
have this₁ : ‖a‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖
Tactic: have : ‖a‖ ≤ ‖(x : E)‖ + ‖a - x‖ := norm_le_insert' _ _
-- 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
this_1 : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
this : ‖a‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖
⊢ ‖a - (↑x : E)‖ < ‖a‖ / 2
have rwa : ∀ (hx : ‖a - (↑x : E)‖ < ‖a‖ / 2) (this : ‖a‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖), ‖a - (↑x : E)‖ < ‖a‖ / 2
Tactic: rwa [dist_eq_norm] at hx
Cleared hypotheses: hx, this
-- 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 : 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
this_1 : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
this : ‖a‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖
⊢ ‖a‖ / 2 < ‖(↑x : E)‖
have this₁ : ‖a - (↑x : E)‖ < ‖a‖ / 2
Tactic: have : ‖a - x‖ < ‖a‖ / 2 := by rwa [dist_eq_norm] at 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 : 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
this_1 : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
this_2 : ‖a‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖
this : ‖a - (↑x : E)‖ < ‖a‖ / 2
⊢ ‖a‖ / 2 < ‖(↑x : E)‖
have linarith : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → 2 / 2 = 1
Tactic: linarith
-- 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
this_1 : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
this_2 : ‖a‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖
this : ‖a - (↑x : E)‖ < ‖a‖ / 2
linarith : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → 2 / 2 = 1
⊢ ‖a‖ / 2 < ‖(↑x : E)‖
have linarith₁ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
this_1 : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
this_2 : ‖a‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖
this : ‖a - (↑x : E)‖ < ‖a‖ / 2
linarith : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → 2 / 2 = 1
linarith₁ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ‖a‖ / 2 < ‖(↑x : E)‖
have linarith₂ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
this_1 : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
this_2 : ‖a‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖
this : ‖a - (↑x : E)‖ < ‖a‖ / 2
linarith : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → 2 / 2 = 1
linarith₁ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → 2 / 2 = 1
linarith₄ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → 2 / 2 = 1
linarith₇ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → GT.gt (α := ℝ) 2 0
⊢ ‖a‖ / 2 < ‖(↑x : E)‖
have linarith₉ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 →
  2 * (‖a‖ - (‖(↑x : E)‖ + ‖a - (↑x : E)‖)) + (2 * ‖a - (↑x : E)‖ - 1 * ‖a‖) + (2 * ‖(↑x : E)‖ - 1 * ‖a‖) = 0
Tactic: linarith
-- 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 : 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
⊢ Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
have I : ‖a‖ / 2 < ‖(↑x : E)‖
Tactic: have I : ‖a‖ / 2 < ‖(x : E)‖ := by
      have : ‖a‖ ≤ ‖(x : E)‖ + ‖a - x‖ := norm_le_insert' _ _
      have : ‖a - x‖ < ‖a‖ / 2 := by rwa [dist_eq_norm] at hx
      linarith
-- 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
I : ‖a‖ / 2 < ‖(↑x : E)‖
h : Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
⊢ False
have h₁ : norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) < norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜)
Tactic: apply lt_irrefl ‖s x x‖
-- 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
I : ‖a‖ / 2 < ‖(↑x : E)‖
h : Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
⊢ 1 * ‖(↑x : E) - a‖ < ‖a‖ / 2
have rw : ‖(↑x : E) - a‖ < ‖a‖ / 2
Tactic: rw [one_mul]
-- 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
I : ‖a‖ / 2 < ‖(↑x : E)‖
h : Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
⊢ ‖(↑x : E) - a‖ < ‖a‖ / 2
have rwa : ∀ (hx : ‖(↑x : E) - a‖ < ‖a‖ / 2) (I : ‖a‖ / 2 < ‖(↑x : E)‖)
  (h : Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)), ‖(↑x : E) - a‖ < ‖a‖ / 2
Tactic: rwa [dist_eq_norm'] at hx
Cleared hypotheses: hx, I, h
-- 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
I : ‖a‖ / 2 < ‖(↑x : E)‖
h : Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
⊢ norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) < norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜)
have x₁ : norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) = norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) ((↑x : E) - a) : 𝕜)
Tactic: calc
      ‖s x x‖ = ‖s x (x - a)‖ := by simp only [h, sub_zero, map_sub]
      _ ≤ 1 * ‖(x : E) - a‖ := ContinuousLinearMap.le_of_opNorm_le _ (hs x).1 _
      _ < ‖a‖ / 2 := by rw [one_mul]; rwa [dist_eq_norm'] at hx
      _ < ‖(x : E)‖ := I
      _ = ‖s x x‖ := by simp [(hs x).2]
-- 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
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
I : ‖a‖ / 2 < ‖(↑x : E)‖
h : Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
x₁ :
  norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) = norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) ((↑x : E) - a) : 𝕜)
⊢ norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) < norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜)
have x₂ : 1 * ‖(↑x : E) - a‖ < ‖a‖ / 2
Tactic: calc
      ‖s x x‖ = ‖s x (x - a)‖ := by simp only [h, sub_zero, map_sub]
      _ ≤ 1 * ‖(x : E) - a‖ := ContinuousLinearMap.le_of_opNorm_le _ (hs x).1 _
      _ < ‖a‖ / 2 := by rw [one_mul]; rwa [dist_eq_norm'] at hx
      _ < ‖(x : E)‖ := I
      _ = ‖s x x‖ := by simp [(hs x).2]