mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this✝ : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
Rp : Type u_1 := Localization.AtPrime p
Sq : Type (max u_1 u_2) := Localization.AtPrime q.asIdeal
Sr : Type u_2 := Localization.AtPrime r
⊢ (length (Localization.AtPrime r) (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) p)).toNat *
      finrank p.ResidueField r.ResidueField =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)

Tactic:
let κp := p.ResidueField

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this✝ : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
Rp : Type u_1 := Localization.AtPrime p
Sq : Type (max u_1 u_2) := Localization.AtPrime q.asIdeal
Sr : Type u_2 := Localization.AtPrime r
κp : Type u_1 := p.ResidueField
⊢ (length (Localization.AtPrime r) (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) p)).toNat *
      finrank p.ResidueField r.ResidueField =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: case e_6
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
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (algebraMap R S) r'' * (algebraMap R S) r * (algebraMap R S) (∏ i ∈ s.erase x, b i) * (x * (algebraMap R S) (b x)) =
    x * (algebraMap R S) (r * ((∏ x ∈ s.erase x, b x) * b x) * r'')

Tactic:
map_mul,

Goal state after:
case e_6
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
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (algebraMap R S) r'' * (algebraMap R S) r * (algebraMap R S) (∏ i ∈ s.erase x, b i) * (x * (algebraMap R S) (b x)) =
    x * ((algebraMap R S) (r * ((∏ x ∈ s.erase x, b x) * b x)) * (algebraMap R S) r'')
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: case e_6
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
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (algebraMap R S) r'' * (algebraMap R S) r * (algebraMap R S) (∏ i ∈ s.erase x, b i) * (x * (algebraMap R S) (b x)) =
    x * ((algebraMap R S) (r * ((∏ x ∈ s.erase x, b x) * b x)) * (algebraMap R S) r'')

Tactic:
map_mul,

Goal state after:
case e_6
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
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (algebraMap R S) r'' * (algebraMap R S) r * (algebraMap R S) (∏ i ∈ s.erase x, b i) * (x * (algebraMap R S) (b x)) =
    x * ((algebraMap R S) r * (algebraMap R S) ((∏ x ∈ s.erase x, b x) * b x) * (algebraMap R S) r'')
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal

Tactic:
let S := (mulSupport fun v : HeightOneSpectrum A => v.maxPowDividing (span {a})).toFinset

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℚ≥0
y : ℝ≥0
⊢ 0 ≤ ↑x * ↑y

Tactic:
exact mul_nonneg x.cast_nonneg y.2

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

Goal state before:
pp: r : ℝ≥0
⊢ ↑r = 0 ↔ r = 0

Tactic:
← coe_zero,

Goal state after:
r : ℝ≥0
⊢ ↑r = ↑0 ↔ r = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ ↑r = 1 ↔ r = 1

Tactic:
by rw [← coe_one, coe_inj]

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 : Ideal R
hI : I ≠ 0
⊢ {x | ¬↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) = 1}.Finite

Tactic:
exact hasFiniteMulSupport_coe hI

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

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0

Tactic:
by
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · exact sInf_empty.le
  · exact sInf_nonpos' ⟨x, hx, hs _ hx⟩

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
hv : Irreducible v
J : Ideal R
hJv : Associates.mk J = v
⊢ v.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = v.count (Associates.mk I).factors

Tactic:
rw [← hJv, Associates.irreducible_mk] at hv

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ v.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = v.count (Associates.mk I).factors
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
· rw [if_pos hx, hx, zero_add, zero_add]

Goal state after:
case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1
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
⊢ spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * ((algebraMap R K) a')⁻¹) * (↑J' * ↑J) =
    spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * (↑J * ↑J')

Tactic:
map_mul,

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
⊢ spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * ((algebraMap R K) a')⁻¹) * (↑J' * ↑J) =
    spanSingleton R⁰ ((algebraMap R K) a * (algebraMap R K) a')⁻¹ * (↑J * ↑J')
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ 0 < ↑x ↔ 0 < x

Tactic:
by
  rw [← coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]

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

Goal state before:
pp: ⊢ ↑2⁻¹ = 2⁻¹

Tactic:
coe_inv _root_.two_ne_zero,

Goal state after:
⊢ (↑2)⁻¹ = 2⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
⊢ x / y ≤ z ↔ x ≤ y * z

Tactic:
by
  rw [mul_comm, ENNReal.div_le_iff h1 h2]

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
by rw [inv_lt_iff_inv_lt, inv_one]

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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
⊢ count K v ↑w.asIdeal = if w = v then 1 else 0

Tactic:
split_ifs with h
  · rw [h, count_self]
  · exact count_maximal_coprime K v h

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
⊢ eball x 0 = ∅

Tactic:
by rw [eball_eq_empty_iff]

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

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal (x * y⁻¹) ≤ ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹

Tactic:
ofReal_mul' (inv_nonneg.2 hy)

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal x * ENNReal.ofReal y⁻¹ ≤ ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
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)) =
    ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))

Tactic:
rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, 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))
⊢ 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)) =
    ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))

Tactic:
rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, 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))
⊢ n ∉ Finset.Ico m n
Module: Mathlib.Topology.EMetricSpace.Basic

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

Tactic:
induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, edist_self]
  | succ n hle ihn =>
    calc
      edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
      _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
      _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
        rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; 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✝ : DiscreteTopology α
a b : α
contra : a < b
⊢ Ioo a b = Icc a b

Tactic:
← closure_discrete (Ioo a b),

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
⊢ closure[inst✝⁴] (Ioo a b) = Icc a b
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ (t \ ({x | IsBot x} ∪ {x | IsTop x})).Countable

pp: case refine_3
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ Dense (t \ ({x | IsBot x} ∪ {x | IsTop x}))

pp: case refine_4
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsBot x
⊢ x ∉ t \ ({x | IsBot x} ∪ {x | IsTop x})

pp: case refine_5
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsTop x
⊢ x ∉ t \ ({x | IsBot x} ∪ {x | IsTop x})

Tactic:
· exact htc.mono sdiff_subset

Goal state after:
case refine_3
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ Dense (t \ ({x | IsBot x} ∪ {x | IsTop x}))

case refine_4
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsBot x
⊢ x ∉ t \ ({x | IsBot x} ∪ {x | IsTop x})

case refine_5
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsTop x
⊢ x ∉ t \ ({x | IsBot x} ∪ {x | IsTop x})
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
obtain ⟨v, hvx, hvt⟩ := exists_seq_forall_of_frequently (htx.frequently_mem ht)

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvx : Tendsto v atTop (𝓝[≤] x)
hvt : ∀ (n : ℕ), v n ∈ t
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case inl.inl
α : 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 : IsTop d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

pp: case inl.inr
α : 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
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
· exact .of_forall (fun _ ↦ h _)

Goal state after:
case inl.inr
α : 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
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α✝ : Type u_1
s✝ t : Set α✝
inst✝⁵ : Bornology α✝
inst✝⁴ : Preorder α✝
inst✝³ : IsOrderBornology α✝
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → Bornology (α i)
inst✝ : ∀ (i : ι), IsOrderBornology (α i)
s : Set ((i : ι) → α i)
⊢ (∀ (i : ι), IsBounded (Function.eval i '' s)) ↔
    (∀ (a : ι), BddBelow (Function.eval a '' s)) ∧ ∀ (a : ι), BddAbove (Function.eval a '' s)

Tactic:
← forall_and,

Goal state after:
α✝ : Type u_1
s✝ t : Set α✝
inst✝⁵ : Bornology α✝
inst✝⁴ : Preorder α✝
inst✝³ : IsOrderBornology α✝
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → Bornology (α i)
inst✝ : ∀ (i : ι), IsOrderBornology (α i)
s : Set ((i : ι) → α i)
⊢ (∀ (i : ι), IsBounded (Function.eval i '' s)) ↔
    ∀ (x : ι), BddBelow (Function.eval x '' s) ∧ BddAbove (Function.eval x '' s)
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
⊢ {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable

Tactic:
suffices H : Set.Countable (x '' t) by
    have : Set.InjOn x t := by
      intro c hc d hd hcd
      have : f (x c) = f (x d) := by simp [hcd]
      rwa [hfx _ hc, hfx _ hd] at this
    exact countable_of_injective_of_countable_image this H

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
⊢ (x '' t).Countable
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
a b c : FractionalIdeal R⁰ K
hac : ¬a ≤ c
⊢ c.divMod b a = 0

Tactic:
by
  simp [divMod, hac]

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

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s = univ

Tactic:
refine eq_univ_of_forall fun x => ?_

Goal state after:
α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x : α
⊢ x ∈ s
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_empty : t = ∅
⊢ s ∈ atBot

Tactic:
rewrite [compl_univ_iff.mpr h_empty, univ_subset_iff] at hts
    convert! univ_mem

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

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

Tactic:
rcases Metric.mem_uniformity_dist.mp hu with ⟨ε, hε, hab⟩

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ 0 ≤ ‖a‖

Tactic:
← dist_one_right

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ 0 ≤ dist a 1
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ ‖a‖₊ = 0 ↔ a = 1

Tactic:
by
  rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero']

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
s : Set β
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ f '' s → ∀ ⦃y : α⦄, y ∈ f '' s → dist x y ≤ C) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C

Tactic:
simp only [forall_mem_image]

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

Goal state before:
pp: case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal

Tactic:
try {· simp}

Goal state after: