mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ False

Tactic:
refine hₐ ?_

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ IsUnit a
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
d' : R[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (q * d')
hr' : Polynomial.map (algebraMap R K) d' = r
⊢ q ∣ p

Tactic:
exact dvd_of_mul_right_eq _ (Polynomial.map_injective _ (IsFractionRing.injective R K) hr.symm)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : (g' * f).content = (b • k).content
h : Associated g'.content (b * k.content)
⊢ g ∈ lifts (algebraMap R K)

Tactic:
obtain ⟨g'', hg⟩ : C b ∣ g' := dvd_content_iff_C_dvd.mp <| (dvd_mul_right ..).trans h.dvd'

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : (g' * f).content = (b • k).content
h : Associated g'.content (b * k.content)
g'' : R[X]
hg : g' = C b * g''
⊢ g ∈ lifts (algebraMap R K)
Module: Mathlib.RingTheory.Trace.Defs

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✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
x : S × T
⊢ (trace R (S × T)) x = (trace R S) x.1 + (trace R T) x.2

Tactic:
let f := (lmul R S).toLinearMap.prodMap (lmul R T).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✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
x : S × T
f : S × T →ₗ[R] End R S × End R T := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap
⊢ (trace R (S × T)) x = (trace R S) x.1 + (trace R T) x.2
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
a : A
ha : (algebraMap A B) a = e.symm x'
⊢ (algebraMap A B') a = x'

Tactic:
← e.commutes,

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
a : A
ha : (algebraMap A B) a = e.symm x'
⊢ e ((algebraMap A B) a) = x'
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
g : ?m.146
hg : g • b ∈ P
⊢ b ∈ ⋃ i ∈ ↑⊤, ↑(i • P)

Tactic:
apply Set.mem_biUnion (Finset.mem_univ g⁻¹) (Ideal.mem_inv_pointwise_smul_iff.mpr hg)

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K L) x = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff

Tactic:
trace_eq_trace_adjoin,

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x) = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

Tactic:
apply iff_of_false _ (mt _ h)

Goal state after:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ ¬a.valMinAbs * 2 = ↑(n + 1)

n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case neg
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))
n : ℕ
hn : ¬n ≤ k
⊢ (algebraMap B (B ⧸ Q)) 0 = q.coeff n

Tactic:
· rw [map_zero, eq_comm, Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_not_ge hn)]

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

Goal state before:
pp: 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
⊢ eval b r ∈ Q

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, ← Ideal.Quotient.algebraMap_eq] at hbQ ⊢

Goal state after:
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 : ¬(algebraMap B (B ⧸ Q)) b = 0
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
⊢ (algebraMap B (B ⧸ Q)) (eval b r) = 0
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs ∨ ↑p ∣ n

Tactic:
Int.natCast_dvd

Goal state after:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ ↑p ∣ n

Tactic:
Int.natCast_dvd

Goal state after:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ n.natAbs
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
⊢ ∃ a, (algebraMap ↥E ↥F) a = x

Tactic:
obtain ⟨a, ha⟩ := hE.isInvariant.isInvariant (algebraMap F L x) (by
        rintro ⟨g, hg⟩
        rw [MulAction.subgroup_smul_def, ← algebraMap.smul']
        exact congr_arg (algebraMap F L) <| h ⟨g, ⟨g, hg, rfl⟩⟩)

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
a : ↥E
ha : (algebraMap (↥E) L) a = (algebraMap (↥F) L) x
⊢ ∃ a, (algebraMap ↥E ↥F) a = x
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Tactic:
let _ := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
x✝ : Algebra (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
⊢ Function.Surjective ⇑(stabilizerHom Q P G)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : Fˣ
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)

Goal state after:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: case calc_1
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
i j : Free.ChooseBasisIndex ℤ M
⊢ (LinearMap.toMatrix b' b') f i j = Matrix.diagonal a i j

Tactic:
LinearMap.toMatrix_apply,

Goal state after:
case calc_1
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
ha : ∀ (i : Free.ChooseBasisIndex ℤ M), f (b' i) = a i • b' i
i j : Free.ChooseBasisIndex ℤ M
⊢ (b'.repr (f (b' j))) i = Matrix.diagonal a i j
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
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₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ p.inertiaDeg' (comap e P) = p.inertiaDeg' P

Tactic:
rw [inertiaDeg'_algebraMap, inertiaDeg'_algebraMap]

Goal state after:
case pos
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₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ finrank (R ⧸ p) (S ⧸ comap e P) = finrank (R ⧸ p) (S₁ ⧸ P)
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
this : Q.LiesOver p
⊢ P.inertiaDeg' Q ≤ p.inertiaDeg' Q

Tactic:
rw [inertiaDeg'_algebraMap, inertiaDeg'_algebraMap]

Goal state after:
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
this : Q.LiesOver p
⊢ finrank (S ⧸ P) (T ⧸ Q) ≤ finrank (R ⧸ p) (T ⧸ Q)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case inr
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
⊢ {I | absNorm I = n}.Finite

Tactic:
let f := fun I : Ideal S => Ideal.map (Ideal.Quotient.mk (@Ideal.span S _ {↑n})) I

Goal state after:
case inr
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 | absNorm I = n}.Finite
Module: Mathlib.RingTheory.RamificationInertia.Inertia

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
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S

Tactic:
by_cases hr : r.IsPrime

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
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S

case neg
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
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S
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)
this✝¹ : Algebra (Localization.AtPrime (under R r)) (Localization.AtPrime r) :=
  Localization.AtPrime.algebraOfLiesOver (under R r) r
this✝ : Algebra (Localization.AtPrime (under R r)) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver (under R r) q
this : Algebra (Localization.AtPrime q) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver q r
⊢ Module.finrank (under R r).ResidueField q.ResidueField * Module.finrank q.ResidueField r.ResidueField =
    Module.finrank (under R r).ResidueField r.ResidueField

Tactic:
apply Module.finrank_mul_finrank

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✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
⊢ p.ramificationIdx' P = 1

Tactic:
rw [← not_ne_iff (b := 1), Ideal.ramificationIdx'_ne_one_iff hpP]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
⊢ ¬map f p ≤ P ^ 2
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case pos
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
⊢ (I.primesOver S).Finite

Tactic:
refine ((finite_comap_preimage_singleton ⟨I, h⟩).image PrimeSpectrum.asIdeal).subset ?_

Goal state after:
case pos
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
⊢ I.primesOver S ⊆ PrimeSpectrum.asIdeal '' PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := I, isPrime := h }}
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case h
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 := ⋯
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 : I
hi : i ∈ f.support
⊢ (a i).support ⊆ f.support.biUnion fun i ↦ (b.repr (b i * x)).support

pp: case hg
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 := ⋯
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 : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (f.support.biUnion fun i ↦ (b.repr (b i * x)).support) \ (a i).support,
    ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1 = 0

pp: case hfg
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 := ⋯
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 : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support, ((a i) x_1 • f i) ⊗ₜ[R] b x_1 = ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1

Tactic:
· exact Finset.subset_biUnion_of_mem (fun i ↦ (a i).support) hi

Goal state after:
case hg
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 := ⋯
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 : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (f.support.biUnion fun i ↦ (b.repr (b i * x)).support) \ (a i).support,
    ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1 = 0

case hfg
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 := ⋯
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 : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support, ((a i) x_1 • f i) ⊗ₜ[R] b x_1 = ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1