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⁻¹
⊢ g * (C g.leadingCoeff⁻¹ * C g.leadingCoeff) = g

Tactic:
← C_mul,

Goal state after:
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⁻¹
⊢ g * C (g.leadingCoeff⁻¹ * g.leadingCoeff) = g
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
⊢ B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
let := b.finiteDimensional_of_finite
  rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis hB hB']

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : IsDomain R
inst✝¹² : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : CommRing L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ minpoly K ((algebraMap S L) s) = map (algebraMap R K) (minpoly R s)

Tactic:
by
  refine (eq_of_irreducible_of_monic ?_ ?_ ?_).symm
  · exact ((monic hs).irreducible_iff_irreducible_map_fraction_map).1 (irreducible hs)
  · rw [aeval_map_algebraMap, aeval_algebraMap_apply, aeval, map_zero]
  · exact (monic hs).map _

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✝ : 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
⊢ C a.leadingCoeff * C b.leadingCoeff = 1

Tactic:
← C_mul,

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
⊢ C (a.leadingCoeff * b.leadingCoeff) = 1
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
h_contra : IsUnit a'
⊢ C a.leadingCoeff * C b.leadingCoeff = 1

Tactic:
← C_mul,

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
h_contra : IsUnit a'
⊢ C (a.leadingCoeff * b.leadingCoeff) = 1
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
h2 : NeZero 2
⊢ ∃ z, x = z * z

Tactic:
rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩
  exact ⟨z, sq z⟩

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
hp : p = C (p.coeff 0)
⊢ (C (p.coeff 0)).roots = 0

Tactic:
roots_C

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
hp : p = C (p.coeff 0)
⊢ 0 = 0
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ (trace R S) s = ((leftMulMatrix b) s).trace

Tactic:
rw [trace_apply, LinearMap.trace_eq_matrix_trace _ b, ← toMatrix_lmul_eq]; rfl

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
h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
⊢ Associated (c * d) ((C c * C d).content * p.content)

Tactic:
← C_mul,

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
h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
⊢ Associated (c * d) ((C (c * d)).content * p.content)
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
⊢ trace R S ∘ₗ ↑R (trace S T) = trace R T

Tactic:
by
  ext
  rw [LinearMap.comp_apply, LinearMap.restrictScalars_apply, trace_trace_of_basis b c]

Goal state after:
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
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ IsOpen L.fixingSubgroup.carrier ∧ L.fixingSubgroup.Normal ↔ FiniteDimensional k ↥L ∧ IsGalois k ↥L

Tactic:
isOpen_iff_finite,

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ FiniteDimensional k ↥L ∧ L.fixingSubgroup.Normal ↔ FiniteDimensional k ↥L ∧ IsGalois k ↥L
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
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable E K
x : K
x✝¹ : x ∈ ⊤
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E ↑S
this : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x✝ : Algebra ↥S ↥L := i.toAlgebra
⊢ x ∈ L

Tactic:
have : IsScalarTower S L K := IsScalarTower.of_algebraMap_eq (congrFun rfl)

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
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable E K
x : K
x✝¹ : x ∈ ⊤
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E ↑S
this✝ : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x✝ : Algebra ↥S ↥L := i.toAlgebra
this : IsScalarTower (↥S) (↥L) K
⊢ x ∈ L
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
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
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
g : G
a' : A'
b : B
⊢ g • a' • b = a' • g • b

Tactic:
obtain ⟨a, rfl⟩ : ∃ a, e a = a' := he' a'

Goal state after:
G : Type u_1
A : Type u_2
A' : Type u_3
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
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
g : G
b : B
a : A
⊢ g • e a • b = e a • g • b
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁸ : Group G
inst✝⁷ : CommSemiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra A B
inst✝⁴ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝³ : FaithfulSMul A B
inst✝² : CommSemiring A'
inst✝¹ : Algebra A' B
inst✝ : FaithfulSMul A' B
hA' : IsGaloisGroup G A' B
x : A
⊢ (algebraMap A' B) ((ringEquiv G A A' B) x) = (algebraMap A B) x

Tactic:
by
  simp [ringEquiv]

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁸ : Group G
inst✝⁷ : CommSemiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra A B
inst✝⁴ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝³ : FaithfulSMul A B
inst✝² : CommSemiring A'
inst✝¹ : Algebra A' B
inst✝ : FaithfulSMul A' B
hA' : IsGaloisGroup G A' B
x : A'
⊢ (algebraMap A B) ((ringEquiv G A A' B).symm x) = (algebraMap A' B) x

Tactic:
by
  simp [ringEquiv]

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
inst✝ : SMulCommClass G A B
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
val✝ : Fintype G
this : ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime], Ideal.under A P = Ideal.under A Q → ∃ g ∈ ⊤, Q ≤ g • P
g : G
hg : Q ≤ g • P
g' : G
hg' : g • P ≤ g' • Q
⊢ ∃ g, Q = g • P

Tactic:
exact ⟨g, le_antisymm hg (smul_eq_of_le_smul (hg.trans hg') ▸ hg')⟩

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ ↑x.val * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
exact ⟨(neg_lt_zero.2 <| mod_cast NeZero.pos n).trans_le (by positivity), h⟩

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

Goal state before:
pp: case inr.refine_1
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a = ↑(-a.valMinAbs)

pp: case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2

pp: case inr.refine_3
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ ↑n

Tactic:
· rw [Int.cast_neg, coe_valMinAbs]

Goal state after:
case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2

case inr.refine_3
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case mp
n : ℕ
a b : ZMod n
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs → a = b ∨ a = -b

pp: case mpr
n : ℕ
a b : ZMod n
⊢ a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs

Tactic:
· rw [Int.natAbs_eq_natAbs_iff, valMinAbs_inj]
    exact Or.imp_right eq_neg_of_valMinAbs_eq_neg_valMinAbs

Goal state after:
case mpr
n : ℕ
a b : ZMod n
⊢ a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n a : ℕ
ha : a ≤ n / 2
⊢ (↑a).valMinAbs = ↑a

Tactic:
by
  cases n
  · simp
  · simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
      ha]

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
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
hg₂ : (expand K (p ^ 0)) g = minpoly K x
⊢ g = minpoly K x

Tactic:
by simpa using hg₂

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

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
⊢ False

Tactic:
have fact_pprime := Fact.mk pprime
    -- G has an element x of order p by Cauchy's theorem
    have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd
    -- F has an element u (= ↑↑x) of order p
    let u := ((x : Kˣ) : K)
    have hu : orderOf u = p := by rwa [orderOf_units, Subgroup.orderOf_coe]
    -- u ^ p = 1 implies (u - 1) ^ p = 0 and hence u = 1 ...
    have h : u = 1 := by
      rw [← sub_left_inj, sub_self 1]
      apply eq_zero_of_pow_eq_zero (n := p)
      rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]
      exact Commute.one_right u
    -- ... meaning x didn't have order p after all, contradiction
    apply pprime.one_lt.ne
    rw [← hu, h, orderOf_one]

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

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝¹¹ : Group G
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : MulSemiringAction G L
H : Subgroup G
hGKL : IsGaloisGroup G K L
E : Type u_5
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra E L
inst✝³ : IsScalarTower K E L
inst✝² : Finite G
inst✝¹ : IsGaloisGroup (↥H) E L
inst✝ : IsGalois K E
⊢ H.Normal

Tactic:
by
  let F := (IsScalarTower.toAlgHom K E L).fieldRange
  have : IsGalois K F := .of_algEquiv (IsScalarTower.toAlgHom K E L).equivFieldRange
  have hFL : IsGaloisGroup H F L := inferInstanceAs (IsGaloisGroup H (algebraMap E L).range L)
  have := isGalois G K L
  have : Finite Gal(L/K) := Finite.of_equiv _ (mulEquivAlgEquiv G K L).toEquiv
  rw [← fixingSubgroup_fixedPoints G K L H, subgroup_iff.mp hFL,
    ← mulEquivCongr_mapSubgroup_fixingSubgroup Gal(L/K) G K, MulEquiv.normal_map_iff]
  exact IsGalois.fixingSubgroup_normal_of_isGalois F

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ IsPrimePow q

Tactic:
by
  obtain ⟨p, _, n, hp, hn⟩ := card' K
  exact ⟨p, n, Nat.prime_iff.mp hp, n.prop, hn.symm⟩

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : (ZMod p)ˣ
⊢ a ^ (p - 1) = 1

