mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ¬Maximal (AlgebraicIndepOn R _root_.id) I
B_base : Maximal (AlgebraicIndepOn R _root_.id) B
⊢ ∃ x ∈ B \ I, AlgebraicIndepOn R _root_.id (insert x I)

Tactic:
contrapose! h

Goal state after:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Maximal (AlgebraicIndepOn R _root_.id) B
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
⊢ Maximal (AlgebraicIndepOn R _root_.id) I
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x✝ : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
⊢ IsAlgebraic (↥(adjoin R I)) x

Tactic:
contrapose! h

Goal state after:
case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x✝ : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
h : ¬IsAlgebraic (↥(adjoin R I)) x
⊢ ∃ x ∈ B \ I, AlgebraicIndepOn R _root_.id (insert x I)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
⊢ IsTranscendenceBasis R x

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R A).mpr hx.algebraMap_injective

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
⊢ IsTranscendenceBasis R x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case adjoin_rootSet'
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ {α} ⊆ (minpoly F α).rootSet E

Tactic:
rw [Set.singleton_subset_iff, Polynomial.mem_rootSet]

Goal state after:
case adjoin_rootSet'
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ minpoly F α ≠ 0 ∧ (Polynomial.aeval α) (minpoly F α) = 0
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: case inst
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := ⋯
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := ⋯
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
⊢ Algebra.EssFiniteType (↥(adjoin F ↑s)) E

Tactic:
exact .of_comp F _ _

Goal state after:
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 : IntermediateField F E
inst✝¹ : IsPurelyInseparable F ↥L
inst✝ : Algebra.IsSeparable F ↥L
x : E
hx : x ∈ L
⊢ x ∈ ⊥

Tactic:
by
  obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩
  exact ⟨y, congr_arg (algebraMap L E) hy⟩

Goal state after:
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 E K
inst✝ : IsScalarTower F E K
q : ℕ
h2✝ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range
h1✝ : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
h✝ : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : (algebraMap E K) y = x ^ q ^ n
m : ℕ
z : F
h1 : (algebraMap F E) z = y ^ q ^ m
⊢ (algebraMap F K) z = x ^ q ^ (n + m)

Tactic:
IsScalarTower.algebraMap_apply F E K,

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 E K
inst✝ : IsScalarTower F E K
q : ℕ
h2✝ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range
h1✝ : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
h✝ : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : (algebraMap E K) y = x ^ q ^ n
m : ℕ
z : F
h1 : (algebraMap F E) z = y ^ q ^ m
⊢ (algebraMap E K) ((algebraMap F E) z) = x ^ q ^ (n + m)
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 ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1

Tactic:
by
  obtain ⟨q, _⟩ := ExpChar.exists F
  simp_rw [isPurelyInseparable_iff_pow_mem F q, minpoly.natSepDegree_eq_one_iff_pow_mem q]

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

Goal state before:
pp: case pos
F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ⊥ = ⊤
⊢ ∃ n, d = q ^ n

Tactic:
rw [← finrank_top', ← h, IntermediateField.finrank_bot] at hd
      exact ⟨0, ((pow_zero q).trans hd).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
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ ¬map (algebraMap R K) p = 0

Tactic:
intro con

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

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : ¬Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E

Tactic:
rw [← Algebra.transcendental_iff_not_isAlgebraic] at H
    simp [finSepDegree_eq_zero_of_transcendental F E] at hdeg

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_3
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
x y : C
h : (algebraMap C L) x = (algebraMap C L) y
⊢ ↑1 * x = ↑1 * y

Tactic:
simp only [IsIntegralClosure.algebraMap_injective C A L h]

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
g : G
a : A
b' : B'
⊢ g • a • b' = a • g • b'

Tactic:
have h' {x'} : e.symm (g • x') = g • e.symm x' := by
      apply e.injective
      simp [he]
    apply e.symm.injective
    simpa [h', map_smul] using hG.commutes.smul_comm g a (e.symm b')

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

Goal state before:
pp: case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i x✝ : ι
| of (fun i j ↦ (trace A B) (b i * b j)) i x✝ * b.equivFun z x✝

Tactic:
rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← map_smul]

Goal state after:
case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i x✝ : ι
| (trace A B) (b.equivFun z x✝ • (b i * b x✝))
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case refine_1
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 * ((b.toMatrix ⇑pb.basis)ᵀ * b.toMatrix ⇑pb.basis).det = 1

Tactic:
calc
      (pb.basis.toMatrix b * (pb.basis.toMatrix b)ᵀ).det *
            ((b.toMatrix pb.basis)ᵀ * b.toMatrix pb.basis).det =
          (pb.basis.toMatrix b * (b.toMatrix pb.basis * pb.basis.toMatrix b)ᵀ *
              b.toMatrix pb.basis).det := by
        simp only [← det_mul, Matrix.mul_assoc, Matrix.transpose_mul]
      _ = 1 := by
        simp only [Basis.toMatrix_mul_toMatrix_flip, Matrix.transpose_one, Matrix.mul_one,
          Matrix.det_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹⁹ : Group G
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : IsDomain C
inst✝¹⁴ : Algebra A B
inst✝¹³ : Algebra A C
inst✝¹² : Algebra B C
inst✝¹¹ : FaithfulSMul A B
inst✝¹⁰ : FaithfulSMul B C
inst✝⁹ : IsScalarTower A B C
inst✝⁸ : Finite G
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
g₁✝ g₂✝ : G ⧸ N
g₁ g₂ : G
this✝ : FaithfulSMul A C
h' : ∀ (g : G), (∀ (x : B), g • x = x) → g ∈ N
this : ∀ {g : G}, Quotient.mk'' g = (QuotientGroup.mk' N) g
h : ∀ (a : B), ((QuotientGroup.mk' N) g₂)⁻¹ • (QuotientGroup.mk' N) g₁ • a = a
⊢ Quotient.mk'' g₁ = Quotient.mk'' g₂

Tactic:
← map_inv,

Goal state after:
G : Type u_1
inst✝¹⁹ : Group G
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : IsDomain C
inst✝¹⁴ : Algebra A B
inst✝¹³ : Algebra A C
inst✝¹² : Algebra B C
inst✝¹¹ : FaithfulSMul A B
inst✝¹⁰ : FaithfulSMul B C
inst✝⁹ : IsScalarTower A B C
inst✝⁸ : Finite G
N : Subgroup G
inst✝⁷ : N.Normal
inst✝⁶ : MulSemiringAction G C
hG : IsGaloisGroup G A C
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction (G ⧸ N) B
inst✝³ : SMulCommClass (G ⧸ N) A B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsScalarTower G (G ⧸ N) B
inst✝ : IsGaloisGroup (↥N) B C
g₁✝ g₂✝ : G ⧸ N
g₁ g₂ : G
this✝ : FaithfulSMul A C
h' : ∀ (g : G), (∀ (x : B), g • x = x) → g ∈ N
this : ∀ {g : G}, Quotient.mk'' g = (QuotientGroup.mk' N) g
h : ∀ (a : B), (QuotientGroup.mk' N) g₂⁻¹ • (QuotientGroup.mk' N) g₁ • a = a
⊢ Quotient.mk'' g₁ = Quotient.mk'' g₂
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:
rw [Int.natCast_dvd, Int.natCast_dvd]
  exact Int.Prime.dvd_mul hp h

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ¬q - 1 ∣ i

Tactic:
contrapose! h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : CommRing R
inst✝ : Algebra K R
x✝¹ x✝ : R
p : ℕ
left✝ : CharP K p
w✝ : ℕ+
hp : Nat.Prime p
card_eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : Nontrivial R
this✝ : CharP R p
this : ExpChar R p
⊢ (x✝¹ + x✝) ^ p ^ ↑w✝ = x✝¹ ^ p ^ ↑w✝ + x✝ ^ p ^ ↑w✝

Tactic:
exact add_pow_expChar_pow ..

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
| 1 x

Tactic:
rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
| x ^ p ^ n
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p) n
⊢ n ^ x ≡ n ^ y [ZMOD ↑p]

Tactic:
← pow_sub_mul_pow n hxy,

Goal state after:
case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p) n
⊢ n ^ (x - y) * n ^ y ≡ n ^ y [ZMOD ↑p]
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
ab_eq :
  ∀ (i : Free.ChooseBasisIndex ℤ M),
    ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i
e' : M ≃ₗ[ℤ] ↥N := b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))
f : M →ₗ[ℤ] M := N.subtype ∘ₗ ↑e'
f_apply : ∀ (x : M), f x = ↑((b'.equiv ab (Equiv.refl (Free.ChooseBasisIndex ℤ M))) x) := fun x ↦ rfl
i : Free.ChooseBasisIndex ℤ M
⊢ ↑(ab i) = a i • b' i

Tactic:
exact ab_eq i

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

Goal state before:

Tactic:
(b.det (N.subtype ∘ bN)).natAbs = (LinearMap.det (N.subtype ∘ₗ (e : M →ₗ[ℤ] N))).natAbs := by
      rw [Basis.det_comp_basis]
    _ = _ := natAbs_det_equiv N e

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq α
s : Finset α
i : α → ℕ
p : α
hps : p ∉ s
is_prime : ∀ q ∈ insert p s, Prime q
is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'
hp : Prime p
d : α
hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'
hd : Prime d
hdp : d ∣ p
q : α
q_mem : q ∈ s.val
q_mem' : q ^ i q ∈ Multiset.map (fun p' ↦ p' ^ i p') s.val
hdq : d ∣ q
this : p ∣ q
⊢ p ∈ s ↔ q ∈ s.val

Tactic:
rw [Finset.mem_val,
    is_coprime _ (Finset.mem_insert_self p s) _ (Finset.mem_insert_of_mem q_mem) this]

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
inst✝² : Nontrivial S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
⊢ (norm R) 0 = 0

Tactic:
nontriviality
  rw [norm_apply, coe_lmul_eq_mul, map_zero, LinearMap.det_zero' (Module.Free.chooseBasis R S)]

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

Goal state before:
pp: case neg
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ 0 = p.inertiaDeg' P

Tactic:
rw [inertiaDeg', dif_neg (fun eq => h ⟨eq.symm⟩)]

Goal state after:
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 R
S₁ : Type u_1
inst✝³ : CommRing S₁
inst✝² : Algebra R S₁
P : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
e : E
⊢ p.inertiaDeg' (comap (↑e).symm P) = p.inertiaDeg' P

Tactic:
exact p.inertiaDeg'_comap_eq (AlgEquivClass.toAlgEquiv e).symm P

Goal state after:
Module: Mathlib.RingTheory.Localization.InvSubmonoid

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

Tactic:
Algebra.adjoin_eq_span,

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
⊢ ∃ x ∈ s, x.asIdeal.IsMaximal

Tactic:
simp_rw [← @Set.notMem_compl_iff _ s, hI', mem_zeroLocus]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
s : Set (PrimeSpectrum R)
hs : IsOpen s
hs' : s.Nonempty
I : Ideal R
hI' : sᶜ = zeroLocus ↑I
⊢ ∃ x, ¬↑I ⊆ ↑x.asIdeal ∧ x.asIdeal.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
| I

Tactic:
← hI.radical

Goal state after:
R : Type u_1
inst✝ : CommRing R
H : JacobsonSpace (PrimeSpectrum R)
I : Ideal R
hI : I.IsRadical
| I.radical
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ IsLocallyClosed (f '' {x})

Tactic:
exact (hx.isLocallyClosed.image hf.isInducing hf.isOpen_range.isLocallyClosed)

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

Goal state before:
pp: 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
⊢ ¬IsFiniteLength A M

Tactic:
contrapose! h

Goal state after:
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 A M
⊢ IsFiniteLength B M
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: 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✝ : Flat A B
h : ¬IsFiniteLength A M
⊢ ¬IsFiniteLength B (B ⊗[A] M)

Tactic:
contrapose! h

Goal state after:
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✝ : Flat A B
h : IsFiniteLength B (B ⊗[A] M)
⊢ IsFiniteLength A M
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
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Ideal T
hp : p = comap f P
h : ¬sSup {n | map (algebraMap R T) p ≤ Q ^ n} = 0
⊢ sSup {n | map (algebraMap S T) P ≤ Q ^ n} ≤ sSup {n | map (algebraMap R T) p ≤ Q ^ n}

Tactic:
refine csSup_le_csSup' (h.imp_symm Nat.sSup_of_not_bddAbove) fun n hn ↦ ?_

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
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Ideal T
hp : p = comap f P
h : ¬sSup {n | map (algebraMap R T) p ≤ Q ^ n} = 0
n : ℕ
hn : n ∈ {n | map (algebraMap S T) P ≤ Q ^ n}
⊢ n ∈ {n | map (algebraMap R T) p ≤ Q ^ n}
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ emultiplicity (normalize P) (map f p) = emultiplicity P (map f p)

pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ Irreducible P

Tactic:
normalize_eq

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ emultiplicity P (map f p) = emultiplicity P (map f p)

R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ Irreducible P