mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ (s.sup S)ᶜ, f a = ∑ a, f a - ∑ a ∈ s.biUnion S, f a

Tactic:
sup_eq_biUnion,

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ (s.biUnion S)ᶜ, f a = ∑ a, f a - ∑ a ∈ s.biUnion S, f a
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ a ≤ y

Tactic:
by
    have hx : x ≠ 0 := ha.ne_zero
    have hx' : x⁻¹ ≠ 0 := by rwa [Ne, inv_eq_zero]
    have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]
    have : a * x⁻¹ * x ≤ y := h _ this
    rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
⊢ f ↑u < 1

Tactic:
hu

Goal state after:
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
⊢ f ↑(if g < 1 then g else g⁻¹) < 1
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case pos
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
exact mem_of_superset hmem' (disjoint_left.1 H)

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hd' : Disjoint (⇑ofDual ⁻¹' s) (closure[instTopologicalSpace] (⇑ofDual ⁻¹' t))
ha' : toDual a ∈ ⇑ofDual ⁻¹' s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a

Tactic:
simpa only [dual_ordSeparatingSet, dual_ordConnectedSection] using!
    compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd' ha'

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

Goal state before:
pp: p : EReal → Prop
r : EReal
hr : p r
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
cases r

Goal state after:
case bot
p : EReal → Prop
hr : p ⊥
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

case coe
p : EReal → Prop
a✝ : ℝ
hr : p ↑a✝
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

case top
p : EReal → Prop
hr : p ⊤
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' Ioi ⊥ = univ

Tactic:
change ((WithBot.some ∘ WithTop.some) ⁻¹' (Ioi (⊥ : WithBot (WithTop ℝ))) : Set ℝ) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Ioi_bot, preimage_univ]

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

Goal state before:
pp: case pos
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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : w = v
⊢ count K v ↑v.asIdeal = 1

Tactic:
count_self

Goal state after:
case pos
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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : w = v
⊢ 1 = 1
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Goal state after:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd : d < a * b
⊢ d ≤ c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case neg.inr.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iSup _

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

Goal state before:
pp: case inl
x : ℝ
hx : 0 < x
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹

Tactic:
simp [ofReal_inv_of_pos hx]

Goal state after:
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sInf s

Tactic:
rw [zero_smul_set hs, zero_smul]
    exact csInf_singleton 0

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ edist x z ≤ edist x y + edist y z

Tactic:
simp only [edist_dist, ← ENNReal.ofReal_add, dist_nonneg]
      rw [ENNReal.ofReal_le_ofReal_iff _]
      · exact dist_triangle _ _ _
      · simpa using add_le_add (dist_nonneg : 0 ≤ dist x y) dist_nonneg

Goal state after:
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sSup s

Tactic:
rw [zero_smul_set hs, zero_smul]
    exact csInf_singleton 0

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

Goal state before:
pp: case refine_1
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
p : HeightOneSpectrum R
hps : p ∈ s
⊢ p.asIdeal < 1

pp: case refine_2
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
p : HeightOneSpectrum R
hps : p ∈ s
⊢ 0 < J * ∏ x ∈ s \ {p}, x.asIdeal

Tactic:
· rw [Ideal.one_eq_top, lt_top_iff_ne_top]
      exact p.2.ne_top

Goal state after:
case refine_2
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
p : HeightOneSpectrum R
hps : p ∈ s
⊢ 0 < J * ∏ x ∈ s \ {p}, x.asIdeal
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun x ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
simp_rw [Prod.map_fst, Prod.map_snd]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ CauchySeq u ↔ Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
by
  rw [cauchySeq_iff_tendsto, Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff,
    Function.comp_def]
  simp_rw [Prod.map_fst, Prod.map_snd]

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

Goal state before:
pp: case neg
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
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ a p' ∈ J * (↑⟨q, hq⟩).asIdeal

Tactic:
refine Ideal.mul_mono_right ?_ (ha p' hp's)
    exact Ideal.prod_le_inf.trans (Finset.inf_le (b := q) (by simpa [hq] using hqp))

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
c : α → Set α
hs : IsCompact s
hc : ∀ x ∈ s, c x ∈ 𝓝[s] x
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ y, eball x δ ∩ s ⊆ c y

Tactic:
by
  simpa only [eball, UniformSpace.ball, preimage_ofPred_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhdsWithin hs hc

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

Goal state before:
pp: case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)

pp: case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)

Tactic:
· rw [← sdiff_subset_closure_iff, Icc_sdiff_Ioo_same hab.le]
      have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab
      simp only [insert_subset_iff, singleton_subset_iff]
      exact ⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩

Goal state after:
case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b c : α
H₁ : (Iio c).Nonempty
H₂ : b ≤ c
⊢ b ∈ closure[inst✝³] (Iio c)

Tactic:
closure_Iio' H₁

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b c : α
H₁ : (Iio c).Nonempty
H₂ : b ≤ c
⊢ b ∈ Iic c
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case grind
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
this : Ioo a b = Icc a b
⊢ False

Tactic:
have : b ∈ Ioo a b

Goal state after:
case grind
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
this✝ : Ioo a b = Icc a b
this : b ∈ Ioo a b
⊢ False
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
⊢ IsOrderBornology α ↔ inst✝² = orderBornology

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun s ↦ by rw [h, orderBornology_isBounded]⟩⟩
  ext s
  exact isBounded_compl_iff.symm.trans (h.1 _)

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

Goal state before:
pp: α : Type u_1
s✝ t : Set α
inst✝⁵ : Bornology α
inst✝⁴ : Preorder α
inst✝³ : IsOrderBornology α
β : Type u_2
inst✝² : Preorder β
inst✝¹ : Bornology β
inst✝ : IsOrderBornology β
s : Set (α × β)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx✝ : b ≤ x
hbx : b < x
⊢ f b ≤ f x

Tactic:
apply ge_of_tendsto h'x

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx✝ : b ≤ x
hbx : b < x
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f b ≤ f c
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
⊢ ∃ a ∈ Ioo x y, f a < m

Tactic:
by
      simpa [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_csInf_lt (h_nonempty.image _) hm

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

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
⊢ u ∈ 𝓤 α → ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

Tactic:
hu

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : SeminormedGroup E
inst✝ : Subsingleton E
a : E
⊢ ‖1‖ = 0

Tactic:
norm_one'

Goal state after:
E : Type u_5
inst✝¹ : SeminormedGroup E
inst✝ : Subsingleton E
a : E
⊢ 0 = 0
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
simpa [h] using norm_le_mul_norm_add' x y

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (sSup (S n)) 0 < ε

Tactic:
refine (Metric.cauchySeq_iff.1 hs (ε / 2) (half_pos ε0)).imp fun N hN n hn => ?_

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
⊢ dist (sSup (S n)) 0 < ε
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ NontrivialTopology E ↔ ∃ x, ‖x‖₊ ≠ 0

Tactic:
simp_rw [TopologicalSpace.nontrivial_iff_exists_not_inseparable, Metric.inseparable_iff_nndist,
    nndist_eq_nnnorm_inv_mul]
  exact ⟨fun ⟨x, y, hxy⟩ => ⟨_, hxy⟩, fun ⟨x, hx⟩ => ⟨x, 1, by simpa using hx⟩⟩

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
x y : E
⊢ dist x⁻¹ y = dist x y⁻¹

Tactic:
by
  simp_rw [dist_eq_norm_inv_mul, ← norm_inv' (x⁻¹ * y⁻¹), mul_inv, inv_inv]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ sphere 1 r} ↔ x ∈ sphere a r

Tactic:
rw [mem_sphere_iff_norm']

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ sphere 1 r} ↔ ‖x / a‖ = r
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : 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}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
t₁b' : t₁ < b
m : α
t₁m : m > t₁
H : Ioo t₁ m ⊆ s
t : α
hat : t₁ < t
ht : t < min m b
t' : α
ht' : t' ∈ Icc a t
h't' : t₁ < t'
⊢ t' ∈ s

Tactic:
· exact H ⟨h't', ht'.2.trans_lt <| ht.trans_le <| min_le_left ..⟩

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in atBot, p ↑n

Tactic:
← Int.comap_cast_atBot (R := R)

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ s ∈ cocompact α

Tactic:
Filter.mem_cocompact

Goal state after:
α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s
Module: Mathlib.Topology.UniformSpace.Real

Goal state before:
pp: u : ℕ → ℝ
⊢ CauchySeq u → ∃ a, Tendsto u atTop (nhds a)

Tactic:
hu

Goal state after:
u : ℕ → ℝ
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (nhds a)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U V : R
hU : ∀ᶠ (a : α) in f, u a ≤ U
hV : ∀ᶠ (a : α) in f, v a ≤ V
a : α
⊢ u a ≤ U → v a ≤ V → u a + v a ≤ U + V

Tactic:
hu

Goal state after:
α : Type u_5
f : Filter α
R : Type u_6
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U V : R
hU : ∀ᶠ (a : α) in f, u a ≤ U
hV : ∀ᶠ (a : α) in f, v a ≤ V
a : α
hu : u a ≤ U
⊢ v a ≤ V → u a + v a ≤ U + V
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
⊢ v x ≤ V → 0 x ≤ v x → (u * v) x ≤ U * V

Tactic:
x_V

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
⊢ 0 x ≤ v x → (u * v) x ≤ U * V
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f p ⊔ blimsup u f fun x ↦ ¬p x) = limsup u f

Tactic:
← blimsup_or_eq_sup,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f fun x ↦ p x ∨ ¬p x) = limsup u f
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
⊢ ∃ n, x + ε < u ↑n

Tactic:
by
  have h : ∀ᶠ n : ℕ in atTop, x + ε < u n := eventually_add_neg_lt_of_le_liminf hu_bdd hu hε
  simp only [eventually_atTop] at h
  obtain ⟨n, hn⟩ := h
  exact ⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩

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

Goal state before:
pp: a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
⊢ a + b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Goal state after:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd : d < a + b
⊢ d ≤ c
Module: Mathlib.Data.EReal.Operations

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

Tactic:
by
  induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg h]

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

Goal state before:
pp: α : Type u_3
inst✝ : Infinite α
⊢ map Finset.card atTop = atTop

Tactic:
by
  rw [map_atTop_eq, atTop]
  refine Function.Surjective.iInf_congr Finset.card Finset.exists_card_eq fun s ↦ congr(𝓟 $(?_))
  ext
  refine ⟨Infinite.exists_superset_card_eq _ _, ?_⟩
  aesop (add safe apply Finset.card_le_card)

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

Goal state before:
pp: a b : EReal
⊢ a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
by
  rw [ne_eq, mul_eq_top]
  -- push the negation while keeping the disjunctions, that is converting `¬(p ∧ q)` into `¬p ∨ ¬q`
  -- rather than `p → ¬q`, since we already have disjunctions in the rhs
  push +distrib Not
  rfl

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

Goal state before:
pp: case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ (n + 1) • x = ↑(n + 1) * x

Tactic:
| succ n ih =>

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

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

Tactic:
by simpa using this

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 : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (c : ↑(mulSupport g)), f (i c) = ∏' (x : ↑(mulSupport g)), g ↑x

Tactic:
simp only [hfg]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ closure[inst✝¹] s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)

Tactic:
by
  rw [← seqClosure_eq_closure]
  rfl

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

Goal state before:
pp: case inr.refine_1.refine_2
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ x + min ε ↑δ < (a, b).2

Tactic:
grw [min_le_right]
        exact hδ

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 α
⊢ u ∈ 𝓝 a → ∀ (a : Finset ((b : β) × γ b)), ∃ b, a ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
hu

Goal state after:
α : 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
⊢ ∀ (a : Finset ((b : β) × γ b)), ∃ b, a ⊆ b ∧ ∏ i ∈ b, f i ∈ u