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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f g : P.Hom P'
x y : P.Ring
this✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
this :
  (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈
    P'.ker ^ 2
⊢ f.toAlgHom (x * y) - g.toAlgHom (x * y) -
      (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) +
        P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) =
    (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x)

Tactic:
simp only [map_mul]

Goal state after:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f g : P.Hom P'
x y : P.Ring
this✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
this :
  (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x) ∈
    P'.ker ^ 2
⊢ f.toAlgHom x * f.toAlgHom y - g.toAlgHom x * g.toAlgHom y -
      (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) +
        P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) =
    (f.toAlgHom x - P'.σ ((algebraMap P.Ring S') x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ ((algebraMap P.Ring S') y)) * (f.toAlgHom x - g.toAlgHom x)
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
⊢ y' • 1 • ↑s = y' • ↑s

Tactic:
one_smul

Goal state after:
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
⊢ ∃ k h₂ h₃, h₁ = h₃ ∘ₗ h₂

Tactic:
by
  have ⟨_, K, ϕ, hK⟩ := FinitePresentation.exists_fin R P
  have : Module.Finite R K := .of_fg hK
  have : (h₁ ∘ₗ ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0 := by
    simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]
  obtain ⟨k, a, y, hay, ha⟩ := exists_factorization_of_comp_eq_zero_of_free this
  use k, (K.liftQ a (by rwa [← range_le_ker_iff, Submodule.range_subtype] at ha)) ∘ₗ ϕ, y
  apply (cancel_right ϕ.symm.surjective).mp
  apply (cancel_right K.mkQ_surjective).mp
  simpa [comp_assoc]

Goal state after:
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)

Tactic:
rcases lt_or_ge j.castSucc i with hji | hij

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
hji : j.castSucc < i
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)

case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
hij : i ≤ j.castSucc
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
⊢ Module.Finite R M

Tactic:
by
  classical
  constructor
  choose s₁ s₂ using (fun g ↦ (H g).1)
  let sf := fun x : t ↦
    IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers x.val) (f x) (s₁ x)
  use t.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  rintro x -
  refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)
  set S : Submonoid R := Submonoid.powers r.val
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ := multiple_mem_span_of_mem_localization_span S (Rₚ r)
    (s₁ r : Set (Mₚ r)) (IsLocalizedModule.mk' (f r) x (1 : S)) (by rw [s₂ r]; trivial)
  rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalizedModule.smul_mem_finsetIntegerMultiple_span
    S (f r) _ (s₁ r) hn₁
  rw [Submonoid.smul_def] at hn₂
  use n₂ + n₁
  apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) r
  rw [pow_add, mul_smul]
  exact hn₂

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ 1 • f (Matrix.vecCons x v) = f (Matrix.vecCons x v)

pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ Even (↑p + ↑p)

Tactic:
one_smul

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ f (Matrix.vecCons x v) = f (Matrix.vecCons x v)

R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ Even (↑p + ↑p)
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ (-1) ^ ↑(j.succAbove i) • (-1) ^ ↑(i.predAbove j) • (-1) ^ ↑i • f (update (j.removeNth v) i (v j)) +
      (-1) ^ ↑j • f (j.removeNth v) =
    0

Tactic:
update_eq_self_iff.2,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ (-1) ^ ↑(j.succAbove i) • (-1) ^ ↑(i.predAbove j) • (-1) ^ ↑i • f (j.removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0

R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ v j = j.removeNth v i
Module: Mathlib.LinearAlgebra.TensorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
n : ℕ
this :
  ∀ (x : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
    (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j
inst✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
i : Fin n
φ₁ φ₂ : Module.Dual R M
v : Fin n → M
⊢ ((PiTensorProduct.lift
            ((MultilinearMap.mkPiRing R (Fin n) 1).compLinearMap (Function.update f i (φ₁ + φ₂)))).compMultilinearMap
        (tprod R))
      v =
    (LinearMap.compMultilinearMap
        (PiTensorProduct.lift ((MultilinearMap.mkPiRing R (Fin n) 1).compLinearMap (Function.update f i φ₁)) +
          PiTensorProduct.lift ((MultilinearMap.mkPiRing R (Fin n) 1).compLinearMap (Function.update f i φ₂)))
        (tprod R))
      v

Tactic:
simp [this]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ EqOn (⇑((Basis.exteriorPower n b).coord s)) (⇑(ιMultiDual R n b s)) (range (ιMulti_family R n ⇑b))

Tactic:
rintro x ⟨t, rfl⟩

Goal state after:
R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s t : ↑(powersetCard I n)
⊢ ((Basis.exteriorPower n b).coord s) (ιMulti_family R n (⇑b) t) = (ιMultiDual R n b s) (ιMulti_family R n (⇑b) t)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
⊢ ∃ b, v = ⇑W.subtype ∘ ⇑b

Tactic:
use Module.Basis.span hv

Goal state after:
case h
K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := ⋯
⊢ v = ⇑W.subtype ∘ ⇑(Basis.span hv)
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ (M.mulMap (Subalgebra.toSubmodule ⊥)) (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = ↑(y • m)

Tactic:
SetLike.val_smul

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ (M.mulMap (Subalgebra.toSubmodule ⊥)) (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • ↑m
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n ↦ ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (reindex R (fun x ↦ M) (finCongr h)) a.snd = b.snd
⊢ (reindex R (fun x ↦ M) (Equiv.cast ⋯)) a.snd = b.snd

Tactic:
← finCongr_eq_equivCast,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n ↦ ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (reindex R (fun x ↦ M) (finCongr h)) a.snd = b.snd
⊢ (reindex R (fun x ↦ M) (finCongr ?m.57)) a.snd = b.snd

R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n ↦ ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : (reindex R (fun x ↦ M) (finCongr h)) a.snd = b.snd
⊢ a.fst = b.fst
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
h₁ : r • z = r • 1 * z
⊢ tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f

Tactic:
have h₂ : r • f i = (r • (1 : R)) • f i := (smul_one_smul _ _ _).symm

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
h₁ : r • z = r • 1 * z
h₂ : r • f i = (r • 1) • f i
⊢ tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ tprodCoeff R (1 • r) f = tprodCoeff R r f

Tactic:
one_smul

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ tprodCoeff R r f = tprodCoeff R r f
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
hJ : ∃ K, J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)
⊢ Submodule.IsPrincipal J

Tactic:
by
  let : NormalizedGCDMonoid R := Classical.arbitrary _
  obtain ⟨K, hJK0, hK⟩ := hJ
  rcases hK.principal with ⟨x, hJK⟩
  have hxmemJK : x ∈ J * K := by simp [hJK]
  -- Shrink `K` to a finitely generated subideal `K'` witnessing `x ∈ J * K'`.
  have : ∃ T : Finset R, (T : Set R) ⊆ K ∧ x ∈ J * span T := by
    obtain ⟨S, T, hSJ, hTK, hx⟩ := Submodule.mem_span_mul_finite_of_mem_mul hxmemJK
    refine ⟨T, hTK, ?_⟩
    rw [← J.span_eq, span_mul_span]
    exact span_mono (Set.mul_subset_mul_right hSJ) hx
  obtain ⟨T, hTK, hxT⟩ := this
  set K' : Ideal R := span T
  -- Let `g` be the gcd of the chosen generators of `K'`; then `K' ≤ (g)`.
  let g : R := T.gcd id
  have hK' : K' ≤ span {g} :=
    span_le.mpr fun z hz ↦ mem_span_singleton.mpr (Finset.gcd_dvd hz)
  -- Upgrade to `x ∈ J * (g)`, hence `(x) ≤ J * (g)`.
  have hxJg : x ∈ J * span {g} := mul_mono_right hK' hxT
  have hx0 : x ≠ 0 := by
    intro hx
    apply hJK0
    simpa [hJK]
  -- From `(x) = J * (g)`, extract `y` with `x = y * g` and cancel `(g)` to show `J` is principal.
  suffices J * span {g} = span {x} by
    obtain ⟨y, hyJ, rfl⟩ := (Ideal.mem_mul_span_singleton).1 hxJg
    rw [← span_singleton_mul_span_singleton, span_singleton_mul_left_inj] at this
    · exact ⟨y, this⟩
    · contrapose hx0
      rw [hx0, mul_zero]
  -- Show `J * (g) ≤ (x)` by proving `x ∣ b * g` for all `b ∈ J`.
  refine le_antisymm
      (mul_le.mpr fun b hb z hz ↦ ?_)
      ((span_singleton_le_iff_mem _).mpr hxJg)
  obtain ⟨z, rfl⟩ := mem_span_singleton.mp hz
  rw [mem_span_singleton, ← mul_assoc]
  apply dvd_mul_of_dvd_left
  suffices x ∣ normalize b * g from this.trans ((associated_normalize b).mul_right g).dvd'
  -- Show `x ∣ b * g` by proving `x ∣ b * c` for all `b ∈ J` and `c ∈ T`.
  rw [← (Finset.gcd_mul_left' ..).dvd_iff_dvd_right, Finset.dvd_gcd_iff]
  intro c hc
  rw [← mem_span_singleton, span, ← hJK, normalize_apply]
  exact mul_mem_mul (J.mul_mem_right _ hb) (hTK hc)

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝⁴ : CommRing A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : IsNoetherianRing A
inst✝ : Module.Finite A M
⊢ ∃ s, s.head = ⊥ ∧ s.last = ⊤

Tactic:
by
  refine WellFoundedGT.induction_top ⟨⊥, .singleton _ ⊥, rfl, rfl⟩ ?_
  rintro N hN ⟨s, hs₁, hs₂⟩
  have := Submodule.Quotient.nontrivial_iff.mpr hN
  obtain ⟨p, hp⟩ := associatedPrimes.nonempty A (M ⧸ N)
  rw [AssociatedPrimes.mem_iff, isAssociatedPrime_iff] at hp
  obtain ⟨hp, x, rfl⟩ := hp
  obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
  have hxN : x ∉ N := fun h ↦ hp.ne_top (by rw [show N.mkQ x = 0 by simpa]; simp)
  have := Submodule.isQuotientEquivQuotientPrime_iff.mpr ⟨x, hp, rfl⟩
  refine ⟨_, by simpa [hs₂], s.snoc _ (hs₂ ▸ this), by simpa, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝⁴ : CommRing A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : IsNoetherianRing A
inst✝ : Module.Finite A M
⊢ (associatedPrimes A M).Finite

Tactic:
induction ‹Module.Finite A M› using
    IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime A with

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (equiv K') ((mk K) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)

Tactic:
rw [ClassGroup.equiv, ClassGroup.mk_def]
  simp only [ClassGroup, QuotientGroup.congr_mk']
  congr
  rw [← Units.val_inj, Units.coe_mapEquiv, Units.coe_mapEquiv, Units.coe_map]
  exact FractionalIdeal.canonicalEquiv_canonicalEquiv _ _ _ _ _

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

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy'⟩) * ↑↑I = ↑↑J

Tactic:
· exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy').mpr h

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∉ U → False ↔ x✝ ∈ U

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∉ U → False ↔ x✝ ∈ U

Tactic:
tauto

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
⊢ map (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl)))
      (IsLocalRing.maximalIdeal (Localization p.primeCompl)) =
    map (↑(Localization.tensorLeftAlgEquiv p.primeCompl S).toRingEquiv)
      (map (↑includeRight) (IsLocalRing.maximalIdeal (Localization.AtPrime p)))

Tactic:
Ideal.map_map

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
⊢ map (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl)))
      (IsLocalRing.maximalIdeal (Localization p.primeCompl)) =
    map ((↑(Localization.tensorLeftAlgEquiv p.primeCompl S).toRingEquiv).comp ↑includeRight)
      (IsLocalRing.maximalIdeal (Localization.AtPrime p))
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ IsNormalClosure F K ↥(normalClosure F K L)

Tactic:
isNormalClosure_iff

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ (∀ (x : K), (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x)).Splits) ∧
    normalClosure F K ↥(normalClosure F K L) = ⊤
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits ∧
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

pp: F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p *
      Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p ≠ 0

Tactic:
· obtain ⟨hL1, hL2⟩ := hL
    let j : E →ₐ[F] L := IsSplittingField.lift E p hL1
    rw [← j.comp_algebraMap, ← Polynomial.map_map] at hL2
    refine ⟨hx, Splits.of_splits_map (j : E →+* L) hL2 fun a ha ↦ ?_⟩
    rw [Polynomial.map_map, j.comp_algebraMap] at ha
    let : Algebra F⟮x⟯ L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toRingHom.toAlgebra
    let j' : E →ₐ[F⟮x⟯] L := IsSplittingField.lift E (p.map (algebraMap F F⟮x⟯)) ?_
    · change a ∈ j.range
      rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
            IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]
      exact ⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩
    · rwa [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p *
      Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p ≠ 0