mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
I : Ideal R
hU : ∃ I_1, (zeroLocus ↑I_1)ᶜ = (zeroLocus ↑I)ᶜ
J : Ideal R
hZ : ∃ I, zeroLocus ↑J = zeroLocus ↑I
hS : zeroLocus ↑J ∩ closedPoints (PrimeSpectrum R) ⊆ zeroLocus ↑I
x : Ideal R
hJx : J ≤ x
hx : x.IsMaximal
⊢ I ≤ x

Tactic:
exact @hS ⟨x, hx.isPrime⟩ ⟨hJx, (isClosed_singleton_iff_isMaximal _).mpr hx⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
p : PrimeSpectrum R
⊢ (∀ (i : PrimeSpectrum R), IsMin i → i ≤ p → i = x) → p = x

Tactic:
· intro hp
      apply h₁.eq_of_ge
      obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le
      exact (hp ⟨q, hq.1.1⟩ (isMin_iff.mpr hq) hq').ge.trans hq'

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

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ (n + 1)
⊢ p.ramificationIdx' P < n + 1

Tactic:
rw [Nat.lt_succ_iff]

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hgt : ¬map f p ≤ P ^ (n + 1)
⊢ p.ramificationIdx' P ≤ n
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
⊢ ⊤.FG

Tactic:
use Finset.image₂ (fun i j ↦ f i * b j) f.support f.support

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
⊢ Submodule.span R ↑(Finset.image₂ (fun i j ↦ f i * b j) f.support f.support) = ⊤
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 σ
x : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2✝ : ↥Q.toExtension.ker = ↥Q.ker
⊢ ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) x = ↑0

Tactic:
simp [aeval_val_eq_zero hx]

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

Goal state before:
pp: R : Type u_4
inst✝⁸ : CommRing R
A : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallySmooth R B
⊢ FormallySmooth A B

Tactic:
refine iff_comp_surjective.mpr fun C _ _ I hI f ↦ ?_

Goal state after:
R : Type u_4
inst✝⁸ : CommRing R
A : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallySmooth R B
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra A C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[A] C ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ A I).comp a = f
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case monomial
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₁
Q : Generators S T ι
y : Q.Ring
n : ι →₀ ℕ
r : S
⊢ (δAux R Q) ((monomial n) r * y) = (monomial n) r • (δAux R Q) y + y • (δAux R Q) ((monomial n) r)

Tactic:
induction y using MvPolynomial.induction_on' with

Goal state after:
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
H : f.toRingHom.FormallyEtale
this✝⁴ : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this✝³ : IsScalarTower R P.Ring Q.Ring
this✝² : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring Q.Ring T
this : FormallyEtale P.Ring Q.Ring
x✝ : Q.CotangentSpace
a : Q.Ring
x : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]
hx : (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring) x = (D R Q.Ring) a
⊢ (LinearMap.liftBaseChange T (CotangentSpace.map f))
      (1 •
        (LinearMap.liftBaseChange Q.Ring
            (↑P.Ring ((TensorProduct.mk S T P.CotangentSpace) 1) ∘ₗ (TensorProduct.mk P.Ring S Ω[P.Ring⁄R]) 1))
          ((tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm ((D R Q.Ring) a))) =
    1 ⊗ₜ[Q.Ring] (D R Q.Ring) a

Tactic:
simp only [one_smul, ← hx, LinearEquiv.symm_apply_apply]

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
P : Extension R S
Q : Extension R T
f : P.Hom Q
H : f.toRingHom.FormallyEtale
this✝⁴ : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this✝³ : IsScalarTower R P.Ring Q.Ring
this✝² : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring Q.Ring T
this : FormallyEtale P.Ring Q.Ring
x✝ : Q.CotangentSpace
a : Q.Ring
x : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]
hx : (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring) x = (D R Q.Ring) a
⊢ (LinearMap.liftBaseChange T (CotangentSpace.map f))
      ((LinearMap.liftBaseChange Q.Ring
          (↑P.Ring ((TensorProduct.mk S T P.CotangentSpace) 1) ∘ₗ (TensorProduct.mk P.Ring S Ω[P.Ring⁄R]) 1))
        x) =
    1 ⊗ₜ[Q.Ring] (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring) x
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case h
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝² : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝¹ : ExpChar (L ⊗[K] L) (ringExpChar K)
this✝ : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
⊢ - -(↑this.unit⁻¹ • b • x) = x

Tactic:
neg_neg,

Goal state after:
case h
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝² : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝¹ : ExpChar (L ⊗[K] L) (ringExpChar K)
this✝ : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
a b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
⊢ ↑this.unit⁻¹ • b • x = x
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)
this : ∀ (x : ↥s), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s → ↥p.primeCompl
hm : ∀ (x : ↥s), ↑(m x) * ↑x = 0
x : R
hxs : x ∈ ↑s
⊢ ↑(∏ i, m i) * x = 0

Tactic:
Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩,

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
m : ↥s → ↥p.primeCompl
hm : ∀ (x : ↥s), ↑(m x) * ↑x = 0
x : R
hxs : x ∈ ↑s
⊢ ↑(m ⟨x, hxs⟩ * ∏ i ∈ {⟨x, hxs⟩}ᶜ, m i) * x = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
⊢ ∃ x, IsLUB s x

Tactic:
let g : CauSeq ℚ abs := ⟨fun n => f n / n, hg⟩

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
⊢ ∃ x, IsLUB s x
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
Real.sInf_empty

Goal state after:
⊢ 0 = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
⊢ 1 / x < 1 ↔ 1 < x

Tactic:
div_lt_iff₀ hx.bot_lt,

Goal state after:
x : ℝ≥0
hx : x ≠ 0
⊢ 1 < 1 * x ↔ 1 < x
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: α : Sort u_2
⊢ ⨅ i, ↑0 = ↑0

Tactic:
exact Real.iInf_const_zero

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
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I = I

Tactic:
rw [← associated_iff_eq, ← Associates.mk_eq_mk_iff_associated]
  apply Associates.eq_of_eq_counts
  · apply Associates.finprod_ne_zero I
  · apply Associates.mk_ne_zero.mpr hI
  intro v hv
  obtain ⟨J, hJv⟩ := Associates.exists_rep v
  rw [← hJv, Associates.irreducible_mk] at hv
  rw [← hJv]
  apply Ideal.finprod_count
    ⟨J, Ideal.isPrime_of_prime (irreducible_iff_prime.mp hv), Irreducible.ne_zero hv⟩ I hI

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

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

Tactic:
rw [NNReal.coe_natCast, Nat.cast_natAbs, Real.coe_nnabs, Int.cast_abs]

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

Goal state before:
pp: x : ℝ
⊢ 0 < nnabs x ↔ x ≠ 0

Tactic:
by simp [← NNReal.coe_pos]

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

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ((1 / ↑k + 1) ^ k) ^ (2 * k) = (1 / ↑k + 1) ^ (2 * k ^ 2)

Tactic:
← pow_mul,

Goal state after:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ (1 / ↑k + 1) ^ (k * (2 * k)) = (1 / ↑k + 1) ^ (2 * k ^ 2)
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✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
⊢ r • p 0 = 0

Tactic:
by
        simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_zero, mul_zero]

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a - ⨅ i, f i = ⨆ i, a - f i

Tactic:
by
  refine eq_of_forall_ge_iff fun c => ?_
  rw [tsub_le_iff_right, add_comm, iInf_add]
  simp [tsub_le_iff_right, add_comm]

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

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

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

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

Goal state before:
pp: case insert
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
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
i : ι
s : Finset ι
hi : i ∉ s
hrec : (∀ i ∈ s, I i ≠ 0) → count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
hS : ∀ i_1 ∈ insert i s, I i_1 ≠ 0
⊢ count K v (∏ i ∈ insert i s, I i) = ∑ i ∈ insert i s, count K v (I i)

Tactic:
| insert i s hi hrec =>

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ⊤ = Ioi x

Tactic:
by
  rw [← Ioi_inter_Iio]
  simp

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

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ⊥ ↑y = Iio y

Tactic:
by
  rw [← Ioi_inter_Iio]
  simp

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

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' Ioo ⊥ ⊤ = univ

Tactic:
by
  rw [← Ioi_inter_Iio]
  simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ count K v (0 ^ (-n)) = -count K v (0 ^ n)

Tactic:
zero_zpow n hn,

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : I = 0
hn : ¬n = 0
⊢ count K v (0 ^ (-n)) = -count K v 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) / c = a / c - b / c

Tactic:
by
  simp_rw [div_eq_mul_inv]
  exact ENNReal.sub_mul (by simpa using h)

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

Goal state before:
pp: x : ℝ≥0∞
m : ℤ
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
by
  obtain hx₀ | hx₀ := eq_or_ne x 0
  · obtain hm | hm | hm := lt_trichotomy m 0 <;>
      simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]
  obtain hx | hx := eq_or_ne x ⊤
  · obtain hm | hm | hm := lt_trichotomy m 0 <;>
      simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]
  exact ENNReal.eq_inv_of_mul_eq_one_left (by simp [← ENNReal.zpow_add hx₀ hx])

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

Goal state before:
pp: case e_toBornology
α : Type u_3
toDist✝ : Dist α
dist_self✝¹ : ∀ (x : α), dist x x = 0
dist_comm✝¹ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝¹ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝¹ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝¹ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝¹ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝¹ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝¹, dist_comm := dist_comm✝¹, dist_triangle := dist_triangle✝¹,
      edist := edist✝¹, edist_dist := hed, toUniformSpace := toUniformSpace✝¹, uniformity_dist := hU,
      toBornology := toBornology✝¹, cobounded_sets := hB }.toDist
edist✝ : α → α → ℝ≥0∞
toUniformSpace✝ : UniformSpace α
toBornology✝ : Bornology α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α :=
  { toDist := d, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝, edist := edist✝,
      edist_dist := hed', toUniformSpace := toUniformSpace✝, uniformity_dist := hU', toBornology := toBornology✝,
      cobounded_sets := hB' }.toDist
s✝ : Set α
⊢ s✝ ∈ (cobounded α).sets ↔ s✝ ∈ (cobounded α).sets

Tactic:
hB,

Goal state after:
case e_toBornology
α : Type u_3
toDist✝ : Dist α
dist_self✝¹ : ∀ (x : α), dist x x = 0
dist_comm✝¹ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝¹ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝¹ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝¹ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝¹ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝¹ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝¹, dist_comm := dist_comm✝¹, dist_triangle := dist_triangle✝¹,
      edist := edist✝¹, edist_dist := hed, toUniformSpace := toUniformSpace✝¹, uniformity_dist := hU,
      toBornology := toBornology✝¹, cobounded_sets := hB }.toDist
edist✝ : α → α → ℝ≥0∞
toUniformSpace✝ : UniformSpace α
toBornology✝ : Bornology α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α :=
  { toDist := d, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝, edist := edist✝,
      edist_dist := hed', toUniformSpace := toUniformSpace✝, uniformity_dist := hU', toBornology := toBornology✝,
      cobounded_sets := hB' }.toDist
s✝ : Set α
⊢ s✝ ∈ {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} ↔ s✝ ∈ (cobounded α).sets
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C

Tactic:
simp only [isBounded_iff_exists_ge 0, NNReal.exists, ← NNReal.coe_le_coe, ← dist_nndist,
    NNReal.coe_mk, exists_prop]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ BoundedSpace α ↔ ∃ C, ∀ (a b : α), edist a b ≤ ↑C

Tactic:
simp [Metric.boundedSpace_iff_nndist]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ PseudoMetricSpace.toUniformSpace = ⊥ ↔ ∃ r, 0 < r ∧ Pairwise fun x1 x2 ↦ r ≤ dist x1 x2

Tactic:
simp only [uniformity_basis_dist.uniformSpace_eq_bot, mem_ofPred_eq, not_lt]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ ∃ a K, J * K = Ideal.span {a} ∧ I + K = ⊤

Tactic:
obtain ⟨K, hK⟩ : J ∣ Ideal.span {∑ p ∈ s, a p} := by
    rw [Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem]
    exact sum_mem fun p hp ↦ Ideal.mul_le_left (ha p hp)

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
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
⊢ ∃ a K, J * K = Ideal.span {a} ∧ I + K = ⊤
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r : ℝ
hr : 0 ≤ r
⊢ sphere x r = {x - r, x + r}

Tactic:
by
  ext; simp [dist_eq]; grind

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

Goal state before:
pp: β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this : UniformSpace α := pseudoMetrizableSpaceUniformity α
⊢ IsSeparable (f ⁻¹' s)

Tactic:
have := pseudoMetrizableSpaceUniformity_countably_generated

Goal state after:
β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this✝ : UniformSpace α := pseudoMetrizableSpaceUniformity α
this : ∀ (X : Type ?u.31) [inst : TopologicalSpace X] [h : PseudoMetrizableSpace X], (𝓤 X).IsCountablyGenerated
⊢ IsSeparable (f ⁻¹' s)
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
⊢ IsSeparable (f ⁻¹' s)

Tactic:
let : UniformSpace α := TopologicalSpace.pseudoMetrizableSpaceUniformity α
  have := pseudoMetrizableSpaceUniformity_countably_generated
  have : SeparableSpace s := hs.separableSpace
  have : SecondCountableTopology s := UniformSpace.secondCountable_of_separable _
  have : IsInducing ((mapsTo_preimage f s).restrict _ _ _) :=
    (hf.comp IsInducing.subtypeVal).codRestrict _
  have := this.secondCountableTopology
  exact .of_subtype _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span {y, x} = Ideal.span {x, y_1}

Tactic:
Set.pair_comm x

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span {y, x} = Ideal.span {y_1, 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:
by
  obtain ⟨v, hvx, hvt⟩ := exists_seq_forall_of_frequently (htx.frequently_mem ht)
  replace hvx := hvx.mono_right nhdsWithin_le_nhds
  have hvx' : ∀ {n}, v n < x := (htx.1 (hvt _)).lt_of_ne (ne_of_mem_of_not_mem (hvt _) notMem)
  have : ∀ k, ∀ᶠ l in atTop, v k < v l := fun k => hvx.eventually (lt_mem_nhds hvx')
  choose N hN hvN using fun k => ((eventually_gt_atTop k).and (this k)).exists
  refine ⟨fun k => v (N^[k] 0), strictMono_nat_of_lt_succ fun _ => ?_, fun _ => hvx',
    hvx.comp (strictMono_nat_of_lt_succ fun _ => ?_).tendsto_atTop, fun _ => hvt _⟩
  · rw [iterate_succ_apply']; exact hvN _
  · rw [iterate_succ_apply']; exact hN _

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
⊢ ∀ (x y : X), d x y = d y x

Tactic:
by simp [hd, dist_comm]

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 : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
by simp [hd, dist_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
⊢ f (sSup s) = sSup (f '' s)

Tactic:
by
  rcases s.eq_empty_or_nonempty with h | h
  · simp [h, fbot]
  · exact Mf.map_csSup_of_continuousWithinAt Cf h

Goal state after: