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

Goal state before:
pp: case succ.refine_2.h
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
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
d : S
⊢ ∃ a, (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) a = ⟦d⟧

Tactic:
| _ d
     => 

Goal state after:
case succ.refine_2.h
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
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
d : S
⊢ ∃ a, (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) a = ⟦d⟧
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Tactic:
refine ⟨r, ?_, ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ r ∉ p

case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ IsIdempotentElem r

case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this : (algebraMap R (Localization p.primeCompl)) r = 1
⊢ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm P)
⊢ ∃ P_1, P_1.IsMaximal ∧ under ℤ P_1 = span {p} ∧ P_1 ∣ P * I

Tactic:
have := (Ideal.isPrime_of_prime hP).isMaximal hP.ne_zero

Goal state after:
case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm P)
this : P.IsMaximal
⊢ ∃ P_1, P_1.IsMaximal ∧ under ℤ P_1 = span {p} ∧ P_1 ∣ P * I
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
⊢ Module.Finite R₀ ↥N

Tactic:
refine hs (h.imp ?_ ?_)

Goal state after:
case refine_1
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
⊢ IsNoetherian R M → IsNoetherian R ↥(Ring.jacobson R • ⊤)

case refine_2
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝³ : AddCommGroup M
x✝² : Module R₀ M
x✝¹ : Module R M
x✝ : IsScalarTower R₀ R M
hs :
  IsNoetherian R ↥(Ring.jacobson R • ⊤) ∨ IsArtinian R ↥(Ring.jacobson R • ⊤) → Module.Finite R₀ ↥(Ring.jacobson R • ⊤)
hq :
  IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ∨ IsArtinian R (M ⧸ Ring.jacobson R • ⊤) →
    Module.Finite R₀ (M ⧸ Ring.jacobson R • ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (Ring.jacobson R • ⊤)
⊢ IsArtinian R M → IsArtinian R ↥(Ring.jacobson R • ⊤)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case inr
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 S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
this✝ : P.IsPrime
this : IsTorsionFree R T
hP : P ≠ ⊥
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q

Tactic:
exact ramificationIdx'_algebra_tower (map_ne_bot_of_ne_bot hP) (map_ne_bot_of_ne_bot hp)
    <| map_le_iff_le_comap.mpr <| le_of_eq <| over_def Q P

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 := R[s]
sA : ↥A := ⟨s, ⋯⟩
f : Localization.Away sA →+* T := IsLocalization.Away.lift sA ⋯
this✝⁵ : Algebra (Localization.Away sA) T := f.toAlgebra
this✝⁴ : Algebra (↥A) (Localization.Away sA) := OreLocalization.instAlgebra
this✝³ : SMul (↥A) (Localization.Away sA) := this✝⁴.toSMul
this✝² : MulAction (↥A) (Localization.Away sA) := toModule.toMulAction
this✝¹ : IsScalarTower R (↥A) (Localization.Away sA)
this✝ : IsScalarTower (↥A) (Localization.Away sA) T
this : IsScalarTower R (Localization.Away sA) T
x : S
n : ℕ
⊢ IsIntegral (Localization.Away sA) (IsLocalization.mk' T x ⟨(fun x ↦ s ^ x) n, ⋯⟩)

Tactic:
have : _root_.IsIntegral (Localization.Away sA) (algebraMap S T x) :=
      (Algebra.IsIntegral.isIntegral (R := R) x).algebraMap.tower_top

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
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := ⟨s, ⋯⟩
f : Localization.Away sA →+* T := IsLocalization.Away.lift sA ⋯
this✝⁶ : Algebra (Localization.Away sA) T := f.toAlgebra
this✝⁵ : Algebra (↥A) (Localization.Away sA) := OreLocalization.instAlgebra
this✝⁴ : SMul (↥A) (Localization.Away sA) := this✝⁵.toSMul
this✝³ : MulAction (↥A) (Localization.Away sA) := toModule.toMulAction
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)
⊢ IsIntegral (Localization.Away sA) (IsLocalization.mk' T x ⟨(fun x ↦ s ^ x) n, ⋯⟩)
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
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
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
x : P₁.infinitesimal.Ring
⊢ (algebraMap P₂.infinitesimal.Ring A) ((Ideal.Quotient.liftₐ (P₁.ker ^ 2) lift ⋯).toRingHom x) =
    (algebraMap A A) ((algebraMap P₁.infinitesimal.Ring A) x)

Tactic:
by
      obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
      exact FormallySmooth.liftOfSurjective_apply _
            (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) _ _ x

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

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝ ⊗ₜ[R] y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ ⊗ₜ[R] y✝)

pp: case add
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S ⊗[R] S
a✝¹ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) x✝
a✝ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) y✝
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * (x✝ + y✝)) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ + y✝)

Tactic:
· simp [TensorProduct.smul_tmul']

Goal state after:
case add
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S = r ⊗ₜ[R] 1 * elem R S
x✝ y✝ : S ⊗[R] S
a✝¹ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * x✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) x✝
a✝ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * y✝) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) y✝
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (r ⊗ₜ[R] 1 * (x✝ + y✝)) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (x✝ + y✝)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2
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.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ (Q.comp P).toExtension.Ring ∙ ↑z ≤
    Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
      (Submodule.comap Extension.Cotangent.mk
        (Submodule.restrictScalars (Q.comp P).Ring
          (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range)))

Tactic:
Submodule.span_singleton_le_iff_mem

Goal state after:
case h2
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.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ ↑z ∈
    Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
      (Submodule.comap Extension.Cotangent.mk
        (Submodule.restrictScalars (Q.comp P).Ring
          (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range)))
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case mul_X.inr
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 σ
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
p : MvPolynomial (ι ⊕ σ) R
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
n : σ
⊢ eval₂ (algebraMap R T) (fun i ↦ Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) i) p •
        (δAux R Q) (Sum.elim X (⇑C ∘ P.val) (Sum.inr n)) +
      (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) (Sum.inr n)) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2 =
    (aeval (Q.comp P).val) p •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) ((Q.comp P).cotangentSpaceBasis (Sum.inr n))).2 +
      Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) (Sum.inr n) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2

Tactic:
simp only [Sum.elim_inr, Function.comp_apply, algHom_C, δAux_C,
        CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply,
        algebraMap_smul, Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply,
        LinearMap.coe_inr, Basis.baseChange_apply, one_smul, LinearMap.baseChange_tmul,
        toKaehler_cotangentSpaceBasis, add_left_inj, LinearMap.coe_inl]

Goal state after:
case mul_X.inr
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 σ
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
p : MvPolynomial (ι ⊕ σ) R
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
n : σ
⊢ eval₂ (algebraMap R T) (fun i ↦ Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) i) p • 1 ⊗ₜ[S] (D R S) (P.val n) =
    (aeval (Q.comp P).val) p • 1 ⊗ₜ[S] (D R S) (P.val n)
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: 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
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
x y : S ⊗[P] Ω[P⁄R]
⊢ ↑(l x) * ↑(l y) ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)

Tactic:
exact Ideal.mul_mem_mul (l x).2 (l y).2

Goal state after:
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✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx : (localRingHom p q (algebraMap R S) ⋯) (IsLocalization.mk' (Localization.AtPrime p) x s) = 0
⊢ IsLocalization.mk' (Localization.AtPrime p) x s = 0

Tactic:
obtain ⟨a, haq, e⟩ : ∃ a ∉ q, a * (algebraMap R S) x = 0 := by
    simpa [Localization.localRingHom_mk', IsLocalization.mk'_eq_zero_iff] using hx

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✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx : (localRingHom p q (algebraMap R S) ⋯) (IsLocalization.mk' (Localization.AtPrime p) x s) = 0
a : S
haq : a ∉ q
e : a * (algebraMap R S) x = 0
⊢ IsLocalization.mk' (Localization.AtPrime p) x s = 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₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x : T ⊗[S] P.toExtension.H1Cotangent
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x),
      x_in⟩ ∈
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
use x

Goal state after:
case h
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 σ
inst✝ : Flat S T
x : T ⊗[S] P.toExtension.H1Cotangent
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) x =
    ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ((lTensor T Extension.h1Cotangentι) x),
      x_in⟩
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'
⊢ (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))).range ≤ (awayMapₐ (Algebra.ofId R S) r').range

Tactic:
rw [← Algebra.map_top, Subalgebra.map_le, ← hs, 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.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : ¬t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
obtain rfl := not_nonempty_iff_eq_empty.1 ht

Goal state after:
case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
a✝ : ∅ ∈ s.powerset
ht : ¬∅.Nonempty
⊢ (-1) ^ #∅ • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #∅ * ((∏ i ∈ s \ ∅, 1) * ∏ i ∈ ∅, (↑(S i)).indicator 1 x)) • f x
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ≥0
h : p ≠ 0
⊢ r < p⁻¹ ↔ r * p < 1

Tactic:
← mul_lt_mul_iff_right₀ (pos_iff_ne_zero.2 h),

Goal state after:
r p : ℝ≥0
h : p ≠ 0
⊢ p * r < p * p⁻¹ ↔ r * p < 1
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2.refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ { q' // x < ↑q' }

Tactic:
exact ⟨y, hxy⟩

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

Goal state before:
pp: r : ℝ
⊢ ∃ x, r = ↑x ∨ r = -↑x

Tactic:
obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by simpa using le_total ..
  all_goals
    rw [← neg_neg r]
    lift (_ : ℝ) to ℝ≥0 using hr with r
    aesop

Goal state after:
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
p✝ q✝ p q : NonarchAddGroupSeminorm E
⊢ (⇑p ⊔ ⇑q) 0 = 0

Tactic:
by rw [Pi.sup_apply, ← map_zero p, sup_eq_left, map_zero p, map_zero q]

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

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

Tactic:
exact ENNReal.sub_mul h

Goal state after: