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

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
h2 : NeZero 2
⊢ ∃ z, x = z * z

Tactic:
rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
h2 : NeZero 2
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1
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
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ L ≤ fixedField M.fixingSubgroup

Tactic:
IntermediateField.le_iff_le

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
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ M.fixingSubgroup ≤ L.fixingSubgroup
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
rw [Ne, Ne, ← not_or, ← mul_eq_zero, ← hab]

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ ¬map (algebraMap R K) p = 0
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : IsTorsionFree A L
⊢ finrank A C = finrank K L

Tactic:
have : Module.Free A C := IsIntegralClosure.module_free A K L C
  have : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L C
  have : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L :=
    IsIntegralClosure.isLocalization A K L C
  let b := Basis.localizationLocalization K A⁰ L (Module.Free.chooseBasis A C)
  rw [Module.finrank_eq_card_chooseBasisIndex, Module.finrank_eq_card_basis b]

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 : x = 0
⊢ x = 0

Tactic:
exact h

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
⊢ ∃ i ∈ Finset.univ, i • b ∈ Q

Tactic:
exact ⟨1, Finset.mem_univ 1, (one_smul G b).symm ▸ hb⟩

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ -↑n ≤ x.valMinAbs * 2

Tactic:
exact x.valMinAbs_mem_Ioc.1.le

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

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

Tactic:
rw [one_pow, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn
        cases H hn

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

Goal state before:
pp: case refine_2
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
h : G
⊢ (algebraMap B (B ⧸ Q)) (h • (a - eval b r)) = (algebraMap B (B ⧸ Q)) (if h • Q = Q then a else 0)

Tactic:
rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem,
      ← Ideal.smul_mem_pointwise_smul_iff (a := h⁻¹), smul_sub, inv_smul_smul]
    simp only [← eq_inv_smul_iff (g := h), eq_comm (a := Q)]
    split_ifs with hh
    · rwa [ha, sub_sub_cancel_left, hh, Q.neg_mem_iff]
    · rw [smul_zero, sub_zero]
      exact hr' h⁻¹ hh

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
κ : Type w
E : Type z
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
b : κ → L
⊢ (traceMatrix K b).map ⇑(algebraMap K E) = embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ

Tactic:
ext (i j); simp [trace_eq_sum_embeddings, embeddingsMatrix, Matrix.mul_apply]

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
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0
⊢ (traceMatrix K ⇑pb.basis).det ≠ 0

Tactic:
by
    refine mt (fun ht => ?_) this
    rw [ht, map_zero]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
⊢ [Algebra.IsSeparable K L, Algebra.trace K L ≠ 0, (traceForm K L).Nondegenerate].TFAE

Tactic:
tfae_have 1 → 3 := fun _ ↦ traceForm_nondegenerate K L
  tfae_have 3 → 2 := fun H₁ H₂ ↦ H₁.ne_zero (by ext; simp [H₂])
  tfae_have 2 → 1 := not_imp_comm.mp Algebra.trace_eq_zero_of_not_isSeparable
  tfae_finish

Goal state after:
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
h : ∀ (y : L), (∃ y_1, (algebraMap (FractionRing B) L) y_1 = y) → g • y = y
x : B
⊢ g • (algebraMap C L) ((algebraMap B C) x) = (algebraMap C L) ((algebraMap B C) x)

Tactic:
apply h

Goal state after:
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 := ⋯
L : Type u_7 := ⋯
this✝ : MulSemiringAction G L := ⋯
this : IsGaloisGroup (↥H) (FractionRing B) L
g : G
h : ∀ (y : L), (∃ y_1, (algebraMap (FractionRing B) L) y_1 = y) → g • y = y
x : B
⊢ ∃ y, (algebraMap (FractionRing B) L) y = (algebraMap C L) ((algebraMap B C) x)
Module: Mathlib.FieldTheory.Finite.Basic

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

Tactic:
apply h

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

Goal state before:
pp: case a
a b : ℤ
⊢ ↑(EuclideanDomain.gcd a b).natAbs ∣ ↑(a.gcd b)

Tactic:
Int.natAbs_dvd

Goal state after:
case a
a b : ℤ
⊢ EuclideanDomain.gcd a b ∣ ↑(a.gcd b)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ZMod p
x✝ : n ∈ ⊤
this : ↑n.val • 1 ∈ ⊥
⊢ n ∈ ⊥

Tactic:
by rwa [natCast_zsmul, Nat.smul_one_eq_cast, ZMod.natCast_zmod_val] at this

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

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P✝ : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P✝
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P✝) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P✝) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P✝] k
f : B ⧸ Q →ₐ[A ⧸ P✝] k := IsScalarTower.toAlgHom (A ⧸ P✝) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P✝) k).comp (algebraMap A (A ⧸ P✝))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P✝) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝¹ : IsScalarTower A (B ⧸ Q) k
this✝ : IsScalarTower A B k
P : Polynomial A
hp : (Polynomial.mapRingHom (algebraMap A B)) P = MulSemiringAction.charpoly G x
this : (Polynomial.aeval x) P = 0
⊢ (σ.comp f).toRingHom ((mk Q) x) ∈ f.range

Tactic:
have : Polynomial.aeval (σ (algebraMap (B ⧸ Q) k (mk _ x))) P = 0 := by
    refine (DFunLike.congr_fun (Polynomial.aeval_algHom ((σ.restrictScalars A).comp
      (IsScalarTower.toAlgHom A (B ⧸ Q) k)) _) P).trans ?_
    rw [AlgHom.comp_apply, ← algebraMap_eq, Polynomial.aeval_algebraMap_apply, this,
      map_zero, map_zero]

Goal state after:
case intro
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P✝ : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P✝
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P✝) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P✝) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k →ₐ[A ⧸ P✝] k
f : B ⧸ Q →ₐ[A ⧸ P✝] k := IsScalarTower.toAlgHom (A ⧸ P✝) (B ⧸ Q) k
hf : Function.Injective ⇑f
x : B
val✝ : Fintype G
algInst✝¹ : Algebra A k := ((algebraMap (A ⧸ P✝) k).comp (algebraMap A (A ⧸ P✝))).toAlgebra
algInst✝ : Algebra B k := ((algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))).toAlgebra
scalarTowerInst✝¹ : IsScalarTower A (A ⧸ P✝) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A k))
scalarTowerInst✝ : IsScalarTower B (B ⧸ Q) k := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap B k))
this✝² : IsScalarTower A (B ⧸ Q) k
this✝¹ : IsScalarTower A B k
P : Polynomial A
hp : (Polynomial.mapRingHom (algebraMap A B)) P = MulSemiringAction.charpoly G x
this✝ : (Polynomial.aeval x) P = 0
this : (Polynomial.aeval (σ ((algebraMap (B ⧸ Q) k) ((mk Q) x)))) P = 0
⊢ (σ.comp f).toRingHom ((mk Q) x) ∈ f.range
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: case mpr.refine_1
ι : 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
mem_I_iff : ∀ (x : M), x ∈ N ↔ ∀ (i : ι), a i ∣ (b'.repr x) i
N' : Submodule R (ι → R) := pi Set.univ fun i ↦ R ∙ a i
x : ι → R
hdvd : ∀ (i : ι), ∃ a_1, x i = a i * a_1
i : ι
⊢ a i ∣ x i

Tactic:
exact hdvd i

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

Goal state before:
pp: M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank ℤ ↥N = finrank ℤ M
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
e : M ⧸ N ≃+ ((i : Free.ChooseBasisIndex ℤ M) → ZMod (smithNormalFormCoeffs b h i).natAbs) := N.quotientEquivPiZMod b h
⊢ Finite (M ⧸ N)

Tactic:
have : ∀ i, NeZero (a i).natAbs := fun i ↦
    ⟨Int.natAbs_ne_zero.mpr (smithNormalFormCoeffs_ne_zero b h i)⟩

Goal state after:
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank ℤ ↥N = finrank ℤ M
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
e : M ⧸ N ≃+ ((i : Free.ChooseBasisIndex ℤ M) → ZMod (smithNormalFormCoeffs b h i).natAbs) := N.quotientEquivPiZMod b h
this : ∀ (i : Free.ChooseBasisIndex ℤ M), NeZero (a i).natAbs
⊢ Finite (M ⧸ N)
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) ^ (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).natDegree *
        (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).roots.prod) =
    ((minpoly R pb.gen).aroots F).prod

Tactic:
this.natDegree_map,

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.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑(Submodule.span R ↑(invSubmonoid M S))

Tactic:
span_invSubmonoid

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑⊤
Module: Mathlib.Topology.JacobsonSpace

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

Tactic:
Z

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
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
⊢ ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z

Tactic:
Z

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.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Algebra.norm ℤ) x ∣ y ↔ ↑((Algebra.norm ℤ) x).natAbs ∣ y

pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ Nat.Prime (absNorm (span {x}))

Tactic:
Int.natAbs_dvd

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Algebra.norm ℤ) x ∣ y ↔ (Algebra.norm ℤ) x ∣ y

S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ Nat.Prime (absNorm (span {x}))
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
h : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
⊢ ∀ (n : ℕ), ∃ a ∈ {n | map f p ≤ P ^ n}, n < a

Tactic:
exact h

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, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : i = 0
x : A
⊢ Subsingleton (B ⧸ I ^ i)

Tactic:
rw [hi, pow_zero, Ideal.one_eq_top]

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, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : i = 0
x : A
⊢ Subsingleton (B ⧸ ⊤)
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✝² : FormallyUnramified R A
C : Type (max u_2 u_3)
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : (Ideal.Quotient.mkₐ B I).comp f₁ = (Ideal.Quotient.mkₐ B I).comp f₂
this✝ : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
this : IsScalarTower R B C
⊢ f₁ = f₂

Tactic:
ext : 1

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✝² : FormallyUnramified R A
C : Type (max u_2 u_3)
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : (Ideal.Quotient.mkₐ B I).comp f₁ = (Ideal.Quotient.mkₐ B I).comp f₂
this✝ : Algebra R C := ⋯
this : IsScalarTower R B C
⊢ (AlgHom.restrictScalars R f₁).comp TensorProduct.includeRight =
    (AlgHom.restrictScalars R f₂).comp TensorProduct.includeRight
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
e : S ⊗[R] S
he : IsIdempotentElem e
hsp : KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e
e₁ : S ⊗[R] S ≃ₐ[S] (S ⊗[R] S ⧸ Ideal.span {e}) × S ⊗[R] S ⧸ Ideal.span {1 - e} :=
  AlgEquiv.prodQuotientOfIsIdempotentElem S he ⋯ ⋯ ⋯
⊢ ∃ T x x_1, Nonempty (S ⊗[R] S ≃ₐ[S] S × T)

Tactic:
let e₂ : (S ⊗[R] S ⧸ Ideal.span {e}) ≃ₐ[S] S :=
    ((Ideal.span {e}).quotientEquivAlgOfEq S hsp.symm).trans <|
      Ideal.quotientKerAlgEquivOfSurjective <|
        (⟨· ⊗ₜ 1, by simp [Algebra.TensorProduct.lmul'']⟩)

Goal state after:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
e : S ⊗[R] S
he : IsIdempotentElem e
hsp : KaehlerDifferential.ideal R S = S ⊗[R] S ∙ e
e₁ : S ⊗[R] S ≃ₐ[S] (S ⊗[R] S ⧸ Ideal.span {e}) × S ⊗[R] S ⧸ Ideal.span {1 - e} :=
  AlgEquiv.prodQuotientOfIsIdempotentElem S he ⋯ ⋯ ⋯
e₂ : (S ⊗[R] S ⧸ Ideal.span {e}) ≃ₐ[S] S :=
  (Ideal.quotientEquivAlgOfEq S ⋯).trans (Ideal.quotientKerAlgEquivOfSurjective ⋯)
⊢ ∃ T x x_1, Nonempty (S ⊗[R] S ≃ₐ[S] S × T)
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
⊢ Ideal.under R (Ideal.map (algebraMap S (Localization.AtPrime Q)) P) =
    Ideal.under R (IsLocalRing.maximalIdeal (Localization.AtPrime Q))

Tactic:
convert! h₂

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
⊢ Ideal.under R (Ideal.map (algebraMap S (Localization.AtPrime Q)) P) = Ideal.under R P

case e'_3
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
⊢ Ideal.under R (IsLocalRing.maximalIdeal (Localization.AtPrime Q)) = Ideal.under R Q