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

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
this : F x' = F ⟨x, xs⟩
⊢ ∃ i, ∃ (_ : ∃ y, (Subtype.val ∘ Finv) y = i), x ∈ ball i ε

Tactic:
exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal

Tactic:
← this,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
⊢ a p' ∈ J * s.inf fun i ↦ i.asIdeal
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoBotOrder α
⊢ (cobounded α).NeBot

Tactic:
simp [Filter.neBot_iff, cobounded_eq_bot_iff, ← isBounded_univ, isBounded_iff_bddBelow_bddAbove]

Goal state after:
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
m : β
hm : m < f x
y : α
hy : y ∈ s ∩ Ioi x
⊢ m < f y

Tactic:
exact hm.trans_le (hf xs hy.1 (le_of_lt hy.2))

Goal state after:
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

Tactic:
obtain ⟨z, ⟨yz, zx⟩, lz⟩ : ∃ a : α, a ∈ Ioo y x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h_nonempty.image _) hl
    filter_upwards [Ioo_mem_nhdsLT zx] with w hw
    exact lz.trans_le <| Mf ⟨yz, zx⟩ ⟨yz.trans_le hw.1.le, hw.2⟩ hw.1.le

Goal state after:
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z

Tactic:
have h : ({x} : Set γ) ×ˢ K ⊆ ↿f ⁻¹' Iio z := by
      rintro ⟨x', y'⟩ ⟨(rfl : x' = x), hy'⟩
      exact (hy y' hy').trans_lt hz

Goal state after:
case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ ↑I ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑J

Tactic:
← this,

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ ↑I ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I)
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace (X b)
⊢ ProperSpace ((b : β) → X b)

Tactic:
refine .of_isCompact_closedBall_of_le 0 fun x r hr => ?_

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (closedBall x r)
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a‖ ≤ ‖a / b‖ + ‖b‖

Tactic:
simpa only [div_one] using norm_div_le_norm_div_add_norm_div a b 1

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x * y‖ = ‖x‖

Tactic:
apply le_antisymm ?_ ?_
  · simpa [h] using norm_mul_le' x y
  · simpa [h] using norm_le_mul_norm_add x y

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
⊢ Icc a a ⊆ s

Tactic:
simp [ha]

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ ∀ (t t' : Set α),
    IsClosed[inst✝³] t →
      IsClosed[inst✝³] t' →
        Icc a b ⊆ t ∪ t' → (Icc a b ∩ t).Nonempty → (Icc a b ∩ t').Nonempty → (Icc a b ∩ (t ∩ t')).Nonempty

Tactic:
rintro s t hs ht hab ⟨x, hx⟩ ⟨y, hy⟩
      -- This used to use `wlog`, but it was causing timeouts.
      rcases le_total x y with h | h
      · exact isPreconnected_Icc_aux x y s t h hs ht hab hx hy
      · rw [inter_comm s t]
        rw [union_comm s t] at hab
        exact isPreconnected_Icc_aux y x t s h ht hs hab hy hx

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
⊢ Dense ↑s ↔ ∀ (a : G), s ≠ zpowers a

Tactic:
simp [xor_iff_iff_not.1 s.dense_xor_cyclic]

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

Goal state before:
pp: x y z : ℝ
h : ↑x + ↑y ≤ ↑x + ↑z
⊢ ↑y ≤ ↑z

Tactic:
simpa only [← coe_add, EReal.coe_le_coe_iff, add_le_add_iff_left] using h

Goal state after:
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ upperBounds (range f)

Tactic:
rintro _ ⟨b, rfl⟩
    exact hf.ge_of_tendsto ha b

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
⊢ LipschitzOnWith K f univ ↔ LipschitzWith K f

Tactic:
by
  simp [LipschitzOnWith, LipschitzWith]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ LipschitzOnWith K f s ↔ LipschitzWith K (s.domRestrict f)

Tactic:
by
  simp [LipschitzOnWith, LipschitzWith]

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

Goal state before:
pp: a b c : EReal
h : a ≤ b + c
⊢ a - c ≤ b

Tactic:
by
  induction c with
  | bot => rw [add_bot, le_bot_iff] at h; simp only [h, bot_sub, bot_le]
  | coe c => exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h
  | top => simp only [sub_top, bot_le]

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
⊢ ∃ r, ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'

Tactic:
simpa using! this

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ z, x < z ∧ z < y
y : β
⊢ x < y → limsup u f < y

Tactic:
x_y

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ z, x < z ∧ z < y
y : β
x_y : x < y
⊢ limsup u f < y
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y
y : β
⊢ x < y → limsup u f < y

Tactic:
x_y

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y
y : β
x_y : x < y
⊢ limsup u f < y
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
b : β
hb : a ∈ f b
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}

Tactic:
exact (eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
inst✝ : Infinite α
s : Finset α
x✝ : ℕ
⊢ x✝ ∈ Ici s.card ↔ x✝ ∈ Finset.card '' {a' | s ⊆ a'}

Tactic:
refine ⟨Infinite.exists_superset_card_eq _ _, ?_⟩

Goal state after:
α : Type u_3
inst✝ : Infinite α
s : Finset α
x✝ : ℕ
⊢ x✝ ∈ Finset.card '' {a' | s ⊆ a'} → x✝ ∈ Ici s.card
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v

Tactic:
obtain ⟨a, ha⟩ := h₁.eventually_ge

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
a : β
ha : ∀ᶠ (x : α) in f, a ≤ u x
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
⊢ -x * y = -(x * y)

Tactic:
induction x, y using induction₂_neg_left with

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
⊢ ∃ᶠ (n : R) in F, F.limsSup ≤ n

Tactic:
apply (frequently_lt_of_lt_limsSup cobdd c_lt).mono

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
⊢ ∀ (x : R), c < x → F.limsSup ≤ x
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case neg
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
⊢ liminf f F ≤ f F.limsSup

Tactic:
by_contra! H

Goal state after:
case neg
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
⊢ False
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe.inr.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a = 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Tactic:
simp [ha]

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + b * c

Tactic:
lift a to ℝ≥0∞ using ha
  lift b to ℝ≥0∞ using hb
  cases c using recENNReal with
  | coe c => exact_mod_cast add_mul a b c
  | neg_coe c hc =>
    simp only [mul_neg, ← coe_ennreal_add, ← coe_ennreal_mul, add_mul]
    rw [coe_ennreal_add, EReal.neg_add (.inl (coe_ennreal_ne_bot _)) (.inr (coe_ennreal_ne_bot _)),
      sub_eq_add_neg]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
⊢ max (limsup u f) (limsup v f) ≤ limsup (fun a ↦ max (u a) (v a)) f

Tactic:
exact max_le (c := limsup (fun a ↦ max (u a) (v a)) f)
      (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_left (u a) (v a))) h₁ bddmax)
      (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_right (u a) (v a))) h₂ bddmax)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inr.inr.e_u
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h✝ : f.NeBot
s_nemp : s.Nonempty
a : α
⊢ (s.sup fun i ↦ F i a) = s.sup' s_nemp fun i ↦ F i a

Tactic:
exact Eq.symm (Finset.sup'_eq_sup s_nemp (fun i ↦ F i a))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
this : (g ∘ Subtype.val) ∘ ⇑e = f ∘ Subtype.val
⊢ HasProd (f ∘ Subtype.val) a ↔ HasProd g a

Tactic:
← this,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
this : (g ∘ Subtype.val) ∘ ⇑e = f ∘ Subtype.val
⊢ HasProd ((g ∘ Subtype.val) ∘ ⇑e) a ↔ HasProd g a
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∏'[L] (b : β), f b = f b

Tactic:
rw [tprod_eq_prod (s := {b}), prod_singleton]
  exact fun b' hb' ↦ hf b' (by simpa using hb')

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : Summable f L
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
ha : a = 0
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x

Tactic:
simp [ha]

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
ha : a = 0
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

Tactic:
simp [ha]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
hf : ∃ b, f b = 0
inst✝ : L.LeAtTop
⊢ HasProd f 0 L

Tactic:
obtain ⟨b, hb⟩ := hf
  apply tendsto_const_nhds.congr'
  filter_upwards [(eventually_ge_atTop {b}).filter_mono L.le_atTop] with s hs
  exact (Finset.prod_eq_zero (Finset.singleton_subset_iff.mp hs) hb).symm

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝ : SeminormedGroup E
f : α → E
a : Filter α
b : E
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (fun e ↦ ‖(f e)⁻¹ * b‖ₑ) a (𝓝 0)

Tactic:
by
  simp only [← edist_eq_enorm_inv_mul, ← tendsto_iff_edist_tendsto_0]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst✝¹.toTopologicalSpace] v
hv : a ∈ v
⊢ ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ image Sigma.fst s ⊆ t0

Tactic:
by
    have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)
    exact (A.and (Ici_mem_atTop _)).exists

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

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ a ≠ 0 ∨ b⁻¹ ≠ ∞

Tactic:
simp [ha]

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

Goal state before:
pp: t : ℝ≥0∞
t_ne_top : t ≠ ∞
x y : ℝ≥0∞
⊢ x ≤ y → t.truncateToReal x ≤ t.truncateToReal y

Tactic:
x_le_y

Goal state after:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ t.truncateToReal x ≤ t.truncateToReal y
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
refine ⟨g, LipschitzWith.of_le_add_mul K fun x y => ?_, E⟩

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
⊢ g x ≤ g y + ↑K * dist x y
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
a b : E
⊢ dist b (b * a) = ‖a‖

Tactic:
by
  rw [← dist_one_left, ← dist_mul_left b 1 a, mul_one]

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

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
x y : G
⊢ edist x⁻¹ y = edist x y⁻¹

Tactic:
← edist_inv_inv,

Goal state after:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
x y : G
⊢ edist x⁻¹⁻¹ y⁻¹ = edist x y⁻¹