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

Goal state before:
pp: case refine_2
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
⊢ (algebraMap B (B ⧸ Q)) (h • (a - eval b r)) - (algebraMap B (B ⧸ Q)) (if h • Q = Q then a else 0) = 0

Tactic:
← map_sub,

Goal state after:
case refine_2
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
⊢ (algebraMap B (B ⧸ Q)) (h • (a - eval b r) - if h • Q = Q then a else 0) = 0
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁸ : Group G
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h✝ : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h✝).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
⊢ ∀ (g : ↥H), g • (algebraMap (↥F) L) x = (algebraMap (↥F) L) x

Tactic:
rintro ⟨g, hg⟩

Goal state after:
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁸ : Group G
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
N : Subgroup G
inst✝³ : N.Normal
inst✝² : IsGaloisGroup (↥N) (↥F) L
E : IntermediateField K L
hE : IsGaloisGroup (↥H) (↥E) L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
h✝ : E ≤ F
this✝³ : Algebra ↥E ↥F := (IntermediateField.inclusion h✝).toAlgebra
this✝² : SMul G ↥F := smulOfNormal G (↥F) L N
this✝¹ : SMulDistribClass G (↥F) L
this✝ : MulSemiringAction G ↥F := mulSemiringActionOfSmulDistribClass (↥F) L G
this : IsScalarTower (↥E) (↥F) L
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
g : G
hg : g ∈ H
⊢ ⟨g, hg⟩ • (algebraMap (↥F) L) x = (algebraMap (↥F) L) x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ
p a m d : ℕ
hd : (p * a + 1) ^ p ^ m - 1 = p ^ m * d
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
rw [tsub_eq_iff_eq_add_of_le (Nat.one_le_pow' _ _), add_comm] at hd

Goal state after:
case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P] k
f : B ⧸ Q →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P) k).comp (algebraMap A (A ⧸ P))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this : IsScalarTower A (B ⧸ Q) k
⊢ (σ.comp f).toRingHom ((mk Q) x) ∈ f.range

Tactic:
have : IsScalarTower A B k := .of_algebraMap_eq fun x ↦
    (IsScalarTower.algebraMap_apply (A ⧸ P) (B ⧸ Q) k (mk P x))

Goal state after:
case intro
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P] k
f : B ⧸ Q →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P) k).comp (algebraMap A (A ⧸ P))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝ : IsScalarTower A (B ⧸ Q) k
this : IsScalarTower A B k
⊢ (σ.comp f).toRingHom ((mk Q) x) ∈ f.range
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P✝ : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P✝
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P✝) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P✝) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P✝] k
f : B ⧸ Q →ₐ[A ⧸ P✝] k := IsScalarTower.toAlgHom (A ⧸ P✝) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P✝) k).comp (algebraMap A (A ⧸ P✝))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P✝) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝¹ : IsScalarTower A (B ⧸ Q) k
this✝ : IsScalarTower A B k
P : Polynomial A
hp : (Polynomial.mapRingHom (algebraMap A B)) P = MulSemiringAction.charpoly G x
this : (Polynomial.aeval x) P = 0
⊢ (((AlgHom.restrictScalars A σ).comp (IsScalarTower.toAlgHom A (B ⧸ Q) k)).comp (Polynomial.aeval ((mk Q) x))) P = 0

Tactic:
rw [AlgHom.comp_apply, ← algebraMap_eq, Polynomial.aeval_algebraMap_apply, this,
      map_zero, map_zero]

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

Goal state before:
pp: F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : Fintype ↥⊥ := fintypeBot F p
⊢ (X ^ p - X).Splits

Tactic:
rw [splits_iff_card_roots, roots_X_pow_char_sub_X_bot, ← Finset.card_def, Finset.card_univ,
    FiniteField.X_pow_card_sub_X_natDegree_eq _ (Fact.out (p := p.Prime)).one_lt,
    Fintype.card_eq_nat_card, card_bot F p]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
⊢ ∃ a, ¬IsSquare a

Tactic:
have h : ¬Function.Injective fun x : F ↦ x * x := fun h ↦
    h.ne (Ring.neg_one_ne_one_of_char_ne_two hF) <| by simp
  simpa [Finite.injective_iff_surjective, Function.Surjective, IsSquare, eq_comm] using h

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this✝ : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis ι R ↥N := smithNormalFormBotBasis b h
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
N' : Submodule R (ι → R) := pi Set.univ fun i ↦ R ∙ a i
this : map (↑b'.equivFun) N = N'
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → R ⧸ Ideal.span {smithNormalFormCoeffs b h i}

Tactic:
refine (Submodule.Quotient.equiv N N' b'.equivFun this).trans (re₂₃ := inferInstance)
    (re₃₂ := inferInstance) ?_

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
N : Submodule R M
b : Basis ι R M
h : finrank R ↥N = finrank R M
this✝ : Fintype ι
a : ι → R := smithNormalFormCoeffs b h
b' : Basis ι R M := smithNormalFormTopBasis b h
ab : Basis ι R ↥N := smithNormalFormBotBasis b h
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
N' : Submodule R (ι → R) := pi Set.univ fun i ↦ R ∙ a i
this : map (↑b'.equivFun) N = N'
⊢ ((ι → R) ⧸ N') ≃ₗ[R] (i : ι) → R ⧸ Ideal.span {smithNormalFormCoeffs b h i}
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
P : Ideal S
T : Type u_2
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Module.Finite R T
Q : Ideal T
inst✝² : P.LiesOver p
inst✝¹ : Q.LiesOver P
inst✝ : p.IsPrime
⊢ P.inertiaDeg' Q ≤ p.inertiaDeg' Q

Tactic:
have : Q.LiesOver p := LiesOver.trans Q P p
  rw [inertiaDeg'_algebraMap, inertiaDeg'_algebraMap]
  have : IsScalarTower (R ⧸ p) (S ⧸ P) (T ⧸ Q) := IsScalarTower.of_algebraMap_eq <| by
    rintro ⟨x⟩
    simp [Submodule.Quotient.quot_mk_eq_mk, IsScalarTower.algebraMap_apply R (S ⧸ P) (T ⧸ Q)]
  exact finrank_top_le_finrank_of_isScalarTower ..

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

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ d, ∃ e ∈ P ^ (i + 1), a * d + e = c

Tactic:
simp only [mul_comm a]

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ d, ∃ e ∈ P ^ (i + 1), d * a + e = c
Module: Mathlib.RingTheory.Noetherian.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
⊢ IsNilpotent (nilradical R)

Tactic:
obtain ⟨n, hn⟩ := Ideal.exists_radical_pow_le_of_fg (⊥ : Ideal R) (IsNoetherian.noetherian _)

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
n : ℕ
hn : ⊥.radical ^ n ≤ ⊥
⊢ IsNilpotent (nilradical R)
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: 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
hq : q.IsPrime
e : q ≠ p
⊢ r ∈ q

Tactic:
have : PrimeSpectrum.mk q inferInstance ≠ ⟨p, inferInstance⟩ := ne_of_apply_ne (·.1) e

Goal state after:
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
hq : q.IsPrime
e : q ≠ p
this : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
⊢ r ∈ q
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
I : Ideal S
⊢ absNorm I = 0 ↔ I = ⊥

Tactic:
constructor
  · intro hI
    rw [← le_bot_iff]
    intro x hx
    rw [mem_bot, ← Algebra.norm_eq_zero_iff (R := ℤ), ← Int.natAbs_eq_zero,
      ← Ideal.absNorm_span_singleton, ← zero_dvd_iff, ← hI]
    apply Ideal.absNorm_dvd_absNorm_of_le
    rwa [Ideal.span_singleton_le_iff_mem]
  · rintro rfl
    exact absNorm_bot

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

Goal state before:
pp: case h₁
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
hI : p ∣ ↑(absNorm 0)
Q : Ideal S
hQ : Q.IsMaximal
e : comap (algebraMap ℤ S) Q = span {p}
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ 0

Tactic:
exact ⟨Q, hQ, e, dvd_zero _⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹⁶ : q.LiesOver p
inst✝¹⁵ : p.IsPrime
inst✝¹⁴ : q.IsPrime
K : Type u_4
L : Type u_5
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra (R ⧸ p) K
inst✝¹⁰ : IsFractionRing (R ⧸ p) K
inst✝⁹ : Algebra (S ⧸ q) L
inst✝⁸ : IsFractionRing (S ⧸ q) L
inst✝⁷ : Algebra R K
inst✝⁶ : IsScalarTower R (R ⧸ p) K
inst✝⁵ : Algebra S L
inst✝⁴ : IsScalarTower S (S ⧸ q) L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R S L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower R K L
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ (algebraMap K L).comp (IsFractionRing.algEquivOfAlgEquiv AlgEquiv.refl).toRingEquiv.toRingHom =
    (IsFractionRing.algEquivOfAlgEquiv AlgEquiv.refl).toRingEquiv.toRingHom.comp
      (algebraMap p.ResidueField q.ResidueField)

Tactic:
apply IsFractionRing.ringHom_ext (A := R ⧸ p)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹⁶ : q.LiesOver p
inst✝¹⁵ : p.IsPrime
inst✝¹⁴ : q.IsPrime
K : Type u_4
L : Type u_5
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra (R ⧸ p) K
inst✝¹⁰ : IsFractionRing (R ⧸ p) K
inst✝⁹ : Algebra (S ⧸ q) L
inst✝⁸ : IsFractionRing (S ⧸ q) L
inst✝⁷ : Algebra R K
inst✝⁶ : IsScalarTower R (R ⧸ p) K
inst✝⁵ : Algebra S L
inst✝⁴ : IsScalarTower S (S ⧸ q) L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R S L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower R K L
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ ∀ (x : R ⧸ p),
    ((algebraMap K L).comp (IsFractionRing.algEquivOfAlgEquiv AlgEquiv.refl).toRingEquiv.toRingHom)
        ((algebraMap (R ⧸ p) p.ResidueField) x) =
      ((IsFractionRing.algEquivOfAlgEquiv AlgEquiv.refl).toRingEquiv.toRingHom.comp
          (algebraMap p.ResidueField q.ResidueField))
        ((algebraMap (R ⧸ p) p.ResidueField) x)
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
hr : r.IsPrime
this✝ : q.IsPrime
this : q.LiesOver (under R r)
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S

Tactic:
let := Localization.AtPrime.algebraOfLiesOver (r.under R) r

Goal state after:
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
hr : r.IsPrime
this✝¹ : q.IsPrime
this✝ : q.LiesOver (under R r)
this : Algebra (Localization.AtPrime (under R r)) (Localization.AtPrime r) :=
  Localization.AtPrime.algebraOfLiesOver (under R r) r
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S
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 ^ 2 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro f₁ f₂ e

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 ^ 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ f₁ = f₂
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I
hntq : ¬⊤ ≤ Q
⊢ Multiset.count Q
      (normalizedFactors
        (map (algebraMap S T) P ^ Multiset.count P (normalizedFactors (map f p)) * map (algebraMap S T) I)) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))

Tactic:
normalizedFactors_mul (pow_ne_zero _ hg0) <| by
    by_contra h
    simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp
    exact hntq (hcp.trans_le hg),

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 S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I
hntq : ¬⊤ ≤ Q
⊢ Multiset.count Q
      (normalizedFactors (map (algebraMap S T) P ^ Multiset.count P (normalizedFactors (map f p))) +
        normalizedFactors (map (algebraMap S T) I)) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map (algebraMap S T) P))
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
x : A
e : (Ideal.Quotient.mk J) (g₁ x) = (Ideal.Quotient.mk J) (g₂ x)
⊢ (Ideal.Quotient.mk I) (g₁ x) - (Ideal.Quotient.mk I) (g₂ x) ∈ Ideal.map (Ideal.Quotient.mk I) J

Tactic:
← map_sub,

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
x : A
e : (Ideal.Quotient.mk J) (g₁ x) = (Ideal.Quotient.mk J) (g₂ x)
⊢ (Ideal.Quotient.mk I) (g₁ x - g₂ x) ∈ Ideal.map (Ideal.Quotient.mk I) J
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case neg
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 (I ^ i)) (g₁ x) - (Ideal.Quotient.mk (I ^ i)) (g₂ x) ∈ Ideal.map (Ideal.Quotient.mk (I ^ i)) I

Tactic:
← map_sub,

Goal state after:
case neg
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 (I ^ i)) (g₁ x - g₂ x) ∈ Ideal.map (Ideal.Quotient.mk (I ^ i)) I
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)
| ∑ i ∈ f.support, f i ⊗ₜ[R] (Finsupp.linearCombination R ⇑b) (a i)

Tactic:
simp only [Finsupp.linearCombination, Finsupp.coe_lsum,
    LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, Finsupp.sum, TensorProduct.tmul_sum,
    ← TensorProduct.smul_tmul]

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)
| ∑ i ∈ f.support, ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x
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 x - (Q.ofComp P).toAlgHom y = 0
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
← map_sub,

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