Tactic:
← card_units p,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : (ZMod p)ˣ
⊢ a ^ Fintype.card (ZMod p)ˣ = 1
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Group G
inst✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
this✝ : P.IsPrime
this : Algebra.IsIntegral A B
x y b : B ⧸ Q
a : A ⧸ P
ha : (algebraMap (A ⧸ P) L) a ≠ 0
hy : (algebraMap (B ⧸ Q) L) y ≠ 0
h : (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y = (algebraMap (B ⧸ Q) L) b / (algebraMap (A ⧸ P) L) a
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((IsFractionRing.stabilizerHom G P Q K L) g) ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b
⊢ f ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b

Tactic:
exact fixed_of_fixed1 G P Q K L f b (fun g ↦ IsFractionRing.injective (B ⧸ Q) L
    ((IsFractionRing.fieldEquivOfAlgEquiv_algebraMap K L L
      (Ideal.Quotient.stabilizerHom Q P G g) b).symm.trans (hx g)))

Goal state after:
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
k : ℕ
hk : k ∈ range p
⊢ p ∣ (p ^ m * d) ^ k * ↑(p.choose (k + 1))

Tactic:
cases m

Goal state after:
case succ.zero
p a d k : ℕ
hk : k ∈ range p
hd : (1 + p * a) ^ p ^ 0 = p ^ 0 * d + 1
⊢ p ∣ (p ^ 0 * d) ^ k * ↑(p.choose (k + 1))

case succ.succ
p a d k : ℕ
hk : k ∈ range p
n✝ : ℕ
hd : (1 + p * a) ^ p ^ (n✝ + 1) = p ^ (n✝ + 1) * d + 1
⊢ p ∣ (p ^ (n✝ + 1) * d) ^ k * ↑(p.choose (k + 1))
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
apply
    (iff_congr _ (by simp [Units.ext_iff])).mp (FiniteField.unit_isSquare_iff hF (Units.mk0 a ha))

Goal state after:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare (Units.mk0 a ha) ↔ IsSquare a
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
hp : p.IsMaximal
hQ : Subsingleton (S ⧸ ⊤)
⊢ p.inertiaDeg' ⊤ = 0

Tactic:
exact dif_neg fun h => hp.ne_top <| h.symm.trans comap_top

Goal state after:
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: case refine_1
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
hfgg : (RingHom.ker g).FG
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A := g.comp ↑(MvPolynomial.algebraTensorAlgEquiv R B).symm
⊢ Function.Surjective ⇑g'

Tactic:
simp_all [g, g']

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

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ normalizedFactors a → id x ^ Multiset.count x (normalizedFactors a) = 1

Tactic:
intro p _ hpa
      simp [hpa]

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

Goal state before:
pp: case intro
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this✝² : IsAddTorsionFree S
this✝¹ : CharZero S
this✝ : Finite (S ⧸ P)
val✝ : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP (S ⧸ P) p
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n

Tactic:
obtain ⟨n, hp, e⟩ := FiniteField.card (S ⧸ P) p

Goal state after:
case intro
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this✝² : IsAddTorsionFree S
this✝¹ : CharZero S
this✝ : Finite (S ⧸ P)
val✝ : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
p : ℕ
hpR : CharP (S ⧸ P) p
n : ℕ+
hp : Nat.Prime p
e : Fintype.card (S ⧸ P) = p ^ ↑n
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hI : p ∣ ↑q ^ n
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
⊢ span {p} ≤ under ℤ P

Tactic:
dvd_prime_pow (Nat.prime_iff_prime_int.mp hq)

Goal state after:
case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hI : ∃ i ≤ n, Associated p (↑q ^ i)
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
⊢ span {p} ≤ under ℤ P
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
p : ℤ
hp : Prime p
I : Ideal S
hI : p ∣ ↑(absNorm I)
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I

Tactic:
induction I using UniqueFactorizationMonoid.induction_on_prime with

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
⊢ IsDiscrete s

Tactic:
have : T1Space s := ⟨fun x ↦ by convert! (hs' x.2).preimage continuous_subtype_val; aesop⟩
  have : Finite s := hs
  exact ⟨inferInstance⟩

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

Goal state before:
pp: J : Ideal ℤ
⊢ span {↑(absNorm J)} = J

Tactic:
obtain ⟨g, rfl⟩ := IsPrincipalIdealRing.principal J
  simp

Goal state after: