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

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x✝¹ x✝ : E
⊢ r • p (x✝¹ + x✝) ≤ r • p x✝¹ + r • p x✝

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x✝¹ x✝ : E
⊢ ↑(r • 1) * p (x✝¹ + x✝) ≤ ↑(r • 1) * (p x✝¹ + p x✝)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q f g : NonarchAddGroupSeminorm E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _, _⟩ := f; cases g; congr

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x✝¹ x✝ : E
⊢ r • p (x✝¹ * x✝) ≤ r • p x✝¹ + r • p x✝

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : GroupSeminorm E
x✝¹ x✝ : E
⊢ ↑(r • 1) * p (x✝¹ * x✝) ≤ ↑(r • 1) * (p x✝¹ + p x✝)
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case refine_1
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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ tᶜ.ordConnectedComponent a

pp: case refine_2
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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x

Tactic:
· exact OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩)
        (hsub' ⟨hac.le, hcb⟩)

Goal state after:
case refine_2
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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case pos
ι : Sort u_1
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

Tactic:
rw [← coe_iSup h, toNNReal_coe]

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Iio x = Ioo ⊥ ↑x

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Iio, WithBot.image_coe_Iio]
  rfl

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Icc ↑x ↑y = Icc x y

Tactic:
← Ici_inter_Iic

Goal state after:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iic ↑y) = Ici x ∩ Iic y
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: r : ℝ≥0
b : ℝ≥0∞
hb : 1 ≤ ↑r * b
⊢ ∀ (p : ℝ≥0), b = ↑p → r⁻¹ ≤ p

Tactic:
rintro b rfl

Goal state after:
r b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ r⁻¹ ≤ b
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case inr.inr
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
C : ℝ
hC : ∀ z ∈ s ∪ t, dist x z ≤ C
⊢ s ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

Tactic:
refine ⟨C + C, fun a ha b hb => (dist_triangle a x b).trans ?_⟩
        simpa only [dist_comm] using add_le_add (hC _ ha) (hC _ hb)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝[univ] b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

Tactic:
tendsto_nhdsWithin_nhdsWithin

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ univ ∧ edist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
⊢ edist x y < ENNReal.ofReal r ↔ dist x y < r

Tactic:
by
  rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝[univ] b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε

Tactic:
tendsto_nhdsWithin_nhdsWithin

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ univ ∧ dist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x : ℝ
⊢ dist x 0 = |x|

Tactic:
by simp [Real.dist_eq]

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

Goal state before:
pp: x y : ℝ
⊢ Ioo x y = Ioo ((x + x) / 2) ((y + x) / 2 + (y - x) / 2)

Tactic:
add_self_div_two,

Goal state after:
x y : ℝ
⊢ Ioo x y = Ioo x ((y + x) / 2 + (y - x) / 2)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x y : ℝ
⊢ Icc x y = Icc ((x + x) / 2) ((y + x) / 2 + (y - x) / 2)

Tactic:
add_self_div_two,

Goal state after:
x y : ℝ
⊢ Icc x y = Icc x ((y + x) / 2 + (y - x) / 2)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
e : β → α
a : α
⊢ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range e) ↔ ∀ ε > 0, ∃ k, dist a (e k) < ε

Tactic:
simp only [mem_closure_iff, exists_range_iff]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
x : α
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range f) ↔ ∀ r > 0, ∃ y, dist x (f y) < r

Tactic:
simp only [mem_closure_iff, exists_range_iff]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
apply UniformSpace.subset_countable_closure_of_almost_dense_set

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
⊢ ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
by
  refine subset_countable_closure_of_almost_dense_set s fun ε hε => ?_
  rcases totallyBounded_iff'.1 hs.totallyBounded ε hε with ⟨t, -, htf, hst⟩
  exact ⟨t, htf.countable, hst.trans <| iUnion₂_mono fun _ _ => eball_subset_closedEBall⟩

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x ↦ x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x ↦ ¬(fun x ↦ x ∈ s) x) x}
⊢ False

Tactic:
rcases ha.exists_between hba with ⟨b', hb's, hb'⟩

Goal state after:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x ↦ x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x ↦ ¬(fun x ↦ x ∈ s) x) x}
b' : α
hb's : b' ∈ s
hb' : b < b' ∧ b' ≤ a
⊢ False
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ioo a b)
hab : a < b
this : closure[inst✝³] (Ioo a b) = Ioo a b
⊢ False

Tactic:
rw [closure_Ioo hab.ne, Icc_eq_Ioo_same_iff] at this

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ioo a b)
hab : a < b
this : ¬a ≤ b
⊢ False
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
⊢ (edist (mk x) (mk y)).toReal = (edist (mk x') (mk y')).toReal

Tactic:
mk_eq_mk.2 hx,

Goal state after:
α✝ : Type u
β : Type v
X : Type u_1
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
⊢ (edist (mk x') (mk y)).toReal = (edist (mk x') (mk y')).toReal
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
x✝ : TopologicalSpace α := Preorder.topology α
⊢ ⊥ = Preorder.topology α

Tactic:
have : OrderTopology α := ⟨rfl⟩

Goal state after:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ ⊥ = Preorder.topology α
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: case pos
ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst✝ : Nonempty ι
hr : 0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

pp: case neg
ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst✝ : Nonempty ι
hr : ¬0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
· exact pi_norm_le_iff_of_nonneg' hr

Goal state after:
case neg
ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst✝ : Nonempty ι
hr : ¬0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
⊢ BddBelow s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne
  · exact bddBelow_empty
  · obtain ⟨a, -, has⟩ := hs.exists_isLeast hne
    exact ⟨a, has⟩

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
⊢ {s | IsPreconnected s} ⊆
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
by
  intro s hs
  rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs) <;> rw [hs] <;>
    simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x✝ : ∃ x, ‖x‖₊ ≠ 0
x : E
hx : ‖x‖₊ ≠ 0
⊢ ¬‖x⁻¹ * 1‖₊ = 0

Tactic:
by simpa using hx

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
y : E
ε : ℝ
⊢ ball y ε = {x | ‖x / y‖ < ε}

Tactic:
by
  simp_rw [ball_eq_norm_inv_mul_lt, norm_inv_mul]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Bornology.IsBounded (range f)

Tactic:
rw [← image_union_image_compl_eq_range]

Goal state after:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Bornology.IsBounded (f '' ?m.75 ∪ f '' ?m.75ᶜ)

α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Set β
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
⊢ IsCompact s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)
  · exact isCompact_empty
  · rcases hb.subset_closedBall x with ⟨r, hr⟩
    exact (isCompact_closedBall x r).of_isClosed_subset hc hr

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

Goal state before:
pp: case mp
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto f atTop (𝓝 l)
⊢ Tendsto (f ∘ φ) atTop (𝓝 l)

Tactic:
exact h.comp hg

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

Goal state before:
pp: case bot
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊥ + y ≠ ⊤ ↔ ⊥ ≠ ⊤

Tactic:
simp [EReal.add_ne_top_iff_ne_top₂, hy, hy']

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

Goal state before:
pp: case coe
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
a✝ : ℝ
⊢ ↑a✝ + y ≠ ⊤ ↔ ↑a✝ ≠ ⊤

Tactic:
simp [EReal.add_ne_top_iff_ne_top₂, hy, hy']

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

Goal state before:
pp: case top
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊤ + y ≠ ⊤ ↔ ⊤ ≠ ⊤

Tactic:
simp [EReal.add_ne_top_iff_ne_top₂, hy, hy']

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

Goal state before:
pp: x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤

Tactic:
by
  induction x <;> simp [EReal.add_ne_top_iff_ne_top₂, hy, hy']

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

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : EReal
hx : ¬0 ≤ x
⊢ 0 < -x

Tactic:
by simpa using hx

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

Goal state before:
pp: case inr.refine_2
ι : 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_1 : α) in atTop, ⨆ i, u i b_1 < b

Tactic:
let b' := if h : (Set.Ioo c b).Nonempty then h.some else c

Goal state after:
case inr.refine_2
ι : 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
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ i, u i b_1 < b
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_2
L : SummationFilter β
c : Set β
hL : ∀ (t' : Set β), (∀ᶠ (a : Finset β) in L.filter, t' ⊆ ↑a) → t' ⊆ c
x : β
hx : ∀ᶠ (s : Finset β) in L.filter, x ∈ s
⊢ ∀ᶠ (a : Finset β) in L.filter, {x} ⊆ ↑a

Tactic:
by simpa using hx

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:
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.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
⊢ (if L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite then finprod (L.support.mulIndicator fun b ↦ f b)
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
L.support_eq_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
⊢ (if L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ Set.univ).Finite then finprod (Set.univ.mulIndicator fun b ↦ f b)
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case pos.convert_5
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ ∀ b ∈ L.support, b ∉ ⋯.toFinset → f b = 1

Tactic:
grind [Set.Finite.mem_toFinset, mem_mulSupport]

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
⊢ HasProd f a ↔ HasProd g a

Tactic:
have : (g ∘ (↑)) ∘ e = f ∘ (↑) := funext he
  rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1

Tactic:
rw [← hasProd_one_iff, hf.hasProd_iff]

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

Tactic:
refine ⟨if h : s.Nonempty then s.max' h + 1 else 0,
      fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩

Goal state after:
case refine_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
t : Set ℕ
ht : t ⊆ {n | (if h : s.Nonempty then s.max' h + 1 else 0) ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝ : SeminormedCommGroup 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_div, ← tendsto_iff_edist_tendsto_0]

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁵ : UniformSpace X
inst✝⁴ : UniformSpace Y
inst✝³ : SMul M X
inst✝² : SMul Mᵐᵒᵖ X
inst✝¹ : IsCentralScalar M X
inst✝ : UniformContinuousConstSMul M X
c : M
⊢ UniformContinuous fun x ↦ MulOpposite.op c • x

Tactic:
simpa only [op_smul_eq_smul] using uniformContinuous_const_smul c

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

Goal state before:
pp: a b : ℝ
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)

Tactic:
rcases le_or_gt a b with (h | h)
  · rw [Real.ediam_eq (isBounded_Icc _ _), csSup_Icc h, csInf_Icc h]
  · simp [h, h.le]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ LipschitzWith 2 (uncurry dist)

Tactic:
rw [← one_add_one_eq_two]
  exact LipschitzWith.uncurry LipschitzWith.dist_left LipschitzWith.dist_right

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ (∀ y < r, ∃ᶠ (a : ι) in f, y < u a) ↔ ∀ y < ↑r, ∃ᶠ (a : ι) in f, y < ↑(u a)

Tactic:
simp [forall_ennreal]

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ ↑(limsup u f) = limsup (fun i ↦ ↑(u i)) f

Tactic:
by
  refine eq_of_forall_nnreal_le_iff fun r ↦ ?_
  rw [coe_le_coe, le_limsup_iff, le_limsup_iff]
  simp [forall_ennreal]

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ (∀ y < r, ∀ᶠ (a : ι) in f, y < u a) ↔ ∀ y < ↑r, ∀ᶠ (a : ι) in f, y < ↑(u a)

Tactic:
simp [forall_ennreal]

Goal state after: