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

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
⊢ f b = b

Tactic:
have hf := congrArg (eval b) (congrArg (Polynomial.mapAlgHom f.toAlgHom) h)

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : eval b ((mapAlgHom ↑f) (map (algebraMap A B) p)) = eval b ((mapAlgHom ↑f) ((X - C b) ^ i * X ^ j))
⊢ f b = b
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : 0 ^ i * b ^ j = (b - ↑↑f b) ^ i * b ^ j
⊢ f b = b

Tactic:
zero_pow hi,

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : 0 * b ^ j = (b - ↑↑f b) ^ i * b ^ j
⊢ f b = b
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
H : Subgroup G
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra A C
inst✝³ : FaithfulSMul A C
inst✝² : MulSemiringAction G C
hGAC : IsGaloisGroup G A C
inst✝¹ : Algebra B C
inst✝ : FaithfulSMul B C
hH : IsGaloisGroup (↥H) B C
this✝² : IsDomain B
this✝¹ : IsDomain A
K : Type u_5 := FractionRing A
L : Type u_7 := FractionRing C
this✝ : MulSemiringAction G L := IsFractionRing.mulSemiringAction G C L
this : IsGaloisGroup (↥H) (FractionRing B) L
g : G
⊢ (∀ (y : L), (∃ y_1, (algebraMap (FractionRing B) L) y_1 = y) → g • y = y) →
    ∀ (y : C), (∃ y_1, (algebraMap B C) y_1 = y) → g • y = y

Tactic:
· rintro h _ ⟨x, rfl⟩
    apply FaithfulSMul.algebraMap_injective C L
    rw [algebraMap.smul']
    apply h
    use algebraMap B (FractionRing B) x
    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Tactic:
have hp : Fact p.Prime := ⟨CharP.char_is_prime K p⟩

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x ↦ ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x ∈ univ \ {0}, x ^ i + 0 ^ i = ∑ x ∈ univ \ {0}, x ^ i

Tactic:
zero_pow hi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x ↦ ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x ∈ univ \ {0}, x ^ i + 0 = ∑ x ∈ univ \ {0}, x ^ i
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).roots = (X ^ q - X).roots.dedup

Tactic:
eq_comm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).roots.dedup = (X ^ q - X).roots
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ orderOf ↑a ∣ n

Tactic:
rw [orderOf_dvd_iff_pow_eq_one, ← Nat.cast_pow, ← Nat.cast_one, ZMod.natCast_eq_natCast_iff, hn]

Goal state after:
case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
h : ¬IsUnit (↑a - 1)
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case h.refine_1
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis (↥s) K ↥K⟮x⟯
⊢ (Subalgebra.toSubmodule K⟮x⟯.toSubalgebra).FG

pp: case h.refine_2
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis (↥s) K ↥K⟮x⟯
⊢ x ∈ K⟮x⟯.toSubalgebra

Tactic:
· exact (Submodule.fg_iff_finiteDimensional _).mpr (b.finiteDimensional_of_finite)

Goal state after:
case h.refine_2
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis (↥s) K ↥K⟮x⟯
⊢ x ∈ K⟮x⟯.toSubalgebra
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
⊢ ((minpoly R pb.gen).aroots F).prod = ∏ x ∈ ((minpoly R pb.gen).aroots F).toFinset, ?g x

pp: case g
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 := ⋯
⊢ F → F

pp: case hfg
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 : { x // x ∈ (minpoly R pb.gen).aroots F }), ↑x = ?g ↑x

Tactic:
Finset.prod_eq_multiset_prod,

Goal state after:
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
⊢ ((minpoly R pb.gen).aroots F).prod = (Multiset.map ?f ((minpoly R pb.gen).aroots F).toFinset.val).prod

case f
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 := ⋯
⊢ F → F

case hfg
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 : { x // x ∈ (minpoly R pb.gen).aroots F }), ↑x = ?f ↑x
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∏ σ, σ ((algebraMap L F) pb.gen) = (∏ σ, σ pb.gen) ^ finrank L F

Tactic:
Fintype.prod_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,

Goal state after:
K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∏ x, x.fst pb.gen = (∏ σ, σ pb.gen) ^ finrank L F

K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P

Tactic:
have he : (P.comap e).comap (algebraMap R S) = p ↔ P.comap (algebraMap R S₁) = p := by
    rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
  by_cases h : P.LiesOver p
  · rw [inertiaDeg'_algebraMap, inertiaDeg'_algebraMap]
    exact (Quotient.algEquivOfEqComap p e rfl).toLinearEquiv.finrank_eq
  · rw [inertiaDeg', dif_neg (fun eq => h ⟨(he.mp eq).symm⟩)]
    rw [inertiaDeg', dif_neg (fun eq => h ⟨eq.symm⟩)]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
P : Submodule R M
⊢ P.toAddSubgroup = ⊤ ↔ P = ⊤

Tactic:
by simp [SetLike.ext_iff]

Goal state after:
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
⊢ FinitePresentation B (B ⊗[R] A)

Tactic:
have hgsurj : Function.Surjective g := Algebra.FiniteType.baseChangeAux_surj B hsurj

Goal state after:
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
⊢ FinitePresentation B (B ⊗[R] A)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDedekindDomain S
P : Ideal S
P_prime : P.IsPrime
hP : P ≠ ⊥
i : ℕ
a b : S
a_notMem : a ∉ P ^ (i + 1)
ab_mem : a * b ∈ P ^ (i + 1)
⊢ b ∈ P

Tactic:
simp only [← Ideal.span_singleton_le_iff_mem, ← Ideal.dvd_iff_le, pow_succ, ←
    Ideal.span_singleton_mul_span_singleton] at a_notMem ab_mem ⊢
  exact (prime_pow_succ_dvd_mul (Ideal.prime_of_isPrime hP P_prime) ab_mem).resolve_left a_notMem

Goal state after:
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

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✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1)

Tactic:
refine ?_ ∘ₗ (TensorProduct.quotTensorEquivQuotSMul _ I).toLinearMap

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✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this✝ : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))
⊢ ↥(I ^ n) ⧸ I • ⊤ →ₗ[S] S ⧸ I ^ (n + 1)
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) = mk' S 1 x

