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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → φ x = x
hxE : x ∈ E
⊢ False

Tactic:
exact hφx (h_in_H hxE)

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : Fintype.card Gal(K/F) ≤ 2
⊢ IsCyclic Gal(K/F)

Tactic:
← Nat.card_eq_fintype_card

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : Nat.card Gal(K/F) ≤ 2
⊢ IsCyclic Gal(K/F)
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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
⊢ g ∈ lifts (algebraMap (↥(integralClosure R K)) K)

Tactic:
refine (lifts_iff_coeff_lifts _).2 fun n => ?_

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
⊢ g.coeff n ∈ Set.range ⇑(algebraMap (↥(integralClosure R K)) K)
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: 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 : IsUnit (map φ f)
u : Sˣ
hu : C ↑u = map φ f
⊢ IsUnit f

Tactic:
have hdeg := degree_C u.ne_zero

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 : IsUnit (map φ f)
u : Sˣ
hu : C ↑u = map φ f
hdeg : (C ↑u).degree = 0
⊢ IsUnit f
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ minpolyDiv R x ≠ 0

Tactic:
intro e

Goal state after:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
⊢ False
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))
⊢ x ∈ ↑(fixedField H ⊓ L)

Tactic:
· have xL := lift_le _ h
    apply (mem_lift (⟨x, xL⟩ : L)).mp at h
    simp only [mem_fixedField_iff, Subgroup.mem_map, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at h
    simp only [coe_inf, Set.mem_inter_iff, SetLike.mem_coe, mem_fixedField_iff, xL, and_true]
    intro σ hσ
    have : ((restrictNormalHom L σ) ⟨x, xL⟩).1 = x := by rw [h σ hσ]
    nth_rw 2 [← this]
    exact (AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩).symm

Goal state after:
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
f : R[X]
hf : f.IsPrimitive
g : K[X]
⊢ g * map (algebraMap R K) f ∈ lifts (algebraMap R K) ↔ g ∈ lifts (algebraMap R K)

Tactic:
let : NormalizedGCDMonoid R := Nonempty.some inferInstance
  refine ⟨fun ⟨k, (hk : k.map _ = _)⟩ ↦ ?_, fun h ↦ mul_mem h ⟨_, rfl⟩⟩
  let g' := integerNormalization R⁰ g
  obtain ⟨b, hb₁, (hb₂ : g'.map _ = _)⟩ := integerNormalization_spec R⁰ g
  have g'_mul_f : g' * f = b • k := by
    apply map_injective (algebraMap R K) (FaithfulSMul.algebraMap_injective R K)
    rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_mul]
  apply_fun content at g'_mul_f
  have h := Associated.of_eq g'_mul_f
  grw [← C_mul', associated_content_mul, associated_content_C_mul, hf.content_eq_one, mul_one] at h
  obtain ⟨g'', hg⟩ : C b ∣ g' := dvd_content_iff_C_dvd.mp <| (dvd_mul_right ..).trans h.dvd'
  use g''
  simp [← smul_right_inj (nonZeroDivisors.ne_zero hb₁), ← hb₂, hg, C_mul']

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Ring E
inst✝² : Algebra F E
L : Subalgebra F E
inst✝¹ : IsPurelyInseparable F ↥L
inst✝ : Algebra.IsSeparable F ↥L
x : E
hx : x ∈ L
⊢ x ∈ ⊥

Tactic:
obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩
  exact ⟨y, congr_arg (Subalgebra.val _) hy⟩

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

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
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x✝ : T
⊢ (trace R S) ((trace S T) x✝) = (trace R T) x✝

Tactic:
trace_trace_of_basis b c

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 R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x✝ : T
⊢ (trace R T) x✝ = (trace R T) x✝
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
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
⊢ (fun f ↦ f.comp (algebraMap F E)) (j.comp ↑f) = (fun f ↦ f.comp (algebraMap F E)) (j.comp ↑g)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ⟨f ↑1, ⋯⟩ = 1

Tactic:
ext; simp only [map_mk, map_one]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Int

Goal state before:
pp: p q m n : ℕ
hp : Prime p
hq : Prime q
hm : m ≠ 0
hn : n ≠ 0
h : p ^ m = q ^ n
⊢ p = q ∧ m = n

Tactic:
by
  obtain ⟨m, rfl⟩ := exists_eq_add_one_of_ne_zero hm
  obtain ⟨n, rfl⟩ := exists_eq_add_one_of_ne_zero hn
  simpa using hp.pow_inj hq h

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

Goal state before:
pp: 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 : ¬(algebraMap B (B ⧸ Q)) b = 0
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 ((algebraMap B (B ⧸ Q)) b) X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) *
      eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) =
    0
⊢ eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) = 0

Tactic:
Polynomial.eval_X,

Goal state after:
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 : ¬(algebraMap B (B ⧸ Q)) b = 0
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 :
  (algebraMap B (B ⧸ Q)) b ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) *
      eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) =
    0
⊢ eval ((algebraMap B (B ⧸ Q)) b) (map (algebraMap B (B ⧸ Q)) r) = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : ¬FiniteDimensional K L
⊢ (trace K L) x = 0 x

pp: case pos
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
⊢ (trace K L) x = 0 x

Tactic:
· rw [trace_eq_zero_of_not_exists_basis]
    rintro ⟨s, ⟨b⟩⟩
    exact h₀ (Module.Finite.of_basis b)

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
⊢ (trace K L) x = 0 x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Fintype.card ↥G
⊢ ∑ x, ↑↑x ^ k = 0

Tactic:
← Nat.card_eq_fintype_card

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
⊢ ∑ x, ↑↑x ^ k = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case refine_2
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 : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
i : Fin pb.dim
left✝ : i ∈ Finset.univ
j : Fin pb.dim
hij : j ∈ Finset.Ioi i
h : (e j) pb.gen = (e i) pb.gen
⊢ False

Tactic:
exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h)

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

Goal state before:
pp: n : ℕ
⊢ (↑(quotientSpanNatEquivZMod n).symm).comp (castRingHom (ZMod n)) = Ideal.Quotient.mk (Ideal.span {↑n})

Tactic:
ext; simp

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

Goal state before:
pp: n : ℤ
⊢ (↑n.quotientSpanEquivZMod.symm).comp (castRingHom (ZMod n.natAbs)) = Ideal.Quotient.mk (Ideal.span {n})

Tactic:
ext; simp

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

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x ↦ g ^ x) n ^ (Fintype.card F / 2) = 1
⊢ IsSquare ((fun x ↦ g ^ x) n)

Tactic:
← Nat.card_eq_fintype_card

Goal state after:
case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : (fun x ↦ g ^ x) n ^ (Nat.card F / 2) = 1
⊢ IsSquare ((fun x ↦ g ^ x) n)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : (fun x ↦ g ^ x) n ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)
⊢ IsSquare ((fun x ↦ g ^ x) n)

Tactic:
have : 0 < Nat.card F / 2 := Nat.div_pos Finite.one_lt_card (by simp)

Goal state after:
case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : (fun x ↦ g ^ x) n ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)
this : 0 < Nat.card F / 2
⊢ IsSquare ((fun x ↦ g ^ x) 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
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
⊢ (norm R) x = 0 ↔ x = 0

Tactic:
constructor
  swap
  · rintro rfl; exact norm_zero
  · let b := Module.Free.chooseBasis R S
    let decEq := Classical.decEq (Module.Free.ChooseBasisIndex R S)
    rw [norm_eq_matrix_det b, ← Matrix.exists_mulVec_eq_zero_iff]
    rintro ⟨v, v_ne, hv⟩
    rw [← b.equivFun.apply_symm_apply v, b.equivFun_symm_apply, b.equivFun_apply,
      leftMulMatrix_mulVec_repr] at hv
    refine (mul_eq_zero.mp (b.ext_elem fun i => ?_)).resolve_right (show ∑ i, v i • b i ≠ 0 from ?_)
    · simpa only [map_zero, Pi.zero_apply] using! congr_fun hv i
    · contrapose v_ne with sum_eq
      apply b.equivFun.symm.injective
      rw [b.equivFun_symm_apply, sum_eq, map_zero]

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

Goal state before:
pp: case neg
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e 1 = 1

pp: case neg.h
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)

Tactic:
map_one

Goal state after:
case neg
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ 1 = 1

case neg.h
A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
⊢ absNorm 1 = 1

Tactic:
map_one

Goal state after:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
⊢ 1 = 1
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
I : Ideal S
hI : I ≠ ⊥
⊢ (toAddSubgroup I).FiniteIndex

Tactic:
AddSubgroup.finiteIndex_iff,

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : I ≠ ⊥
⊢ (toAddSubgroup I).index ≠ 0
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
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) = mk' S 1 x

Tactic:
by
  rw [← (IsLocalization.map_units S x).mul_left_inj]
  simp

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

Goal state before:
pp: case inr.refine_2
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I ↦ map (Quotient.mk (span {↑n})) I
⊢ Set.InjOn f {I | absNorm I = n}

Tactic:
intro I hI J hJ h
      rw [← comap_map_mk (span_singleton_absNorm_le I), ← hI.symm, ←
        comap_map_mk (span_singleton_absNorm_le J), ← hJ.symm]
      congr

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
⊢ {I | absNorm I ≤ n} = ⋃ i ∈ Set.Icc 0 n, {I | absNorm I = i}

Tactic:
ext; simp

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)
⊢ ¬p.ramificationIdx' P ≠ 1

Tactic:
Ideal.ramificationIdx'_ne_one_iff hpP

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)
⊢ ¬map f p ≤ P ^ 2
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I → ∃ e, IsIdempotentElem e ∧ I = R ∙ e

Tactic:
intro e

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ ∃ e, IsIdempotentElem e ∧ I = R ∙ e
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mp
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
⊢ FormallyUnramified R A →
    ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

pp: case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
⊢ (∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
    FormallyUnramified R A

Tactic:
· intros; exact comp_injective _ ‹_›

Goal state after:
case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
⊢ (∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
    FormallyUnramified R A
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✝ : QuasiFinite R S
I : Ideal R
⊢ (I.primesOver S).Finite

Tactic:
by_cases h : I.IsPrime
  · refine ((finite_comap_preimage_singleton ⟨I, h⟩).image PrimeSpectrum.asIdeal).subset ?_
    exact fun J hJ ↦ ⟨⟨_, hJ.1⟩, PrimeSpectrum.ext hJ.2.1.symm, rfl⟩
  · convert! Set.finite_empty
    by_contra!
    obtain ⟨J, h₁, ⟨rfl⟩⟩ := this
    exact h inferInstance

Goal state after:
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
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : QuasiFiniteAt R p
f : T ≃ₐ[R] S
⊢ p = Ideal.comap (↑f.symm).toRingHom (Ideal.comap f.toRingEquiv.toRingHom p)

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : FiniteType R A
p : Ideal A
inst✝¹ : p.IsPrime
inst✝ : IsUnramifiedAt R p
⊢ ∃ f ∉ p, Unramified R (Localization.Away f)

Tactic:
by
  obtain ⟨f, hfp, H⟩ := exists_formallyUnramified_of_isUnramifiedAt (R := R) p
  exact ⟨f, hfp, ⟨H, .trans ‹_› (IsLocalization.finiteType_of_monoid_fg (.powers f) _)⟩⟩

Goal state after:
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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ (tensorKaehlerQuotKerSqEquiv R P S)
      (s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
        (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)) =
    s ⊗ₜ[P] (D R P) t

Tactic:
change s • (derivationQuotKerSq R P S).liftKaehlerDifferential
    (.D _ _ (Ideal.Quotient.mk _ t)) = _

Goal state after:
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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ s •
      (derivationQuotKerSq R P S).liftKaehlerDifferential
        ((D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)) =
    s ⊗ₜ[P] (D R P) t
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := ⋯
this : Function.Injective ⇑f
⊢ ∀ (J : Ideal (AlgebraicClosure K ⊗[K] A)) (x_1 : J.IsMaximal),
    (algebraMap (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime J)) (f x) = 0

Tactic:
intro M hM

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
⊢ (algebraMap (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)) (f x) = 0
Module: Mathlib.RingTheory.Etale.Kaehler

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✝ : Algebra.FormallyEtale S T
⊢ IsBaseChange T (map R R S T)

Tactic:
change Function.Bijective _

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 R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
⊢ Function.Bijective ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T))))
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case pos
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
⊢ x ∈ (algebraMap K L).range

Tactic:
have h := h'.linearIndepOn_id

Goal state after:
case pos
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
⊢ x ∈ (algebraMap K L).range