mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g' : R[X]
hg' : map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
⊢ map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ a) → IsUnit a

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ b) → IsUnit b

Tactic:
all_goals apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ a ∣ f

R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ b ∣ f
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✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit (Polynomial.map (algebraMap R K) b' * C b.leadingCoeff)

Tactic:
← Polynomial.coe_mapRingHom

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✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit ((mapRingHom (algebraMap R K)) b' * C b.leadingCoeff)
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ IsUnit (Polynomial.map (algebraMap R K) a' * C a.leadingCoeff)

Tactic:
← Polynomial.coe_mapRingHom

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ IsUnit ((mapRingHom (algebraMap R K)) a' * C a.leadingCoeff)
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
inst✝ : IsGalois k K
H : (ClosedSubgroup Gal(K/k))ᵒᵈ
⊢ { toSubgroup := (IntermediateField.fixedField ↑H).fixingSubgroup, isClosed' := ⋯ } = H

Tactic:
fixingSubgroup_fixedField H

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : (ClosedSubgroup Gal(K/k))ᵒᵈ
⊢ { toSubgroup := ↑H, isClosed' := ⋯ } = H
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
⊢ IsPurelyInseparable F E ↔ Subsingleton (Emb F E)

Tactic:
by
  rw [isPurelyInseparable_iff_finSepDegree_eq_one, Field.finSepDegree, Nat.card_eq_one_iff_unique,
    and_iff_left_iff_imp]
  infer_instance

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

Goal state before:
pp: case intro
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
val✝ : Fintype G
⊢ Algebra.IsIntegral A B

Tactic:
refine ⟨fun b ↦ ?_⟩

Goal state after:
case intro
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
val✝ : Fintype G
b : B
⊢ IsIntegral A b
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case pos
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))
n : ℕ
hn : n ≤ k
⊢ (X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q).coeff (n + j) = q.coeff n

Tactic:
Polynomial.coeff_X_pow_mul

Goal state after:
case pos
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))
n : ℕ
hn : n ≤ k
⊢ q.coeff n = q.coeff n
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  __src
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Tactic:
obtain ⟨n, h⟩ := VectorSpace.card_fintype (ZMod p) K

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  __src
n : ℕ
h : q = Fintype.card (ZMod p) ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case hnc
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x ↦ ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ¬q - 1 ∣ i

Tactic:
exact hiq

Goal state after:
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
x✝ : ℤ
⊢ (fun x ↦ ↑x) x✝ = 0 ↔ ↑n ∣ x✝

Tactic:
ZMod.intCast_zmod_eq_zero_iff_dvd

Goal state after:
n : ℕ
x✝ : ℤ
⊢ ↑n ∣ x✝ ↔ ↑n ∣ x✝
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * 1 ^ (p - (k + 1)) * ↑(p.choose (k + 1))

Tactic:
simp_rw [one_pow, mul_one, pow_succ', mul_assoc, ← Finset.mul_sum]

Goal state after:
case succ
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ p ^ m * (d * ∑ i ∈ range p, (p ^ m * d) ^ i * ↑(p.choose (i + 1)))
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: ι : 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
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → R ⧸ Ideal.span {smithNormalFormCoeffs b h i}

Tactic:
have ab_eq := smithNormalFormBotBasis_def b h

Goal state after:
ι : 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
⊢ (M ⧸ N) ≃ₗ[R] (i : ι) → R ⧸ Ideal.span {smithNormalFormCoeffs b h i}
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

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

Tactic:
i

Goal state after:
ι : 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
x : M
c : ι → R
i : ι
⊢ (b'.repr (∑ j, c j • a j • b' j)) i = a i * c i
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)

Tactic:
have ab_eq := smithNormalFormBotBasis_def b h

Goal state after:
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
a : Free.ChooseBasisIndex ℤ M → ℤ := smithNormalFormCoeffs b h
b' : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := smithNormalFormTopBasis b h
ab : Basis (Free.ChooseBasisIndex ℤ M) ℤ ↥N := smithNormalFormBotBasis b h
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (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) *
      (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).coeff 0 =
    ((minpoly R pb.gen).aroots F).prod

Tactic:
hf.coeff_zero_eq_prod_roots_of_monic (this.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) ^ (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
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hP : P.LiesOver ⊥
⊢ ⊥.inertiaDeg' P = finrank R S

Tactic:
by
  rw [inertiaDeg', dif_pos (over_def P (⊥ : Ideal R)).symm]
  replace hP : P = ⊥ := eq_bot_of_liesOver_bot R P
  rw [Algebra.finrank_eq_of_equiv_equiv (RingEquiv.quotientBot R).symm
    ((quotEquivOfEq hP).trans (RingEquiv.quotientBot S)).symm]
  rfl

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: case zero
R₀ : Type u_1
R : Type u_2
inst✝⁷ : Ring R₀
inst✝⁶ : Ring R
inst✝⁵ : Module R₀ R
inst✝⁴ : IsSemiprimaryRing R
P : (M : Type u) → [inst : AddCommGroup M] → [Module R₀ M] → [Module R M] → Prop
ss : IsSemisimpleRing (R ⧸ Ring.jacobson R)
Jac : Ideal R := Ring.jacobson R
h0 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M]
    [IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑Jac → P M
h1 :
  ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M],
    let N := Jac • ⊤;
    P ↥N → P (M ⧸ N) → P M
this :
  ∀ {M : Type u} [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [IsScalarTower R₀ R M],
    Jac ≤ Module.annihilator R M → P M
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R₀ M
inst✝¹ : Module R M
inst✝ : IsScalarTower R₀ R M
hn : Jac ^ 0 ≤ Module.annihilator R M
⊢ P M

Tactic:
rw [Jac.pow_zero, Ideal.one_eq_top] at hn; exact this (le_top.trans hn)

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

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

Tactic:
true_and

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ closedPoints X).Nonempty

Tactic:
← hU.iUnion_inter Z,

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ : (⋃ i, Z ∩ ↑(U i)).Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ closedPoints X).Nonempty
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∈ U j
x✝ : ↥(U j)
⊢ x✝ ∈ Subtype.val ⁻¹' {↑y} ↔ x✝ ∈ {⟨↑y, h⟩}

Tactic:
simp [← Subtype.coe_inj]

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∈ U j
x✝ : ↥(U j)
⊢ x✝ ∈ {⟨↑y, h⟩} ↔ x✝ ∈ Subtype.val ⁻¹' Subtype.val '' {y}

Tactic:
simp [← Subtype.coe_inj]

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

Goal state before:
pp: case pos.zero
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length A ↥(RelSeries.head s) = ↑↑0 * length (ResidueField A) (ResidueField B)

Tactic:
hs_bot

Goal state after:
case pos.zero
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
s : CompositionSeries (Submodule B M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
⊢ length A ↥⊥ = ↑↑0 * length (ResidueField A) (ResidueField B)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
⊢ ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I

Tactic:
← map_sup,

Goal state after:
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 S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
⊢ ⊤ = map (algebraMap S T) (P ⊔ I)
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : QuasiFinite R S
inst✝¹ : IsArtinianRing R
inst✝ : IsLocalRing R
e : (maximalIdeal R).Fiber S ≃ₐ[R] S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) :=
  (TensorProduct.congr
        (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (maximalIdeal R).ResidueField) ⋯) ⋯).symm
        AlgEquiv.refl).trans
    ((TensorProduct.comm R (R ⧸ maximalIdeal R) S).trans
      (AlgEquiv.restrictScalars R (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)).symm))
this : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
⊢ nilradical R ≤ Ideal.comap (algebraMap R S) (nilradical S)

Tactic:
exact fun x hx ↦ IsNilpotent.map hx _

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✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
⊢ ∃ a, elem R S = a.sum fun i x ↦ x ⊗ₜ[R] b i

Tactic:
let b' := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)
    use b'.repr (elem R S)
    conv_lhs => rw [← b'.linearCombination_repr (elem R S), Finsupp.linearCombination_apply]
    congr! with _ i x
    simp [b', Basis.tensorProduct, TensorProduct.smul_tmul']

Goal state after:
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
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H✝² : IsClopen {p}
this✝¹ : IsNoetherianRing S
this✝ : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H✝¹ : {p} = ↑(PrimeSpectrum.basicOpen e)
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal := IsLocalization.Away.liftAlgHom e ⋯
h₁ : Set.range (PrimeSpectrum.comap (algebraMap S (Localization.Away e))) = {p}
this : Subsingleton (PrimeSpectrum (Localization.Away e))
x : S
s : ↥p.asIdeal.primeCompl
H✝ : ¬IsUnit ((algebraMap S (Localization.Away e)) ↑s)
M : Ideal (Localization.Away e)
hM : M.IsMaximal
H : Ideal.span {(algebraMap S (Localization.Away e)) ↑s} ≤ M
⊢ False

Tactic:
have := Subsingleton.elim ((IsLocalRing.closedPoint _).comap f.toRingHom) ⟨M, inferInstance⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H✝² : IsClopen {p}
this✝² : IsNoetherianRing S
this✝¹ : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H✝¹ : {p} = ↑(PrimeSpectrum.basicOpen e)
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal := IsLocalization.Away.liftAlgHom e ⋯
h₁ : Set.range (PrimeSpectrum.comap (algebraMap S (Localization.Away e))) = {p}
this✝ : Subsingleton (PrimeSpectrum (Localization.Away e))
x : S
s : ↥p.asIdeal.primeCompl
H✝ : ¬IsUnit ((algebraMap S (Localization.Away e)) ↑s)
M : Ideal (Localization.Away e)
hM : M.IsMaximal
H : Ideal.span {(algebraMap S (Localization.Away e)) ↑s} ≤ M
this :
  PrimeSpectrum.comap f.toRingHom (IsLocalRing.closedPoint (Localization.AtPrime p.asIdeal)) =
    { asIdeal := M, isPrime := ⋯ }
⊢ False
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing P
inst✝² : CommRing S
inst✝¹ : Algebra R P
inst✝ : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - y = ↑(l (1 ⊗ₜ[P] (D R P) (x - y)))

Tactic:
exact congr_arg Subtype.val (LinearMap.congr_fun hl.symm ⟨x - y, by simp [RingHom.mem_ker, h]⟩)

Goal state after: