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

Goal state before:
pp: case refine_1
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
⊢ a ∉ Q

Tactic:
rwa [← Ideal.Quotient.eq_zero_iff_mem, ← Ideal.Quotient.algebraMap_eq, ← Polynomial.coeff_map,
      ← zero_add j, hq, Polynomial.coeff_X_pow_mul, ← Polynomial.X_dvd_iff]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
⊢ u ^ p - 1 ^ p = 0

pp: case h
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
⊢ Commute u 1

Tactic:
one_pow,

Goal state after:
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
⊢ u ^ p - 1 = 0

case h
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
u : K := ↑↑x
hu : orderOf u = p
⊢ Commute u 1
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
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
⊢ f b = b

Tactic:
by_cases ha : b = 0
  · rw [ha, map_zero]
  have hf := congrArg (eval b) (congrArg (Polynomial.mapAlgHom f.toAlgHom) h)
  rw [coe_mapAlgHom, map_map, f.toAlgHom.comp_algebraMap, h] at hf
  simp_rw [Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_sub, map_X, map_C,
    eval_mul, eval_pow, eval_sub, eval_X, eval_C, sub_self, zero_pow hi, zero_mul,
    zero_eq_mul, or_iff_left (pow_ne_zero j ha), pow_eq_zero_iff hi, sub_eq_zero] at hf
  exact hf.symm

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

Goal state before:
pp: case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ ¬(vandermonde fun i ↦ (e i) pb.gen).det = 0

Tactic:
simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero]

Goal state after:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ ∀ (x : Fin pb.dim), ¬(x ∈ Finset.univ ∧ ∃ a ∈ Finset.Ioi x, (e a) pb.gen = (e x) pb.gen)
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
⊢ [Algebra.IsSeparable K L, Algebra.trace K L ≠ 0, (traceForm K L).Nondegenerate].TFAE

Tactic:
tfae_have 1 → 3 := fun _ ↦ traceForm_nondegenerate K L

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
tfae_1_to_3 : Algebra.IsSeparable K L → (traceForm K L).Nondegenerate
⊢ [Algebra.IsSeparable K L, Algebra.trace K L ≠ 0, (traceForm K L).Nondegenerate].TFAE
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.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
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
h : x * (algebraMap (A ⧸ P) (B ⧸ Q)) a = b * y
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
⊢ (algebraMap (B ⧸ Q) L) x * (algebraMap (A ⧸ P) L) a = (algebraMap (B ⧸ Q) L) (b * y)

Tactic:
← h,

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
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y) =
      (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
b : B ⧸ Q
a : A ⧸ P
h : x * (algebraMap (A ⧸ P) (B ⧸ Q)) a = b * y
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
⊢ (algebraMap (B ⧸ Q) L) x * (algebraMap (A ⧸ P) L) a = (algebraMap (B ⧸ Q) L) (x * (algebraMap (A ⧸ P) (B ⧸ Q)) a)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p) n
⊢ n ^ (x - y) * n ^ y ≡ n ^ y [ZMOD ↑p]

Tactic:
← h,

Goal state after:
case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p) n
⊢ n ^ ((p - 1) * ((x - y) / (p - 1))) * n ^ y ≡ n ^ y [ZMOD ↑p]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p) n
⊢ 1 ^ ((x - y) / (p - 1)) * n ^ y ≡ n ^ y [ZMOD ↑p]

Tactic:
one_pow,

Goal state after:
case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p) n
⊢ 1 * n ^ y ≡ n ^ y [ZMOD ↑p]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1)) + 1 ^ (p - 0) * ↑(p.choose 0) ≡ 1 [MOD
    p ^ m * p]

Tactic:
one_pow,

Goal state after:
case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1)) + 1 * ↑(p.choose 0) ≡ 1 [MOD p ^ m * p]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1))

Tactic:
one_pow,

Goal state after:
case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ ∑ x ∈ range p, (p ^ m * d) ^ (x + 1) * 1 * ↑(p.choose (x + 1))
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
x : M
⊢ x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i

Tactic:
simp_rw [ab.mem_submodule_iff', ab, ab_eq]

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
x : M
⊢ (∃ c, x = ∑ x, c x • smithNormalFormCoeffs b h x • (smithNormalFormTopBasis b h) x) ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: case neg
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', dif_neg (fun eq => h ⟨(he.mp eq).symm⟩)]

Goal state after:
case neg
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
⊢ 0 = p.inertiaDeg' P
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 S ↥(I ^ n)
⊢ Module.Finite R ((S ⧸ I) ⊗[S] ↥(I ^ n))

Tactic:
exact .trans (S ⧸ I) _

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ {x | IsMin x}.Finite

Tactic:
refine Set.Finite.of_finite_image (f := asIdeal) ?_ this.injOn

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ (asIdeal '' {x | IsMin x}).Finite
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
I : Ideal R
hU : ∃ I_1, (zeroLocus ↑I_1)ᶜ = (zeroLocus ↑I)ᶜ
J : Ideal R
hZ : ∃ I, zeroLocus ↑J = zeroLocus ↑I
hS : zeroLocus ↑J ∩ closedPoints (PrimeSpectrum R) ⊆ zeroLocus ↑I
⊢ ∀ b ∈ {J_1 | J ≤ J_1 ∧ J_1.IsMaximal}, I ≤ b

Tactic:
rintro x ⟨hJx, hx⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
I : Ideal R
hU : ∃ I_1, (zeroLocus ↑I_1)ᶜ = (zeroLocus ↑I)ᶜ
J : Ideal R
hZ : ∃ I, zeroLocus ↑J = zeroLocus ↑I
hS : zeroLocus ↑J ∩ closedPoints (PrimeSpectrum R) ⊆ zeroLocus ↑I
x : Ideal R
hJx : J ≤ x
hx : x.IsMaximal
⊢ I ≤ x
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
⊢ (closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z = ∅

Tactic:
← Set.not_nonempty_iff_eq_empty

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
⊢ ¬((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
⊢ JacobsonSpace X

Tactic:
rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]
  intro Z hZ hZ'
  obtain ⟨_, ⟨x, hx, rfl⟩, hx'⟩ := nonempty_inter_closedPoints
    (hZ.image f) (hZ'.image hf.isInducing hf.isOpen_range.isLocallyClosed)
  exact ⟨_, hx, hx'⟩

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.IsMaximal
inst✝ : q.IsMaximal
⊢ q.inertiaDeg R = Module.finrank (R ⧸ p) (S ⧸ q)

Tactic:
by
  let : Field (R ⧸ p) := Quotient.field p
  let : Field (S ⧸ q) := Quotient.field q
  exact inertiaDeg_eq_of_isFractionRing p q (R ⧸ p) (S ⧸ q)

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
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ map ((algebraMap S (Localization.AtPrime P)).comp f) p = maximalIdeal (Localization.AtPrime P)

Tactic:
← Ideal.map_map,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
P : Ideal S
inst✝ : P.IsPrime
hp : P ≠ ⊥
hpP : map f p ≤ P
Sₚ : Type v := Localization.AtPrime P
H₁ : ¬map f p ≤ P * P
a : Ideal S
ha : map f p = P * a
ha' : ¬a ≤ P
⊢ map (algebraMap S (Localization.AtPrime P)) (map f p) = maximalIdeal (Localization.AtPrime P)
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✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
⊢ (∃ e, IsIdempotentElem e ∧ KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e) ↔
    ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (TensorProduct.lmul' R) t = 1

Tactic:
simp_rw [this, ← KaehlerDifferential.span_range_eq_ideal]

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
⊢ (∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = S ⊗[R] S ∙ e) ↔
    ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
Module: Mathlib.RingTheory.Unramified.Basic

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

Tactic:
have e' :=
    FormallyUnramified.lift_unique I ⟨2, hI⟩ (f₁.comp <| IsScalarTower.toAlgHom R A B)
      (f₂.comp <| IsScalarTower.toAlgHom R A B) (by rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc])

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
A : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
B : Type u_3
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)
⊢ f₁ = f₂
Module: Mathlib.RingTheory.Etale.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
⊢ FormallyEtale Rₘ Sₘ

Tactic:
by
  have : FormallyEtale S Sₘ := FormallyEtale.of_isLocalization (M.map (algebraMap R S))
  have : FormallyEtale R Sₘ := FormallyEtale.comp R S Sₘ
  exact FormallyEtale.localization_base M

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
P₁ : Extension R A
P₂ : Extension R A
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (equivOfFormallySmooth P₁ P₂) x = (map f) x

Tactic:
rw [← equivOfFormallySmooth_toLinearMap, LinearEquiv.coe_coe]

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 : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈ Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range

Tactic:
let z : (Q.comp P).ker := ⟨x - y, Ideal.sub_mem _ hx' (Ideal.mul_le_right hy)⟩

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
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈ Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x✝¹ : CommRing Q
x✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f

Tactic:
let f : Sₘ →ₐ[Rₘ] Q := by
    refine { FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) with commutes' := ?_ }
    intro r
    change
      (RingHom.comp (FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) : Sₘ →+* Q)
            (algebraMap _ _))
          r =
        algebraMap _ _ r
    congr 1
    refine IsLocalization.ringHom_ext M ?_
    rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
      AlgHom.comp_algebraMap]

Goal state after:
R : Type u_4
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
M : Submonoid R
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : IsScalarTower R Rₘ Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : FormallySmooth R Sₘ
Q : Type (max u_6 u_7)
x✝¹ : CommRing Q
x✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f✝ : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
f : Sₘ →ₐ[Rₘ] Q :=
  let __src := lift I ⋯ (AlgHom.restrictScalars R f✝);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f✝