mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
x : X
hx : IsLocallyClosed {x}
⊢ IsClosed[inst✝¹] {x}

Tactic:
obtain ⟨_, ⟨y, rfl : y = x, rfl⟩, hy'⟩ :=
    nonempty_inter_closedPoints (Set.singleton_nonempty x) hx
  exact hy'

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos.succ
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
i : Fin s.length
hi : length A ↥(s.toFun i.castSucc) = ↑↑i.castSucc * length (ResidueField A) (ResidueField B)
⊢ length A ↥(s.toFun i.succ) = ↑↑i.succ * length (ResidueField A) (ResidueField B)

Tactic:
| succ i hi =>

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos.succ
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
i : Fin s.length
hi :
  length B ↥(Submodule.baseChange B (s.toFun i.castSucc)) =
    ↑↑i.castSucc * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B ↥(Submodule.baseChange B (s.toFun i.succ)) =
    ↑↑i.succ * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
| succ i hi =>

Goal state after:
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ ∃ e, IsIdempotentElem e ∧ I = R ∙ e

Tactic:
obtain ⟨r, hr, hr'⟩ :=
      Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I I h
        (by
          rw [smul_eq_mul]
          exact e.ge)

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r • n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = R ∙ e
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤

Tactic:
intro H
    obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H
    simp only [Ideal.submodule_span_eq, Ideal.span_singleton_eq_bot]
    apply Or.imp id _ (IsIdempotentElem.iff_eq_zero_or_one.mp he)
    rintro rfl
    simp

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
inst✝¹ : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst✝ : w.LiesOver v
h : p ≤ v
⊢ p = v

Tactic:
exact ((isPrime_of_prime hp).isMaximal hp.ne_zero).eq_of_le (isPrime_of_prime hv.prime).ne_top h

Goal state after:
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f g : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp g
⊢ Ideal.comap (Shrink.ringEquiv B) I ^ 2 = ⊥

Tactic:
← Ideal.map_symm,

Goal state after:
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f g : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp g
⊢ Ideal.map (Shrink.ringEquiv B).symm I ^ 2 = ⊥
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0
ht₂ : 1 - t ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ IsIdempotentElem (1 - t) ∧ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = S ⊗[R] S ∙ (1 - t)

Tactic:
← sub_sub_self 1 t

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - (1 - t)) = 0
ht₂ : 1 - t ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ IsIdempotentElem (1 - t) ∧ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = S ⊗[R] S ∙ (1 - t)
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : QuasiFinite R S
inst✝¹ : IsArtinianRing R
inst✝ : IsLocalRing R
e : (maximalIdeal R).Fiber S ≃ₐ[R] S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) :=
  (TensorProduct.congr
        (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (maximalIdeal R).ResidueField) ⋯) ⋯).symm
        AlgEquiv.refl).trans
    ((TensorProduct.comm R (R ⧸ maximalIdeal R) S).trans
      (AlgEquiv.restrictScalars R (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)).symm))
this : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
⊢ RingHom.ker (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (maximalIdeal R))) ≤ nilradical S

Tactic:
refine Ideal.mk_ker.trans_le ?_
    rw [Ideal.map_le_iff_le_comap, ← Ring.KrullDimLE.nilradical_eq_maximalIdeal]
    exact fun x hx ↦ IsNilpotent.map hx _

Goal state after:
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : FormallySmooth R P
f : P →ₐ[R] A
g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
h : f.kerSquareLift.comp g = AlgHom.id R A
⊢ FormallySmooth R A

Tactic:
by
  refine (iff_split_surjection f fun x ↦ ?_).mpr ⟨g, h⟩
  obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (g x)
  exact ⟨y, congr(f.kerSquareLift $hy).trans congr($h x)⟩

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ (∏ i ∈ s, (1 - (S i).indicator 1 a)) • f a = 0

Tactic:
have : Set.indicator (⋃ i ∈ s, S i) 1 a = (1 : ℤ) := Set.indicator_of_mem ha 1

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
this : (⋃ i ∈ s, S i).indicator 1 a = 1
⊢ (∏ i ∈ s, (1 - (S i).indicator 1 a)) • f a = 0
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
Real.toNNReal_mul (inv_nonneg.2 hy),

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ y⁻¹.toNNReal * x.toNNReal = y.toNNReal⁻¹ * x.toNNReal
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
⊢ ⨅ r, f ↑r ≤ ⨅ q, f ↑↑q

Tactic:
refine le_ciInf fun r => ?_

Goal state after:
case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
r : { q' // x < ↑q' }
⊢ ⨅ r, f ↑r ≤ f ↑↑r
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: n : ℤ
⊢ ↑|n| = ↑(nnabs ↑n)

Tactic:
Real.coe_nnabs,

Goal state after:
n : ℤ
⊢ ↑|n| = |↑n|
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ∃ m, ↑m + 1 < a ^ m

Tactic:
use 2 * k ^ 2

Goal state after:
case h
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ↑(2 * k ^ 2) + 1 < a ^ (2 * k ^ 2)
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a b : ℝ≥0∞
hab : a < b
c : ℝ≥0
ac : a < ↑c
cb : ↑c < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b

Tactic:
lift a to ℝ≥0 using ac.ne_top

Goal state after:
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : ↑a < ↑c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case hbc
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 ℝ
r : R
p : AddGroupSeminorm E
x✝¹ x✝ : E
⊢ p (x✝¹ + x✝) ≤ p x✝¹ + p x✝

Tactic:
apply map_add_le_add

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

Tactic:
have h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0 := by
    rw [ne_eq, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
      Injective.eq_iff (IsLocalization.injective K (le_refl R⁰))]
    rw [ne_eq, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h_a_ne_zero
    exact h_a_ne_zero

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ ↑x✝¹ + ↑c - (↑x✝ + ↑c) = ↑x✝¹ - ↑x✝

Tactic:
norm_cast
    rw [add_tsub_add_eq_tsub_right]

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

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

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Ioc, WithBot.image_coe_Ioc]
  rfl

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

Goal state before:
pp: x : ℝ
⊢ WithBot.some '' Iic ↑x = Ioc ⊥ ↑x

Tactic:
WithBot.image_coe_Iic

Goal state after:
x : ℝ
⊢ Ioc ⊥ ↑↑x = Ioc ⊥ ↑x
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
hw : w ≠ v
⊢ count K v ↑w.asIdeal = 0

Tactic:
have hw_fact : (w.asIdeal : FractionalIdeal R⁰ K) =
      spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal := by
    rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]
  have hw_ne_zero : (w.asIdeal : FractionalIdeal R⁰ K) ≠ 0 :=
    coeIdeal_ne_zero.mpr w.ne_bot
  have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible
  have hw' : Irreducible (Associates.mk w.asIdeal) := by apply w.associates_irreducible
  rw [count_well_defined K v hw_ne_zero hw_fact, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero hv, ofNat_zero, sub_zero,
    natCast_eq_zero, ← pow_one (Associates.mk w.asIdeal), Associates.factors_prime_pow hw',
    Associates.count_some hv, Multiset.replicate_one, Multiset.count_eq_zero,
    Multiset.mem_singleton]
  simp only [Subtype.mk.injEq]
  rw [Associates.mk_eq_mk_iff_associated, associated_iff_eq, ← HeightOneSpectrum.ext_iff]
  exact Ne.symm hw

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

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ x ≠ 0

Tactic:
simpa only [Ne, coe_eq_zero] using hx

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ x ∈ eball a δ ∩ s → f x ∈ eball b ε ∩ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Tactic:
by simp; tauto

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

Goal state before:
pp: m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ x ≠ 0

Tactic:
simpa only [Ne, coe_eq_zero] using hx

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
⊢ (uniformSpaceOfEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace ≤ e

Tactic:
let hβ := PseudoEMetricSpace.ofEDist m.edist edist_self edist_comm edist_triangle

Goal state after:
α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
⊢ (uniformSpaceOfEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace ≤ e
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sInf s

Tactic:
zero_smul_set hs,

Goal state after:
case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf 0 = 0 • sInf s
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sSup s

Tactic:
zero_smul_set hs,

Goal state after:
case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup 0 = 0 • sSup s
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, q.asIdeal < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1

Tactic:
Finset.prod_eq_mul_prod_sdiff_singleton_of_mem hps,

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 * (p.asIdeal * ∏ x ∈ s \ {p}, x.asIdeal) < (J * ∏ q ∈ s \ {p}, q.asIdeal) * 1
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sSup s

Tactic:
zero_smul_set hs,

Goal state after:
case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf 0 = 0 • sSup s
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sInf s

Tactic:
zero_smul_set hs,

Goal state after:
case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sSup 0 = 0 • sInf s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
l : Filter β
inst✝ : l.NeBot
hf₀ : ∀ (i : β), p i → 0 < f i
hf₁ : ∀ᶠ (i : β) in l, p i
hf : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ closedBall 0 i
ε : ℝ
hε : 0 < ε
i : β
hp : p i
hi : f i ∈ closedBall 0 ε
⊢ f i ≤ ε

Tactic:
simpa [Metric.mem_closedBall, Real.dist_eq, abs_of_nonneg (hf₀ i hp).le] using hi

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ val '' closedBall a r = closedBall (↑a) r ∩ {a | p a}

Tactic:
← preimage_closedBall,

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ val '' val ⁻¹' closedBall (↑a) r = closedBall (↑a) r ∩ {a | p a}
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
i : PseudoMetricSpace (α × β) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun x y ↦ max (dist x.1 y.1) (dist x.2 y.2)) ⋯ ⋯
s : Set (α × β)
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
by
    simp only [← isBounded_image_fst_and_snd, isBounded_iff_eventually, forall_mem_image, ←
      eventually_and, ← forall_and, ← max_le_iff]
    rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ closure[inst✝³] (Ioi a) = Ici a

Tactic:
apply Subset.antisymm
  · exact closure_minimal Ioi_subset_Ici_self isClosed_Ici
  · rw [← sdiff_subset_closure_iff, Ici_sdiff_Ioi_same, singleton_subset_iff]
    exact isGLB_Ioi.mem_closure h

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
hs : s.Nonempty
⊢ ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s

Tactic:
rcases hs with ⟨a', ha'⟩

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
⊢ ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by
  obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x
  rcases exists_seq_strictMono_tendsto' hy with ⟨u, hu_mono, hu_mem, hux⟩
  exact ⟨u, hu_mono, fun n => (hu_mem n).2, hux⟩

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ toUniformSpace = toUniformSpace

Tactic:
dsimp +instances [replaceDist]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ toBornology = toBornology

Tactic:
dsimp +instances [replaceDist]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ |‖a‖ - ‖b‖| ≤ ‖a⁻¹ * b‖

Tactic:
simpa [dist_eq_norm_inv_mul] using abs_dist_sub_le a b 1

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

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

Tactic:
rw [mem_closedBall, dist_eq_norm_inv_mul]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
by
    /- `s` is a Cauchy sequence. The sequence `b` will be constructed by taking
      the supremum of the distances between `s n` and `s m` for `n m ≥ N`.
      First, we prove that all these distances are bounded, as otherwise the Sup
      would not make sense. -/
    let S N := (fun p : ℕ × ℕ => dist (s p.1) (s p.2)) '' { p | p.1 ≥ N ∧ p.2 ≥ N }
    have hS : ∀ N, ∃ x, ∀ y ∈ S N, y ≤ x := by
      rcases cauchySeq_bdd hs with ⟨R, -, hR⟩
      refine fun N => ⟨R, ?_⟩
      rintro _ ⟨⟨m, n⟩, _, rfl⟩
      exact le_of_lt (hR m n)
    -- Prove that it bounds the distances of points in the Cauchy sequence
    have ub : ∀ m n N, N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N) := fun m n N hm hn =>
      le_csSup (hS N) ⟨⟨_, _⟩, ⟨hm, hn⟩, rfl⟩
    have S0m : ∀ n, (0 : ℝ) ∈ S n := fun n => ⟨⟨n, n⟩, ⟨le_rfl, le_rfl⟩, dist_self _⟩
    have S0 := fun n => le_csSup (hS n) (S0m n)
    -- Prove that it tends to `0`, by using the Cauchy property of `s`
    refine ⟨fun N => sSup (S N), S0, ub, Metric.tendsto_atTop.2 fun ε ε0 => ?_⟩
    refine (Metric.cauchySeq_iff.1 hs (ε / 2) (half_pos ε0)).imp fun N hN n hn => ?_
    rw [Real.dist_0_eq_abs, abs_of_nonneg (S0 n)]
    refine lt_of_le_of_lt (csSup_le ⟨_, S0m _⟩ ?_) (half_lt_self ε0)
    rintro _ ⟨⟨m', n'⟩, ⟨hm', hn'⟩, rfl⟩
    exact le_of_lt (hN _ (le_trans hn hm') _ (le_trans hn hn'))

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

Goal state before:
pp: ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, dist (f b) (a b) ≤ d b
⊢ dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

Tactic:
simp_rw [dist_eq_norm_inv_mul] at h
  rw [dist_eq_norm_inv_mul, ← Finset.prod_inv_distrib, ← Finset.prod_mul_distrib]
  exact norm_prod_le_of_le s h

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

Goal state before:
pp: x : ℤ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋

Tactic:
← preimage_closedBall,

Goal state after:
x : ℤ
r : ℝ
⊢ Int.cast ⁻¹' closedBall (↑x) r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