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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : S →ₐ[R] F), x pb.gen = ↑(pb.liftEquiv' x)

Tactic:
intro σ; simp only [PowerBasis.liftEquiv'_apply_coe]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f ((normalizedFactors a).prod * ↑ua * ((normalizedFactors b).prod * ↑ub)) =
    f ((normalizedFactors a).prod * ↑ua) * f ((normalizedFactors b).prod * ↑ub)

Tactic:
mul_right_comm (Multiset.prod (normalizedFactors a)) ua
        (Multiset.prod (normalizedFactors b) * ub),

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f ((normalizedFactors a).prod * ((normalizedFactors b).prod * ↑ub) * ↑ua) =
    f ((normalizedFactors a).prod * ↑ua) * f ((normalizedFactors b).prod * ↑ub)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f ((Multiset.map id (normalizedFactors a)).prod * (normalizedFactors b).prod) =
    f (Multiset.map id (normalizedFactors a)).prod * f (normalizedFactors b).prod

Tactic:
← (normalizedFactors b).map_id,

Goal state after:
case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ f ((Multiset.map id (normalizedFactors a)).prod * (Multiset.map id (normalizedFactors b)).prod) =
    f (Multiset.map id (normalizedFactors a)).prod * f (Multiset.map id (normalizedFactors b)).prod
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
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
⊢ Module.IsTorsionBySet R M ↑Jac → P M

Tactic:
intro h

Goal state after:
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
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
n : ℕ
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
hn : Jac ^ n ≤ Module.annihilator R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
h : Module.IsTorsionBySet R M ↑Jac
⊢ P M
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ comap (Quotient.mk (span {↑(absNorm I)})) (map (Quotient.mk (span {↑(absNorm I)})) I) = J

Tactic:
← hI.symm,

Goal state after:
case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) I) = J
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: 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
x✝¹ : IsSemisimpleModule R M
hJ : Module.IsTorsionBySet R M ↑(Ring.jacobson R)
h : IsNoetherian R M ∨ IsArtinian R M
x✝ : Module (R ⧸ Ring.jacobson R) M := hJ.module
this :
  [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE
⊢ Module.Finite R₀ M

Tactic:
simp_rw [this.out 1 0, this.out 2 0, or_self,
      hJ.semilinearMap.finite_iff_of_bijective Function.bijective_id] at h

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
x✝¹ : IsSemisimpleModule R M
hJ : Module.IsTorsionBySet R M ↑(Ring.jacobson R)
x✝ : Module (R ⧸ Ring.jacobson R) M := hJ.module
this :
  [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE
h : Module.Finite (R ⧸ Ring.jacobson R) M
⊢ Module.Finite R₀ M
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
| Nat.card { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }

Tactic:
enter [1, 1, I]

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
I : Ideal S
| I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg.mp
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ Nat.find H ≠ 1 → map f p ≤ P ^ 2

Tactic:
intro he

Goal state after:
case neg.mp
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
he : Nat.find H ≠ 1
⊢ map f p ≤ P ^ 2
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg.mpr
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ map f p ≤ P ^ 2 → Nat.find H ≠ 1

Tactic:
intro he

Goal state after:
case neg.mpr
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
he : map f p ≤ P ^ 2
⊢ Nat.find H ≠ 1
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)
⊢ Algebra.IsAlgebraic p.ResidueField q.ResidueField

Tactic:
let := ((algebraMap (B ⧸ q) q.ResidueField).comp (algebraMap (A ⧸ p) (B ⧸ q))).toAlgebra

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.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
⊢ Algebra.IsAlgebraic p.ResidueField q.ResidueField
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
Rₘ : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ ∀ ⦃B : Type u_3⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro Q _ _ I _ f₁ f₂ _

Goal state after:
R : Type u_1
Rₘ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing Rₘ
M : Submonoid R
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁ = f₂
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
⊢ Module.Finite R S

Tactic:
let e : R ≃ₐ[R] PrimeSpectrum.PiLocalization R :=
    .ofBijective (IsScalarTower.toAlgHom _ _ _)
      (PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective.mp inferInstance)
  have : Fintype (PrimeSpectrum R) := .ofFinite _
  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 _ _ _
  have (p : PrimeSpectrum R) : Module.Finite R (Localization p.asIdeal.primeCompl ⊗[R] S) :=
    have : Module.Finite R (Localization.AtPrime p.asIdeal) :=
      .of_surjective (Algebra.linearMap _ _)
        (IsArtinianRing.localization_surjective p.asIdeal.primeCompl _)
    have : Module.Finite (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] S) := finite_of_isArtinianRing_of_isLocalRing
    .trans (Localization.AtPrime p.asIdeal) _
  exact .of_surjective e'.symm.toLinearMap e'.symm.surjective

Goal state after:
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
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ k ∈ f.support.biUnion fun i ↦ ((fun i ↦ b.repr (b i * x)) i).support,
      (b.repr (f.sum fun i y ↦ ((fun i ↦ b.repr (b i * x)) i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k

Tactic:
simp_rw [map_finsuppSum, map_smul, h₁, Finsupp.sum, Finset.sum_comm (t := f.support),
    TensorProduct.smul_tmul', ← TensorProduct.sum_tmul, ← Finset.smul_sum, h₂]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ x_1 ∈ f.support,
      ∑ x_2 ∈ f.support.biUnion fun i ↦ (b.repr (b i * x)).support, ((b.repr (b x_1 * x)) x_2 • f x_1) ⊗ₜ[R] b x_2
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := ⋯
sA : ↥A := ⋯
f : Localization.Away sA →+* T := ⋯
this✝⁶ : Algebra (Localization.Away sA) T := ⋯
this✝⁵ : Algebra (↥A) (Localization.Away sA) := ⋯
this✝⁴ : SMul (↥A) (Localization.Away sA) := ⋯
this✝³ : MulAction (↥A) (Localization.Away sA) := ⋯
this✝² : IsScalarTower R (↥A) (Localization.Away sA)
this✝¹ : IsScalarTower (↥A) (Localization.Away sA) T
this✝ : IsScalarTower R (Localization.Away sA) T
x : S
n : ℕ
this : IsIntegral (Localization.Away sA) ((algebraMap S T) x)
⊢ (sA • Localization.Away.invSelf sA) ^ n • (algebraMap S T) x =
    Localization.Away.invSelf sA ^ n • ((algebraMap S T) x * (algebraMap S T) s ^ n)

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

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)
⊢ (algebraMap S T) s ^ n * (algebraMap (Localization.Away ⟨s, ⋯⟩) T) (Localization.Away.invSelf ⟨s, ⋯⟩) ^ n *
      (algebraMap S T) x =
    (algebraMap (Localization.Away ⟨s, ⋯⟩) T) (Localization.Away.invSelf ⟨s, ⋯⟩) ^ n *
      ((algebraMap S T) x * (algebraMap S T) s ^ n)
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
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R := ⋯
⊢ (Finsupp.equivCongrLeft (Equiv.prodComm I I)) (Finsupp.curryEquiv.symm F) =
    (Finsupp.equivCongrLeft (Equiv.prodComm I I)) (Finsupp.curryEquiv.symm G)

Tactic:
apply (b.tensorProduct b).repr.symm.injective

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R := ⋯
⊢ (b.tensorProduct b).repr.symm ((Finsupp.equivCongrLeft (Equiv.prodComm I I)) (Finsupp.curryEquiv.symm F)) =
    (b.tensorProduct b).repr.symm ((Finsupp.equivCongrLeft (Equiv.prodComm I I)) (Finsupp.curryEquiv.symm G))
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 σ
⊢ Function.Surjective ⇑(Extension.Cotangent.map (Q.ofComp P).toExtensionHom)

Tactic:
intro x
  obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x
  have : x ∈ Q.ker := hx
  rw [← map_ofComp_ker Q P, Ideal.mem_map_iff_of_surjective
    _ (toAlgHom_ofComp_surjective Q P)] at this
  obtain ⟨x, hx', rfl⟩ := this
  exact ⟨.mk ⟨x, hx'⟩, Extension.Cotangent.map_mk _ _⟩

Goal state after:
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 : (Q.ofComp P).toAlgHom y = (Q.ofComp P).toAlgHom x
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
rw [eq_comm, ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, ← map_toComp_ker] at e

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
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range