mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ (matroid R A).closure s = ↑(algebraicClosure (↥(adjoin R s)) A)

Tactic:
simp_rw [← hB.closure_eq_closure, hB.1.1.1.closure_eq_setOfPred_isBasis_insert, Set.ext_iff,
    mem_ofPred, matroid_isBasis_iff, ← matroid_indep_iff, hB.1.1.1, subset_insert, true_and,
    SetLike.mem_coe, mem_algebraicClosure, ← isAlgebraic_adjoin_iff_of_matroid_isBasis hB,
    forall_mem_insert]

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (IsAlgebraic (↥(adjoin R B)) x ∧ ∀ x ∈ B, IsAlgebraic (↥(adjoin R B)) x) ↔ IsAlgebraic (↥(adjoin R B)) x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ (matroid R A).closure s = ↑(algebraicClosure (↥(adjoin R s)) A)

Tactic:
by
  have ⟨B, hB⟩ := (matroid R A).exists_isBasis s
  simp_rw [← hB.closure_eq_closure, hB.1.1.1.closure_eq_setOfPred_isBasis_insert, Set.ext_iff,
    mem_ofPred, matroid_isBasis_iff, ← matroid_indep_iff, hB.1.1.1, subset_insert, true_and,
    SetLike.mem_coe, mem_algebraicClosure, ← isAlgebraic_adjoin_iff_of_matroid_isBasis hB,
    forall_mem_insert]
  exact fun _ ↦ and_iff_left fun x hx ↦ isAlgebraic_algebraMap (⟨x, subset_adjoin hx⟩ : adjoin R B)

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case convert_2.refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0

Tactic:
obtain ⟨n, y, hx⟩ := (minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h
    exact ⟨n, y, hx ▸ aeval F x⟩

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (T.rootSet ↥K) = ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ T'.rootSet E = T.rootSet E

Tactic:
simp [Set.ext_iff, Polynomial.mem_rootSet', T']

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
⊢ (X ^ n - C x).degree ≠ 0

Tactic:
rw [degree_X_pow_sub_C hn' x]

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
⊢ ↑n ≠ 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : ¬x = 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ ∃ z, z ^ n = x

Tactic:
use z

Goal state after:
case h
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : ¬x = 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ z ^ n = x
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
⊢ FiniteDimensional k ↥L

Tactic:
have := hM.out

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
⊢ FiniteDimensional k ↥L
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ ∃ x, eval x p = 0

Tactic:
exact ⟨x, by simpa [Algebra.ofId_apply] using hx⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly

Goal state before:
pp: case inr.hp
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ (aeval h.gen) ((leftMulMatrix h.basis) h.gen).charpoly = 0

Tactic:
apply (injective_iff_map_eq_zero (G := S) (leftMulMatrix _)).mp
      (leftMulMatrix_injective h.basis)

Goal state after:
case inr.hp
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ (leftMulMatrix h.basis) ((aeval h.gen) ((leftMulMatrix h.basis) h.gen).charpoly) = 0
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 F K) z = x ^ q ^ (n + m)

Tactic:
rw [IsScalarTower.algebraMap_apply F E K, h1, map_pow, h2, ← pow_mul, ← pow_add]

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

Goal state before:
pp: case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsGalois k ↥L
⊢ L.fixingSubgroup.Normal

Tactic:
simpa only [IntermediateFieldEquivClosedSubgroup, RelIso.coe_fn_mk, Equiv.coe_fn_mk,
      ← L.restrictNormalHom_ker] using MonoidHom.normal_ker (restrictNormalHom L)

Goal state after:
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
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
⊢ IsPurelyInseparable (↥L) E

Tactic:
let : SMul (separableClosure F E) L := Algebra.toSMul

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this✝ : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
this : SMul ↥(separableClosure F E) ↥L := this✝.toSMul
⊢ IsPurelyInseparable (↥L) E
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
inst✝ : IsAlgClosure F E
H : IsPurelyInseparable F E
this : IsAlgClosed E
⊢ IsSepClosed F

Tactic:
rwa [← separableClosure.eq_bot_iff, IsSepClosed.separableClosure_eq_bot_iff] at H

Goal state after:
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'
⊢ e (e.symm x') = x'

Tactic:
AlgEquiv.apply_symm_apply

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'
⊢ x' = x'
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ↑⟨f ↑0, ⋯⟩ = ↑0

Tactic:
simp only [map_mk, map_zero]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
h : (algebraMap K L) ↑x = ↑((algebraMap (𝓞 K) (𝓞 L)) x)
⊢ x = 0

Tactic:
simp only [hx, map_zero, map_eq_zero, RingOfIntegers.coe_eq_zero_iff] at h

Goal state after:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
h : x = 0
⊢ x = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg.succ
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ ↑(finrank (↥K⟮x⟯) L) * -((expand K (p ^ (n + 1))) g).coeff (((expand K (p ^ (n + 1))) g).natDegree - 1) = 0 x

pp: case neg.succ.hnc
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ ¬(minpoly K x).natDegree = 0

Tactic:
coeff_expand (by positivity),

Goal state after:
case neg.succ
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ (↑(finrank (↥K⟮x⟯) L) *
      -if p ^ (n + 1) ∣ ((expand K (p ^ (n + 1))) g).natDegree - 1 then
          g.coeff ((((expand K (p ^ (n + 1))) g).natDegree - 1) / p ^ (n + 1))
        else 0) =
    0 x

case neg.succ.hnc
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ ¬(minpoly K x).natDegree = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg.succ
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = 0 x

Tactic:
rw [nextCoeff, if_neg, ← hg₂, coeff_expand (by positivity),
        if_neg, neg_zero, mul_zero, LinearMap.zero_apply]
      · rw [natDegree_expand]
        intro h
        have := Nat.dvd_sub (dvd_mul_left (p ^ (n + 1)) g.natDegree) h
        rw [tsub_tsub_cancel_of_le, Nat.dvd_one] at this
        · obtain rfl : g = minpoly K x := by simpa [this] using hg₂
          cases hx hg₁
        · rw [Nat.one_le_iff_ne_zero]
          have : g.natDegree ≠ 0 := fun e ↦ by
            have := congr(natDegree $hg₂)
            rw [natDegree_expand, e, zero_mul] at this
            exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne this
          positivity
      · exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne'

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

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
⊢ traceMatrix A (b ᵥ* P.map ⇑(algebraMap A B)) = Pᵀ * traceMatrix A b * P

Tactic:
ext (α β)

Goal state after:
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β : κ
⊢ traceMatrix A (b ᵥ* P.map ⇑(algebraMap A B)) α β = (Pᵀ * traceMatrix A b * P) α β
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
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
F : IntermediateField K L
⊢ Subgroup.map (↑(mulEquivAlgEquiv G K L)) (fixingSubgroup G ↑F) = F.fixingSubgroup

Tactic:
ext g
  obtain ⟨g, rfl⟩ := (mulEquivAlgEquiv G K L).surjective g
  simp [mem_fixingSubgroup_iff]

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

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1

Tactic:
intro h y

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
h : x ^ i = 1
y : Kˣ
⊢ y ^ i = 1
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: case mp
ι : 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
this : ∀ (c : ι → R) (i : ι), (b'.repr (∑ j, c j • a j • b' j)) i = a i * c i
c : ι → R
i : ι
⊢ a i ∣ (b'.repr (∑ x, c x • smithNormalFormCoeffs b h x • (smithNormalFormTopBasis b h) x)) i

Tactic:
exact ⟨c i, this c i⟩

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 : F
this : x ∈ (Polynomial.map ⊥.subtype (X ^ p - X)).roots ↔ ∃ a ∈ univ.val, ⊥.subtype a = x
⊢ x ∈ ⊥ ↔ x ^ p = x

Tactic:
simpa [sub_eq_zero, iff_comm, FiniteField.X_pow_card_sub_X_ne_zero F (Fact.out : p.Prime).one_lt]

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ (∃ v, v ≠ 0 ∧ (leftMulMatrix b) x *ᵥ v = 0) → x = 0

Tactic:
rintro ⟨v, v_ne, hv⟩

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv : (leftMulMatrix b) x *ᵥ v = 0
⊢ x = 0
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(TensorProduct.map (AlgHom.id B B) f)

Tactic:
change Function.Surjective (TensorProduct.map (AlgHom.id R B) f)

Goal state after:
R : Type w₁
inst✝⁴ : CommRing R
A : Type w₂
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w₃
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(TensorProduct.map (AlgHom.id R B) f)
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case e'_6
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) :=
  (I • ⊤).liftQ (Submodule.mkQ (I ^ (n + 1)) ∘ₗ Submodule.subtype (I ^ n)) ⋯ ∘ₗ ↑(quotTensorEquivQuotSMul (↥(I ^ n)) I)
e_3✝ : inst✝⁵.toSemiring = CommRing.toCommSemiring.toSemiring
e_4✝ : (Submodule.Quotient.addCommGroup (I ^ (n + 1))).toAddCommMonoid = Submodule.Quotient.addCommMonoid (I ^ (n + 1))
e_5✝ : Submodule.Quotient.module' (I ^ (n + 1)) ≍ Submodule.Quotient.module' (I ^ (n + 1))
⊢ φ.toLinearMap.ker = Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n)

Tactic:
apply Submodule.comap_injective_of_surjective (I ^ (n + 1)).mkQ_surjective

Goal state after:
case e'_6
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 := ⋯
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) := ⋯
e_3✝ : inst✝⁵.toSemiring = CommRing.toCommSemiring.toSemiring
e_4✝ : (Submodule.Quotient.addCommGroup (I ^ (n + 1))).toAddCommMonoid = Submodule.Quotient.addCommMonoid (I ^ (n + 1))
e_5✝ : Submodule.Quotient.module' (I ^ (n + 1)) ≍ Submodule.Quotient.module' (I ^ (n + 1))
⊢ Submodule.comap (Submodule.mkQ (I ^ (n + 1))) φ.toLinearMap.ker =
    Submodule.comap (Submodule.mkQ (I ^ (n + 1))) (Submodule.map (Submodule.mkQ (I ^ (n + 1))) (I ^ n))
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
⊢ JacobsonSpace (PrimeSpectrum R)

Tactic:
by
  rw [jacobsonSpace_iff_locallyClosed]
  rintro S hS ⟨U, Z, hU, hZ, rfl⟩
  simp only [← isClosed_compl_iff, isClosed_iff_zeroLocus_ideal, @compl_eq_comm _ U] at hU hZ
  obtain ⟨⟨I, rfl⟩, ⟨J, rfl⟩⟩ := And.intro hU hZ
  simp only [Set.nonempty_iff_ne_empty, ne_eq, Set.inter_assoc,
    ← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset,
    zeroLocus_subset_zeroLocus_iff, Ideal.radical_eq_jacobson, Ideal.jacobson, le_sInf_iff] at hS ⊢
  contrapose hS
  rintro x ⟨hJx, hx⟩
  exact @hS ⟨x, hx.isPrime⟩ ⟨hJx, (isClosed_singleton_iff_isMaximal _).mpr hx⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
x✝ : IsOpen {x}
h : IsOpen {x} := x✝
⊢ IsClopen {x}

Tactic:
by
    obtain ⟨y, rfl : y = x, h'⟩ := exists_isClosed_singleton_of_isJacobsonRing _ h
      ⟨x, Set.mem_singleton x⟩
    exact ⟨h', h⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsClosed {x}
h₂ : StableUnderGeneralization {x}
⊢ IsOpen {x}

Tactic:
isClosed_singleton_iff_isMaximal,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : x.asIdeal.IsMaximal
h₂ : StableUnderGeneralization {x}
⊢ IsOpen {x}
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
p q : Submodule B M
h : p ⋖ q
⊢ length A ↥q = length A ↥p + length (ResidueField A) (ResidueField B)

Tactic:
by
  let f : p →ₗ[B] q := inclusion h.le
  have key : IsSimpleModule B (q ⧸ f.range) := by
    rwa [range_inclusion, ← covBy_iff_quot_is_simple h.le]
  obtain ⟨m, hm, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp key
  rw [eq_maximalIdeal hm] at e
  -- `0 -> p -> q -> κ(B) -> 0` is exact, and length is additive
  let g : q →ₗ[B] ResidueField B := e.comp f.range.mkQ
  have : Function.Injective f := inclusion_injective _
  have : Function.Surjective g := e.surjective.comp f.range.mkQ_surjective
  have : Function.Exact f g := exact_iff.mpr ((e.ker_comp f.range.mkQ).trans f.range.ker_mkQ)
  rw [length_eq_add_of_exact (f.restrictScalars A) (g.restrictScalars A)
    (by simpa) (by simpa) (by simpa), Module.length_eq_of_surjective (M := ResidueField B)
      (residue_surjective (R := A)), Module.length_eq_rank]

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
n : ℕ
hle : map f p ≤ P ^ n
hgt : ¬map f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun m ↦ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m
k : ℕ
⊢ map f p ≤ P ^ k → k ≤ n

Tactic:
hk

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
n : ℕ
hle : map f p ≤ P ^ n
hgt : ¬map f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun m ↦ ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m
k : ℕ
hk : map f p ≤ P ^ k
⊢ k ≤ n
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
n : ℕ
hn : n ≤ p.ramificationIdx' P
⊢ map f p ≤ P ^ n

Tactic:
contrapose! hn
  exact ramificationIdx'_lt hn

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hp_bot : map f p ≠ ⊥
hvp : ¬v = p
⊢ emultiplicity w (map f p) = ↑(v.ramificationIdx' w) * emultiplicity v p

Tactic:
rw [emultiplicity_eq_zero_of_irreducible_ne hv hp.irreducible hvp, mul_zero,
      emultiplicity_map_eq_zero_of_ne hv hp hvp]

Goal state after:
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
⊢ ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S

Tactic:
intro t

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
t : S ⊗[R] S
⊢ (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S