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

Goal state before:
pp: case refine_2
R✝ : Type u
A✝ : Type v
inst✝¹⁴ : CommRing R✝
inst✝¹³ : CommRing A✝
inst✝¹² : Algebra R✝ A✝
B✝ : Type u_1
P : Type u_2
C✝ : Type u_3
inst✝¹¹ : CommRing B✝
inst✝¹⁰ : Algebra R✝ B✝
inst✝⁹ : CommRing C✝
inst✝⁸ : Algebra R✝ C✝
inst✝⁷ : CommRing P
inst✝⁶ : Algebra R✝ P
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✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
this : IsScalarTower R B C
⊢ (Ideal.Quotient.mkₐ B I).comp
      (TensorProduct.productLeftAlgHom (ofId B C)
        (lift I ⋯ ((AlgHom.restrictScalars R f).comp TensorProduct.includeRight))) =
    f

Tactic:
· apply AlgHom.restrictScalars_injective R
    apply TensorProduct.ext'
    intro b a
    suffices algebraMap B _ b * f (1 ⊗ₜ[R] a) = f (b ⊗ₜ[R] a) by simpa [Algebra.ofId_apply]
    rw [← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
Q : Generators S T ι
r : S
⊢ (δAux R Q) (C r) = 1 ⊗ₜ[S] (D R S) r

Tactic:
by
  rw [← monomial_zero', δAux_monomial, Finsupp.prod_zero_index]

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

Goal state before:
pp: 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
⊢ ¬Subsingleton (L ⊗[K] L)

Tactic:
← rank_zero_iff (R := K),

Goal state after:
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
⊢ ¬Module.rank K (L ⊗[K] L) = 0
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₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx : Extension.Cotangent.mk ⟨y, hy⟩ ∈ Q'.toExtension.cotangentComplex.ker
⊢ (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩) =
    (δ Q' P') ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩

Tactic:
change δ _ _ ⟨_, _⟩ = δ _ _ _

Goal state after:
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₃
σ : Type w₂
σ' : Type w₄
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx : Extension.Cotangent.mk ⟨y, hy⟩ ∈ Q'.toExtension.cotangentComplex.ker
⊢ (δ Q P)
      ⟨((Extension.Cotangent.map f.toExtensionHom).domRestrict Q'.toExtension.cotangentComplex.ker)
          ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩,
        ⋯⟩ =
    (δ Q' P') ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : P.toInfinitesimal.toRingHom ↑x ∈ ⊥
⊢ ↑x ∈ P.ker ^ 2

Tactic:
simpa only [toInfinitesimal, Ideal.mem_bot, infinitesimal,
        Ideal.Quotient.eq_zero_iff_mem] using hx

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

Goal state before:
pp: case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := ⋯
Sq : Type u_1 := ⋯
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) ≠
    0

Tactic:
← pos_iff_ne_zero,

Goal state after:
case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ 0 <
    Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
inst✝¹ : q.LiesOver p
inst✝ : q.IsPrime
⊢ (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) p)).toNat

Tactic:
over_def q p

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : q.LiesOver p
inst✝ : q.IsPrime
⊢ (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case left
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
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.H1Cotangent
hx : (LinearMap.liftBaseChange T (H1Cotangent.map f)) x = 0
⊢ x = 0

Tactic:
apply Module.Flat.lTensor_preserves_injective_linearMap _ h1Cotangentι_injective

Goal state after:
case left
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
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.H1Cotangent
hx : (LinearMap.liftBaseChange T (H1Cotangent.map f)) x = 0
⊢ (LinearMap.lTensor T h1Cotangentι) x = (LinearMap.lTensor T h1Cotangentι) 0
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
h :
  map (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R S) p)) * I
hqI : I ≤ q
⊢ q ⊔ I ≠ ⊤

Tactic:
rw [sup_of_le_left hqI]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
h :
  map (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R S) p)) * I
hqI : I ≤ q
⊢ q ≠ ⊤
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    map (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx' q) *
      map (algebraMap S (Localization.AtPrime q)) I
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
Ideal.map_pow,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    map (algebraMap S (Localization.AtPrime q)) q ^ p.ramificationIdx' q * map (algebraMap S (Localization.AtPrime q)) I
⊢ p.ramificationIdx' q = q.ramificationIdx R
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

Tactic:
have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)

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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S
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
κp : Type u_1 := p.ResidueField
κr : Type u_2 := r.ResidueField
A : Type u_2 := Sr ⧸ map (algebraMap R Sr) p
this : length Sr A * ↑(finrank κp κr) = ↑(finrank κp Sq)
⊢ (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:
simpa using congr_arg ENat.toNat this

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

Goal state before:
pp: case refine_2
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 ⋯
this✝ :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (Algebra.linearMap P.Ring S).ker =
    RingHom.ker fQ
this :
  F =
    ↑(LinearEquiv.restrictScalars P.Ring
          (LinearEquiv.ofEq
            (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker)
            (RingHom.ker fQ) this✝)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker
⊢ IsLocalizedModule M'
    (↑(LinearEquiv.restrictScalars P.Ring
          (LinearEquiv.ofEq
            (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker)
            (RingHom.ker fQ) this✝)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker)

Tactic:
exact IsLocalizedModule.of_linearEquiv _ _ _

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha' : a ∈ ⋃ i ∈ s, S i
ha : ∃ i ∈ s, a ∈ S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

Tactic:
obtain ⟨i, hi, ha⟩ := ha

Goal state after:
case pos
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha' : a ∈ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
ha : a ∈ S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0
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
a : A
ha : a ∈ 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
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
hPairwise : (↑S).Pairwise fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
⊢ ∀ x ∈ ⨆ i ∈ S, torsionBySet A M ↑(i.maxPowDividing (span {a})), x ∈ ⨆ P, primaryComponent M P.asIdeal

Tactic:
← SetLike.le_def

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
a : A
ha : a ∈ 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
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
hPairwise : (↑S).Pairwise fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
⊢ ⨆ i ∈ S, torsionBySet A M ↑(i.maxPowDividing (span {a})) ≤ ⨆ P, primaryComponent M P.asIdeal
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ 0 = ⊥

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε

Tactic:
· rcases H ε ε_pos with ⟨x, x_in, hx⟩
    exact csInf_lt_of_lt h x_in hx

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:
by rw [← pow_mul, mul_left_comm, sq]

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

Goal state before:
pp: α : Type u_1
⊢ 0 = ⊥

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: r : ℝ
⊢ ENNReal.ofReal r ≠ 0 ↔ 0 < r

Tactic:
← pos_iff_ne_zero,

Goal state after:
r : ℝ
⊢ 0 < ENNReal.ofReal r ↔ 0 < r
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ a < a + b

Tactic:
← pos_iff_ne_zero,

Goal state after:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : 0 < b
⊢ a < a + b
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ a < a + b

Tactic:
by
  rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb

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

Goal state before:
pp: case mpr.inl
a b : ℝ≥0∞
ha : a < ∞
hb : b < ∞
⊢ a * b < ∞

Tactic:
exact mul_lt_top ha hb

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

Goal state before:
pp: case inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ¬∃ i, f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
replace h i : 0 ≤ f i := le_of_not_ge fun hi ↦ h ⟨i, hi⟩

Goal state after:
case inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0
n : ℕ
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)

Tactic:
by
    rcases eq_or_ne a 0 with (rfl | ha)
    · simp [top_pow]
    · have := pow_ne_zero (n + 1) ha
      norm_cast
      rw [inv_pow]

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
hv : ↑v.asIdeal ≠ 0
⊢ ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal

Tactic:
rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]

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

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

Tactic:
by rw [lt_inv_iff_lt_inv, inv_one]

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

Goal state before:
pp: case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ∞
⊢ a / c ≤ b

Tactic:
exact (ENNReal.div_le_iff_le_mul (Or.inl h0) (Or.inl hinf)).2 h

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
hw : w ≠ v
⊢ ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal

Tactic:
rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]

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

Goal state before:
pp: ⊢ 2 / 2 = 1

Tactic:
ENNReal.div_self two_ne_zero ofNat_ne_top

Goal state after:
⊢ 1 = 1
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ∞

Tactic:
← pos_iff_ne_zero,

Goal state after:
a b : ℝ≥0∞
⊢ 0 < a / b ↔ a ≠ 0 ∧ 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
exps : HeightOneSpectrum R →₀ ℤ
⊢ count K v (exps.prod fun x1 x2 ↦ ↑x1.asIdeal ^ x2) = exps v

Tactic:
by
  rw [Finsupp.prod, count_prod]
  · classical simp only [count_zpow, count_maximal, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq',
      exps.mem_support_iff, ne_eq, ite_not, ite_eq_right_iff, @eq_comm ℤ 0, imp_self]
  · exact fun v hv ↦ zpow_ne_zero _ (coeIdeal_ne_zero.mpr v.ne_bot)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ eball x ε ↔ edist x y < ε

Tactic:
rw [edist_comm, mem_eball]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ x ∈ closedEBall x ε

Tactic:
rw [mem_closedEBall, edist_self]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ 0 ≤ ε
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
I J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : ↑J' = J⁻¹ * I
⊢ ↑J' ≠ 0

Tactic:
exact hJ' ▸ mul_ne_zero (inv_ne_zero hJ) hI

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
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

Tactic:
· convert! finite_factors' hI (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2
    rw [count_ne_zero K _ hI]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h

Tactic:
apply le_trans (dist_triangle4 a f g h)
  gcongr
  apply le_trans (dist_triangle4 a d e f)
  gcongr
  exact dist_triangle4 a b c d

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ¬(ball x ε).Nonempty ↔ ε ≤ 0

Tactic:
nonempty_ball,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ¬0 < ε ↔ ε ≤ 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α✝
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
⊢ PseudoMetricSpace.toBornology = PseudoMetricSpace.toBornology

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α✝
α : Type u_3
B : Bornology α
m : PseudoMetricSpace α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ PseudoMetricSpace.toUniformSpace = PseudoMetricSpace.toUniformSpace

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
inst✝² : Finite ι
inst✝¹ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
t : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
⊢ (pseudoMetrizableSpaceUniformity X).toTopologicalSpace = t

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
⊢ TotallyBounded s

Tactic:
by
  rcases s.eq_empty_or_nonempty with hs | hs
  · rw [hs]
    exact totallyBounded_empty
  rcases hs with ⟨x0, hx0⟩
  have : Inhabited s := ⟨⟨x0, hx0⟩⟩
  refine totallyBounded_iff.2 fun ε ε0 => ?_
  rcases H ε ε0 with ⟨β, fβ, F, hF⟩
  let Finv := Function.invFun F
  refine ⟨range (Subtype.val ∘ Finv), finite_range _, fun x xs => ?_⟩
  let x' := Finv (F ⟨x, xs⟩)
  have : F x' = F ⟨x, xs⟩ := Function.invFun_eq ⟨⟨x, xs⟩, rfl⟩
  simp only [Set.mem_iUnion, Set.mem_range]
  exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩

Goal state after: