mathlib-initiative/mathlib-tactics huggingface dataset:
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
h1 :
  C (integerNormalization R⁰ a).content * (integerNormalization R⁰ a).primPart * integerNormalization R⁰ b =
    C (c * d) * p
u : Rˣ
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ IsUnit a ∨ IsUnit b

Tactic:
(integerNormalization R⁰ b).eq_C_content_mul_primPart,

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
h1 :
  C (integerNormalization R⁰ a).content * (integerNormalization R⁰ a).primPart *
      (C (integerNormalization R⁰ b).content * (integerNormalization R⁰ b).primPart) =
    C (c * d) * p
u : Rˣ
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : Type w
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Algebra.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
this : Algebra.IsSeparable ↥L ↥(↥L)⟮x⟯
⊢ x ∈ (algebraMap (↥L) E).range

Tactic:
have : Algebra.IsSeparable F (restrictScalars F L⟮x⟯) := Algebra.IsSeparable.trans F L L⟮x⟯

Goal state after:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : Type w
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Algebra.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
this✝ : Algebra.IsSeparable ↥L ↥(↥L)⟮x⟯
this : Algebra.IsSeparable F ↥(IntermediateField.restrictScalars F (↥L)⟮x⟯)
⊢ x ∈ (algebraMap (↥L) E).range
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
n : ℕ
g : G
⊢ g • (charpoly G b).coeff n = (charpoly G b).coeff n

Tactic:
rw [← coeff_smul, smul_charpoly]

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:
by
  apply FaithfulSMul.algebraMap_injective L (AlgebraicClosure L)
  rw [_root_.map_sum (algebraMap L (AlgebraicClosure L))]
  rw [← Fintype.sum_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
  · rw [← trace_eq_sum_embeddings (AlgebraicClosure L) (x := x)]
    simp only [algebraMap_eq_smul_one, smul_one_smul]
  · intro σ
    simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk,
      AlgEquiv.coe_ofBijective, AlgHom.restrictNormal_commutes, algebraMap_self, RingHom.id_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
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b = 1

pp: K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((LinearMap.BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠
    0

Tactic:
· apply Basis.toMatrix_mul_toMatrix_flip

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((LinearMap.BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠
    0
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ ↑p ∣ m ∨ ↑p ∣ n

Tactic:
Int.natCast_dvd,

Goal state after:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs ∨ ↑p ∣ n
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ n.natAbs

Tactic:
Int.natCast_dvd,

Goal state after:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : p ∣ (n ^ k).natAbs
⊢ p ∣ n.natAbs
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ
p a m : ℕ
hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
| succ m hm =>

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

Goal state before:
pp: case mpr
ι : 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 := ⋯
b' : Basis ι R M := ⋯
ab : Basis ι R ↥N := ⋯
ab_eq : ∀ (i : ι), ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
x : M
this : ∀ (c : ι → R) (i : ι), (b'.repr (∑ j, c j • a j • b' j)) i = a i * c i
⊢ (∀ (i : ι), a i ∣ (b'.repr x) i) → ∃ c, x = ∑ x, c x • smithNormalFormCoeffs b h x • (smithNormalFormTopBasis b h) x

Tactic:
rintro ha
      choose c hc using ha
      exact ⟨c, b'.ext_elem fun i => Eq.trans (hc i) (this c i).symm⟩

Goal state after:
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) ^ pb.dim * (minpoly R pb.gen).coeff 0) = ((minpoly R pb.gen).aroots F).prod

Tactic:
← pb.natDegree_minpoly,

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 * (minpoly R pb.gen).coeff 0) =
    ((minpoly R pb.gen).aroots F).prod
Module: Mathlib.RingTheory.Norm.Basic

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

Tactic:
refine (mul_eq_zero.mp (b.ext_elem fun i => ?_)).resolve_right (show ∑ i, v i • b i ≠ 0 from ?_)

Goal state after:
case mp.refine_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv : ⇑(b.repr (x * ∑ i, v i • b i)) = 0
i : Free.ChooseBasisIndex R S
⊢ (b.repr (x * ∑ i, v i • b i)) i = (b.repr 0) i

case mp.refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv : ⇑(b.repr (x * ∑ i, v i • b i)) = 0
⊢ ∑ i, v i • b i ≠ 0
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
ι : Type w
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : IsDomain S
b : Basis ι R S
x : S
⊢ (norm R) x = 0 ↔ x = 0

Tactic:
have : Module.Free R S := Module.Free.of_basis b

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
ι : Type w
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : IsDomain S
b : Basis ι R S
x : S
this : Free R S
⊢ (norm R) x = 0 ↔ x = 0
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite R (S ⧸ I)
⊢ Module.Finite R (S ⧸ 1)

Tactic:
Ideal.one_eq_top

Goal state after:
case zero
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite R (S ⧸ I)
⊢ Module.Finite R (S ⧸ ⊤)
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 : 1 ≤ Module.annihilator R M
⊢ P M

Tactic:
Ideal.one_eq_top

Goal state after:
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 : ⊤ ≤ Module.annihilator R M
⊢ P M
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
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
I : Ideal S
⊢ ¬((I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) ∧ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n)

Tactic:
by tauto

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
x : X
hx : x ∈ Z
hx' : f x ∈ closedPoints Y
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
exact ⟨_, hx, hx'⟩

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
x : X
hx : x ∈ Z
hx' : f x ∈ closedPoints Y
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
exact ⟨_, hx, hx'⟩

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case pos
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
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' {↑y})

pp: case neg
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
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' {↑y})

Tactic:
· convert_to IsClosed {(⟨y, h⟩ : U j)}
    · ext; simp [← Subtype.coe_inj]
    apply isClosed_singleton_of_isLocallyClosed_singleton
    convert!
      (hy'.isLocallyClosed.image IsEmbedding.subtypeVal.isInducing
            (U i).2.isOpenEmbedding_subtypeVal.isOpen_range.isLocallyClosed).preimage
        continuous_subtype_val
    ext
    simp [← Subtype.coe_inj]

Goal state after:
case neg
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
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' {↑y})
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 ↔ x ∣ ↑y

Tactic:
rw [← Ideal.mem_span_singleton (y := x), ← eq_intCast (algebraMap ℤ S), ← Ideal.mem_comap,
    ← Ideal.span_singleton_absNorm, Ideal.mem_span_singleton, Ideal.absNorm_span_singleton,
    Int.natAbs_dvd]
  rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
⊢ ¬map f p ≤ P ^ 2

Tactic:
intro h₂

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
h₂ : map f p ≤ P ^ 2
⊢ False
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mpr.refine_1
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
⊢ RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom ^ 2 = ⊥

Tactic:
AlgHom.ker_kerSquareLift

Goal state after:
case mpr.refine_1
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
⊢ (RingHom.ker (TensorProduct.lmul' R).toRingHom).cotangentIdeal ^ 2 = ⊥
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✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ [inst : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
apply Ideal.IsNilpotent.induction_on (S := B) I hI

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

case h₂
R : Type v
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type w⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [inst_1 : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (S ⧸ I)],
            Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R J).comp
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 ⧸ 1)

Tactic:
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.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
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q

Tactic:
obtain rfl | hp := eq_or_ne p ⊥

Goal state after:
case inl
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
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver ⊥
⊢ ⊥.ramificationIdx' Q = ⊥.ramificationIdx' P * P.ramificationIdx' Q

case inr
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
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q
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
⊢ ∀ ⦃B_1 : Type u_3⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro Q _ _ I hI f₁ f₂ e

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₂
⊢ f₁ = f₂
Module: Mathlib.RingTheory.QuasiFinite.Basic

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 R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : QuasiFinite R S
inst✝ : QuasiFinite S T
⊢ QuasiFinite R T

Tactic:
by
  refine ⟨fun P hP ↦ ?_⟩
  have : Module.Finite (P.Fiber S) ((P.Fiber S) ⊗[S] T) :=
    iff_of_isArtinianRing.mp inferInstance
  have : Module.Finite P.ResidueField ((P.Fiber S) ⊗[S] T) :=
    .trans (P.Fiber S) _
  let e : P.Fiber S ≃ₐ[S] S ⊗[R] P.ResidueField :=
    { __ := Algebra.TensorProduct.comm _ _ _, commutes' _ := rfl }
  let e' : (P.Fiber S) ⊗[S] T ≃ₐ[R] P.Fiber T :=
    ((Algebra.TensorProduct.congr e .refl).restrictScalars R).trans <|
    ((Algebra.TensorProduct.comm _ _ _).restrictScalars R).trans <|
    ((Algebra.TensorProduct.cancelBaseChange _ _ T _ _).restrictScalars R).trans
    (Algebra.TensorProduct.comm _ _ _)
  let e'' : (P.Fiber S) ⊗[S] T ≃ₐ[P.ResidueField] P.Fiber T :=
    { __ := e', commutes' _ := by simp [e', e] }
  exact .of_surjective e''.toLinearMap e''.surjective

Goal state after: