mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ f ⁻¹' closedPoints Y = closedPoints X

Tactic:
ext x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
x : X
⊢ x ∈ f ⁻¹' closedPoints Y ↔ x ∈ closedPoints X
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
U Z : Set (PrimeSpectrum R)
hS : (U ∩ Z).Nonempty
hU : ∃ I, (zeroLocus ↑I)ᶜ = U
hZ : ∃ I, Z = zeroLocus ↑I
⊢ (U ∩ Z ∩ closedPoints (PrimeSpectrum R)).Nonempty

Tactic:
obtain ⟨⟨I, rfl⟩, ⟨J, rfl⟩⟩ := And.intro hU hZ

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
I : Ideal R
hU : ∃ I_1, (zeroLocus ↑I_1)ᶜ = (zeroLocus ↑I)ᶜ
J : Ideal R
hZ : ∃ I, zeroLocus ↑J = zeroLocus ↑I
hS : ((zeroLocus ↑I)ᶜ ∩ zeroLocus ↑J).Nonempty
⊢ ((zeroLocus ↑I)ᶜ ∩ zeroLocus ↑J ∩ closedPoints (PrimeSpectrum R)).Nonempty
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✝ : IsSemiprimaryRing R
M : Type u
x✝³ : AddCommGroup M
x✝² x✝¹ : Module R M
x✝ : IsScalarTower R R M
h : IsNoetherian R ↥(Ring.jacobson R • ⊤) ↔ IsArtinian R ↥(Ring.jacobson R • ⊤)
h' : IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
N : Submodule R M := Ring.jacobson R • ⊤
⊢ IsNoetherian R ↥N ∧ IsNoetherian R (M ⧸ N) ↔ IsArtinian R M

Tactic:
isArtinian_iff_submodule_quotient N,

Goal state after:
R : Type u_2
M✝ : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M✝
inst✝¹ : Module R M✝
inst✝ : IsSemiprimaryRing R
M : Type u
x✝³ : AddCommGroup M
x✝² x✝¹ : Module R M
x✝ : IsScalarTower R R M
h : IsNoetherian R ↥(Ring.jacobson R • ⊤) ↔ IsArtinian R ↥(Ring.jacobson R • ⊤)
h' : IsNoetherian R (M ⧸ Ring.jacobson R • ⊤) ↔ IsArtinian R (M ⧸ Ring.jacobson R • ⊤)
N : Submodule R M := Ring.jacobson R • ⊤
⊢ IsNoetherian R ↥N ∧ IsNoetherian R (M ⧸ N) ↔ IsArtinian R ↥N ∧ IsArtinian R (M ⧸ N)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R B
inst✝⁶ : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
inst✝⁴ : p.IsMaximal
inst✝³ : q.IsMaximal
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ q)
⊢ (algebraMap p.ResidueField q.ResidueField).comp ↑(RingEquiv.ofBijective (algebraMap (A ⧸ p) p.ResidueField) ⋯) =
    (↑(RingEquiv.ofBijective (algebraMap (B ⧸ q) q.ResidueField) ⋯)).comp (algebraMap (A ⧸ p) (B ⧸ q))

Tactic:
ext x

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R B
inst✝⁶ : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
inst✝⁴ : p.IsMaximal
inst✝³ : q.IsMaximal
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ q)
x : A
⊢ (((algebraMap p.ResidueField q.ResidueField).comp ↑(RingEquiv.ofBijective (algebraMap (A ⧸ p) p.ResidueField) ⋯)).comp
        (Ideal.Quotient.mk p))
      x =
    (((↑(RingEquiv.ofBijective (algebraMap (B ⧸ q) q.ResidueField) ⋯)).comp (algebraMap (A ⧸ p) (B ⧸ q))).comp
        (Ideal.Quotient.mk p))
      x
Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R B
inst✝⁶ : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
inst✝⁴ : p.IsMaximal
inst✝³ : q.IsMaximal
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ q)
x : A
⊢ (((algebraMap p.ResidueField q.ResidueField).comp ↑(RingEquiv.ofBijective (algebraMap (A ⧸ p) p.ResidueField) ⋯)).comp
        (Ideal.Quotient.mk p))
      x =
    (((↑(RingEquiv.ofBijective (algebraMap (B ⧸ q) q.ResidueField) ⋯)).comp (algebraMap (A ⧸ p) (B ⧸ q))).comp
        (Ideal.Quotient.mk p))
      x

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R B
inst✝⁶ : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
inst✝⁴ : p.IsMaximal
inst✝³ : q.IsMaximal
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsSeparable p.ResidueField q.ResidueField
x : A
⊢ (RingEquiv.ofBijective (algebraMap (B ⧸ q) q.ResidueField) ⋯)
      ((algebraMap (A ⧸ p) (B ⧸ q)) ((Ideal.Quotient.mk p) x)) =
    (algebraMap p.ResidueField q.ResidueField)
      ((RingEquiv.ofBijective (algebraMap (A ⧸ p) p.ResidueField) ⋯) ((Ideal.Quotient.mk p) x))

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra R B
inst✝⁶ : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst✝⁵ : q.LiesOver p
inst✝⁴ : p.IsPrime
inst✝³ : q.IsPrime
inst✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra p q
inst✝ : Algebra.IsIntegral A B
this✝² : Algebra.IsIntegral (A ⧸ p) (B ⧸ q)
this✝¹ : Algebra (A ⧸ p) q.ResidueField :=
  ((algebraMap (B ⧸ q) q.ResidueField).comp (algebraMap (A ⧸ p) (B ⧸ q))).toAlgebra
this✝ : IsScalarTower (A ⧸ p) (B ⧸ q) q.ResidueField
this : Algebra.IsAlgebraic (A ⧸ p) q.ResidueField
x : A
⊢ (algebraMap (A ⧸ p) q.ResidueField) ((Ideal.Quotient.mk p) x) =
    (algebraMap p.ResidueField q.ResidueField) ((algebraMap (A ⧸ p) p.ResidueField) ((Ideal.Quotient.mk p) x))

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]

Goal state after:
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✝ : IsDedekindDomain S
hp0 : map f p ≠ ⊥
hP : P.IsPrime
hP0 : P ≠ ⊥
⊢ p.ramificationIdx' P = Multiset.count P (normalizedFactors (map f p))

Tactic:
by
  have hPirr := (Ideal.prime_of_isPrime hP0 hP).irreducible
  refine ramificationIdx'_spec (Ideal.le_of_dvd ?_) (mt Ideal.dvd_iff_le.mpr ?_) <;>
    rw [dvd_iff_normalizedFactors_le_normalizedFactors (pow_ne_zero _ hP0) hp0,
      normalizedFactors_pow, normalizedFactors_irreducible hPirr, normalize_eq,
      Multiset.nsmul_singleton, ← Multiset.le_count_iff_replicate_le]
  exact (Nat.lt_succ_self _).not_ge

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

Goal state before:
pp: case mpr.refine_2
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
⊢ (Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₁ =
    (Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₂

Tactic:
ext x

Goal state after:
case mpr.refine_2
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
x : A
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₁) x =
    ((Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₂) x
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₂
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R J).comp g₁ = (Ideal.Quotient.mkₐ R J).comp g₂
⊢ (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g₁) =
    (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g₂)

Tactic:
ext x

Goal state after:
case h₂
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [inst : Algebra R (B ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
inst✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R J).comp g₁ = (Ideal.Quotient.mkₐ R J).comp g₂
x : A
⊢ ((Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g₁)) x =
    ((Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g₂)) x
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: 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
inst✝¹ : FormallyUnramified R A
C : Type u_1
inst✝ : Ring C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : f.comp ↑g₁ = f.comp ↑g₂
⊢ (Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₁ = (Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₂

Tactic:
ext x

Goal state after:
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
inst✝¹ : FormallyUnramified R A
C : Type u_1
inst✝ : Ring C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : f.comp ↑g₁ = f.comp ↑g₂
x : A
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₁) x = ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₂) x
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
⊢ (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂

Tactic:
ext x

Goal state after:
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
⊢ ((Ideal.Quotient.mkₐ R (I ^ i)).comp g₁) x = ((Ideal.Quotient.mkₐ R (I ^ i)).comp g₂) x
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: 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)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
⊢ g₁ = g₂

Tactic:
ext x

Goal state after:
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)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
x : A
⊢ g₁ x = g₂ x
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁ = f₂

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : B
⊢ f₁ x = f₂ x
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ (Ideal.Quotient.mkₐ R I).comp (f₁.comp f) = (Ideal.Quotient.mkₐ R I).comp (f₂.comp f)

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x✝ x : A
⊢ ((Ideal.Quotient.mkₐ R I).comp (f₁.comp f)) x = ((Ideal.Quotient.mkₐ R I).comp (f₂.comp f)) x
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
inst✝ : QuasiFinite R S
I : Ideal R
h : ¬I.IsPrime
this : (I.primesOver S).Nonempty
⊢ False

Tactic:
obtain ⟨J, h₁, ⟨rfl⟩⟩ := this

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : QuasiFinite R S
J : Ideal S
h₁ : J.IsPrime
h : ¬(Ideal.under R J).IsPrime
⊢ False
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
inst✝¹ : IsArtinianRing R
inst✝ : QuasiFinite R S
e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom R R (PrimeSpectrum.PiLocalization R)) ⋯
this : Fintype (PrimeSpectrum R)
⊢ Module.Finite R S

Tactic:
let e' : S ≃ₐ[R] Π p : PrimeSpectrum R, Localization p.asIdeal.primeCompl ⊗[R] S :=
    (Algebra.TensorProduct.rid R R S).symm.trans <| (Algebra.TensorProduct.congr .refl e).trans <|
      (Algebra.TensorProduct.piRight _ _ _ _).trans <| AlgEquiv.piCongrRight
      fun _ ↦ Algebra.TensorProduct.comm _ _ _

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
inst✝ : QuasiFinite R S
e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
  AlgEquiv.ofBijective (IsScalarTower.toAlgHom R R (PrimeSpectrum.PiLocalization R)) ⋯
this : Fintype (PrimeSpectrum R)
e' : S ≃ₐ[R] (p : PrimeSpectrum R) → Localization p.asIdeal.primeCompl ⊗[R] S :=
  (TensorProduct.rid R R S).symm.trans
    ((TensorProduct.congr AlgEquiv.refl e).trans
      ((TensorProduct.piRight R R S fun p ↦ Localization p.asIdeal.primeCompl).trans
        (AlgEquiv.piCongrRight fun x ↦ TensorProduct.comm R S (Localization x.asIdeal.primeCompl))))
⊢ Module.Finite R S
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
inst✝ : FiniteType R S
H : ∀ (x : PrimeSpectrum R), (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {x}).Finite
P : Ideal R
x✝ : P.IsPrime
⊢ Module.Finite P.ResidueField (P.Fiber S)

Tactic:
Module.finite_iff_isArtinianRing,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
H : ∀ (x : PrimeSpectrum R), (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {x}).Finite
P : Ideal R
x✝ : P.IsPrime
⊢ IsArtinianRing (P.Fiber S)
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
⊢ Algebra.IsIntegral (Localization.Away sA) T

Tactic:
refine ⟨fun x ↦ ?_⟩

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 : T
⊢ IsIntegral (Localization.Away sA) x
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 : PrimeSpectrum S
inst✝² : IsArtinianRing R
inst✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R p.asIdeal
this : IsJacobsonRing S
⊢ IsClopen {p}

Tactic:
have : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing R S

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : PrimeSpectrum S
inst✝² : IsArtinianRing R
inst✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R p.asIdeal
this✝ : IsJacobsonRing S
this : IsNoetherianRing S
⊢ IsClopen {p}
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
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H : IsOpen {p}
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
have : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing R S

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H : IsOpen {p}
this : IsNoetherianRing S
⊢ QuasiFiniteAt R p.asIdeal
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h1
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 σ
⊢ Extension.Cotangent.map ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom) = 0

Tactic:
ext x

Goal state after:
case h1
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Cotangent
⊢ ((Extension.Cotangent.map ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom)) x).val = (0 x).val
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).toExtension.Cotangent
hx : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x = 0
⊢ x ∈ (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
obtain ⟨⟨x : (Q.comp P).Ring, hx'⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

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
hx : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) (Extension.Cotangent.mk ⟨x, hx'⟩) = 0
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
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
⊢ TensorProduct.AlgebraTensorModule.lift (↑R (lsmul S S M).toLinearMap.flip).flip ∘ₗ sec R S M = LinearMap.id

Tactic:
ext x

Goal state after:
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
x : M
⊢ (TensorProduct.AlgebraTensorModule.lift (↑R (lsmul S S M).toLinearMap.flip).flip ∘ₗ sec R S M) x = LinearMap.id x