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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
⊢ f.natSepDegree = 1 ↔ ∃ n y, f = X ^ q ^ n - C y

Tactic:
hi.natSepDegree_eq_one_iff_of_monic' q hm,

Goal state after:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
⊢ (∃ n y, f = (expand F (q ^ n)) (X - C y)) ↔ ∃ n y, f = X ^ q ^ n - C y
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h2 : f.roots.card ≠ 0
y : F
h1 : f = (Multiset.map (fun x ↦ X - C x) (f.roots.card • {y})).prod
h3 : f.roots = f.roots.card • {y}
⊢ f = (X - C y) ^ f.roots.card

Tactic:
Multiset.map_nsmul,

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h2 : f.roots.card ≠ 0
y : F
h1 : f = (f.roots.card • Multiset.map (fun x ↦ X - C x) {y}).prod
h3 : f.roots = f.roots.card • {y}
⊢ f = (X - C y) ^ f.roots.card
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: 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
hα : F⟮α⟯ = ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun e ↦ ↑e, invFun := fun e ↦ ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯,
    commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
⊢ Nat.card Gal(E/F) = finrank F E

Tactic:
have h_splits : ((minpoly F α).map (algebraMap F E)).Splits := IsGalois.splits F α

Goal state after:
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
hα : F⟮α⟯ = ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun e ↦ ↑e, invFun := fun e ↦ ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯,
    commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F E) (minpoly F α)).Splits
⊢ Nat.card Gal(E/F) = finrank F E
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup Gal(E/F)
x : E
⊢ x ∈ MulAction.fixedPoints (↥H) E ↔ ∀ f ∈ H, f x = x

Tactic:
simp only [MulAction.mem_fixedPoints, Subtype.forall, Subgroup.mk_smul, AlgEquiv.smul_def]

Goal state after:
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
σ τ : Gal(L/K)
h_diff : σ ≠ τ
⊢ ¬σ⁻¹ * τ = 1

Tactic:
inv_mul_eq_one

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
⊢ ¬σ = τ
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ eval₂ (↑σ₁) (σ₂ x) (minpolyDiv R x) = if σ₁ x = σ₂ x then σ₁ ((aeval x) (derivative (minpoly R x))) else 0

Tactic:
apply eval₂_minpolyDiv_of_eval₂_eq_zero

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ eval₂ ((↑σ₁).comp (algebraMap R S)) (σ₂ x) (minpoly R x) = 0
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
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
x : S
hx : IsIntegral R x
hx' : R[x] = ⊤
⊢ (PowerBasis.ofAdjoinEqTop' hx hx').gen = x

Tactic:
simp [PowerBasis.ofAdjoinEqTop']

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
⊢ IsSepClosed k

Tactic:
refine ⟨fun p hp ↦ ?_⟩

Goal state after:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
⊢ p.Splits
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : StrongRankCondition R
inst✝ : Free R S
x : R
H : ∃ s, Nonempty (Basis (↥s) R S)
⊢ (trace R S) ((algebraMap R S) x) = finrank R S • x

Tactic:
trace_algebraMap_of_basis H.choose_spec.some,

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : StrongRankCondition R
inst✝ : Free R S
x : R
H : ∃ s, Nonempty (Basis (↥s) R S)
⊢ Fintype.card ↥H.choose • x = finrank R S • 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
q : ℕ
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
⊢ ∃ n, finrank F E = q ^ n

Tactic:
suffices ∀ (F E : Type v) [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q]
      [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n by
    simpa using this (⊥ : IntermediateField F E) E q

Goal state after:
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
⊢ ∀ (F E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q]
    [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n
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✝
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 : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
this : finrank F ↥F⟮x⟯ = q ^ m
⊢ finrank (↥F⟮x⟯) E < d

Tactic:
by
      rw [← hd, ← finrank_mul_finrank F F⟮x⟯, Nat.lt_mul_iff_one_lt_left finrank_pos, this]
      by_contra! H
      refine hx (finrank_adjoin_simple_eq_one_iff.mp (le_antisymm (this ▸ H) ?_))
      exact Nat.one_le_iff_ne_zero.mpr Module.finrank_pos.ne'

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

Goal state before:
pp: case inr
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
x : R ⊗[k] K
a✝ : Nontrivial (R ⊗[k] K)
hq : q = 1
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
subst hq
    have : CharZero k := charZero_of_expChar_one' k
    exact ⟨0, (Algebra.TensorProduct.includeLeft_surjective R _ <|
      IsPurelyInseparable.surjective_algebraMap_of_isSeparable k K) _⟩

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

Goal state before:
pp: case inl
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
hq : Nat.Prime q
⊢ 0 < q

pp: case inr
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
hq : q = 1
⊢ 0 < q

Tactic:
<;>

Goal state after:
case inl
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
hq : Nat.Prime q
⊢ 0 < q

case inr
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
hq : q = 1
⊢ 0 < q
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
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
⊢ IsGaloisGroup H A B ↔ IsGaloisGroup G A B

Tactic:
by
  refine ⟨fun h ↦ h.of_mulEquiv e.symm fun g x ↦ ?_, fun h ↦ h.of_mulEquiv e he⟩
  rw [← he, e.apply_symm_apply]

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]

Goal state after:
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'
h' : ∀ {x' : B'}, e.symm (g • x') = g • e.symm x'
⊢ g • a • b' = a • g • b'
Module: Mathlib.Data.Nat.Prime.Int

Goal state before:
pp: p q m n : ℕ
hp : Prime p
hq : Prime q
h : p ^ (m + 1) = q ^ (n + 1)
⊢ p = q ∧ m = n

Tactic:
by
  have H := dvd_antisymm (Prime.dvd_of_dvd_pow hp <| h ▸ dvd_pow_self p (succ_ne_zero m))
    (Prime.dvd_of_dvd_pow hq <| h.symm ▸ dvd_pow_self q (succ_ne_zero n))
  exact ⟨H, succ_inj.mp <| Nat.pow_right_injective hq.two_le (H ▸ h)⟩

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

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K (adjoin.powerBasis hx).gen).aroots F).sum = ((minpoly K x).aroots F).sum

pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen)).Splits

Tactic:
<;>

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K (adjoin.powerBasis hx).gen).aroots F).sum = ((minpoly K x).aroots F).sum

case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen)).Splits
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x))).aroots F).sum = ((minpoly K x).aroots F).sum

pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x)))).Splits

Tactic:
<;>

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x))).aroots F).sum = ((minpoly K x).aroots F).sum

case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x)))).Splits
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis (↥s) B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
i j : ↥s
⊢ ((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x).map (⇑e) i j = (leftMulMatrix b) x i j

Tactic:
simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]

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

Goal state before:
pp: case h2.left
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < x.valMinAbs * 2 - y * 2

pp: case h2.right
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs * 2 - y * 2 < ↑n * 2

Tactic:
<;>

Goal state after:
case h2.left
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < x.valMinAbs * 2 - y * 2

case h2.right
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs * 2 - y * 2 < ↑n * 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inl
a b : ZMod 0
h : a.valMinAbs = -b.valMinAbs
⊢ a = -b

pp: case inr
n : ℕ
a b : ZMod n
h : a.valMinAbs = -b.valMinAbs
hn : NeZero n
⊢ a = -b

Tactic:
<;>

Goal state after:
case inl
a b : ZMod 0
h : a.valMinAbs = -b.valMinAbs
⊢ a = -b

case inr
n : ℕ
a b : ZMod n
h : a.valMinAbs = -b.valMinAbs
hn : NeZero n
⊢ a = -b
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

Tactic:
rw [Int.natAbs_eq_natAbs_iff, valMinAbs_inj]

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h✝ : a.val ≤ n / 2
⊢ ↑a.val = ↑a.val + ↑0

pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h✝ : ¬a.val ≤ n / 2
⊢ ↑a.val = ↑a.val - ↑n + ↑n

Tactic:
<;>

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h✝ : a.val ≤ n / 2
⊢ ↑a.val = ↑a.val + ↑0

case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h✝ : ¬a.val ≤ n / 2
⊢ ↑a.val = ↑a.val - ↑n + ↑n
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
a : Kˣ
⊢ a ∈ univ.erase (-1) → a⁻¹ ∈ univ.erase (-1)

Tactic:
by simp [@inv_eq_iff_eq_inv _ _ a]

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
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
⊢ FixedPoints.intermediateField ↥H = F

Tactic:
refine IntermediateField.ext_iff.mpr fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩

Goal state after:
case refine_1
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
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ FixedPoints.intermediateField ↥H
⊢ x ∈ F

case refine_2
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
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
⊢ x ∈ FixedPoints.intermediateField ↥H
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
hg : G ≠ ⊥
⊢ ∑ x, ↑↑x = 0

Tactic:
Subgroup.ne_bot_iff_exists_ne_one

Goal state after:
K : Type u_1
inst✝² : Ring K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
hg : ∃ a, a ≠ 1
⊢ ∑ x, ↑↑x = 0
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
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ Function.Surjective ⇑(trace K L)

Tactic:
by
  rw [← LinearMap.range_eq_top]
  apply (IsSimpleOrder.eq_bot_or_eq_top (α := Ideal K) _).resolve_left
  rw [LinearMap.range_eq_bot]
  exact Algebra.trace_ne_zero K L

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
⊢ ∀ (x y : Kˣ), ↑(x * y) ^ i = ↑x ^ i * ↑y ^ i

Tactic:
by simp [mul_pow]

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

Goal state before:
pp: case h.inl
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

pp: case h.inr
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

Tactic:
<;>

Goal state after:
case h.inl
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = 1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

case h.inr
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case a
a b : ℤ
⊢ (EuclideanDomain.gcd a b).natAbs ∣ a.gcd b

pp: case a
a b : ℤ
⊢ a.gcd b ∣ (EuclideanDomain.gcd a b).natAbs

Tactic:
<;>

Goal state after:
case a
a b : ℤ
⊢ (EuclideanDomain.gcd a b).natAbs ∣ a.gcd b

case a
a b : ℤ
⊢ a.gcd b ∣ (EuclideanDomain.gcd a b).natAbs
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: a b : ℤ
⊢ (EuclideanDomain.gcd a b).natAbs = a.gcd b

Tactic:
by
  apply Nat.dvd_antisymm <;> rw [← Int.natCast_dvd_natCast]
  · rw [Int.natAbs_dvd]
    exact Int.dvd_coe_gcd (EuclideanDomain.gcd_dvd_left _ _) (EuclideanDomain.gcd_dvd_right _ _)
  · rw [Int.dvd_natAbs]
    exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left ..) (Int.gcd_dvd_right ..)

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

Goal state before:
pp: case inl
b c : ℤ
k : ℕ
hk : Odd k
d : ℤ
hab : IsCoprime (d ^ k) b
h : d ^ k * b = c ^ k
⊢ ∃ d_1, d ^ k = d_1 ^ k

pp: case inr
b c : ℤ
k : ℕ
hk : Odd k
d : ℤ
hab : IsCoprime ((-d) ^ k) b
h : (-d) ^ k * b = c ^ k
⊢ ∃ d_1, (-d) ^ k = d_1 ^ k

Tactic:
<;>

Goal state after:
case inl
b c : ℤ
k : ℕ
hk : Odd k
d : ℤ
hab : IsCoprime (d ^ k) b
h : d ^ k * b = c ^ k
⊢ ∃ d_1, d ^ k = d_1 ^ k

case inr
b c : ℤ
k : ℕ
hk : Odd k
d : ℤ
hab : IsCoprime ((-d) ^ k) b
h : (-d) ^ k * b = c ^ k
⊢ ∃ d_1, (-d) ^ k = d_1 ^ k
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).roots = univ.val

Tactic:
rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
this : (X ^ q - X).roots.toFinset = univ
⊢ (X ^ q - X).roots.Nodup
Module: Mathlib.FieldTheory.Finite.Basic

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

pp: case succ.zero.succ
p a d : ℕ
hd : p * a = d
n✝ : ℕ
hk : n✝ + 1 ∈ range p
⊢ p ∣ (p ^ 0 * d) ^ (n✝ + 1) * ↑(p.choose (n✝ + 1 + 1))

Tactic:
<;>

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

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

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

pp: case succ.succ.succ
p a d n✝¹ : ℕ
hd : (1 + p * a) ^ p ^ (n✝¹ + 1) = p ^ (n✝¹ + 1) * d + 1
n✝ : ℕ
hk : n✝ + 1 ∈ range p
⊢ p ∣ (p ^ (n✝¹ + 1) * d) ^ (n✝ + 1) * ↑(p.choose (n✝ + 1 + 1))

Tactic:
<;>

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

case succ.succ.succ
p a d n✝¹ : ℕ
hd : (1 + p * a) ^ p ^ (n✝¹ + 1) = p ^ (n✝¹ + 1) * d + 1
n✝ : ℕ
hk : n✝ + 1 ∈ range p
⊢ p ∣ (p ^ (n✝¹ + 1) * d) ^ (n✝ + 1) * ↑(p.choose (n✝ + 1 + 1))
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: case h₀
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ ∀ b ∈ Finset.univ, b ≠ i → ((p b).mapQ q (f b) ⋯) (Pi.single i x b) = 0

pp: case h₁
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ i ∉ Finset.univ → ((p i).mapQ q (f i) ⋯) (Pi.single i x i) = 0

Tactic:
· rintro j - hj
    rw [Pi.single_eq_of_ne hj, map_zero]

Goal state after:
case h₁
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ i ∉ Finset.univ → ((p i).mapQ q (f i) ⋯) (Pi.single i x i) = 0