mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_4
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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ⊤ ≤
    Submodule.map (Submodule.comap (↑I').subtype ↑J').mkQ
      (Submodule.comap (↑I').subtype (Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I))

Tactic:
H,

Goal state after:
case refine_4
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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ⊤ ≤
    Submodule.map (Submodule.comap (↑I').subtype ↑J').mkQ
      (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I))
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
x y : X
inst✝ : PseudoEMetricSpace X
⊢ ediam {x, y} = edist x y

Tactic:
simp [ediam_insert]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0

Tactic:
simpa using nontrivialTopology_iff_exists_norm_ne_zero' (E := E).not

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 atTop, p x
⊢ ∀ᶠ (n : ℤ) in atTop, p ↑n

Tactic:
← Int.comap_cast_atTop (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 atTop, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atTop, p ↑n
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
have has : a ∈ s := mem_of_mem_nhdsWithin self_mem_Ici hs
  refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩
  · filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      (h_mono has hxs hxa)
  · rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
    have : a < c := not_le.1 fun h => hac.not_ge <| h_mono hcs has h
    filter_upwards [hs, Ico_mem_nhdsGE this]
    rintro x hx ⟨_, hxc⟩
    exact (h_mono hx hcs hxc.le).trans_lt hcb

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

Goal state before:
pp: case cons.refine_2
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = ∞
j : ι
hj : j ∈ s
⊢ f j ≠ 0

Tactic:
exact imp_iff_not_or.2 (hf (by simp [hj]) (by simp) <| ne_of_mem_of_not_mem hj hi).symm hi₀

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

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f 0

Tactic:
exact ⟨0, by simp_all only [eventually_map, Pi.zero_apply, eventually_true]⟩

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

Goal state before:
pp: case bot.bot
⊢ ⊥ - ⊥ ≤ 0 ↔ ⊥ ≤ ⊥

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case bot.coe
a✝ : ℝ
⊢ ⊥ - ↑a✝ ≤ 0 ↔ ⊥ ≤ ↑a✝

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case bot.top
⊢ ⊥ - ⊤ ≤ 0 ↔ ⊥ ≤ ⊤

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ ↑a✝ - ⊥ ≤ 0 ↔ ↑a✝ ≤ ⊥

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ - ↑a✝ ≤ 0 ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ ↑a✝ - ⊤ ≤ 0 ↔ ↑a✝ ≤ ⊤

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case top.bot
⊢ ⊤ - ⊥ ≤ 0 ↔ ⊤ ≤ ⊥

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ ⊤ - ↑a✝ ≤ 0 ↔ ⊤ ≤ ↑a✝

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case top.top
⊢ ⊤ - ⊤ ≤ 0 ↔ ⊤ ≤ ⊤

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case bot.bot
⊢ 0 < ⊥ - ⊥ ↔ ⊥ < ⊥

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case bot.coe
a✝ : ℝ
⊢ 0 < ⊥ - ↑a✝ ↔ ↑a✝ < ⊥

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case bot.top
⊢ 0 < ⊥ - ⊤ ↔ ⊤ < ⊥

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊥ ↔ ⊥ < ↑a✝

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ 0 < ↑a✝¹ - ↑a✝ ↔ ↑a✝ < ↑a✝¹

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊤ ↔ ⊤ < ↑a✝

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case top.bot
⊢ 0 < ⊤ - ⊥ ↔ ⊥ < ⊤

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ 0 < ⊤ - ↑a✝ ↔ ↑a✝ < ⊤

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case top.top
⊢ 0 < ⊤ - ⊤ ↔ ⊤ < ⊤

Tactic:
simp [← EReal.coe_sub]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Subsingleton α
⊢ ClusterPt f.limsSup f

Tactic:
simp_all [ClusterPt, Filter.eq_top_of_neBot]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
⊢ b₁ ∈ t → ∀ x ∈ s, ∀ y ∈ t, edist (f a₁ b₁) (f x y) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t

Tactic:
hb₁

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
⊢ ∀ x ∈ s, ∀ y ∈ t, edist (f a₁ b₁) (f x y) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t
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
⊢ (if h : (Set.Ioo c b).Nonempty then h.some else c) < b

Tactic:
split_ifs with h

Goal state after:
case pos
ι : 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
h : (Set.Ioo c b).Nonempty
⊢ h.some < b

case neg
ι : 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
h : ¬(Set.Ioo c b).Nonempty
⊢ c < b
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
⊢ ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ if h : (Set.Ioo c b).Nonempty then h.some else c

Tactic:
split_ifs with h

Goal state after:
case pos
ι : 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
h : (Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ h.some

case neg
ι : 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
h : ¬(Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ c
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 : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ if h : (Set.Ioo c b).Nonempty then h.some else c

Tactic:
split_ifs with h

Goal state after:
case pos
ι : 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 : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
h : (Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ h.some

case neg
ι : 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 : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
h : ¬(Set.Ioo c b).Nonempty
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ c
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: β : Type u_4
γ : Type u_5
inst✝ : DecidableEq β
i : β → γ
j : γ → β
h : Function.LeftInverse j i
a : β
⊢ a ∈ Finset.image j {i a}

Tactic:
by simp only [Finset.image_singleton, h a, Finset.mem_singleton]

Goal state after:
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
⊢ liminf u f ≤ limsup v f

Tactic:
rcases f.eq_or_neBot with rfl | _
  · exact (frequently_bot h).rec
  have h₃ : f.IsCoboundedUnder (· ≥ ·) u := by
    obtain ⟨a, ha⟩ := h₂.eventually_le
    apply IsCoboundedUnder.of_frequently_le (a := a)
    exact (h.and_eventually ha).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x
  have h₄ : f.IsCoboundedUnder (· ≤ ·) v := by
    obtain ⟨a, ha⟩ := h₁.eventually_ge
    apply IsCoboundedUnder.of_frequently_ge (a := a)
    exact (ha.and_frequently h).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x
  refine (le_limsup_iff h₄ h₂).2 fun y y_v ↦ ?_
  have := (le_liminf_iff h₃ h₁).1 (le_refl (liminf u f)) y y_v
  exact (h.and_eventually this).mono fun x ⟨ux_vx, y_ux⟩ ↦ y_ux.trans_le ux_vx

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

Goal state before:
pp: case bot.bot
hx : 0 ≤ ⊥
⊢ (⊥ * ⊥).toENNReal = ⊥.toENNReal * ⊥.toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

Goal state before:
pp: case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
⊢ (⊥ * ↑a✝).toENNReal = ⊥.toENNReal * (↑a✝).toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

Goal state before:
pp: case bot.top
hx : 0 ≤ ⊥
⊢ (⊥ * ⊤).toENNReal = ⊥.toENNReal * ⊤.toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊥).toENNReal = (↑a✝).toENNReal * ⊥.toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

Goal state before:
pp: case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
⊢ (↑a✝¹ * ↑a✝).toENNReal = (↑a✝¹).toENNReal * (↑a✝).toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

Goal state before:
pp: case top.bot
hx : 0 ≤ ⊤
⊢ (⊤ * ⊥).toENNReal = ⊤.toENNReal * ⊥.toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

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

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

Goal state before:
pp: case top.top
hx : 0 ≤ ⊤
⊢ (⊤ * ⊤).toENNReal = ⊤.toENNReal * ⊤.toENNReal

Tactic:
{· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ v', f b

Tactic:
refine ⟨s.image g, fun t ht => ?_⟩
    simp only [← prod_preimage _ _ hg.injOn _ fun x _ => hf x]
    exact ⟨_, (image_subset_iff_subset_preimage _).1 ht, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
⊢ f n = (if n = b then f n else 1) * update f b 1 n

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
h : n = b
⊢ f n = f n * update f b 1 n

case neg
α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
h : ¬n = b
⊢ f n = 1 * update f b 1 n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

Tactic:
by
  rcases L.neBot_or_eq_bot with _ | hL
  · constructor
    · exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩
    · exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩
  · simp [Summable, HasSum, hL]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ dist x' y'

Tactic:
refine (dist_pi_le_iff dist_nonneg).2 fun b =>
    (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b) <;> refine Icc_subset_uIcc ?_
  exacts [⟨hx.1 _, hx.2 _⟩, ⟨hy.1 _, hy.2 _⟩]

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
have : IsTrans X fun x y => d x y = 0 := by
    refine ⟨fun a b c hab hbc ↦ ?_⟩
    rw [← nonpos_iff_eq_zero]
    simpa only [nonpos_iff_eq_zero, hab, hbc, dist_self c, max_self, mul_zero] using hd a b c c

Goal state after:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
this : IsTrans X fun x y ↦ d x y = 0
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

Tactic:
have (j : ℕ) : ∃ᶠ k in atTop, ∃ n ≥ j, y n ∈ closure {x k} := by
      refine frequently_atTop.2 fun a => ?_
      have := (Filter.eventually_all_finite (by simp : (Iic a).Finite)).2 fun i hi => hm i
      simp only [mem_Iic, eventually_atTop] at this
      obtain ⟨c, hc⟩ := this
      obtain ⟨b, hb⟩ := mem_iUnion.1 (hy (c + j))
      refine ⟨b, ?_, c + j, j.le_add_left c, hb⟩
      by_contra! hab
      simp_all [hc (c + j) (c.le_add_right j) b hab.le]

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
this : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, y n ∈ closure[inst✝¹] {x k}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: x : ℝ≥0∞
xt : x ≠ ∞
⊢ (𝓝 x).HasBasis (fun x ↦ 0 < x) fun ε ↦ Icc (x - ε) (x + ε)

Tactic:
simpa only [pos_iff_ne_zero] using hasBasis_nhds_of_ne_top' xt

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

Goal state before:
pp: case pos
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ε = ∞
⊢ min 1 (ε / 2) < ε

Tactic:
simp [hε_top]

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (pkg'.extend f ∘ pkg.map pkg' g) (pkg.coe a) = pkg.extend (f ∘ g) (pkg.coe a)

Tactic:
by
    rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]
    rfl

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

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

Tactic:
by rw [← comp_apply, h, comp_apply]

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
x y : X
⊢ (if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0) = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i

Tactic:
split_ifs with h

Goal state after:
case pos
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
x y : X
h : ∃ n, (x, y) ∉ U n
⊢ (1 / 2) ^ Nat.find h = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i

case neg
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
x y : X
h : ¬∃ n, (x, y) ∉ U n
⊢ 0 = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i