Tactic:
← (IsLocalization.map_units S x).mul_left_inj

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) * (algebraMap R S) ↑x = mk' S 1 x * (algebraMap R S) ↑x
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
⊢ Set.univ = zeroLocus ↑I

Tactic:
eq_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
⊢ zeroLocus ↑I = Set.univ
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
p q : Submodule A M
h : p ⋖ q
f : ↥p →ₗ[A] ↥q := inclusion ⋯
⊢ length B (B ⊗[A] ↥q) = length B (B ⊗[A] ↥p) + length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
have key : IsSimpleModule A (q ⧸ f.range) := by
    rwa [range_inclusion, ← covBy_iff_quot_is_simple h.le]

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
p q : Submodule A M
h : p ⋖ q
f : ↥p →ₗ[A] ↥q := inclusion ⋯
key : IsSimpleModule A (↥q ⧸ f.range)
⊢ length B (B ⊗[A] ↥q) = length B (B ⊗[A] ↥p) + length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
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
inst✝² : IsDedekindDomain S
inst✝¹ : IsDedekindDomain R
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hvp : v ≠ p
inst✝ : w.LiesOver v
⊢ emultiplicity w (map f p) = 0

Tactic:
by
  refine emultiplicity_eq_zero.2 fun h ↦ hvp.symm ?_
  rw [Ideal.dvd_iff_le, Ideal.map_le_iff_le_comap, ← under_def, ← Ideal.over_def w v] at h
  exact ((isPrime_of_prime hp).isMaximal hp.ne_zero).eq_of_le (isPrime_of_prime hv.prime).ne_top h

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

Goal state before:
pp: case mpr.refine_1
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
⊢ RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom ^ 2 = ⊥

Tactic:
rw [AlgHom.ker_kerSquareLift]
      exact Ideal.cotangentIdeal_square _

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✝ : QuasiFinite R T
⊢ QuasiFinite S T

Tactic:
by
  refine ⟨fun P hP ↦ ?_⟩
  let f : P.ResidueField ⊗[R] T →ₐ[P.ResidueField] P.Fiber T :=
    Algebra.TensorProduct.lift (Algebra.ofId _ _)
      (Algebra.TensorProduct.includeRight.restrictScalars R) fun _ _ ↦ .all _ _
  have hf : Function.Surjective f := by
    rw [← AlgHom.coe_restrictScalars' (R := S), ← AlgHom.coe_toLinearMap, ← LinearMap.range_eq_top,
      ← top_le_iff, ← TensorProduct.span_tmul_eq_top, Submodule.span_le]
    rintro _ ⟨a, b, rfl⟩
    exact ⟨a ⊗ₜ b, by simp [f]⟩
  have : Module.Finite P.ResidueField (P.ResidueField ⊗[R] T) := .of_quasiFinite
  exact .of_surjective f.toLinearMap hf

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
⊢ QuasiFinite R T

Tactic:
have : Algebra.IsIntegral (Localization.Away sA) T := by
    refine ⟨fun x ↦ ?_⟩
    obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) x
    have : _root_.IsIntegral (Localization.Away sA) (algebraMap S T x) :=
      (Algebra.IsIntegral.isIntegral (R := R) x).algebraMap.tower_top
    convert! this.smul (Localization.Away.invSelf sA ^ n)
    rw [IsLocalization.mk'_eq_iff_eq_mul]
    simp only [map_pow, Algebra.smul_mul_assoc]
    trans (sA • Localization.Away.invSelf sA) ^ n • (algebraMap S T x)
    · simp [Algebra.smul_def, -map_pow, Localization.Away.invSelf, Localization.mk_eq_mk']
    · simp only [Algebra.smul_def, map_pow, map_mul, mul_pow,
        ← IsScalarTower.algebraMap_apply, Subalgebra.algebraMap_def, sA]
      ring

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
this : Algebra.IsIntegral (Localization.Away sA) T
⊢ QuasiFinite R T
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:
eq_comm,

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

Tactic:
eq_comm,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Module.support A Ω[A⁄R] = ∅ ↔ FormallyUnramified R A
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
this : 0 = f₂ ((aeval x) (derivative (minpoly K x))) * (f₁ x - f₂ x)
⊢ f₁ x = f₂ x

Tactic:
eq_comm,

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 : f₂ ((aeval x) (derivative (minpoly K x))) * (f₁ x - f₂ x) = 0
⊢ f₁ x = f₂ x