mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ R[x]
⊢ (minpolyDiv R x).coeff (i + (j + 1)) ∉ R[x]

Tactic:
intro H

Goal state after:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ R[x]
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ R[x]
⊢ False
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
P : R[X]
hmo : P.Monic
hP : (Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree
hs : IsIntegral R s
hnz : ¬minpoly R s - P = 0
⊢ (Polynomial.aeval s) (minpoly R s - P) = 0

Tactic:
by simp [hP]

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

Goal state before:
pp: case mpr
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
⊢ (∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))) → IsIntegrallyClosed R

Tactic:
intro H

Goal state after:
case mpr
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
H : ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
⊢ IsIntegrallyClosed R
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
q : ℕ
h2✝ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range
h1✝ : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
h✝ : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : (algebraMap E K) y = x ^ q ^ n
m : ℕ
z : F
h1 : (algebraMap F E) z = y ^ q ^ m
⊢ (algebraMap E K) (y ^ q ^ m) = x ^ q ^ (n + m)

Tactic:
map_pow,

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
q : ℕ
h2✝ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range
h1✝ : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
h✝ : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : (algebraMap E K) y = x ^ q ^ n
m : ℕ
z : F
h1 : (algebraMap F E) z = y ^ q ^ m
⊢ (algebraMap E K) y ^ q ^ m = x ^ q ^ (n + m)
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
F E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
q : ℕ
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
d : ℕ
hd : finrank F E = d
⊢ ∃ n, d = q ^ n

Tactic:
induction d using Nat.strongRecOn generalizing F with
  | ind d IH =>
    by_cases h : (⊥ : IntermediateField F E) = ⊤
    · rw [← finrank_top', ← h, IntermediateField.finrank_bot] at hd
      exact ⟨0, ((pow_zero q).trans hd).symm⟩
    obtain ⟨x, -, hx⟩ := SetLike.exists_of_lt (lt_of_le_of_ne bot_le h :)
    obtain ⟨m, y, e⟩ := IsPurelyInseparable.minpoly_eq_X_pow_sub_C F q x
    have : finrank F F⟮x⟯ = q ^ m := by
      rw [adjoin.finrank (Algebra.IsIntegral.isIntegral x), e, natDegree_sub_C, natDegree_X_pow]
    obtain ⟨n, hn⟩ := IH _ (by
      rw [← hd, ← finrank_mul_finrank F F⟮x⟯, Nat.lt_mul_iff_one_lt_left finrank_pos, this]
      by_contra! H
      refine hx (finrank_adjoin_simple_eq_one_iff.mp (le_antisymm (this ▸ H) ?_))
      exact Nat.one_le_iff_ne_zero.mpr Module.finrank_pos.ne') (F⟮x⟯) rfl
    exact ⟨m + n, by rw [← hd, ← finrank_mul_finrank F F⟮x⟯, hn, pow_add, this]⟩

Goal state after:
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case inr
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
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ 0 = finrank K L

Tactic:
eq_comm

Goal state after:
case inr
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
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ finrank K L = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
a : Kˣ
⊢ a ∈ univ.erase (-1) → a ≠ 1 → a⁻¹ ≠ a

Tactic:
simp +contextual [Units.inv_eq_self_iff]

Goal state after:
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
hGKL : IsGaloisGroup G K L
hF : FixedPoints.intermediateField ↥H = F
⊢ IsGaloisGroup (↥H) (↥F) L

Tactic:
eq_comm

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
hGKL : IsGaloisGroup G K L
hF : F = FixedPoints.intermediateField ↥H
⊢ IsGaloisGroup (↥H) (↥F) L
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
G : Subgroup Kˣ
inst✝¹ : Fintype ↥G
inst✝ : Decidable (G = ⊥)
G_bot : ¬G = ⊥
⊢ ∑ x, ↑↑x = if G = ⊥ then 1 else 0

Tactic:
· simp only [G_bot, ite_false]
    exact sum_subgroup_units_eq_zero G_bot

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

Goal state before:
pp: case refine_1
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
⊢ Fintype.card (L →ₐ[K] AlgebraicClosure L) = pb.dim

Tactic:
rw [AlgHom.card, pb.finrank]

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

Goal state before:
pp: case e_s
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
as_comp : (fun x ↦ (↑↑x * ↑↑a) ^ k) = (fun x ↦ ↑↑x ^ k) ∘ fun x ↦ x * a
⊢ univ.val = Multiset.map (fun x ↦ x * a) univ.val

Tactic:
eq_comm

Goal state after:
case e_s
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
a✝ : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
as_comp : (fun x ↦ (↑↑x * ↑↑a) ^ k) = (fun x ↦ ↑↑x ^ k) ∘ fun x ↦ x * a
⊢ Multiset.map (fun x ↦ x * a) univ.val = univ.val
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).Separable

Tactic:
separable_def

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
⊢ IsCoprime (X ^ q - X) (derivative (X ^ q - X))
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
⊢ (expand K q) f = f ^ q

Tactic:
by
  obtain ⟨p, hp⟩ := CharP.exists K
  rcases FiniteField.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩
  have : Fact p.Prime := ⟨hp⟩
  dsimp at hn
  rw [hn, ← map_iterateFrobenius_expand, iterateFrobenius_eq_pow,
    frobenius_pow hn, RingHom.one_def, map_id]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
⊢ a ^ (p - 1) = if a ≠ 0 then 1 else 0

Tactic:
split_ifs with ha
  · exact pow_card_sub_one_eq_one ha
  · simp [of_not_not ha, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]

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

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

Tactic:
add_comm,

Goal state after:
case succ
p a m : ℕ
hm : 1 ≡ (p * a + 1) ^ p ^ m [MOD p ^ m]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ.zero
p a d k : ℕ
hk : k ∈ range p
hd : 1 + p * a = d + 1
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))

Tactic:
add_comm,

Goal state after:
case succ.zero
p a d k : ℕ
hk : k ∈ range p
hd : p * a + 1 = d + 1
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: 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
this : (LinearMap.det f).natAbs = Nat.card (M ⧸ N)
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)

Tactic:
by
    calc
      _ = (LinearMap.det (N.subtype ∘ₗ
            (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N))).natAbs := rfl
      _ = (LinearMap.det (N.subtype ∘ₗ _)).natAbs :=
            Int.natAbs_eq_iff_associated.mpr (LinearMap.associated_det_comp_equiv _ _ _)
      _ = Nat.card (M ⧸ N) := this

Goal state after:
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
hf : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
this✝ : Nontrivial R
this : (minpoly R pb.gen).Monic
⊢ (algebraMap R F) ((-1) ^ (minpoly R pb.gen).natDegree) *
      ((-1) ^ (minpoly R pb.gen).natDegree * (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).roots.prod) =
    ((minpoly R pb.gen).aroots F).prod

Tactic:
map_pow,

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
hf : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
this✝ : Nontrivial R
this : (minpoly R pb.gen).Monic
⊢ (algebraMap R F) (-1) ^ (minpoly R pb.gen).natDegree *
      ((-1) ^ (minpoly R pb.gen).natDegree * (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).roots.prod) =
    ((minpoly R pb.gen).aroots F).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

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

Tactic:
simp_rw [id, ← pow_add, this]

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:
by
        refine ?_ ∘ₗ (TensorProduct.quotTensorEquivQuotSMul _ I).toLinearMap
        refine Submodule.liftQ _ ((Submodule.mkQ _).comp (I ^ n).subtype) ?_
        rw [LinearMap.ker_comp, ← Submodule.map_le_map_iff_of_injective (I ^ n).subtype_injective,
          Submodule.map_smul'', Submodule.map_comap_eq]
        simpa [pow_succ'] using Ideal.mul_le_right (I := I) (J := I ^ n)

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S.leftInv
b : M
⊢ 1 = ↑a * b ↔ ↑a * b = 1

Tactic:
eq_comm

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a : ↥S.leftInv
b : M
⊢ ↑a * b = 1 ↔ ↑a * b = 1
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z ≠ ∅ → IsClosed[inst✝] (closure[inst✝] Z \ Z) → Z ∩ closedPoints X ≠ ∅

Tactic:
intro H

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
⊢ ∀ (Z : Set X), Z ≠ ∅ → IsClosed[inst✝] (closure[inst✝] Z \ Z) → Z ∩ closedPoints X ≠ ∅
Module: Mathlib.Topology.JacobsonSpace

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

Tactic:
intro H

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}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ vanishingIdeal (zeroLocus ↑I.jacobson) ≤ vanishingIdeal (zeroLocus ↑I)

Tactic:
apply vanishingIdeal_anti_mono

Goal state after:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
⊢ zeroLocus ↑I ⊆ zeroLocus ↑I.jacobson
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }

Tactic:
by
    refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)
    · intro _
      simp_rw [← or_and_right, em, true_and]
    · exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos
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✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)

Tactic:
rw [← length_compositionSeries s hs_bot hs_top]

Goal state after:
case pos
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✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length A M = ↑s.length * length (ResidueField A) (ResidueField B)
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 r.ResidueField =
    Module.finrank (under R r).ResidueField q.ResidueField * Module.finrank q.ResidueField r.ResidueField

Tactic:
eq_comm

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
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
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: 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

Tactic:
· rw [inertiaDeg_of_not_isPrime r R hr, inertiaDeg_of_not_isPrime r S hr, mul_zero]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos
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
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length B (B ⊗[A] M) = length A M * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
rw [← length_compositionSeries s hs_bot hs_top]

Goal state after:
case pos
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
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length B (B ⊗[A] M) = ↑s.length * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤

Tactic:
intro H

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
⊢ (∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
    FormallyUnramified R A

Tactic:
intro H

Goal state after:
case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
⊢ FormallyUnramified R A
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
⊢ (∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
    FormallyUnramified R A

Tactic:
intro H
    replace H : ∀ ⦃B : Type u⦄ [CommRing B] [Small.{w} B],
        ∀ [Algebra R B] (I : Ideal B) (_ : I ^ 2 = ⊥),
          Function.Injective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I) := by
      intro B _ _ _ I hI f g e
      simpa [DFunLike.ext_iff] using H (B := Shrink B) (I.comap (Shrink.ringEquiv _))
        (by rw [← Ideal.map_symm, ← Ideal.map_pow, hI]; simp)
        (a₁ := (Shrink.algEquiv _ _).symm.toAlgHom.comp f)
        (a₂ := (Shrink.algEquiv _ _).symm.toAlgHom.comp g)
        (by simpa [DFunLike.ext_iff, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Shrink.ringEquiv] using e)
    constructor
    by_contra! h
    obtain ⟨f₁, f₂, e⟩ := (KaehlerDifferential.endEquiv R A).injective.nontrivial
    apply e
    ext1
    let f := RingHom.ker (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom
    refine H
      (RingHom.ker (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom) ?_ ?_
    · rw [AlgHom.ker_kerSquareLift]
      exact Ideal.cotangentIdeal_square _
    · ext x
      apply RingHom.kerLift_injective (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom
      simpa using DFunLike.congr_fun (f₁.2.trans f₂.2.symm) x

Goal state after: