mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous₂ (pkg.extend₂ pkg' f)

Tactic:
uniformContinuous₂_def,

Goal state after:
α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous (uncurry (pkg.extend₂ pkg' f))
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ extend f (pureCauchy a) = f a

Tactic:
rw [extend, if_pos hf]
  exact uniformly_extend_of_ind isUniformInducing_pureCauchy denseRange_pureCauchy hf _

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: n : ℕ
⊢ Continuous fun x ↦ x ^ Int.negSucc n

Tactic:
simpa using (ENNReal.continuous_pow _).fun_inv

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
⊢ ∃ᶠ (i : ι) in l, ↑(q + 1) < x i

Tactic:
refine fun hcon => hbdd ↑(q + 1) ?_

Goal state after:
case inl.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i ↦ ↑(q + 1) < x i) x_1
⊢ ∀ᶠ (a : ι) in l, x a ≤ ↑(q + 1)
Module: Mathlib.Topology.Bornology.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
⊢ UniformContinuousOn (Function.uncurry fun x1 x2 ↦ x1 • x2) s

Tactic:
Metric.uniformContinuousOn_iff_le

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ x ∈ s,
        ∀ y ∈ s,
          dist x y ≤ δ → dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) x) (Function.uncurry (fun x1 x2 ↦ x1 • x2) y) ≤ ε
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||

Tactic:
rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||

Tactic:
rw [abs_of_nonneg (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ‖x‖ = 1

Tactic:
have : IsOpen {(0 : 𝕜)} := isOpen_discrete {0}

Goal state after:
case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}
⊢ ‖x‖ = 1
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : ‖x‖ < 1
⊢ 1 < ‖x‖⁻¹

Tactic:
exact (one_lt_inv₀ (norm_pos_iff.2 hx)).2 hlt

Goal state after:
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist (f x) (f y) = ↑(ratio f) * edist x y

Tactic:
by
  rw [ratio]; split_ifs with key
  · rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩
    replace hr := hr x y
    rcases key x y with h | h
    · simp only [hr, h, mul_zero]
    · simp [hr, h, hne]
  exact (DilationClass.edist_eq' f).choose_spec.2 x y

Goal state after:
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ (g.comp f₁) x = g (f₂ x)

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ (g.comp f₂) x = g (f₂ x)
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
⊢ x • y ≠ ∞ ↔ y ≠ ∞

Tactic:
nnreal_smul_ne_top_iff hx

Goal state after:
x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
⊢ y ≠ ∞ ↔ y ≠ ∞
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
⊢ UniformContinuousOn Inv.inv s

Tactic:
Metric.uniformContinuousOn_iff_le

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
⊢ TendstoLocallyUniformly F⁻¹ f⁻¹ l

Tactic:
by
  rw [← tendstoLocallyUniformlyOn_univ] at *
  apply hF.inv₀_of_disjoint
  simpa

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : Set α
ht : t ∈ supClosure s
⊢ MeasurableSet t

Tactic:
rcases ht with ⟨P, hP, PC, rfl⟩

Goal state after:
α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : ↑P ⊆ s
⊢ MeasurableSet (P.sup' hP id)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ ⋃ n, (fun n ↦ s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n = univ

Tactic:
iUnion_unpair_prod,

Goal state after:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ (⋃ n, s n) ×ˢ ⋃ n, t n = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (Subtype.val '' Subtype.val ⁻¹' u)

Tactic:
Subtype.image_preimage_coe

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (s ∩ u)
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
⊢ (⋃ n, s n) \ s n ⊆ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono

Goal state after:
α : 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
⊢ (⋃ n, s n) \ s n ⊆ ⋃ i, s (i + n + 1) \ s (i + n)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₁
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ measurableAtom x
i : β
hi : i ∉ measurableAtom x
⊢ z ∈ s i

Tactic:
exact mem_of_mem_measurableAtom hz (hs i hi).2.1 (hs i hi).1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)

Tactic:
set g' : (i : ι) → t i → β := fun i => g i ∘ (↑)

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (i : δ) → MeasurableSpace (X i)
l : List δ
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod l s)

Tactic:
induction l with
  | nil => exact MeasurableSet.univ
  | cons i l ih => exact (hs i).prod ih

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace β
g : β → Finset α
⊢ Measurable g ↔ ∀ (a : α), Measurable fun x ↦ a ∈ g x

Tactic:
rw [measurable_finset_iff_measurable_set, measurable_set_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace β
g : β → Finset α
⊢ (∀ (a : α), Measurable fun x ↦ a ∈ ↑(g x)) ↔ ∀ (a : α), Measurable fun x ↦ a ∈ g x
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace β
g : β → Finset α
⊢ Measurable g ↔ ∀ (a : α), Measurable fun x ↦ a ∈ g x

Tactic:
by
  rw [measurable_finset_iff_measurable_set, measurable_set_iff]; rfl

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
inst✝ : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : s.topologicalClosure = ⊤
⊢ (map (↑f) s).topologicalClosure = ⊤

Tactic:
rw [SetLike.ext'_iff] at hs ⊢
  simp only [Subalgebra.topologicalClosure_coe, coe_top, ← dense_iff_closure_eq,
    Subalgebra.coe_map] at hs ⊢
  exact hf'.dense_image f.continuous hs

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n ↦ ↑n * c) atTop (𝓝 (∞ * c))
B : ∀ (n : ℕ), ↑n * c ≤ ∑' (x : α), c
⊢ ∑' (x : α), c = ∞

Tactic:
simpa [hc] using le_of_tendsto' A B

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

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ -sign (x✝ * y✝) = -sign x✝ * sign y✝

Tactic:
h,

Goal state after:
case neg_left
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ -(sign x✝ * sign y✝) = -sign x✝ * sign y✝
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ b * (c / b) = a * b

Tactic:
h,

Goal state after:
case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ b * a = a * b
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ c / b = a

Tactic:
h,

Goal state after:
case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ a * b / b = a
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
⊢ LowerSemicontinuousOn (fun x ↦ f (M x) x) s

Tactic:
intro x hx b hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun x ↦ f (M x) x) x > b
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) x' b
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ liminf f (𝓝[s] x)

Tactic:
simp only [← lowerSemicontinuousWithinAt_iff_le_liminf, lowerSemicontinuousOn_iff]

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ ⊥ ≠ ⊤ ∨ limsup v f ≠ ⊥

Tactic:
exact .inl bot_ne_top

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥

Tactic:
h,

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ ⊥ + limsup v f ≤ ⊥
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ ⊤ ≤ liminf u f + liminf v f

Tactic:
h,

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ ⊤ ≤ ⊤ + liminf v f
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu

Goal state after:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousAt f x
gmon : Monotone g
⊢ LowerSemicontinuousAt (g ∘ f) x

Tactic:
by
  simp only [← lowerSemicontinuousWithinAt_univ_iff] at hf ⊢
  exact hg.comp_lowerSemicontinuousWithinAt hf gmon

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case bot.top
h : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ ⊥
h' : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ⊤)

Tactic:
simp at h'

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rcases lt_or_ge r 1 with hr | hr
  · rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
    norm_cast at *
    convert! ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)
    rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]
  · rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]
    refine fun a ha ↦
      (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn ↦ lt_of_lt_of_le hn ?_
    calc
      (n : ℝ≥0∞) = ∑ i ∈ range n, 1 := by rw [sum_const, nsmul_one, card_range]
      _ ≤ ∑ i ∈ range n, r ^ i := by gcongr; apply one_le_pow₀ hr

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val) ((comap Subtype.val) (OuterMeasure.ofFunction m m_empty)) =
    OuterMeasure.ofFunction (fun t ↦ m (s ∩ t)) ⋯

Tactic:
rw [comap_ofFunction _ (Or.inl hm)]

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val) (OuterMeasure.ofFunction (fun s_1 ↦ m (Subtype.val '' s_1)) ⋯) =
    OuterMeasure.ofFunction (fun t ↦ m (s ∩ t)) ⋯
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
⊢ boundedBy 0 = 0

Tactic:
← coe_bot,

Goal state after:
α : Type u_1
⊢ boundedBy 0 = ⊥
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ (1 / m) ^ a

Tactic:
rw [div_pow, one_pow]

Goal state after:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ 1 / m ^ a
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

Tactic:
rw [Finset.mem_range] at hx

Goal state after:
case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
rw [Finset.mem_range] at hx

Goal state after:
case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hfh
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a

Tactic:
· refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    rw [div_le_iff₀ (zero_lt_one.trans_le hx)]
    simp [Nat.floor_le (mul_nonneg ha (zero_le_one.trans hx))]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
⊢ m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂)

Tactic:
rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_sdiff_assoc,
    union_sdiff_cancel_left h]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case h.left
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
a : α
⊢ ((∀ i ∈ T_s, a ∈ f_s i) ∧ ∀ i ∈ T_t', a ∈ f_t' i) ↔
    ∀ i ∈ T_s ∪ T_t', a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅

Tactic:
Finset.mem_union

Goal state after:
case h.left
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
a : α
⊢ ((∀ i ∈ T_s, a ∈ f_s i) ∧ ∀ i ∈ T_t', a ∈ f_t' i) ↔
    ∀ (i : β),
      i ∈ T_s ∨ i ∈ T_t' →
        a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
⊢ extend m s₁ ≤ extend m s₂

Tactic:
refine le_iInf ?_
  intro h₂
  rw [extend_eq m h₁]
  exact m_mono h₁ h₂ hs

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case neg
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∉ T_s
hbt : b ∉ T_t'
⊢ ∅ ∈ g b

Tactic:
Finset.mem_union

Goal state after:
case neg
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
b : β
h_b : b ∈ T_s ∨ b ∈ T_t'
hbs : b ∉ T_s
hbt : b ∉ T_t'
⊢ ∅ ∈ g b
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x
x : ι
hx_mem : x ∈ ht_p
⊢ MeasurableSet (ft x)

Tactic:
exact measurableSet_generateFrom (hft_mem_pi x hx_mem)

Goal state after: