mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
x : Q'.toExtension.Cotangent
hx : x ∈ Q'.toExtension.cotangentComplex.ker
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) ⟨x, hx⟩) = (δ Q' P') ⟨x, hx⟩

Tactic:
obtain ⟨⟨y, hy⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
ι' : Type w₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx : Extension.Cotangent.mk ⟨y, hy⟩ ∈ Q'.toExtension.cotangentComplex.ker
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩) =
    (δ Q' P') ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S

Tactic:
apply eq_maximalIdeal

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ (Ideal.map (algebraMap R S) (maximalIdeal R)).IsMaximal
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsGLB s (-sSup (-s))

Tactic:
← isLUB_neg',

Goal state after:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsLUB (-s) (- -sSup (-s))
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r₁ r₂ : ℝ≥0
h : r₂ ≤ r₁
⊢ ↑r₂ ≤ ↑r₁ - 0

Tactic:
by simp [show (r₂ : ℝ) ≤ r₁ from h]

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * 1 ≤ y
⊢ a ≤ y

Tactic:
mul_one

Goal state after:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a ≤ y
⊢ a ≤ y
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ ∃ n, 0 < n ∧ (↑n)⁻¹ < b

Tactic:
refine (exists_nat_gt b⁻¹).imp fun k hk ↦ ?_

Goal state after:
b : ℝ
hb : 0 < b
k : ℕ
hk : b⁻¹ < ↑k
⊢ 0 < k ∧ (↑k)⁻¹ < b
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : f ↑g ≠ 0
hg1' : 1 < g
⊢ f ↑g⁻¹ < 1

Tactic:
Units.val_inv_eq_inv_val,

Goal state after:
case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : f ↑g ≠ 0
hg1' : 1 < g
⊢ f (↑g)⁻¹ < 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

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

Tactic:
by cases f; cases g; congr

Goal state after:
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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    ∏ᶠ (i : HeightOneSpectrum R),
      ↑i.asIdeal ^ ↑((Associates.mk i.asIdeal).count (Associates.mk J).factors) *
        ↑i.asIdeal ^ (-↑((Associates.mk i.asIdeal).count (Associates.mk (span {a})).factors))

Tactic:
apply finprod_congr

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ ∀ (x : HeightOneSpectrum R),
    ↑x.asIdeal ^
        (↑((Associates.mk x.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors)) =
      ↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk J).factors) *
        ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors))
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x y : ℝ≥0
⊢ ofNNReal '' uIcc x y = uIcc ↑x ↑y

Tactic:
by simp [uIcc]

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

Goal state before:
pp: a : ℝ≥0∞
h : a ≠ 0
⊢ a / 0 = ∞

Tactic:
simp [div_eq_mul_inv, h]

Goal state after:
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
n : ℕ
⊢ ↑n * 1 = ↑n

Tactic:
mul_one

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
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * b⁻¹ * 1 = a * b⁻¹

Tactic:
mul_one

Goal state after:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * b⁻¹ = a * b⁻¹
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
n : ℤ
⊢ n * 1 = n

Tactic:
mul_one

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
n : ℤ
⊢ n = n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ∞
h : a / b = 1
⊢ b * 1 = b

Tactic:
mul_one

Goal state after:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ∞
h : a / b = 1
⊢ b = b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ a * 1 = a

Tactic:
mul_one

Goal state after:
a : ℝ≥0∞
⊢ a = a
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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I =
    ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))

Tactic:
apply finprod_congr

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∀ (x : HeightOneSpectrum R),
    ↑x.asIdeal ^ count K x I =
      ↑x.asIdeal ^
        (↑((Associates.mk x.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
          ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∀ᶠ (x : ι × α) in f ×ˢ 𝓝 x₀, p x) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
rw [eventually_swap_iff, Metric.eventually_nhds_prod_iff]
  constructor <;>
    · rintro ⟨a1, a2, a3, a4, a5⟩
      exact ⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩

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

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑a * ↑(⨆ i, f i) = ↑(⨆ i, a * f i)

Tactic:
NNReal.coe_iSup,

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑a * ⨆ i, ↑(f i) = ↑(⨆ i, a * f i)
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
⊢ SeparableSpace ↑s

Tactic:
by
  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, hst⟩
  lift t to Set s using hts
  refine ⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩
  rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun f g ↦ ↑(Finset.univ.sup fun b ↦ nndist (f b) (g b))) ⋯ ⋯
⊢ PseudoMetricSpace ((b : β) → X b)

Tactic:
refine i.replaceBornology fun s => ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun f g ↦ ↑(Finset.univ.sup fun b ↦ nndist (f b) (g b))) ⋯ ⋯
s : Set ((b : β) → X b)
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case pos
β : Type u_2
X : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (X b)
inst✝ : Nonempty β
f g : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
exact dist_pi_le_iff hr

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
⊢ ∃ y, I = Ideal.span {x, y}

Tactic:
by
  obtain ⟨y, rfl⟩ := exists_sup_span_eq (I.span_singleton_le_iff_mem.mpr hxI) (by simpa)
  simp_rw [← Ideal.span_union, Set.union_singleton, Set.pair_comm x]
  use y

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

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ ENNReal.ofReal ‖r‖ = ENNReal.ofReal r

Tactic:
norm_of_nonneg hr

Goal state after:
r : ℝ
hr : 0 ≤ r
⊢ ENNReal.ofReal r = ENNReal.ofReal r
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: case right
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
f : ι → E
x : ι
⊢ (fun x ↦ ‖f x‖) x ≤ ‖f‖

Tactic:
exact norm_le_pi_norm' f x

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoBotOrder α
⊢ (cobounded α).NeBot

Tactic:
by
  simp [Filter.neBot_iff, cobounded_eq_bot_iff, ← isBounded_univ, isBounded_iff_bddBelow_bddAbove]

Goal state after:
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J

Tactic:
have := FractionalIdeal.sup_mul_inf J' (spanSingleton R⁰ (I'.divMod I J') * I)

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 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) * (J' ⊔ spanSingleton R⁰ (I'.divMod I J') * I) =
    J' * (spanSingleton R⁰ (I'.divMod I J') * I)
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : l₁.NeBot
inst✝ : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst✝³] (s.domRestrict f)
hg : Continuous[instTopologicalSpaceSubtype, inst✝³] (s.domRestrict g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x ∈ s, f x = g x

Tactic:
obtain ⟨b, h⟩ :=
    @intermediate_value_univ₂_eventually₂ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) _ _
      (comap_coe_neBot_of_le_principal hl₁) (comap_coe_neBot_of_le_principal hl₂) _ _ hf hg
      (he₁.comap _) (he₂.comap _)

Goal state after:
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : l₁.NeBot
inst✝ : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst✝³] (s.domRestrict f)
hg : Continuous[instTopologicalSpaceSubtype, inst✝³] (s.domRestrict g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
b : ↑s
h : s.domRestrict f b = s.domRestrict g b
⊢ ∃ x ∈ s, f x = g x
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
⊢ sSup (f '' K) < y

Tactic:
obtain ⟨x, hx, h2x⟩ := hK.exists_isMaxOn h0K hf

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : K.Nonempty
hf : ContinuousOn f K
y : α
h : ∀ x ∈ K, f x < y
x : β
hx : x ∈ K
h2x : IsMaxOn f K x
⊢ sSup (f '' K) < y
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ ContinuousAt (fun x ↦ sSup (f x '' K)) x

Tactic:
rw [ContinuousAt, h2y, tendsto_order]

Goal state after:
case inr
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
⊢ (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {univ, ∅}

Tactic:
exact Or.inl (hs.eq_univ_of_unbounded hb ha)

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 ∈ sphere a r ↔ ‖b / a‖ = r

Tactic:
by simp [dist_eq_norm_div]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0 * 1

Tactic:
mul_one

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0
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
⊢ 1 < a ^ (m + 1)

Tactic:
exact hg.trans_le hm

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

Goal state before:
pp: ⊢ Pairwise fun x y ↦ 1 ≤ dist ↑x ↑y

Tactic:
simpa using Nat.pairwise_one_le_dist

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

Goal state before:
pp: ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℚ
h : dist x✝¹ x✝ < ε
⊢ dist |x✝¹| |x✝| ≤ dist x✝¹ x✝

Tactic:
simpa [Rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
s : Set β
hs : ∀ᶠ (x : β) in f, x ∈ s
b : α
hb : b ∈ upperBounds (u '' s)
⊢ ∀ x ∈ s, u x ∈ {x | (fun x ↦ (fun x1 x2 ↦ x1 ≤ x2) x b) x}

Tactic:
simpa [upperBounds] using hb

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)
⊢ ∀ᶠ (x : R) in map 0 f, r x 0

Tactic:
by simp_all only [eventually_map, Pi.zero_apply, eventually_true]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b > a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, ↑b_1 < b

Tactic:
· exact Eventually.of_forall fun x => (ha.1 x.2).trans_lt hb

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
by
  obtain (h | h) := eq_or_ne atTop (⊥ : Filter ι)
  · simp [h]
  · obtain ⟨h₁, h₂⟩ := Filter.atTop_neBot_iff.mp ⟨h⟩
    exact tendsto_atTop_isLUB h_mono <|
      h_mono.directed_le.directedOn_range.isLUB_csSup (Set.range_nonempty f) hbdd

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

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

Tactic:
← neg_lt_neg_iff,

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

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

Tactic:
← neg_lt_neg_iff,

Goal state after:
a b : EReal
⊢ - -b < -a ↔ b < -a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter ι
u : ι → α
a : α
hu : ∃ᶠ (i : ι) in f, a ≤ u i
hu_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ a ≤ limsup u f

Tactic:
by
  refine le_limsup_of_le hu_le fun b hb ↦ ?_
  obtain ⟨n, han, hnb⟩ := (hu.and_eventually hb).exists
  exact han.trans hnb

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ liminf u f ≤ x

Tactic:
rw [liminf_eq]
  refine sSup_le fun b hb => ?_
  have hbx : ∃ᶠ _ in f, b ≤ x := by
    contrapose! h
    exact hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))
  exact hbx.exists.choose_spec

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

Goal state before:
pp: case inr
ι : 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' < b''
hb''b : b'' < b
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b''

Tactic:
have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b'')

Goal state after:
case inr
ι : 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' < b''
hb''b : b'' < b
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b''
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case mk
β : Type u_4
inst✝² : Finite β
this : Fintype β
F : Filter (Finset β)
inst✝¹ : { filter := F }.LeAtTop
inst✝ : { filter := F }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
⊢ F = pure Finset.univ

Tactic:
refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)

Goal state after:
case mk
β : Type u_4
inst✝² : Finite β
this : Fintype β
F : Filter (Finset β)
inst✝¹ : { filter := F }.LeAtTop
inst✝ : { filter := F }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
⊢ ∀ s ∈ F, Finset.univ ∈ s