mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ¬∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ¬∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ¬∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), m (f ⁻¹' (fun n ↦ (range f)ᶜ ∪ f '' t n) n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), m (f ⁻¹' (fun n ↦ (range f)ᶜ ∪ f '' t n) n) ≤ ∑' (n : ℕ), m (t n)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_1
x : ℝ
⊢ IsOpen (Ioi (max (↑x) 0) ×ˢ Ioi 1)

pp: case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)

pp: case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1

Tactic:
·

Goal state after:
case h.refine_2.refine_1
x : ℝ
⊢ IsOpen (Ioi (max (↑x) 0) ×ˢ Ioi 1)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PseudoMetricSpace α
r : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n
⊢ HasSum (fun n ↦ 0 * r ^ n) (0 / (1 - r))

pp: case inr
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n ↦ C * r ^ n) (C / (1 - r))

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : PseudoMetricSpace α
r : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n
⊢ HasSum (fun n ↦ 0 * r ^ n) (0 / (1 - r))
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)

pp: case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1

Tactic:
·

Goal state after:
case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1

Tactic:
·

Goal state after:
case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g z ≤ g x
⊢ min (g z) (g x) ∈ v

pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g x < g z
⊢ min (g z) (g x) ∈ v

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g z ≤ g x
⊢ min (g z) (g x) ∈ v
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n ↦ C * r ^ n) (C / (1 - r))

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n ↦ C * r ^ n) (C / (1 - r))
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g x < g z
⊢ min (g z) (g x) ∈ v

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g x < g z
⊢ min (g z) (g x) ∈ v
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ y ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2

pp: case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2))

pp: case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)

pp: case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
·

Goal state after:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ y ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C / 2 ^ n

Tactic:
convert! dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ (n + m)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ¬∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ¬∃ l, l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ (Monotone fun s ↦ ⨆ (_ : s.Nonempty), m s) ∨ Surjective f

pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ = boundedBy fun s ↦ m (f '' s)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ (Monotone fun s ↦ ⨆ (_ : s.Nonempty), m s) ∨ Surjective f
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ = boundedBy fun s ↦ m (f '' s)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ = boundedBy fun s ↦ m (f '' s)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ c ∉ Set.range Encodable.encode, 0 ≤ f c

pp: case refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ (i : ι), (f ∘ Encodable.encode) i ≤ f (Encodable.encode i)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ c ∉ Set.range Encodable.encode, 0 ≤ f c
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)

pp: case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case inl
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
⊢ ⨆ (_ : ∅.Nonempty), sInfGen m ∅ = ⨅ μ ∈ m, μ ∅

pp: case inr
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
ht : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t

Tactic:
·

Goal state after:
case inl
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
⊢ ⨆ (_ : ∅.Nonempty), sInfGen m ∅ = ⨅ μ ∈ m, μ ∅
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ (i : ι), (f ∘ Encodable.encode) i ≤ f (Encodable.encode i)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ (i : ι), (f ∘ Encodable.encode) i ≤ f (Encodable.encode i)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case inr
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
ht : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t

Tactic:
·

Goal state after:
case inr
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
ht : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) i

pp: case refine_2
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ HasSum (fun i ↦ (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) ↑i) c

Tactic:
·

Goal state after:
case refine_1
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) i
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2))

pp: case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)

pp: case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
·

Goal state after:
case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2))
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)

pp: case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
·

Goal state after:
case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inl
α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

Tactic:
·

Goal state after:
case inl
α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
·

Goal state after:
case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'

Tactic:
·

Goal state after:
case inr
α : Type u_4
β : Type u_5
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ HasSum (fun i ↦ (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) ↑i) c

Tactic:
·

Goal state after:
case refine_2
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ HasSum (fun i ↦ (fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1) ↑i) c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
a : ℝ
h : a ≠ 0
a_neg : a < 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)

pp: case inr
a : ℝ
h : a ≠ 0
a_pos : 0 < a
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)

Tactic:
·

Goal state after:
case inl
a : ℝ
h : a ≠ 0
a_neg : a < 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
a : ℝ
h : a ≠ 0
a_pos : 0 < a
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)

Tactic:
·

Goal state after:
case inr
a : ℝ
h : a ≠ 0
a_pos : 0 < a
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_1
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ n, f '' t n ∪ (range f)ᶜ

pp: case refine_2
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), ⨅ i, (m i) (f '' f ⁻¹' (fun n ↦ f '' t n ∪ (range f)ᶜ) n) ≤ ∑' (n : ℕ), ⨅ i, (m i) (f '' t n)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ n, f '' t n ∪ (range f)ᶜ
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), ⨅ i, (m i) (f '' f ⁻¹' (fun n ↦ f '' t n ∪ (range f)ᶜ) n) ≤ ∑' (n : ℕ), ⨅ i, (m i) (f '' t n)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), ⨅ i, (m i) (f '' f ⁻¹' (fun n ↦ f '' t n ∪ (range f)ᶜ) n) ≤ ∑' (n : ℕ), ⨅ i, (m i) (f '' t n)