mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Real.Pointwise

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

Tactic:
Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_neg ha').1 h),

Goal state after:
case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddAbove s
⊢ 0 = a • sSup s
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: z : ℝ≥0
⊢ nndist z 0 = z

Tactic:
nndist_comm

Goal state after:
z : ℝ≥0
⊢ nndist 0 z = z
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ s ∈ Filter.atBot ⊔ Filter.atTop → s ∈ cobounded α

Tactic:
rw [Filter.mem_sup, Filter.atTop_basis.mem_iff, Filter.atBot_basis.mem_iff,
    ← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove, compl_compl s]

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ ((∃ i, True ∧ Iic i ⊆ s) ∧ ∃ i, True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
hK : IsCompact ∅
⊢ Continuous[inst✝, inst✝³] fun x ↦ sSup (f x '' ∅)

Tactic:
simp_rw [image_empty]

Goal state after:
case inl
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
hK : IsCompact ∅
⊢ Continuous[inst✝, inst✝³] fun x ↦ sSup ∅
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u⁻¹ * v * v⁻¹‖ = ‖u⁻¹‖

Tactic:
group

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
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
have S0 := fun n => le_csSup (hS n) (S0m n)

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)
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (s ∩ t)).Nonempty

Tactic:
inter_comm s t

Goal state after:
case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (t ∩ s)).Nonempty
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a

Tactic:
by
  rcases h with ⟨i, i_s, b, hb⟩
  use b
  refine fun c hc ↦ hb c ?_
  rw [eventually_map] at hc ⊢
  refine hc.mono fun a h ↦ ?_
  simp only [sup'_le_iff] at h ⊢
  exact h i i_s

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
⊢ ∃ᶠ (x' : S) in map f F, f l ≤ x'

Tactic:
refine fun ev ↦ freq_ge ?_

Goal state after:
R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, ¬(fun x' ↦ f l ≤ x') x
⊢ ∀ᶠ (x : R) in F, ¬(fun x ↦ l ≤ x) x
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
⊢ 0 < -a ↔ a < 0

Tactic:
by rw [lt_neg_comm, neg_zero]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ blimsup u f p = blimsup v f p

Tactic:
simpa only [blimsup_eq_limsup] using! limsup_congr <| eventually_inf_principal.2 h

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : b < limsup u f
⊢ ∃ᶠ (x : α) in f, b < u x

Tactic:
by
  contrapose! h
  apply limsSup_le_of_le hu
  simpa using h

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

Goal state before:
pp: a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ -a - b ≤ -c

Tactic:
refine add_le_of_forall_lt fun a' ha' b' hb' ↦ EReal.le_neg_of_le_neg ?_

Goal state after:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -(a' + b')
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_2
L : SummationFilter β
⊢ L.support = (map SetLike.coe L.filter).limsInf

Tactic:
by
  refine eq_of_forall_ge_iff fun c ↦ ?_
  simpa [support, limsInf, ofPred_subset] using
    ⟨fun hL b hb x hx ↦ hL x <| hb.mp <| .of_forall fun c hc ↦ hc hx,
      fun hL x hx ↦ singleton_subset_iff.mp <| hL _ <| by simpa using hx⟩

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
⊢ L.LeAtTop

Tactic:
have hLs : L.support = Set.univ := by
    simp [SummationFilter.support, L.neBot_or_eq_bot.resolve_left hL]

Goal state after:
β : Type u_2
L : SummationFilter β
hL : ¬L.NeBot
hLs : L.support = univ
⊢ L.LeAtTop
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
b : Finset β
x✝ : True
⊢ ∃ i, True ∧ (fun s ↦ ∏ b ∈ s, f b) '' Set.Ici i ⊆ (fun s ↦ ∏ x ∈ s, g x) '' Set.Ici b

Tactic:
let ⟨v, hv⟩ := h_eq b

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
b : Finset β
x✝ : True
v : Finset α
hv : ∀ (v' : Finset α), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
⊢ ∃ i, True ∧ (fun s ↦ ∏ b ∈ s, f b) '' Set.Ici i ⊆ (fun s ↦ ∏ x ∈ s, g x) '' Set.Ici b
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
b : β
hb : ∀ i ∈ s, limsup (F i) f < b
⊢ ∀ i ∈ s, ∀ᶠ (x : α) in f, F i x < b

Tactic:
exact fun i i_s ↦ eventually_lt_of_limsup_lt (hb i i_s) (h₂ i i_s)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ HasProd (fun b ↦ f b / g b) (a₁ / a₂) L

Tactic:
by
  simp only [div_eq_mul_inv]
  exact hf.mul hg.inv

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ Tendsto (fun x ↦ (∏ b ∈ x.2, f b) / ∏ b ∈ x.1, f b) atTop (𝓝 1) ↔
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
rw [tendsto_atTop']

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ (∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s) ↔
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case inl
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ extend e f 1 (e i) ≤ g (e i)

pp: case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ extend e f 1 c ≤ g c

Tactic:
· rw [he.extend_apply]
    exact h _

Goal state after:
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ extend e f 1 c ≤ g c
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
hfs : (mulSupport fun x ↦ g (f x)).Finite
⊢ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
hfs : ¬(mulSupport fun x ↦ g (f x)).Finite
⊢ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

Tactic:
· simp [tprod_bot hL, finprod_eq_prod _ hfs, ← _root_.map_prod]

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
hfs : ¬(mulSupport fun x ↦ g (f x)).Finite
⊢ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∀ (b' : β), b' ≠ b → (if b = b' then a b' else 1) = 1

Tactic:
· intro b' hb'; simp [hb'.symm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)

Tactic:
simp only [AntilipschitzWith, edist_nndist]
  norm_cast

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

Goal state before:
pp: β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
⊢ ProperSpace β

Tactic:
refine ⟨fun x₀ r => ?_⟩

Goal state after:
β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
⊢ IsCompact (closedBall x₀ r)
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
⊢ IsSeqCompact (f '' K)

Tactic:
intro ys ys_in_fK
  choose xs xs_in_K fxs_eq_ys using ys_in_fK
  obtain ⟨a, a_in_K, phi, phi_mono, xs_phi_lim⟩ := K_cpt xs_in_K
  refine ⟨f a, mem_image_of_mem f a_in_K, phi, phi_mono, ?_⟩
  exact (f_cont xs_phi_lim).congr fun x ↦ fxs_eq_ys (phi x)

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

Goal state before:
pp: α : Type u_1
m : α → ℝ≥0∞
f : Filter α
⊢ Tendsto m f (𝓝 ∞) ↔ ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, ↑x < m a

Tactic:
simp only [nhds_top', tendsto_iInf, tendsto_principal, mem_Ioi]

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

Goal state before:
pp: case inr.refine_1
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

Tactic:
rcases exists_between (tsub_pos_of_lt ha) with ⟨ε, ε0, hε⟩

Goal state after:
case inr.refine_1
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
⊢ ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n k : ℕ
hk : k < n
⊢ (w 0)⁻¹ * w (k + 1) = (w 0)⁻¹ * w k * ((w k)⁻¹ * w (k + 1))

Tactic:
group

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

Goal state before:
pp: a b : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ↑b ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (↑a, ↑b)) (𝓝 (↑a - ↑b))

Tactic:
simp only [nhds_coe_coe, tendsto_map'_iff, ← ENNReal.coe_sub, Function.comp_def, tendsto_coe]

Goal state after:
a b : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ↑b ≠ ∞
⊢ Tendsto (fun a ↦ a.1 - a.2) (𝓝 (a, b)) (𝓝 (a - b))
Module: Mathlib.Topology.Algebra.UniformMulAction

Goal state before:
pp: R : Type u_3
β : Type u_4
inst✝³ : DivisionRing R
inst✝² : UniformSpace R
inst✝¹ : UniformContinuousConstSMul Rᵐᵒᵖ R
inst✝ : UniformSpace β
f : β → R
hf : UniformContinuous f
a : R
⊢ UniformContinuous fun x ↦ f x / a

Tactic:
by
  simpa [div_eq_mul_inv] using hf.mul_const' a⁻¹

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

Goal state before:
pp: case inr
a b : ℝ
h : a < b
⊢ ENNReal.ofReal (b - sInf (Ioo a b)) = ENNReal.ofReal (b - a)

Tactic:
csInf_Ioo h

Goal state after:
case inr
a b : ℝ
h : a < b
⊢ ENNReal.ofReal (b - a) = ENNReal.ofReal (b - a)
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: x y : ℝ
⊢ dist x.toNNReal y.toNNReal ≤ ↑1 * dist x y

Tactic:
simpa only [NNReal.coe_one, dist_prod_same_right, one_mul, Real.dist_eq] using!
    lipschitzWith_iff_dist_le_mul.mp lipschitzWith_max (x, 0) (y, 0)

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

Goal state before:
pp: R : Type u_3
R' : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R'
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R' M'
σ₁₂ : R →+* R'
f : M →ₛₗ[σ₁₂] M'
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
hf : Continuous ⇑f
p : Submodule R M
⊢ Continuous ⇑(f.domRestrict p)

Tactic:
by
  rw [coe_domRestrict]
  fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: ⊢ LipschitzWith 2 fun p ↦ p.1 - p.2

Tactic:
rw [← NNReal.isometry_coe.lipschitzWith_iff]

Goal state after:
⊢ LipschitzWith 2 (toReal ∘ fun p ↦ p.1 - p.2)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
⊢ MeasurableSet {x | p x ↔ q x}

Tactic:
have h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x} := by ext; simp; grind

Goal state after:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x}
⊢ MeasurableSet {x | p x ↔ q x}
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
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples e)

Tactic:
have : IsAddTorsionFree E := .of_module_rat E
  rcases eq_or_ne e 0 with (rfl | he)
  · rw [AddSubgroup.zmultiples_zero_eq_bot]
    exact Subsingleton.discreteTopology (α := ↑(⊥ : Subspace ℚ E))
  · rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]
    refine ⟨Metric.ball 0 ‖e‖, Metric.isOpen_ball, ?_⟩
    ext ⟨x, hx⟩
    obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
    rw [mem_preimage, mem_ball_zero_iff, AddSubgroup.coe_mk, mem_singleton_iff, Subtype.ext_iff,
      AddSubgroup.coe_mk, AddSubgroup.coe_zero, norm_zsmul ℚ k e, Int.norm_cast_rat,
      Int.norm_eq_abs, mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ← @Int.cast_one ℝ _,
      ← Int.cast_abs, Int.cast_lt, Int.abs_lt_one_iff, smul_eq_zero, or_iff_left he]

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

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖

Tactic:
norm_pos_iff

Goal state after:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ x ≠ 0
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖

Tactic:
by
  rw [norm_algebraMap, norm_one, mul_one]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
⊢ Measurable fun x ↦ Nat.find ⋯

Tactic:
refine measurable_to_nat fun x => ?_
  rw [preimage_find_eq_disjointed (fun k => {x | p x k})]
  exact MeasurableSet.disjointed hm _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
x✝¹ x✝ : Set α
h : x✝¹ ⊆ x✝
⊢ x✝¹.indicator (fun x ↦ 1) a ≤ x✝.indicator (fun x ↦ 1) a

Tactic:
by grw [h]

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

Goal state before:
pp: case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : j = i
⊢ Measurable fun v ↦ v.elim hj

pp: case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v ↦ v.elim hj

Tactic:
· subst hji
      simpa using measurable_fst

Goal state after:
case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v ↦ v.elim hj
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ⊤.abs = ⊤.abs * (↑x✝).abs

Tactic:
abs_top,

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ∞ = ∞ * (↑x✝).abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp
x y : EReal
h : x ≤ y
⊢ sign x < sign y ∨
    sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
      sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs

Tactic:
refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)

Goal state after:
case mp
x y : EReal
h : x ≤ y
hs : sign x = sign y
⊢ sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
    sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

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

Tactic:
rw [← sign_eq_and_abs_eq_iff_eq]

Goal state after:
x y z : EReal
⊢ (x * y * z).abs = (x * (y * z)).abs ∧ sign (x * y * z) = sign (x * (y * z))
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case mpr
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ ((∀ (x : α), Summable fun y ↦ f ⟨x, y⟩) ∧ Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩) → Summable f

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mpr
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
h₁ : ∀ (x : α), Summable fun y ↦ f ⟨x, y⟩
h₂ : Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩
⊢ Summable f
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf : Summable f
⊢ ∑' (i : α), ENNReal.ofReal (f i) < ∞

Tactic:
unfold ENNReal.ofReal
  rw [lt_top_iff_ne_top, ENNReal.tsum_coe_ne_top_iff_summable]
  exact hf.toNNReal

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

Goal state before:
pp: ⊢ (𝓝 ⊤).HasBasis (fun x ↦ True) fun x ↦ Ioi ↑x

Tactic:
refine (nhds_top_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩
  rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩
  exact ⟨_, trivial, Ioi_subset_Ioi hxy.le⟩

Goal state after: