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

Goal state before:
pp: case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
hx : (Cotangent.map P.toInfinitesimal) x ∈ P.infinitesimal.cotangentComplex.ker
⊢ x ∈ P.cotangentComplex.ker

Tactic:
simpa [← CotangentSpace.map_cotangentComplex,
      map_eq_zero_iff _ (CotangentSpace.map_toInfinitesimal_bijective P).injective] using hx

Goal state after:
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₂
Q : Generators S T ι
P : Generators R S σ
⊢ (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)).range ≤
    (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker

Tactic:
rw [range_liftBaseChange, coe_range, Submodule.span_le, Set.range_subset_iff]
  rintro ⟨x, _⟩
  obtain ⟨⟨(x : P.Ring), x_in⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
  ext; suffices (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom x) ∈ Q.toExtension.ker ^ 2 by
    simpa [Ideal.toCotangent_eq_zero]
  rw [← Generators.ker, Generators.ker_eq_ker_aeval_val] at x_in
  rw [toComp_toAlgHom, toAlgHom_ofComp_rename, Generators.algebraMap_eq, RingHom.coe_coe,
    x_in, RingHom.map_zero]
  exact Ideal.zero_mem _

Goal state after:
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
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
hq : p.primesOver S = {q}
inst✝³ : Module.Finite R S
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s✝ : Finset S
hs : Submodule.span R ↑s✝ = ⊤
x s : S
hsq : s ∈ q.primeCompl
r : R
hr : r ∉ p
t : S
e' : (algebraMap R S) r = s * t
⊢ (algebraMap S (Localization.AtPrime q)) t * (algebraMap S (Localization.AtPrime q)) x ∈
    Submodule.span (Localization.AtPrime p) (Set.range ⇑(algebraMap S (Localization.AtPrime q)))

Tactic:
← map_mul

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
hq : p.primesOver S = {q}
inst✝³ : Module.Finite R S
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s✝ : Finset S
hs : Submodule.span R ↑s✝ = ⊤
x s : S
hsq : s ∈ q.primeCompl
r : R
hr : r ∉ p
t : S
e' : (algebraMap R S) r = s * t
⊢ (algebraMap S (Localization.AtPrime q)) (t * x) ∈
    Submodule.span (Localization.AtPrime p) (Set.range ⇑(algebraMap S (Localization.AtPrime q)))
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
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset R
hs : Ideal.span ↑s = RingHom.ker (algebraMap R S)
⊢ ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')

Tactic:
have (x : s) : algebraMap R (Localization.AtPrime p) x.1 = 0 := by
    apply H
    simp [localRingHom_to_map, -FaithfulSMul.algebraMap_eq_zero_iff,
      show algebraMap R S _ = 0 from hs.le (Ideal.subset_span x.2)]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
inst✝² : p.IsPrime
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset R
hs : Ideal.span ↑s = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s), (algebraMap R (Localization.AtPrime p)) ↑x = 0
⊢ ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x : Localization M'
⊢ x ∈
      (LinearMap.extendScalarsOfIsLocalization M' (Localization M')
          ((IsLocalizedModule.map M' (Algebra.linearMap P.Ring (Localization M'))
              (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)
            (Algebra.linearMap P.Ring S))).ker ↔
    x ∈ RingHom.ker fQ

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M' x

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
⊢ IsLocalization.mk' (Localization M') x ⟨s, hs⟩ ∈
      (LinearMap.extendScalarsOfIsLocalization M' (Localization M')
          ((IsLocalizedModule.map M' (Algebra.linearMap P.Ring (Localization M'))
              (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)
            (Algebra.linearMap P.Ring S))).ker ↔
    IsLocalization.mk' (Localization M') x ⟨s, hs⟩ ∈ RingHom.ker fQ
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.inf fun i ↦ (S i)ᶜ)) = ∑ t ∈ s.powerset, (-1) ^ #t * ↑(#(t.inf S))

Tactic:
by
  simpa using inclusion_exclusion_sum_inf_compl (G := ℤ) s S (f := 1)

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨆ x, 0 = 0

Tactic:
· exact ciSup_const

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

Goal state before:
pp: r : ℝ
⊢ r.toNNReal = 0 ↔ r ≤ 0

Tactic:
simpa [-toNNReal_pos] using not_iff_not.2 (@toNNReal_pos r)

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

Goal state before:
pp: case pos
x : EReal
h : x ≠ ⊥
h' : x = ⊤
⊢ ↑x.toReal ≤ x

pp: case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑x.toReal ≤ x

Tactic:
· simp only [h', le_top]

Goal state after:
case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑x.toReal ≤ x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ WithBot.some '' WithTop.some '' Ioi x = Ioo ↑x ⊤

Tactic:
WithTop.image_coe_Ioi,

Goal state after:
x : ℝ
⊢ WithBot.some '' Ioo ↑x ⊤ = Ioo ↑x ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Ioc ↑x ↑y = Ioc x y

Tactic:
by
  simp_rw [← Ioi_inter_Iic]
  simp

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

Goal state before:
pp: case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : ↑b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
← ENNReal.mul_le_mul_iff_left hb coe_ne_top,

Goal state after:
case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : ↑b ≠ 0
⊢ a * ↑b ≤ c / ↑b * ↑b ↔ a * ↑b ≤ c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ a / 3 + a / 3 + a / 3 = a

Tactic:
rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]

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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
⊢ (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0

Tactic:
if_pos h,

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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
⊢ count K v I + count K v I' = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case e'_2.h
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)

Tactic:
rw [Finite.coe_toFinset]
    intro v hv h
    rw [mem_mulSupport, h, zpow_zero] at hv
    exact hv (Eq.refl 1)

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

Goal state before:
pp: case e'_2.h
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)

Tactic:
· rw [Finite.coe_toFinset]
    intro v hv h
    rw [mem_mulSupport, h, zpow_zero] at hv
    exact hv (Eq.refl 1)

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

Goal state before:
pp: case mpr.right
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ∞

Tactic:
apply lt_trans h'n _
      exact ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ eball x r ×ˢ eball y r ↔ z ∈ eball (x, y) r

Tactic:
simp [Prod.edist_eq]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ closedEBall x r ×ˢ closedEBall y r ↔ z ∈ closedEBall (x, y) r

Tactic:
simp [Prod.edist_eq]

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:
by
  rcases hr.lt_or_eq with (hr | rfl)
  · rw [closedBall_eq_empty.2 hr]
    exact subsingleton_empty
  · rw [closedBall_zero]
    exact subsingleton_singleton

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)

Tactic:
add_left_comm,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₁ x₂ + (dist x₁ y₁ + dist y₁ y₂)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ closedBall x ε ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ

Tactic:
rw [mem_closedBall, ← forall_gt_iff_le, mem_iInter₂]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ i > ε, y ∈ ball x i
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), (T n).Countable
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)
x : α
⊢ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ n, T n)

Tactic:
rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering α) x with ⟨n, hn⟩

Goal state after:
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), (T n).Countable
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)
x : α
n : ℕ
hn : x ∈ compactCovering α n
⊢ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ n, T n)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
⊢ Ioo a b = Icc a b

Tactic:
rw [← closure_discrete (Ioo a b), closure_Ioo contra.ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
inst✝¹ : Fintype β
inst✝ : Nonempty β
a b : α
⊢ (dist (fun x ↦ a) fun x ↦ b) = dist a b

Tactic:
simpa only [dist_edist] using congr_arg ENNReal.toReal (edist_pi_const a b)

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ nndist (f b) (g b) ≤ nndist f g

Tactic:
rw [← ENNReal.coe_le_coe, ← edist_nndist, ← edist_nndist]

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ edist (f b) (g b) ≤ edist f g
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ inst✝³ = Preorder.topology α

Tactic:
rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_preorderTopology]

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]

Goal state after:
case left
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
f : ι → E
⊢ ↑(Finset.univ.sup fun b ↦ ‖f b‖₊) ∈ Set.range fun x ↦ ‖f x‖
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 y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Ioo y x)))

Tactic:
refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
  · obtain ⟨z, ⟨yz, zx⟩, lz⟩ : ∃ a : α, a ∈ Ioo y x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h_nonempty.image _) hl
    filter_upwards [Ioo_mem_nhdsLT zx] with w hw
    exact lz.trans_le <| Mf ⟨yz, zx⟩ ⟨yz.trans_le hw.1.le, hw.2⟩ hw.1.le
  · rcases h_nonempty with ⟨_, hy, hx⟩
    filter_upwards [Ioo_mem_nhdsLT (hy.trans hx)] with w hw
    exact (le_csSup h_bdd (mem_image_of_mem _ hw)).trans_lt hm

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

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
⊢ cocompact α ≤ atBot ⊔ atTop

Tactic:
by
  refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro
  · exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
  · obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs.1
    obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2
    refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩
    exact (not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_ge h)) fun h ↦ hu x (le_of_not_ge h)

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
⊢ IsClosed[inst✝²] (s ∩ Icc a y)

Tactic:
suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y from this ▸ hs.inter isClosed_Icc

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ENormedMonoid E
a : E
⊢ ‖a‖ₑ = 0 ↔ a = 1

Tactic:
by
  simp [ENormedMonoid.enorm_eq_zero]

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

Goal state before:
pp: x y : ℤ
⊢ dist ↑x ↑y = dist x y

Tactic:
rw [← Int.dist_cast_real, ← Rat.dist_cast]

Goal state after:
x y : ℤ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_decr : Antitone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x2 ≤ x1) F
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f

Tactic:
obtain ⟨l, hl⟩ := IsCobounded.frequently_le cobdd
  exact IsCobounded.of_frequently_ge <| f_decr.frequently_ge_map_of_frequently_le hl

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

Goal state before:
pp: α : 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)
⊢ IsLUB (range f) a

Tactic:
constructor
  · rintro _ ⟨b, rfl⟩
    exact hf.ge_of_tendsto ha b
  · exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)

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

Goal state before:
pp: α : 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)
⊢ IsLUB (range f) a

Tactic:
by
  constructor
  · rintro _ ⟨b, rfl⟩
    exact hf.ge_of_tendsto ha b
  · exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)

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 : ι
this : ∀ᶠ (r : α) in atTop, u n r ≤ b'
⊢ ∃ r, ∀ s ≥ r, u n s ≤ b''

Tactic:
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:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe_coe
x y : ℝ
⊢ ↑x * ↑y = ⊤ ↔ ↑x = ⊥ ∧ ↑y < 0 ∨ ↑x < 0 ∧ ↑y = ⊥ ∨ ↑x = ⊤ ∧ 0 < ↑y ∨ 0 < ↑x ∧ ↑y = ⊤

Tactic:
simpa only [EReal.coe_ne_bot, EReal.coe_neg', false_and, and_false, EReal.coe_ne_top,
      EReal.coe_pos, or_self, iff_false, EReal.coe_mul] using! EReal.coe_ne_top _

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

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

Tactic:
by
  induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    simpa only [EReal.coe_ne_bot, EReal.coe_neg', false_and, and_false, EReal.coe_ne_top,
      EReal.coe_pos, or_self, iff_false, EReal.coe_mul] using! EReal.coe_ne_top _
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder β
inst✝² : Nonempty β
inst✝¹ : IsDirectedOrder β
inst✝ : IsCodirectedOrder β
⊢ (conditional β).filter.NeBot

Tactic:
rw [conditional_filter]; infer_instance

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

Goal state before:
pp: case pos
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 = ∅
⊢ liminf f F ≤ f F.limsSup

Tactic:
rcases h' with ⟨c, c_lt, hc⟩

Goal state after:
case pos
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 = ∅
⊢ liminf f F ≤ f F.limsSup
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hg : Multipliable g L
hfg : Multipliable (fun b ↦ f b / g b) L
⊢ Multipliable f L

Tactic:
simpa only [div_mul_cancel] using hfg.mul hg

Goal state after: