mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case succ
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
⊢ cardQuot (P ^ (i + 1)) = cardQuot P ^ (i + 1)

Tactic:
have : P ^ (i + 1) < P ^ i := Ideal.pow_succ_lt_pow hP i

Goal state after:
case succ
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
⊢ cardQuot (P ^ (i + 1)) = cardQuot P ^ (i + 1)
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
⊢ ↑y * (↑x * ↑(S.fromLeftInv x) * ↑(S.fromLeftInv y)) = 1

Tactic:
mul_fromLeftInv,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : ↥S.leftInv
⊢ ↑y * (1 * ↑(S.fromLeftInv y)) = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ s = Set.univᶜ

Tactic:
eq_compl_comm,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
this : ∀ (x : PrimeSpectrum R), x.asIdeal.IsMaximal → ↑I ⊆ ↑x.asIdeal
⊢ Set.univ = sᶜ
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst✝] (closure[inst✝] Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure[inst✝] Z ∩ closedPoints X ⊆ closure[inst✝] Z \ Z

Tactic:
Set.subset_sdiff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst✝] (closure[inst✝] Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure[inst✝] Z ∩ closedPoints X ⊆ closure[inst✝] Z ∧ Disjoint (closure[inst✝] Z ∩ closedPoints X) Z
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst✝] (closure[inst✝] Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure[inst✝] Z \ Z
⊢ False

Tactic:
Set.subset_sdiff,

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst✝] (closure[inst✝] Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure[inst✝] Z ∧ Disjoint Z Z
⊢ False
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: 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}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ IsOpen {x}

Tactic:
rw [this, isOpen_compl_iff]
      refine Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)
      exact (finite_setOfPred_isMin R).subset fun x h ↦ h.1

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsArtinianRing R ↔ Ring.KrullDimLE 0 R

Tactic:
by
  rwa [isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, and_iff_right]

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ nilradical R ≠ ⊤

Tactic:
by simp [nilradical, Ideal.radical_eq_top]

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

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
inst✝² : p.IsPrime
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : p = under R q
⊢ q.inertiaDeg R = Module.finrank p.ResidueField q.ResidueField

Tactic:
subst this

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : q.LiesOver (under R q)
inst✝² : (under R q).IsPrime
inst✝¹ : Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ q.inertiaDeg R = Module.finrank (under R q).ResidueField q.ResidueField
Module: Mathlib.RingTheory.Ideal.IdempotentFG

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

Tactic:
rintro (rfl | rfl)

Goal state after:
case mpr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ⊥.FG
⊢ IsIdempotentElem ⊥

case mpr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ⊤.FG
⊢ IsIdempotentElem ⊤
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
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    maximalIdeal (Localization P.primeCompl) * maximalIdeal (Localization P.primeCompl)
this : map (algebraMap S (Localization.AtPrime P)) P = ⊥
⊢ Function.Injective ⇑(algebraMap S (Localization.AtPrime P))

Tactic:
exact IsLocalization.injective _ hp'

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

Goal state before:
pp: case pos
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : i = 0
x : A
this : Subsingleton (B ⧸ I ^ i)
⊢ ((Ideal.Quotient.mkₐ R (I ^ i)).comp g₁) x = ((Ideal.Quotient.mkₐ R (I ^ i)).comp g₂) x

Tactic:
exact Subsingleton.elim _ _

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I✝ : Ideal B
x✝ : I✝ ^ 2 = ⊥
f₁ f₂ : R →ₐ[R] B
a✝ : (Ideal.Quotient.mkₐ R I✝).comp f₁ = (Ideal.Quotient.mkₐ R I✝).comp f₂
⊢ f₁ = f₂

Tactic:
exact Subsingleton.elim _ _

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
⊢ Ideal.under R (Ideal.map (algebraMap S (Localization.AtPrime Q)) P) =
    Ideal.under R (IsLocalRing.maximalIdeal (Localization.AtPrime Q))

Tactic:
convert! h₂ <;> rw [← Ideal.under_under (B := S)]

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
⊢ Ideal.under R (Ideal.under S (Ideal.map (algebraMap S (Localization.AtPrime Q)) P)) = Ideal.under R P

case e'_3
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
⊢ Ideal.under R (Ideal.under S (IsLocalRing.maximalIdeal (Localization.AtPrime Q))) = Ideal.under R Q
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 ι
n : ι →₀ ℕ
r : S
⊢ (δAux R Q) ((monomial n) r) = (n.prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) r

Tactic:
simp [δAux]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Ideal R
inst✝⁴ : P.IsPrime
Q : Ideal A
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
inst✝¹ : IsUnramifiedAt R Q
Q' : Ideal (P.Fiber A)
inst✝ : Q'.IsPrime
hQ' : Q = Ideal.comap TensorProduct.includeRight.toRingHom Q'
⊢ IsUnramifiedAt P.ResidueField Q'

Tactic:
let f₀ : Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q' :=
    Localization.localAlgHom Q Q' _ hQ'
  have hf₀ : Function.Surjective f₀ := by
    subst hQ'; exact P.surjectiveOnStalks_residueField.baseChange' _ _
  let f : P.Fiber (Localization.AtPrime Q) →ₐ[P.ResidueField] Localization.AtPrime Q' :=
    Algebra.TensorProduct.lift (Algebra.ofId _ _) f₀ fun _ _ ↦ .all _ _
  have hf : Function.Surjective f := hf₀.forall.mpr fun x ↦ ⟨1 ⊗ₜ x, by simp [f]⟩
  exact .of_surjective _ hf

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (Module.support A Ω[A⁄R])ᶜ = Set.univ ↔ FormallyUnramified R A

Tactic:
compl_eq_comm,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Set.univᶜ = Module.support A Ω[A⁄R] ↔ FormallyUnramified R A
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case e_a
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ g ((algebraMap P S) p) * ↑m = p * ↑m

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← hf', pow_two, ← sub_mul]

Goal state after:
case e_a
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ (g ((algebraMap P S) p) - p) * ↑m ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
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✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
this : f₁ x - f₂ x ∈ I
⊢ f₁ x = f₂ x

Tactic:
have := Polynomial.eval_add_of_sq_eq_zero ((minpoly K x).map (algebraMap K B)) (f₂ x)
    (f₁ x - f₂ x) (show (f₁ x - f₂ x) ^ 2 ∈ ⊥ from hI ▸ Ideal.pow_mem_pow this 2)

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
this✝ : f₁ x - f₂ x ∈ I
this :
  eval (f₂ x + (f₁ x - f₂ x)) (map (algebraMap K B) (minpoly K x)) =
    eval (f₂ x) (map (algebraMap K B) (minpoly K x)) +
      eval (f₂ x) (derivative (map (algebraMap K B) (minpoly K x))) * (f₁ x - f₂ x)
⊢ f₁ x = f₂ x
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hz
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 : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y

Tactic:
← CotangentSpace.compEquiv_symm_inr

Goal state after:
case hz
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 : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (↑(CotangentSpace.compEquiv Q P).symm ∘ₗ
        LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
      z =
    (Q.comp P).toExtension.cotangentComplex y
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 σ
r : S
hr : C r ∈ Q.ker
⊢ (δ Q P) ⟨Extension.Cotangent.mk ⟨C r, hr⟩, ⋯⟩ = 1 ⊗ₜ[S] (D R S) r

Tactic:
δ_eq_δAux,

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₂
Q : Generators S T ι
P : Generators R S σ
r : S
hr : C r ∈ Q.ker
⊢ (δAux R Q) ↑⟨C r, hr⟩ = 1 ⊗ₜ[S] (D R S) r
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₄
Q : Generators S T ι
P : Generators R S σ
P' : Generators R S σ'
x : ↥Q.toExtension.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
⊢ (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δ Q P') ⟨Extension.Cotangent.mk x, hx⟩

Tactic:
δ_eq_δAux,

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₄
Q : Generators S T ι
P : Generators R S σ
P' : Generators R S σ'
x : ↥Q.toExtension.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
⊢ (δAux R Q) ↑x = (δ Q P') ⟨Extension.Cotangent.mk x, hx⟩
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: 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✝¹ : Algebra.EssFiniteType R S
inst✝ : Algebra.IsUnramifiedAt R q
⊢ q.ramificationIdx R = 1

Tactic:
let p := q.under R
  let Rp := Localization.AtPrime p
  let Sq := Localization.AtPrime q
  let : Algebra Rp Sq := Localization.AtPrime.algebraOfLiesOver p q
  have : Algebra.EssFiniteType Rp Sq := Algebra.EssFiniteType.of_comp R Rp Sq
  rw [ramificationIdx_def, ENat.toNat_eq_iff_eq_natCast, Nat.cast_one, Module.length_eq_one_iff,
    isSimpleModule_iff_isCoatom, ← Ideal.isMaximal_def, IsLocalRing.isMaximal_iff,
    IsScalarTower.algebraMap_eq R Rp Sq, ← map_map, Localization.AtPrime.map_eq_maximalIdeal]
  exact Algebra.FormallyUnramified.map_maximalIdeal

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
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
⊢ IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap

Tactic:
rw [isLocalizedModule_iff_isLocalization]

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
⊢ IsLocalization (algebraMapSubmonoid S M') T
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✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

Tactic:
by_cases hr : r.IsPrime
  · have : q.IsPrime := isPrime_of_liesOver r q
    let := Localization.AtPrime.algebraOfLiesOver q r
    apply ramificationIdx_tower'
  · rw [ramificationIdx_of_not_isPrime r R hr, ramificationIdx_of_not_isPrime r S hr, mul_zero]

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

Goal state before:
pp: case a
ι : 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
t : Finset ι
a✝ : t ∈ s.powerset
⊢ (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a = ((-1) ^ #t * (⋂ i ∈ t, S i).indicator 1 a) • f a

Tactic:
simp [Set.indicator]

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

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ∈ lowerBounds (range fun i ↦ f i)

Tactic:
simpa [mem_lowerBounds]

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

Goal state before:
pp: a : ℝ≥0∞
s : Set ℝ≥0∞
⊢ a + sInf s = ⨅ b ∈ s, a + b

Tactic:
rw [sInf_eq_iInf, add_iInf₂]

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

Goal state before:
pp: x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ ∃ j, j < z

Tactic:
by exact ⟨0, hz.bot_lt⟩

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

Goal state before:
pp: case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑x.toReal

Tactic:
· simp only [le_refl, coe_toReal h h']

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

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

Tactic:
by
  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 : EReal
hx : 0 ≤ x
⊢ ↑x.toENNReal = x

Tactic:
rw [toENNReal]

Goal state after:
x : EReal
hx : 0 ≤ x
⊢ ↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) = x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a⁻¹⁻¹ = a

Tactic:
by_cases a = 0 <;> cases a <;> simp_all [-coe_inv, (coe_inv _).symm]

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

Goal state before:
pp: case top
a : ℝ≥0∞
c : ℝ≥0
h0 : ∞ ≠ 0 ∨ ↑c ≠ 0
ht : ∞ ≠ ∞ ∨ ↑c ≠ ∞
⊢ a = 0 ↔ a * ∞ ≤ ↑c

Tactic:
rcases eq_or_ne a 0 with (rfl | ha) <;> simp [*]

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a / 2 + a / 2 = a

Tactic:
by
  rw [div_eq_mul_inv, ← mul_add, inv_two_add_inv_two, mul_one]

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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : ¬(I ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = 0

Tactic:
· rw [count_mul' K v, if_neg h]

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

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

Tactic:
ENNReal.zpow_neg

Goal state after:
x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
⊢ x ^ m * (x ^ n)⁻¹ = x ^ m * (x ^ n)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inr
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹

Tactic:
rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ

Tactic:
mem_iInter₂

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ i > ε, y ∈ ball x 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
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
⊢ ∃ a, J * I ⊔ Ideal.span {a} = J

Tactic:
exact ⟨a, by rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]⟩

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
⊢ ∃ a K, J * K = Ideal.span {a} ∧ I + K = ⊤

Tactic:
let s := (I.finite_factors hI).toFinset

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
⊢ ∃ a K, J * K = Ideal.span {a} ∧ I + K = ⊤