awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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)
⊢ ∀ (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)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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)‖ : 𝕜) : 𝕜)
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
⊢ f =ᶠ[ae μ] 0

Tactic:
choose s hs using this
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : 𝕜)
contrapose! : ∀ (ha : a ≠ 0), ∃ (x : (↑d : Type u_2)), Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
⊢ a = 0

Tactic:
contrapose! ha
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
⊢ 0 < ‖a‖

Tactic:
simp only [ha, norm_pos_iff, Ne, not_false_iff]

Premises used: norm_pos_iff, Ne, not_false_iff
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
⊢ 0 < ‖a‖

Tactic:
have a_pos : 0 < ‖a‖ := by simp only [ha, norm_pos_iff, Ne, not_false_iff]
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d

Tactic:
have a_mem : a ∈ closure d := hd hat
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
rcases : ∀ (x : E) (h'x : x ∈ d) (hx : dist a x < ‖a‖ / 2), ∃ (x : (↑d : Type u_2)), dist a (↑x : E) < ‖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⟩

Premises used: Norm.norm, half_pos, HDiv.hDiv, Metric.mem_closure_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : E
h'x : x ∈ d
hx : dist a x < ‖a‖ / 2
⊢ ∃ (x : (↑d : Type u_2)), dist a (↑x : E) < ‖a‖ / 2

Tactic:
⟨⟨x, h'x⟩, hx⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : E
h'x : x ∈ d
hx : dist a x < ‖a‖ / 2
⊢ ∃ (x : (↑d : Type u_2)), dist a (↑x : E) < ‖a‖ / 2

Tactic:
exact ⟨⟨x, h'x⟩, hx⟩
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
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 : 𝕜)
⊢ ∃ (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⟩
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
h : Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
⊢ ∃ (x : (↑d : Type u_2)), Ne.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)

Tactic:
use x
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖

Tactic:
have : ‖a‖ ≤ ‖(x : E)‖ + ‖a - x‖ := norm_le_insert' _ _
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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)‖
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hx : ‖a - (↑x : E)‖ < ‖a‖ / 2) (this : ‖a‖ ≤ ‖(↑x : E)‖ + ‖a - (↑x : E)‖), ‖a - (↑x : E)‖ < ‖a‖ / 2
⊢ ‖a - (↑x : E)‖ < ‖a‖ / 2

Tactic:
rwa [dist_eq_norm] at hx

Premises used: dist_eq_norm
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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

Tactic:
have : ‖a - x‖ < ‖a‖ / 2 := by rwa [dist_eq_norm] at hx
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
linarith₉ :
  ‖(↑x : E)‖ ≤ ‖a‖ / 2 →
    2 * (‖a‖ - (‖(↑x : E)‖ + ‖a - (↑x : E)‖)) + (2 * ‖a - (↑x : E)‖ - 1 * ‖a‖) + (2 * ‖(↑x : E)‖ - 1 * ‖a‖) = 0
linarith₁₀ : ‖(↑x : E)‖ ≤ ‖a‖ / 2 → GT.gt (α := ℝ) 2 0
⊢ ‖a‖ / 2 < ‖(↑x : E)‖

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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)‖

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
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : 𝕜)
h₁ : norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) < norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜)
⊢ False

Tactic:
apply lt_irrefl ‖s x x‖

Premises used: Norm.norm, lt_irrefl, Subtype.val, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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) - a) : 𝕜)

Tactic:
simp only [h, sub_zero, map_sub]

Premises used: map_sub, sub_zero
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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) - a) : 𝕜) ≤ 1 * ‖(↑x : E) - a‖

Tactic:
ContinuousLinearMap.le_of_opNorm_le _ (hs x).1 _

Premises used: ContinuousLinearMap.le_of_opNorm_le, And.left
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : 𝕜)
rw : ‖(↑x : E) - a‖ < ‖a‖ / 2
⊢ 1 * ‖(↑x : E) - a‖ < ‖a‖ / 2

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : 𝕜)
rwa rwa₁ rwa₂ 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
⊢ ‖(↑x : E) - a‖ < ‖a‖ / 2

Tactic:
rwa [dist_eq_norm'] at hx

Premises used: dist_eq_norm'
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : 𝕜)
⊢ ‖a‖ / 2 < ‖(↑x : E)‖

Tactic:
I
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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)‖ = norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜)

Tactic:
simp [(hs x).2]

Premises used: And.right