mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
N : ι
hN :
  ∀ n_1 ≥ N, μ (s ∩ notConvergentSeq f g n n_1) ∈ Icc (0 - ENNReal.ofReal (ε * 2⁻¹ ^ n)) (ENNReal.ofReal (ε * 2⁻¹ ^ n))
⊢ ∃ j, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
n : ℕ
N : ι
hN :
  ∀ n_1 ≥ N, μ (s ∩ notConvergentSeq f g n n_1) ∈ Icc (0 - ENNReal.ofReal (ε * 2⁻¹ ^ n)) (ENNReal.ofReal (ε * 2⁻¹ ^ n))
⊢ ∃ j, μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
⊢ ∀ (s : Set α), MeasurableSet s → Measurable fun b ↦ (μ.withDensity (f b)) s

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
⊢ ∀ (s : Set α), MeasurableSet s → Measurable fun b ↦ (μ.withDensity (f b)) s
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
⊢ a * (x * x) + b * x + c = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
⊢ a * (x * x) + b * x + c = 0
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)

Tactic:
]

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2 * 2⁻¹ ^ a) ≤ ENNReal.ofReal ε

Tactic:
ENNReal.ofReal_mul (half_pos hε).le

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2) * ENNReal.ofReal (2⁻¹ ^ a) ≤ ENNReal.ofReal ε
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = 0 * 0
⊢ x = -b / (2 * a) ↔ x = -b / (2 * a)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : 0 ≤ᵐ[μ] f
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ < ∞ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
⊢ f a ≤ g a

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
a : α
hn : 0 ≤ f a
ha : f a ≤ g a
⊢ f a ≤ g a
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ b * b - 4 * a * c ≤ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ b * b - 4 * a * c ≤ 0
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (fun x ↦ (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ (a * x + b) * x + c < 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (fun x ↦ (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ (a * x + b) * x + c < 0
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
x : α
⊢ ENNReal.ofReal (f x).toReal = ENNReal.ofReal (f x).toReal

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
m n : ℕ
hmn : m ≤ n
x : α
⊢ f x * g n x ≤ f x * g n x

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ENNReal.ofReal ε ≤ ENNReal.ofReal ε

pp: case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n

pp: case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)

Tactic:
]

Goal state after:
case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n

case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow 2⁻¹)
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + (-c - 1) + c
⊢ b * b - 4 * 0 * c ≤ 0

Tactic:
]

Goal state after:
case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + (-c - 1) + c
⊢ b * b - 4 * 0 * c ≤ 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (x : α) in s, (f * g) x ∂μ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow (1 / 2))

Tactic:
]

Goal state after:
case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow (1 / 2))
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f * g) a ∂μ
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ -b / (2 * a) = -b / (2 * a)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ s ∩ ⋃ i, notConvergentSeq f g i (notConvergentSeqLTIndex ⋯ hf hsm hs hfg i) ⊆ s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ s ∩ ⋃ i, notConvergentSeq f g i (notConvergentSeqLTIndex ⋯ hf hsm hs hfg i) ⊆ s
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ ε_1 > 0, ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f n x) < ε_1

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ ε_1 > 0, ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f n x) < ε_1
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ x ≤ 1 ↔ x ≤ 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ 1 ≤ x ↔ 1 ≤ x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ≥0
⊢ x * y ≤ max x y * max x y

Tactic:
]

Goal state after:
x y : ℝ≥0
⊢ x * y ≤ max x y * max x y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ≥0
⊢ x * y = x * y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ≥0
⊢ ↑(NNReal.sqrt x) = ↑(NNReal.sqrt x)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ Continuous fun x ↦ √x

Tactic:
unfold sqrt

Goal state after:
⊢ Continuous fun x ↦ ↑(NNReal.sqrt x.toNNReal)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ map (fun x ↦ √x) atTop = atTop

Tactic:
unfold sqrt

Goal state after:
⊢ map (fun x ↦ ↑(NNReal.sqrt x.toNNReal)) atTop = atTop
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ comap (fun x ↦ √x) atTop = atTop

Tactic:
unfold sqrt

Goal state after:
⊢ comap (fun x ↦ ↑(NNReal.sqrt x.toNNReal)) atTop = atTop
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N)⁻¹ < δ
⊢ ∃ a, ∀ (b : ι), a ≤ b → ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f b x) < δ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N)⁻¹ < δ
⊢ ∃ a, ∀ (b : ι), a ≤ b → ∀ x ∈ s \ iUnionNotConvergentSeq hε hf hsm hs hfg, edist (g x) (f b x) < δ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ 0 ≤ √x

Tactic:
unfold sqrt

Goal state after:
x : ℝ
⊢ 0 ≤ ↑(NNReal.sqrt x.toNNReal)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.restrict {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x

Tactic:
]

Goal state after:
case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.restrict {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : √x = y
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : x = y * y
⊢ y = y

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace β
μ : Measure α
inst✝³ : SemilatticeSup ι
inst✝² : Nonempty ι
inst✝¹ : Countable ι
f : ι → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
left✝ : t ⊆ univ
ht : MeasurableSet t
htendsto : μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
⊢ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace β
μ : Measure α
inst✝³ : SemilatticeSup ι
inst✝² : Nonempty ι
inst✝¹ : Countable ι
f : ι → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
left✝ : t ⊆ univ
ht : MeasurableSet t
htendsto : μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
⊢ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ x = 1 ↔ x = 1

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x = y * y ↔ x = y * y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ |x| = |x|

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ x ≤ y ↔ x ≤ y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ x < y ↔ x < y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
h : x ≤ y
⊢ x.toNNReal ≤ y.toNNReal

Tactic:
]

Goal state after:
x y : ℝ
h : x ≤ y
⊢ x.toNNReal ≤ y.toNNReal
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ x ≤ y * y ↔ x ≤ y * y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
⊢ 0 ≤ y → (√x ≤ y ↔ x ≤ y ^ 2)

Tactic:
]

Goal state after:
x y : ℝ
⊢ 0 ≤ y → (√x ≤ y ↔ x ≤ y ^ 2)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x < y ↔ √x < y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ √x < y ↔ √x < y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
h : x ^ 2 ≤ y
⊢ √(x ^ 2) ≤ √y

Tactic:
]

Goal state after:
x y : ℝ
h : x ^ 2 ≤ y
⊢ √(x ^ 2) ≤ √y