mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = ∞ → Nonempty ι
⊢ a⁻¹ = 0 → Nonempty ι

Tactic:
simpa

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr : r ≤ 0
⊢ (closedBall x r).Subsingleton

Tactic:
rcases hr.lt_or_eq with (hr | rfl)

Goal state after:
case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ (closedBall x r).Subsingleton

case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ (closedBall x 0).Subsingleton
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
simp [ofReal_of_nonpos hx]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist x y < ε₁ + ε₂

Tactic:
rw [add_comm, dist_comm]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist y x < ε₂ + ε₁
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Dense s ↔ ∀ r > 0, ∀ (x : α), x ∈ ⋃ c ∈ s, ball c r

Tactic:
mem_iUnion,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i, ∃ (_ : i ∈ s), x ∈ ball i r
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1)) =
    dist (f n) (f (n + 1)) + ∑ x ∈ Finset.Ico m n, dist (f x) (f (x + 1))

pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
add_comm

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ dist (f n) (f (n + 1)) + ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) =
    dist (f n) (f (n + 1)) + ∑ x ∈ Finset.Ico m n, dist (f x) (f (x + 1))

α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
    edist (f n) (f (n + 1)) + ∑ x ∈ Finset.Ico m n, edist (f x) (f (x + 1))

pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
add_comm

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ edist (f n) (f (n + 1)) + ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) =
    edist (f n) (f (n + 1)) + ∑ x ∈ Finset.Ico m n, edist (f x) (f (x + 1))

α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∀ (i : ↑c), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ↑i

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
x : R
hxI : x ∈ I
hx : x ≠ 0
⊢ Ideal.span {x} ≠ 0

Tactic:
simpa

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ dist (x', y') x = r ↔ dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r

Tactic:
Prod.dist_eq,

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ max (dist x' x.1) (dist y' x.2) = r ↔ dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

Tactic:
obtain hr | rfl | hr := lt_trichotomy r 0
  · simp [hr]
  · cases x
    simp_rw [← closedBall_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]
  · ext ⟨x', y'⟩
    simp_rw [Set.mem_union, Set.mem_prod, Metric.mem_closedBall, Metric.mem_sphere, Prod.dist_eq,
      max_eq_iff]
    refine or_congr (and_congr_right ?_) (and_comm.trans (and_congr_left ?_))
    all_goals rintro rfl; rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∀ (i : ↑c), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑i

Tactic:
simpa

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

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝¹ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
x : α
hx : x ∈ Icc a b
x✝ : {x} ∈ f
⊢ ↑f ≤ pure x

Tactic:
simpa

Goal state after:
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✝³] (Ico a b)
hab : a < b
this : closure[inst✝³] (Ico a b) = Ico a b
⊢ False

Tactic:
rw [closure_Ico hab.ne, Icc_eq_Ico_same_iff] at this

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
⊢ (Ioi d).Nonempty

Tactic:
simpa

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

Goal state before:
pp: case left
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
f : ι → E
⊢ ‖f‖ ∈ Set.range fun x ↦ ‖f x‖

Tactic:
rw [Pi.norm_def' f]
    obtain ⟨x, -, hx⟩ := (Finset.univ (α := ι)).exists_mem_eq_sup (by simp) (‖f ·‖₊)
    simp [hx]

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

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
⊢ cobounded α ≤ Filter.atBot ⊔ Filter.atTop

Tactic:
by
  have := Nonempty.of_isOrderBornology α
  intro s
  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]
  intro ⟨⟨b, _, hb⟩, ⟨a, _, ha⟩⟩
  refine ⟨⟨b, fun x hx ↦ ?_⟩, ⟨a, fun x hx ↦ ?_⟩⟩ <;> by_contra! hx'
  · exact hx (hb hx'.le)
  · exact hx (ha hx'.le)

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖v‖ + ‖u / v‖

Tactic:
add_comm

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
add_comm

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u * v‖ + ‖u‖ = ‖u * v‖ + ‖u‖
Module: Mathlib.Topology.MetricSpace.Cauchy

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

Tactic:
rintro _ ⟨⟨m', n'⟩, ⟨hm', hn'⟩, rfl⟩

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

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
t₁b' : t₁ < b
m : α
t₁m : m > t₁
H : Ioo t₁ m ⊆ s
t : α
hat : t₁ < t
ht : t < min m b
t' : α
ht' : t' ∈ Icc a t
h't' : t₁ < t'
⊢ t' ∈ s

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

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ tᶜ ∩ Ioc z y ∈ 𝓝[>] z

Tactic:
rw [← nhdsWithin_Ioc_eq_nhdsGT hz.2]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ tᶜ ∩ Ioc z y ∈ 𝓝[Ioc z y] z
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
this : emultiplicity p.asIdeal I = ↑(Multiset.count p.asIdeal (normalizedFactors I))
⊢ ↑(Multiset.count p.asIdeal (normalizedFactors I)) = ↑(multiplicity p.asIdeal I)

Tactic:
← this

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
p : HeightOneSpectrum R
this : emultiplicity p.asIdeal I = ↑(Multiset.count p.asIdeal (normalizedFactors I))
⊢ emultiplicity p.asIdeal I = ↑(multiplicity p.asIdeal I)
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ∃ f,
    Monotone f ∧
      ⋃ i, f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

Tactic:
obtain rfl | ⟨x, -⟩ := U.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ ∃ f,
    Monotone f ∧
      ⋃ i, f i = ∅ ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

case inr
α : Type u
inst✝ : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
⊢ ∃ f,
    Monotone f ∧
      ⋃ i, f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : r ≤ ↑n
⊢ r ≤ ↑↑n

Tactic:
simpa

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

Goal state before:
pp: case inr
α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
x : α
r : ℝ
hr : s ⊆ closedBall x r
⊢ IsCompact s

Tactic:
exact (isCompact_closedBall x r).of_isClosed_subset hc hr

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

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ s ≤ ↑n • r

Tactic:
simpa

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
n N : ℕ
hn : n ≤ N
⊢ u N ∈ s n

Tactic:
apply mem_of_subset_of_mem _ (h N).choose_spec

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := ⋯
n N : ℕ
hn : n ≤ N
⊢ ⋂ n, ⋂ (_ : n ≤ N), s n ⊆ s n
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)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ 0 ≤ m

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)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ (↑m + 1)
hm' : a ^ ↑m < g
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
· rw [← Int.lt_add_one_iff, ← zpow_lt_zpow_iff_right h₀, zpow_zero]
      exact hg.trans_le hm

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)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ (↑m + 1)
hm' : a ^ ↑m < g
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
have H {I' : Ideal R} (h : I' ≠ ⊥) : FiniteMultiplicity p.asIdeal I' :=
    FiniteMultiplicity.of_prime_left (prime p) h

Goal state after:
case inr.inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
H : ∀ {I' : Ideal R}, I' ≠ ⊥ → FiniteMultiplicity p.asIdeal I'
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
hu : BddAbove (range u)
⊢ BddAbove (u '' univ)

Tactic:
simpa

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

Goal state before:
pp: case inl.inl
y : EReal
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
h : ⊥ < y
htop : ⊤ = ⊤ → ⊤ = ⊤ → ⊥ = ⊥
⊢ ⊥ + ⊤ < y + ⊤

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
h : f.HasBasis p s
⊢ ⨅ i, ⨅ (_ : p i), sSup (u '' s i) = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, u a

Tactic:
simp only [sSup_image]

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

Goal state before:
pp: case refine_1
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊥ ∨ c ≠ ⊥

Tactic:
simpa

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

Goal state before:
pp: case refine_2
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊤ ∨ c ≠ ⊤

Tactic:
simpa

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

Goal state before:
pp: a b c : EReal
h : a < b + c
⊢ a < c + b

Tactic:
add_comm

Goal state after:
a b c : EReal
h : a < b + c
⊢ a < b + c
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
⊢ ∃ c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}, b < c

Tactic:
exact exists_lt_of_lt_csSup hu h

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

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

Tactic:
obtain ⟨a', ha', hd⟩ := exists_lt_add_left hd

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

Goal state before:
pp: x y : ℝ≥0∞
hy_top : y ≠ ∞
h_le : y ≤ x
⊢ ↑(x - y) = ↑x - ↑y

Tactic:
by
  lift y to ℝ≥0 using hy_top
  cases x with
  | top => simp [coe_nnreal_eq_coe_real]
  | coe x =>
    simp only [coe_nnreal_eq_coe_real, ← ENNReal.coe_sub, NNReal.coe_sub (mod_cast h_le), coe_sub]

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

Goal state before:
pp: case top_top
⊢ (⊤ * ⊤).toReal = ⊤.toReal * ⊤.toReal

Tactic:
| top_top =>

Goal state after:
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, ∀ s ≥ r, u n s ≤ b''

Tactic:
suffices ∀ᶠ r in atTop, u n r ≤ b' by
      simp only [eventually_atTop] at this
      rcases this with ⟨r, hr⟩
      exact ⟨r, fun s hs ↦ (hr s hs).trans hb''b.1⟩

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 : ι
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ b'
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_top
⊢ 0 < ⊤ * ⊤ ↔ 0 < ⊤ ∧ 0 < ⊤ ∨ ⊤ < 0 ∧ ⊤ < 0

Tactic:
| top_top =>

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

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

Tactic:
filter_upwards [(tendsto_order.1 (h_all n)).2 b hb] 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 < b
⊢ u n r ≤ c
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto f (pure (Fintype.card α)) l

Tactic:
rw [← map_card_atTop_of_fintype, tendsto_map'_iff]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Fintype α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto (f ∘ Finset.card) atTop l
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top_top
⊢ -⊤ * ⊤ = -(⊤ * ⊤)

Tactic:
| top_top =>

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

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

Tactic:
induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]

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

Goal state before:
pp: case top_top
⊢ ⊤ * ⊤ = ⊤ ↔ ⊤ = ⊥ ∧ ⊤ < 0 ∨ ⊤ < 0 ∧ ⊤ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ⊤ ∨ 0 < ⊤ ∧ ⊤ = ⊤

Tactic:
| top_top =>

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

Goal state before:
pp: a b c : EReal
hb : 0 ≤ b
hc : c ≤ 0
⊢ 0 ≤ -c

Tactic:
simpa

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

Goal state before:
pp: case zero
x : EReal
⊢ 0 • x = ↑0 * x

Tactic:
rw [zero_smul, Nat.cast_zero, zero_mul]

Goal state after: