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

Goal state before:
pp: 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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk J * Associates.mk J').factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a * a'})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
      (↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors))

Tactic:
Associates.count_mul hJ_ne_zero hJ'_ne_zero hv,

Goal state after:
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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors +
          (Associates.mk v.asIdeal).count (Associates.mk J').factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a * a'})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
      (↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors))
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x z : EReal
h : x < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
by
  obtain ⟨a, ha₁, ha₂⟩ := exists_between h
  induction a with
  | bot => exact (not_lt_bot ha₁).elim
  | coe a₀ => exact ⟨a₀, ha₁, ha₂⟩
  | top => exact (not_top_lt ha₂).elim

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

Goal state before:
pp: x y : ℝ
⊢ WithBot.some '' WithTop.some '' Ioc x y = Ioc ↑x ↑y

Tactic:
WithTop.image_coe_Ioc,

Goal state after:
x y : ℝ
⊢ WithBot.some '' Ioc ↑x ↑y = Ioc ↑x ↑y
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
h0 : a ≠ 0
ht : a ≠ ∞
⊢ a * a⁻¹ = 1

Tactic:
lift a to ℝ≥0 using ht

Goal state after:
a : ℝ≥0
h0 : ↑a ≠ 0
⊢ ↑a * (↑a)⁻¹ = 1
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
⊢ count K v (I ^ (-0)) = -count K v (I ^ 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
⊢ count K v (I ^ 0) = -count K v (I ^ 0)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ha
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ 0 ∨ c⁻¹ ≠ ∞

pp: case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0

Tactic:
· simpa

Goal state after:
case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case hb
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ b ≠ ∞ ∨ c⁻¹ ≠ 0

Tactic:
· simpa

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

Goal state before:
pp: a : ℝ≥0∞
hz : a ≠ 0
ht : a ≠ ∞
⊢ a / 2 < a

Tactic:
lift a to ℝ≥0 using ht

Goal state after:
a : ℝ≥0
hz : ↑a ≠ 0
⊢ ↑a / 2 < ↑a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ ∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))

Tactic:
have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'

Goal state after:
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))

Tactic:
have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'

Goal state after:
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds_nhds]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : x ∈ ball y ε
⊢ ∃ ε' < ε, x ∈ ball y ε'

Tactic:
simpa [mem_ball] using exists_between' h

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
⊢ p y

Tactic:
by
  obtain ⟨R, hR, h⟩ : ∃ R ≥ dist y x, ∀ z : α, z ∈ closedBall x R → p z :=
    frequently_iff.1 H (Ici_mem_atTop (dist y x))
  exact h _ hR

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds_nhds]

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x✝¹ x✝ : α
⊢ edist x✝¹ x✝ = edist x✝ x✝¹

Tactic:
simp only [edist_dist, dist_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
| J * ∏ q ∈ s \ {p}, q.asIdeal

Tactic:
← mul_one (J * _)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
| (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ g * iInf h

Tactic:
rw [mul_iInf]
  exact le_ciInf H

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

Goal state before:
pp: c : ℝ≥0
⊢ ball 0 ↑c = Ico 0 c

Tactic:
by ext x; simp

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

Goal state before:
pp: c : ℝ≥0
⊢ closedBall 0 ↑c = Icc 0 c

Tactic:
by ext x; simp

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ interior (Icc a b) = Ioo a b

Tactic:
by
  rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]

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

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ Function.eval default ⁻¹' sphere (x default) 0

Tactic:
intro x hx

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x✝ : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → X x
hx : x ∈ sphere x✝ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsClosed[inst✝¹] s
⊢ IsClosed[inst✝¹] ↑(upperClosure s)

Tactic:
by
  obtain rfl | h₁ := s.eq_empty_or_nonempty
  · simp
  by_cases h₂ : BddBelow s
  · exact upperClosure_eq_Ici_csInf h₁ h₂ hs ▸ isClosed_Ici
  · exact upperClosure_eq_bot h₂ ▸ isClosed_univ

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

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ r.toNNReal = ‖r‖₊

Tactic:
rw [Real.toNNReal_of_nonneg hr]
  congr
  rw [Real.norm_eq_abs r, abs_of_nonneg hr]

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

Goal state before:
pp: case refine_1
α : 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)
l : β
hl : l < sInf (f '' Ioo x y)
⊢ ∀ᶠ (b : α) in 𝓝[>] x, l < f b

Tactic:
rcases h_nonempty with ⟨p, hy, hx⟩
    filter_upwards [Ioo_mem_nhdsGT (hy.trans hx)] with w hw
    exact hl.trans_le <| csInf_le h_bdd (mem_image_of_mem _ hw)

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

Goal state before:
pp: case refine_1
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
⊢ ∀ x ∈ ↑I, ((Algebra.lsmul R R K) (I'.divMod I J')) x ∈ ↑I'

Tactic:
intro x hx

Goal state after:
case refine_1
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
x : K
hx : x ∈ ↑I
⊢ ((Algebra.lsmul R R K) (I'.divMod I J')) x ∈ ↑I'
Module: Mathlib.RingTheory.DedekindDomain.Factorization

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

Tactic:
intro x hx

Goal state after:
case refine_2
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
x : K
hx : x ∈ ↑J
⊢ x ∈ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J'
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
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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J')

Tactic:
intro x hx

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
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 : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
x : K
hx : x ∈ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J'
⊢ x ∈ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J')
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:
by simp [ediam_insert]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ closedBall 1 r} ↔ x ∈ closedBall a r

Tactic:
rw [mem_closedBall_iff_norm'']

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ closedBall 1 r} ↔ ‖x / a‖ ≤ r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ closedBall a r ↔ ‖b‖ ≤ r

Tactic:
rw [mem_closedBall_iff_norm'']

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖a * b / a‖ ≤ r ↔ ‖b‖ ≤ r
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
⊢ map (algebraMap S R) p = ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

Tactic:
rw [← finprod_heightOneSpectrum_factorization (I := p.map (algebraMap S R)) h]

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (algebraMap S R) p) =
    ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S
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:
by
  rw [← Int.comap_cast_atTop (R := R)]; exact h.comap _

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

Goal state before:
pp: α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
c : α
h : ∃ r, (closedBall c r)ᶜ ⊆ s
⊢ s ∈ cocompact α

Tactic:
rcases h with ⟨r, h⟩

Goal state after:
α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ s ∈ cocompact α
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ map (fun a ↦ a - k) atTop = atTop

Tactic:
by
  simp_rw [sub_eq_add_neg]
  apply map_add_atTop_eq

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : StrictAntiOn f (Icc s t) → False
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
⊢ f x < f y

Tactic:
replace : Icc x y ⊆ Icc s t := Icc_subset_Icc hsx hyt

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
this : Icc x y ⊆ Icc s t
⊢ f x < f y
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 : ℕ → α := ⋯
n N : ℕ
hn : n ≤ N
⊢ ⋂ n, ⋂ (_ : n ≤ N), s n ⊆ s n

Tactic:
intro x hx

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 : ℕ → α := fun N ↦ ⋯.some
n N : ℕ
hn : n ≤ N
x : α
hx : x ∈ ⋂ n, ⋂ (_ : n ≤ N), s n
⊢ x ∈ s n
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∀ x ∈ s, f x = ↑(f x).toNNReal

Tactic:
intro x hx

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
x : α
hx : x ∈ s
⊢ f x = ↑(f x).toNNReal
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : (↑s).Pairwise fun i j ↦ g i ≠ 0 ∨ g j ≠ ∞
⊢ ∏ i ∈ s, f i / g i = (∏ i ∈ s, f i) / ∏ i ∈ s, g i

Tactic:
simp only [div_eq_mul_inv, prod_inv_distrib hg, ← Finset.prod_mul_distrib]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB s (a, b)
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))

Tactic:
isLUB_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (fst '' s) (a, b).1 ∧ IsLUB (snd '' s) (a, b).2
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x ↦ True) = liminf u f

Tactic:
simp [bliminf_eq, liminf_eq]

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

Goal state before:
pp: case bot.bot
h1 : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(⊥ + ⊥) = -⊥ - ⊥

Tactic:
try tauto

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

Goal state before:
pp: case bot.coe
a✝ : ℝ
h1 : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(⊥ + ↑a✝) = -⊥ - ↑a✝

Tactic:
try tauto

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

Goal state before:
pp: case bot.top
h1 : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(⊥ + ⊤) = -⊥ - ⊤

Tactic:
try tauto

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(↑a✝ + ⊥) = -↑a✝ - ⊥

Tactic:
try tauto

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(↑a✝¹ + ↑a✝) = -↑a✝¹ - ↑a✝

Tactic:
try tauto

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(↑a✝¹ + ↑a✝) = -↑a✝¹ - ↑a✝
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
h1 : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(↑a✝ + ⊤) = -↑a✝ - ⊤

Tactic:
try tauto

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

Goal state before:
pp: case top.bot
h1 : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊥
⊢ -(⊤ + ⊥) = -⊤ - ⊥

Tactic:
try tauto

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

Goal state before:
pp: case top.coe
a✝ : ℝ
h1 : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(⊤ + ↑a✝) = -⊤ - ↑a✝

Tactic:
try tauto

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

Goal state before:
pp: case top.top
h1 : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(⊤ + ⊤) = -⊤ - ⊤

Tactic:
try tauto

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
⊢ ∀ ⦃c : β⦄, c < x → c < limsup u f

Tactic:
intro y y_x

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
y : β
y_x : y < x
⊢ y < limsup u f
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
inst✝ : Fintype α
⊢ Tendsto Finset.card atTop (pure (Fintype.card α))

Tactic:
rw [Tendsto, map_card_atTop_of_fintype]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
⊢ ∀ (x : R), c < x → F.limsSup ≤ x

Tactic:
intro x hx

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
x : R
hx : c < x
⊢ F.limsSup ≤ x
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
⊢ ∃ l, l < F.limsSup

Tactic:
simpa [IsBot] using! not_bot

Goal state after: