mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : x < 0
h'x : x ≠ ⊥
⊢ x.toReal < 0

Tactic:
by
  lift x to ℝ using by aesop
  simpa using hx

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

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

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

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

Goal state before:
pp: x : EReal
hx : x ≤ 0
⊢ x.toENNReal = 0

Tactic:
rw [toENNReal, if_neg (fun h ↦ ?_)]
  · exact ENNReal.ofReal_of_nonpos (toReal_nonpos hx)
  · exact zero_ne_top <| top_le_iff.mp <| h ▸ hx

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 : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : n = 0
⊢ 0 = -0

Tactic:
neg_zero

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 : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : n = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ 0 = -0

Tactic:
neg_zero

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ 0 = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else if 0 < n then 0 else ∞

Tactic:
obtain ((_ | n) | n) := n

Goal state after:
case ofNat.zero
⊢ 0 ^ Int.ofNat 0 = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then 0 else ∞

case ofNat.succ
n : ℕ
⊢ 0 ^ Int.ofNat (n + 1) = if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then 0 else ∞

case negSucc
n : ℕ
⊢ 0 ^ Int.negSucc n = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then 0 else ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: n : ℤ
⊢ ∞ ^ n = if n = 0 then 1 else if 0 < n then ∞ else 0

Tactic:
obtain ((_ | n) | n) := n

Goal state after:
case ofNat.zero
⊢ ∞ ^ Int.ofNat 0 = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then ∞ else 0

case ofNat.succ
n : ℕ
⊢ ∞ ^ Int.ofNat (n + 1) = if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then ∞ else 0

case negSucc
n : ℕ
⊢ ∞ ^ Int.negSucc n = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then ∞ else 0
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ 0 < dist x y ↔ x ≠ y

Tactic:
by
  simpa only [not_le] using not_congr dist_le_zero

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

Goal state before:
pp: case h₁
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a f ≤ dist a b + dist b c + dist c d + dist d e + dist e f

Tactic:
apply le_trans (dist_triangle4 a d e f)

Goal state after:
case h₁
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a d + dist d e + dist e f ≤ dist a b + dist b c + dist c d + dist d e + dist e f
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[inst✝¹] t

Tactic:
apply subset_countable_closure_of_almost_dense_set

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this✝ : UniformSpace X := ⋯
this : (𝓤 X).IsCountablyGenerated
⊢ ∀ U ∈ 𝓤 X, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), edist x y = ENNReal.ofReal (d x y)

Tactic:
simp [hd, edist_dist]

Goal state after:
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (nhds a).IsCountablyGenerated

Tactic:
rw [nhds_discrete]; exact isCountablyGenerated_pure

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

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : s ∈ cobounded α
⊢ s ∈ Filter.atTop

Tactic:
rw [← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove] at hs

Goal state after:
α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : BddBelow sᶜ ∧ BddAbove sᶜ
⊢ s ∈ Filter.atTop
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:
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.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_3
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
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J') ∘ₗ (↑I).subtype) ↑J' ≤ Submodule.comap (↑I).subtype ↑J

Tactic:
Submodule.comap_comp,

Goal state after:
case refine_3
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
⊢ Submodule.comap (↑I).subtype (Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J') ≤
    Submodule.comap (↑I).subtype ↑J
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ a ∈ ball 1 r ↔ ‖a‖ < r

Tactic:
by rw [mem_ball, dist_one_right]

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

Goal state before:
pp: case inr.inl
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
have Z := A b h'b a h'a
    rwa [edist_comm] at Z

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖b / a‖ < r

Tactic:
rw [mem_ball, dist_eq_norm_div]

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
⊢ False

Tactic:
rcases hxmin x ⟨hxH, (one_le_pow_of_one_le'  h₀.le _).trans_lt hnx⟩ with ⟨y, ⟨hyH, hy₀⟩, hxy⟩

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
⊢ False
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case mpr.coe
r : ℝ
h : ↑r ≠ ⊥
⊢ ⊤ + ↑r = ⊤

Tactic:
exact top_add_of_ne_bot h

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

Goal state before:
pp: x : EReal
⊢ ⊤ + x = ⊤ ↔ x ≠ ⊥

Tactic:
constructor <;> intro h
  · rintro rfl
    rw [add_bot] at h
    exact bot_ne_top h
  · cases x with
    | bot => contradiction
    | top => rfl
    | coe r => exact top_add_of_ne_bot h

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

Goal state before:
pp: case mpr.inr
ι₁ : 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)
l' : α
hl' : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l)

Tactic:
tendsto_nhds_unique h (hl'.comp hg)

Goal state after:
case mpr.inr
ι₁ : 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)
l' : α
hl' : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l')
Module: Mathlib.Topology.Order.MonotoneConvergence

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

Tactic:
rintro _ ⟨b, rfl⟩

Goal state after:
case left
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ f b ≤ a
Module: Mathlib.Data.EReal.Operations

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

Tactic:
neg_zero

Goal state after:
a : EReal
⊢ 0 < a ↔ 0 < a
Module: Mathlib.Data.EReal.Operations

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

Tactic:
neg_zero

Goal state after:
a : EReal
⊢ 0 ≤ a ↔ 0 ≤ a
Module: Mathlib.Data.EReal.Operations

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

Tactic:
neg_zero

Goal state after:
a : EReal
⊢ a < 0 ↔ a < 0
Module: Mathlib.Data.EReal.Operations

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

Tactic:
neg_zero

Goal state after:
a : EReal
⊢ a ≤ 0 ↔ a ≤ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
⊢ x - y ≤ 0 ↔ x ≤ y

Tactic:
cases x <;> cases y <;> simp [← EReal.coe_sub]

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

Goal state before:
pp: x y : EReal
⊢ 0 < x - y ↔ y < x

Tactic:
cases x <;> cases y <;> simp [← EReal.coe_sub]

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

Goal state before:
pp: α : Type u_2
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter α
x : α
hx : (𝓝 x ⊓ f).NeBot
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
this : (𝓝 x ⊓ f).limsSup = x
⊢ x ≤ f.limsSup

Tactic:
refine this ▸ limsSup_le_limsSup_of_le inf_le_right ?_ hb

Goal state after:
α : Type u_2
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter α
x : α
hx : (𝓝 x ⊓ f).NeBot
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
this : (𝓝 x ⊓ f).limsSup = x
⊢ IsCobounded (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x ⊓ f)
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
⊢ ContinuousAt f x

Tactic:
rcases (hf x) with ⟨K, t, ht, hK⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hK : LipschitzOnWith K f t
⊢ ContinuousAt f x
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case neg
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : ¬y = ⊤
hxy : ¬x = y
⊢ x < y + (t - z)

Tactic:
rw [← add_zero x]

Goal state after:
case neg
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : ¬y = ⊤
hxy : ¬x = y
⊢ x + 0 < y + (t - z)
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 : ι
this : ∀ᶠ (r : α) in atTop, u n r ≤ b'
⊢ ∃ r, ∀ s ≥ r, u n s ≤ b''

Tactic:
simp only [eventually_atTop] at this

Goal state after:
ι : 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 : ι
this : ∃ a, ∀ (b : α), a ≤ b → u n b ≤ b'
⊢ ∃ r, ∀ s ≥ r, u n s ≤ b''
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: 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

Tactic:
filter_upwards [(tendsto_order.1 (h_all n)).2 _ h.some_mem.1] with r hr

Goal state after:
ι : 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 : α
hr : u n r < h.some
⊢ u n r ≤ h.some
Module: Mathlib.Data.EReal.Operations

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

Tactic:
neg_zero

Goal state after:
a b : EReal
⊢ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ 0 ≤ a ∧ b ≤ -0 ∨ a ≤ 0 ∧ -0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
neg_zero

Goal state after:
a b : EReal
⊢ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ a = ⊤ ∧ b < 0 ∨ -0 < a ∧ b = ⊥ ∨ a = ⊥ ∧ 0 < b ∨ a < -0 ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
neg_zero

Goal state after:
a b : EReal
⊢ a = ⊤ ∧ b < 0 ∨ 0 < a ∧ b = ⊥ ∨ a = ⊥ ∧ 0 < b ∨ a < 0 ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ 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
⊢ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f ≤ s.sup' hs fun i ↦ limsup (F i) f

Tactic:
have h₃ : ∃ i ∈ s, f.IsCoboundedUnder (· ≤ ·) (F i) := by
      rcases hs with ⟨i, i_s⟩
      use i, i_s
      exact h₁ i i_s

Goal state after:
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)
⊢ limsup (fun a ↦ s.sup' hs fun i ↦ F i a) f ≤ s.sup' hs fun i ↦ limsup (F i) f
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
hL : L.NeBot
⊢ 1 ≤ ∏'[L] (i : ι), g i

Tactic:
exact hg.hasProd.one_le h

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
h : ¬Multipliable f L
⊢ 0 ≤ ∏'[L] (x : ι), f x

Tactic:
simp [tprod_eq_one_of_not_multipliable h]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∏'[L] (x : ι), f x

Tactic:
by
  by_cases h : Multipliable f L
  · by_cases hbot : L.NeBot
    · exact h.hasProd.nonneg hf
    · simpa [tprod_bot hbot] using finprod_nonneg hf
  · simp [tprod_eq_one_of_not_multipliable h]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : UniformSpace α
inst✝¹ : IsUniformGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 1 ≤ f x}
h1 : ∀ (x : ↑s), |f ↑x|ₘ = f ↑x
h2 : ∀ (x : ↑sᶜ), |f ↑x|ₘ = (f ↑x)⁻¹
⊢ ((Multipliable fun x ↦ f ↑x) ∧ Multipliable fun x ↦ (f ↑x)⁻¹) ↔ Multipliable f

Tactic:
by simp only [multipliable_inv_iff, multipliable_subtype_and_compl]

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

Goal state before:
pp: case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x ↦ a
⊢ a = 1

pp: case refine_2
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
⊢ a = 1 → Multipliable fun x ↦ a

Tactic:
· by_contra ha
    have : {a}ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha)
    have : Finite β := by
      simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this
    exact not_finite β

Goal state after:
case refine_2
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
⊢ a = 1 → Multipliable fun x ↦ a
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case disjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
rw [disjoint_iff_inf_le]

Goal state after:
case disjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Set.range Nat.cast ⊓ Set.range Int.negSucc ⊆ ⊥
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 α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : (mulSupport f).Finite
⊢ tprod (f ∘ g) = ∏' (b : β), f b

Tactic:
have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage hg.injOn

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : (mulSupport f).Finite
hfg_fin : (mulSupport (f ∘ g)).Finite
⊢ tprod (f ∘ g) = ∏' (b : β), f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun i ↦ f i * a₂) (a₁ * a₂) L
⊢ HasSum f a₁ L

Tactic:
simpa only [mul_inv_cancel_right₀ h] using H.mul_right a₂⁻¹

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
⊢ tprod (f ∘ g) = ∏' (b : β), f b

Tactic:
have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by
      rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
    simp_rw [tprod_def, SummationFilter.support_eq_univ, Set.inter_univ,
      show (unconditional β).HasSupport by infer_instance,
      show (unconditional γ).HasSupport by infer_instance, true_and,
      if_neg hf_fin, if_neg hf_fin', Multipliable]
    simp [hg.hasProd_iff (mulSupport_subset_iff'.1 hf)]

Goal state after: