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

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : IsNoetherian R M → Module.Finite R M
tfae_1_to_3 : Module.Finite R M → IsArtinian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian]

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : IsNoetherian R M → Module.Finite R M
tfae_1_to_3 : Module.Finite R M → IsArtinian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M].TFAE
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
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
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
hr : r.IsPrime
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S

pp: case neg
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
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
hr : ¬r.IsPrime
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S

Tactic:
· have : q.IsPrime := isPrime_of_liesOver r q
    have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)
    let := Localization.AtPrime.algebraOfLiesOver (r.under R) r
    let := Localization.AtPrime.algebraOfLiesOver (r.under R) q
    let := Localization.AtPrime.algebraOfLiesOver q r
    rw [inertiaDeg_def, inertiaDeg_eq (r.under R), inertiaDeg_eq q, eq_comm]
    apply Module.finrank_mul_finrank

Goal state after:
case neg
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
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
hr : ¬r.IsPrime
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime (g • q)) :=
  Localization.AtPrime.algebraOfLiesOver p (g • q)
e₂ : (g • q).ResidueField ≃ₐ[p.ResidueField] q.ResidueField := p.residueFieldAlgEquiv' (g • q) q f₀.symm ⋯
⊢ Module.finrank p.ResidueField (g • q).ResidueField = Module.finrank p.ResidueField q.ResidueField

Tactic:
exact e₂.toLinearEquiv.finrank_eq

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
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ x ∈ R ∙ r

Tactic:
← hr' x hx

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
x : R
hx : x ∈ I
⊢ r * x ∈ R ∙ r
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case h₃
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : I ≠ ⊥ → emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v I
h : p * I ≠ ⊥
⊢ emultiplicity w (map f p) + emultiplicity w (map f I) =
    ↑(v.ramificationIdx' w) * (emultiplicity v p + emultiplicity v I)

Tactic:
IH hI,

Goal state after:
case h₃
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
I p : Ideal R
hI : I ≠ 0
hp : Prime p
IH : I ≠ ⊥ → emultiplicity w (map f I) = ↑(v.ramificationIdx' w) * emultiplicity v I
h : p * I ≠ ⊥
⊢ emultiplicity w (map f p) + ↑(v.ramificationIdx' w) * emultiplicity v I =
    ↑(v.ramificationIdx' w) * (emultiplicity v p + emultiplicity v I)
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ FormallyUnramified R R

Tactic:
rw [iff_comp_injective]
  intro B _ _ _ _ f₁ f₂ _
  exact Subsingleton.elim _ _

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

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
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := ⋯
sA : ↥A := ⋯
f : Localization.Away sA →+* T := ⋯
this✝⁶ : Algebra (Localization.Away sA) T := ⋯
this✝⁵ : Algebra (↥A) (Localization.Away sA) := ⋯
this✝⁴ : SMul (↥A) (Localization.Away sA) := ⋯
this✝³ : MulAction (↥A) (Localization.Away sA) := ⋯
this✝² : IsScalarTower R (↥A) (Localization.Away sA)
this✝¹ : IsScalarTower (↥A) (Localization.Away sA) T
this✝ : IsScalarTower R (Localization.Away sA) T
x : S
n : ℕ
this : IsIntegral (Localization.Away sA) ((algebraMap S T) x)
⊢ (sA • Localization.Away.invSelf sA) ^ n • (algebraMap S T) x =
    Localization.Away.invSelf sA ^ n • ((algebraMap S T) x * (algebraMap S T) s ^ n)

Tactic:
simp only [Algebra.smul_def, map_pow, map_mul, mul_pow,
        ← IsScalarTower.algebraMap_apply, Subalgebra.algebraMap_def, sA]
      ring

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

Goal state before:
pp: R : Type u
A : Type v
B : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
S : Type u_2
inst✝ : CommRing S
⊢ Etale (R × S) R

Tactic:
algebraize [RingHom.fst R S]
  exact Algebra.Etale.of_isLocalizationAway (1, 0)

Goal state after:
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
⊢ ∃ a, (map P.toInfinitesimal) a = ⟨(Cotangent.map P.toInfinitesimal) x, hx⟩

Tactic:
refine ⟨⟨x, ?_⟩, rfl⟩

Goal state after:
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
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 s : P.Ring
hs : s ∈ M'
⊢ IsLocalization.mk' (Localization M') x ⟨s, hs⟩ =
    IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩

Tactic:
IsLocalization.mk'_eq_iff_eq_mul,

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'
⊢ (algebraMap P.Ring (Localization M')) x =
    IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩ *
      (algebraMap P.Ring (Localization M')) ↑⟨s, hs⟩
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
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
hr' : r * ∏ i ∈ s, b i ∣ r'
⊢ Algebra.adjoin R ↑s ≤
    Subalgebra.comap (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))) (awayMapₐ (Algebra.ofId R S) r').range

Tactic:
Algebra.adjoin_le_iff

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
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
hr' : r * ∏ i ∈ s, b i ∣ r'
⊢ ↑s ⊆
    ↑(Subalgebra.comap (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r')))
        (awayMapₐ (Algebra.ofId R S) r').range)
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
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
⊢ v.asIdeal ^ 0 = 1

Tactic:
pow_zero _

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
⊢ 1 = 1
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case inl
q : ℝ≥0∞
hpq : 0 ≤ q
⊢ 0 = 0 ∧ q = 0 ∨
    0 = 0 ∧ q = ∞ ∨
      0 = 0 ∧ 0 < q.toReal ∨
        0 = ∞ ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ q = ∞ ∨ 0 < ENNReal.toReal 0 ∧ 0 < q.toReal ∧ ENNReal.toReal 0 ≤ q.toReal

pp: case inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
· simpa using q.trichotomy

Goal state after:
case inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case mp
a b : ℝ≥0∞
h : a * b < ∞
⊢ ¬b = 0 → a < ∞ ∧ b < ∞ ∨ a = 0

Tactic:
or_iff_not_imp_right

Goal state after:
case mp
a b : ℝ≥0∞
h : a * b < ∞
⊢ ¬b = 0 → ¬a = 0 → a < ∞ ∧ b < ∞
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ 1 = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑1

Tactic:
rw [(algebraMap R K).map_one, Ideal.one_eq_top, coeIdeal_top, mul_one, inv_one,
      spanSingleton_one]

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

Goal state before:
pp: x : ℝ≥0
⊢ ↑(∞ * ↑x) = ⊤ * ↑↑x

Tactic:
rcases eq_or_ne x 0 with (rfl | h0)

Goal state after:
case inl
⊢ ↑(∞ * ↑0) = ⊤ * ↑↑0

case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(∞ * ↑x) = ⊤ * ↑↑x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : a ≠ ∞ ∨ b ≠ 0
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
by
  cases b
  case top =>
    simp_all only [Ne, not_true_eq_false, or_false, top_ne_zero, not_false_eq_true, or_true,
      mul_top, inv_top, mul_zero]
  cases a
  case top =>
    simp_all only [Ne, top_ne_zero, not_false_eq_true, coe_ne_top, or_self, not_true_eq_false,
      coe_eq_zero, false_or, top_mul, inv_top, zero_mul]
  grind [_=_ coe_mul, coe_zero, inv_zero, = mul_inv, coe_ne_top, ENNReal.inv_eq_zero,
    =_ coe_inv, zero_mul, = mul_eq_zero, mul_top, mul_zero, top_mul]

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 * ↑b ≤ c / ↑b * ↑b ↔ a * ↑b ≤ c

Tactic:
ENNReal.div_mul_cancel 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 ↔ a * ↑b ≤ c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
⊢ c / b = d / a ↔ a * c = b * d

Tactic:
rw [eq_div_iff ha ha']
  conv_rhs => rw [eq_comm]
  rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LT β
U : Filter (α × α)
z : β
D : α → α → β
H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s
s : Set (α × α)
⊢ s ∈ U ↔ ∃ i > z, {p | D p.1 p.2 < i} ⊆ s

Tactic:
by simp only [H, subset_def, Prod.forall, mem_ofPred]

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

Goal state before:
pp: α : Type u_2
m' : PseudoEMetricSpace α
ed : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
h :
  { toEDist := ed, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        toUniformSpace := U, uniformity_edist := hU }.toEDist =
    m'.toEDist
⊢ { toEDist := ed, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      toUniformSpace := U, uniformity_edist := hU } =
    m'

Tactic:
obtain ⟨_, _, _, U', hU'⟩ := m'

Goal state after:
α : Type u_2
ed : EDist α
edist_self✝¹ : ∀ (x : α), edist x x = 0
edist_comm✝¹ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝¹ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U' : UniformSpace α
hU' : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
h :
  { toEDist := ed, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
        toUniformSpace := U, uniformity_edist := hU }.toEDist =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        toUniformSpace := U', uniformity_edist := hU' }.toEDist
⊢ { toEDist := ed, edist_self := edist_self✝¹, edist_comm := edist_comm✝¹, edist_triangle := edist_triangle✝¹,
      toUniformSpace := U, uniformity_edist := hU } =
    { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      toUniformSpace := U', uniformity_edist := hU' }
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
⊢ 0 < a ^ n

Tactic:
cases n
  · simpa using ENNReal.pow_pos ha.bot_lt _
  · simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne, ENNReal.inv_pos, false_and,
      not_false_eq_true]

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

Goal state before:
pp: case inr.inl
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
ht : ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
⊢ s ∪ ∅ ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

Tactic:
rwa [union_empty]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
a : α
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, u x ∈ eball a ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε

Tactic:
by
    simp only [true_and, mem_Ici, mem_eball]

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

Goal state before:
pp: x r : ℝ
⊢ closedBall x r = Icc (x - r) (x + r)

Tactic:
by
  ext y
  rw [mem_closedBall, dist_comm, Real.dist_eq, abs_sub_le_iff, mem_Icc, ← sub_le_iff_le_add',
    sub_le_comm]

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

Goal state before:
pp: x y : ℝ
⊢ Ioo x y = Ioo x ((y + x) / 2 + (y - x) / 2)

Tactic:
← add_div,

Goal state after:
x y : ℝ
⊢ Ioo x y = Ioo x ((y + x + (y - x)) / 2)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x y : ℝ
⊢ Icc x y = Icc x ((y + x) / 2 + (y - x) / 2)

Tactic:
← add_div,

Goal state after:
x y : ℝ
⊢ Icc x y = Icc x ((y + x + (y - x)) / 2)
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: case neg
ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

Tactic:
simp only [hne, false_or]

Goal state after:
case neg
ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ ∀ (i : ι), IsBounded (S i)
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
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
⊢ False

Tactic:
apply ha' _ hp's

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) := ⋯
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
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := ⋯
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
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
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : q = p'
⊢ a p' ∈ J * (↑⟨q, hq⟩).asIdeal

pp: case neg
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
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ a p' ∈ J * (↑⟨q, hq⟩).asIdeal

Tactic:
· subst hqp
    convert! sub_mem H₁ H₂
    rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem hp's, add_sub_cancel_right]

Goal state after:
case neg
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
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ a p' ∈ J * (↑⟨q, hq⟩).asIdeal
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
t : Set α
htf : t.Finite
hst : s ⊆ ⋃ y ∈ t, eball y ε
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε

Tactic:
exact ⟨t, htf.countable, hst.trans <| iUnion₂_mono fun _ _ => eball_subset_closedEBall⟩

Goal state after: