mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝¹ : Type u_1
𝕜' : Type u_2
E✝¹ : Type u_3
F : Type u_4
α : Type u_5
𝕜✝ : Type u_6
E✝ : Type u_7
inst✝⁶ : NormedField 𝕜✝
inst✝⁵ : AddCommGroup E✝
inst✝⁴ : Module 𝕜✝ E✝
inst✝³ : Norm E✝
𝕜 : Type u_8
E : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
core : Core 𝕜 E
r : 𝕜
x : E
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
core.norm_smul r x

Goal state after:
𝕜✝¹ : Type u_1
𝕜' : Type u_2
E✝¹ : Type u_3
F : Type u_4
α : Type u_5
𝕜✝ : Type u_6
E✝ : Type u_7
inst✝⁶ : NormedField 𝕜✝
inst✝⁵ : AddCommGroup E✝
inst✝⁴ : Module 𝕜✝ E✝
inst✝³ : Norm E✝
𝕜 : Type u_8
E : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
core : Core 𝕜 E
r : 𝕜
x : E
⊢ ‖r‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
p : α → Prop
inst✝ : MeasurableSingletonClass α
x : Subtype p
⊢ val ⁻¹' {↑x} = {x}

Tactic:
← image_singleton,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
p : α → Prop
inst✝ : MeasurableSingletonClass α
x : Subtype p
⊢ val ⁻¹' val '' {x} = {x}
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case inr.refine_1
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s (j - (n + 1) + n + 1)

Tactic:
this

Goal state after:
case inr.refine_1
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s j
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case inr.refine_2
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j - (n + 1) + n + 1 ≤ j

Tactic:
this

Goal state after:
case inr.refine_2
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j ≤ j
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
⊢ MeasurableSet (measurableAtom x)

Tactic:
this

Goal state after:
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
⊢ MeasurableSet (⋂ y ∈ (measurableAtom x)ᶜ, s y)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ c • m (⋃ i, s i) ≤ ∑' (i : ℕ), c • m (s i)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ c • m (⋃ i, s i) ≤ ∑' (i : ℕ), c • m (s i)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
⊢ (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)

Tactic:
have := iSup_apply (fun b => cond b m₁ m₂) s; rwa [iSup_bool_eq, iSup_bool_eq] at this

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ y, ((fun x ↦ f (x, y)) ⁻¹' s) ×ˢ measurableAtom y
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ y, ((fun x ↦ f (x, y)) ⁻¹' s) ×ˢ measurableAtom y
⊢ MeasurableSet (⋃ y, ((fun x ↦ f (x, y)) ⁻¹' s) ×ˢ measurableAtom y)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ Measurable g ↔ ∀ (a : δ), Measurable fun x ↦ g x a

Tactic:
[

Goal state after:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ Measurable g ↔ ∀ (a : δ), Measurable fun x ↦ g x a
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ MeasurableSpace.comap (fun b a ↦ X a b) inferInstance = ⨆ a, MeasurableSpace.comap (X a) inferInstance

Tactic:
[

Goal state after:
β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ MeasurableSpace.comap (fun b a ↦ X a b) inferInstance = ⨆ a, MeasurableSpace.comap (X a) inferInstance
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable uniqueElim

Tactic:
[

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Unique δ
⊢ Measurable uniqueElim
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
i : δ
⊢ Measurable fun x ↦ (Equiv.piCongrLeft X f) x i

Tactic:
[

Goal state after:
δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
i : δ
⊢ Measurable fun x ↦ (Equiv.piCongrLeft X f) x i
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | p a ↔ q a}

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | p a ↔ q a}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableEq α
⊢ ∀ (x : α), MeasurableSet {x}

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableEq α
⊢ ∀ (x : α), MeasurableSet {x}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ MeasurableSet (diagonal α)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ MeasurableSet (diagonal α)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
⊢ a ≤ a

Tactic:
by cases a <;> constructor

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
k : ℕ
⊢ s ^ (2 * k + 1) = s

Tactic:
rw [pow_add, pow_one, pow_mul, sq]

Goal state after:
s : SignType
k : ℕ
⊢ (s * s) ^ k * s = s
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = zero
⊢ sign (∑ i ∈ s, f i) = zero

Tactic:
[

Goal state after:
case zero
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = zero
⊢ sign (∑ i ∈ s, f i) = zero
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case neg
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = neg
⊢ sign (∑ i ∈ s, f i) = neg

Tactic:
[

Goal state after:
case neg
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = neg
⊢ sign (∑ i ∈ s, f i) = neg
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos

Tactic:
[

Goal state after:
case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ #(univ.sigma fun a ↦ range (f ↑a).natAbs) = ∑ a ∈ s, (f a).natAbs

Tactic:
simp [sum_attach (f := fun a => (f a).natAbs)]

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : IsSemitopologicalSemiring A
s : Subalgebra R A
r : R
⊢ (algebraMap R A) r ∈ s.topologicalClosure.carrier

Tactic:
simp only [Subsemiring.coe_carrier_toSubmonoid, Subsemiring.topologicalClosure_coe,
      Subalgebra.coe_toSubsemiring]
    apply subset_closure
    exact algebraMap_mem s r

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ 0 ≤ 1 - 1 / ↑n

Tactic:
rw [sub_nonneg, one_div]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ (↑n)⁻¹ ≤ 1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
[

Goal state after:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
⊢ sign (-a) = -sign a
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
[

Goal state after:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ sign (-a) = -sign a
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), r x y ↔ r' x y
b : β
hb : r' a b
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), r x y ↔ r' x y
b : β
hb : r' a b
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ (Semicontinuous fun x1 x2 ↦ ¬f x1 ≤ x2) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ (Semicontinuous fun x1 x2 ↦ ¬f x1 ≤ x2) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
⊢ LowerHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
⊢ LowerHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
⊢ LowerHemicontinuous f ↔ ∀ (x : α) (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
⊢ LowerHemicontinuous f ↔ ∀ (x : α) (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
⊢ UpperHemicontinuousOn f s ↔
    ∀ x ∈ s, ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
⊢ UpperHemicontinuousOn f s ↔
    ∀ x ∈ s, ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuous f ↔
    ∀ (x : α) (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
⊢ UpperHemicontinuous f ↔
    ∀ (x : α) (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
this : {x | x.2 ∈ f x.1 ∩ g x.1} = {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}
⊢ IsOpen[instTopologicalSpaceProd] {x | x.2 ∈ f x.1 ∩ g x.1}

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
this : {x | x.2 ∈ f x.1 ∩ g x.1} = {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}
⊢ IsOpen[instTopologicalSpaceProd] ({x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1})
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf_nonneg : ∀ (n : α), 0 ≤ f n
hf : Summable f
⊢ ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)

Tactic:
[

Goal state after:
α : Type u_1
f : α → ℝ
hf_nonneg : ∀ (n : α), 0 ≤ f n
hf : Summable f
⊢ ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf_nonneg : ∀ (n : α), 0 ≤ f n
hf : Summable f
⊢ ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)

Tactic:
simp_rw [ENNReal.ofReal, ENNReal.tsum_coe_eq (NNReal.hasSum_real_toNNReal_of_nonneg hf_nonneg hf)]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl.inr
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤

Tactic:
obtain ⟨a', a0', aa'⟩ := exists_between ha

Goal state after:
case inl.inr
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Ioo 0 b, c < a * b'

Tactic:
[

Goal state after:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Ioo 0 b, c < a * b'
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : α), c = ↑(ENat.card α) * c

Tactic:
rw [← tsum_univ]; simpa [encard_univ] using tsum_set_const univ c

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
s : Set α
inst✝ : Preorder β
⊢ LowerSemicontinuousOn f s ↔ ∀ (b : β), ∃ u, IsOpen[inst✝¹] u ∧ s ∩ f ⁻¹' Ioi b = s ∩ u

Tactic:
by
  simp only [← lowerSemicontinuous_restrict_iff, domRestrict_eq,
    lowerSemicontinuous_iff_isOpen_preimage, preimage_comp, isOpen_induced_iff,
    Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : a * b < c
⊢ ∃ b' ∈ Ioo b ⊤, a * b' < c

Tactic:
[

Goal state after:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : a * b < c
⊢ ∃ b' ∈ Ioo b ⊤, a * b' < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case neg
x✝¹ : ℝ
hx : ⊥ < ↑x✝¹
hx_top : ¬↑x✝¹ = ⊤
x : EReal
x✝ : x ∈ Ioc ⊥ ↑x✝¹
h1 : ⊥ < x
h2 : x ≤ ↑x✝¹
⊢ x ∈ Iic ↑x✝¹ ∩ {⊥}ᶜ

Tactic:
simp [h2, h1.ne_bot]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ LowerSemicontinuousOn f s ↔ IsClosed[instTopologicalSpaceProd] {p | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
[

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ LowerSemicontinuousOn f s ↔ IsClosed[instTopologicalSpaceProd] {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ContinuousAt (fun x ↦ ENNReal.ofReal x.toReal) x

pp: case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : ¬x = ⊥
⊢ ContinuousAt (fun x ↦ ENNReal.ofReal x.toReal) x

Tactic:
· refine tendsto_nhds_of_eventually_eq ?_
    rw [h_bot, nhds_bot_basis.eventually_iff]
    simpa [toReal_bot, ENNReal.ofReal_zero, ENNReal.ofReal_eq_zero, true_and] using
      ⟨0, fun _ hx ↦ toReal_nonpos hx.le⟩

Goal state after:
case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : ¬x = ⊥
⊢ ContinuousAt (fun x ↦ ENNReal.ofReal x.toReal) x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ c * u x) f = c * limsup u f

Tactic:
[

Goal state after:
case inr
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup (fun x ↦ c * u x) f = c * limsup u f
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n ↦ 1 / (1 + x / ↑n)) atTop (𝓝 1)

Tactic:
this

Goal state after:
case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n ↦ 1 / (1 + x / ↑n)) atTop (𝓝 (1 / (1 + x * 0)))
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n ↦ x / ↑n) atTop (𝓝 (x * 0))

Tactic:
[

Goal state after:
case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n ↦ x / ↑n) atTop (𝓝 (x * 0))
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case a
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n)

Tactic:
[

Goal state after:
case a
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤
    ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x ↦ f x / g x) l (𝓝 a)
⊢ Tendsto (fun x ↦ g x / f x) l (𝓝 a⁻¹)

Tactic:
[

Goal state after:
α : Type u_4
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x ↦ f x / g x) l (𝓝 a)
⊢ Tendsto (fun x ↦ g x / f x) l (𝓝 a⁻¹)