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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R Subtype.val

Tactic:
nontriviality R
  rwa [algebraicIndependent_subtype_range hx.injective]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

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
i : E ≃ₐ[F] K
x✝ : Algebra E K := (↑i).toAlgebra
x : K
h : IsAlgebraic E (↑i (↑i.symm x))
⊢ IsAlgebraic E x

Tactic:
simpa only [AlgEquiv.coe_toAlgHom, AlgEquiv.apply_symm_apply] using h

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
this : IsAlgebraic (↥(adjoin R (v '' (insert i (Set.univ \ {i}) \ {j})))) (v j) → IsTranscendenceBasis R fun x ↦ v ↑x
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
insert_sdiff_self_of_mem (mem_univ _),

Goal state after:
case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
this : IsAlgebraic (↥(adjoin R (v '' (Set.univ \ {j})))) (v j) → IsTranscendenceBasis R fun x ↦ v ↑x
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝ : TopologicalSpace R := B'.topology
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
x₀ : R
U : Set R
⊢ U ∈ B' → ∃ ia ∈ B', ∀ x ∈ id ia, x₀ * x ∈ id U

Tactic:
simpa using! B.mul_left x₀

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case h
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
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (algebraMap F E) y = x ^ q ^ n
⊢ Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]

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

Goal state before:
pp: case h_splits
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ (Polynomial.map (algebraMap K E) (minpoly K x)).Splits

Tactic:
apply sp.splits.of_dvd (Polynomial.map_ne_zero h1)

Goal state after:
case h_splits
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := ⋯
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.map (algebraMap K E) (minpoly K x) ∣ Polynomial.map (algebraMap F E) p
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
⊢ a✝ * b✝ ∈ ⋃ n, V ^ (n + 1)

Tactic:
rcases mem_iUnion.mp ha with ⟨k, hk⟩
      rcases mem_iUnion.mp hb with ⟨l, hl⟩
      apply mem_iUnion.mpr
      use k + 1 + l
      rw [add_assoc, pow_add]
      exact Set.mul_mem_mul hk hl

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.IsSplittingField F (↥K) T
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ Polynomial.IsSplittingField (↥L) E T'

Tactic:
isSplittingField_iff_intermediateField

Goal state after:
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
⊢ (Polynomial.map (algebraMap (↥L) E) T').Splits ∧ adjoin (↥L) (T'.rootSet E) = ⊤
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ

Tactic:
have := IntermediateField.adjoin.finiteDimensional
    (Algebra.IsIntegral.isIntegral (R := K) x)

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K ↥K⟮x⟯
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ
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
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly R s ∣ p

Tactic:
let _ : Algebra K L := FractionRing.liftAlgebra R L

Goal state after:
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
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly R s ∣ p
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
hs : IsIntegral R s
p : R[X]
hp : minpoly R s ∣ p
⊢ (Polynomial.aeval s) p = 0

Tactic:
simpa only [RingHom.mem_ker, RingHom.coe_comp, coe_evalRingHom, coe_mapRingHom,
      Function.comp_apply, eval_map_algebraMap] using
      aeval_eq_zero_of_dvd_aeval_eq_zero hp (minpoly.aeval R s)

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

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

Tactic:
have : ∀ j, coeff (minpolyDiv R x) (i + j) ∉ R[x] := by
    intro j; induction j with
    | zero => exact H
    | succ j IH =>
      intro H; apply IH
      rw [coeff_minpolyDiv]
      refine add_mem ?_ (mul_mem H (self_mem_adjoin_singleton R x))
      exact Subalgebra.algebraMap_mem _ _

Goal state after:
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]
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ R[x]
⊢ False
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
⊢ (minpolyDiv R x).Monic

Tactic:
by
  nontriviality S
  have := congr_arg leadingCoeff (minpolyDiv_spec R x)
  rw [leadingCoeff_mul', ((minpoly.monic hx).map (algebraMap R S)).leadingCoeff] at this
  · simpa using! this
  · simpa using! minpolyDiv_ne_zero hx

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
⊢ p.roots = 0 ↔ p = C (p.coeff 0)

Tactic:
refine ⟨fun h => ?_, fun hp => by rw [hp, roots_C]⟩
  rcases le_or_gt (degree p) 0 with hd | hd
  · exact eq_C_of_degree_le_zero hd
  · obtain ⟨z, hz⟩ := IsSepClosed.exists_root p hd.ne' hsep
    rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz
    simp at hz

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

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
x : E
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

pp: case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

Tactic:
· obtain ⟨g, h1, n, h2⟩ := (minpoly.irreducible (h x).1).hasSeparableContraction q
    exact ⟨n, (h _).2 <| h1.of_dvd <| minpoly.dvd F _ <| by
      simpa only [expand_aeval, minpoly.aeval] using congr_arg (aeval x) h2⟩

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

Tactic:
have hdeg := (minpoly.natSepDegree_eq_one_iff_pow_mem q).2 (h x)

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
⊢ IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case inr
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
x : R ⊗[k] K
a✝ : Nontrivial (R ⊗[k] K)
hq : q = 1
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
· subst hq
    have : CharZero k := charZero_of_expChar_one' k
    exact ⟨0, (Algebra.TensorProduct.includeLeft_surjective R _ <|
      IsPurelyInseparable.surjective_algebraMap_of_isSeparable k K) _⟩

Goal state after:
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
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ (algebraMap A B) a ∈ P

Tactic:
← P.mem_comap,

Goal state after:
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
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ a ∈ Ideal.comap (algebraMap A B) P
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a = b ∨ a = -b

Tactic:
by
  constructor
  · rw [Int.natAbs_eq_natAbs_iff, valMinAbs_inj]
    exact Or.imp_right eq_neg_of_valMinAbs_eq_neg_valMinAbs
  · rintro (rfl | rfl)
    · rfl
    · rw [natAbs_valMinAbs_neg]

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
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap K L) ((Algebra.trace K L) x) = ∑ σ, σ x

Tactic:
apply FaithfulSMul.algebraMap_injective L (AlgebraicClosure L)

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) =
    (algebraMap L (AlgebraicClosure L)) (∑ σ, σ x)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos.succ.prime
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ (n + 1)
hprime : Nat.Prime p
hchar✝ : CharP K p
⊢ p • (trace K ↥(separableClosure K L)) (p ^ n • x) = 0 ((algebraMap (↥(separableClosure K L)) L) x)

Tactic:
nsmul_eq_mul,

Goal state after:
case pos.succ.prime
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ (n + 1)
hprime : Nat.Prime p
hchar✝ : CharP K p
⊢ ↑p * (trace K ↥(separableClosure K L)) (p ^ n • x) = 0 ((algebraMap (↥(separableClosure K L)) L) x)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
j : ℕ
⊢ (fun x_1 ↦ x ^ x_1) j ^ i = 1

Tactic:
rw [← pow_mul, mul_comm, pow_mul, h, one_pow]

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

Goal state before:
pp: case refine_1
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : Finite (M ⧸ N)
x : M
⊢ ((LinearMap.lsmul ℤ M) ↑(Nat.card (M ⧸ N))) x ∈ N

Tactic:
simpa using! AddSubgroup.nsmul_index_mem N.toAddSubgroup x

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Free ℤ R
inst✝¹ : Module.Finite ℤ R
p : ℤ
P : Ideal R
inst✝ : P.LiesOver (span {p})
hp : Prime p
⊢ span {p} ≠ ⊥

Tactic:
simpa using hp.ne_zero

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

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

Tactic:
eq_b

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ d, ∃ e ∈ P ^ (i + 1), a * d + e = c
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
p : ℤ
hp : Prime p
I : Ideal S
hI : p ∣ ↑(absNorm I)
this✝ : IsAddTorsionFree S
this : CharZero S
⊢ span {p} ≠ ⊥

Tactic:
simpa using hp.ne_zero

Goal state after:
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
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
hI : p ∣ ↑(absNorm 0)
x : ℤ
⊢ x ∈ RingHom.ker (algebraMap ℤ S) → x ∈ span {p}

Tactic:
by simp +contextual

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
⊢ IsNoetherian R M

Tactic:
by
  obtain ⟨s, fin, span⟩ := Submodule.fg_def.mp (Module.finite_def.mp ‹_›)
  rw [← s.iUnion_of_singleton_coe, Submodule.span_iUnion] at span
  rw [← Set.finite_coe_iff] at fin
  rw [← isNoetherian_top_iff, ← span]
  have _ (i : M) : IsNoetherian R (Submodule.span R {i}) := by
    rw [LinearMap.span_singleton_eq_range, ← (LinearMap.quotKerEquivRange _).isNoetherian_iff]
    let e (I : Ideal R) : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := ⟨.id _, fun _ _ ↦ rfl⟩
    rw [(e _).isNoetherian_iff_of_bijective Function.bijective_id]
    refine @instIsNoetherianRingOfIsArtinianRing _ _ ?_
    rw [IsArtinianRing, ← (e _).isArtinian_iff_of_bijective Function.bijective_id,
      (LinearMap.quotKerEquivRange _).isArtinian_iff]
    infer_instance
  infer_instance

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

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : I ^ 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
this✝ : Algebra A B := f₁.toAlgebra
this : IsScalarTower R A B
⊢ f₁ = f₂

Tactic:
have :=
    ((KaehlerDifferential.linearMapEquivDerivation R A).toEquiv.trans
          (derivationToSquareZeroEquivLift I hI)).surjective.subsingleton

Goal state after:
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : I ^ 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
this✝¹ : Algebra A B := f₁.toAlgebra
this✝ : IsScalarTower R A B
this : Subsingleton { f // (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I) }
⊢ f₁ = f₂
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
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
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f g : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp g
⊢ Ideal.comap (Shrink.ringEquiv B) I ^ 2 = ⊥

Tactic:
rw [← Ideal.map_symm, ← Ideal.map_pow, hI]; simp

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

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

Tactic:
apply FormallyUnramified.comp_injective I hI

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ (Ideal.Quotient.mkₐ R I).comp (f₁.comp f) = (Ideal.Quotient.mkₐ R I).comp (f₂.comp f)
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✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
s : S
⊢ (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * elem R S = 0

Tactic:
one_tmul_sub_tmul_one_mul_elem

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
s : S
⊢ 0 = 0
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case h₁
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommRing B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ [inst_1 : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro B _ I hI _; exact FormallySmooth.comp_surjective R A I hI

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

Goal state before:
pp: case h₁
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : FiniteType R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : q.LiesOver p
inst✝² : QuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S p) ⟨q, ⋯⟩).asIdeal
hq' : q = Ideal.comap TensorProduct.includeRight.toRingHom q'
this✝ : QuasiFiniteAt p.ResidueField q'
this : q'.IsMaximal
x✝ : R
⊢ ((((Ideal.ResidueField.map q q' TensorProduct.includeRight.toRingHom hq').comp
                ↑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField)
                    ⋯)).comp
            TensorProduct.includeLeftRingHom).comp
        (algebraMap R p.ResidueField))
      x✝ =
    (((algebraMap (p.Fiber S) q'.ResidueField).comp TensorProduct.includeLeftRingHom).comp
        (algebraMap R p.ResidueField))
      x✝

Tactic:
simp [IsScalarTower.algebraMap_apply R S q.ResidueField]

Goal state after: