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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ (MvPolynomial.map ↑f) q = 0

Tactic:
H q (hg (by rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom])),

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ (MvPolynomial.map ↑f) 0 = 0
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case inl
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : ((expand F (q ^ s)) g').Separable
h : IsUnit g'
⊢ ((expand F (q ^ s)) g').natDegree = g'.natDegree

pp: case inr
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
hm : m ≤ m + 0
hg : ((expand F (q ^ 0)) g').Separable
⊢ ((expand F (q ^ 0)) g').natDegree = g'.natDegree

Tactic:
· rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]

Goal state after:
case inr
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
hm : m ≤ m + 0
hg : ((expand F (q ^ 0)) g').Separable
⊢ ((expand F (q ^ 0)) g').natDegree = g'.natDegree
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m)) g = f
g' : F[X] := Classical.choose hf
hg' : (Classical.choose hf).Separable
m' : ℕ
hm' : (expand F (q ^ m')) (Classical.choose hf) = f
this : Fact (Nat.Prime q)
⊢ g.natDegree = hf.degree

Tactic:
refine contraction_degree_eq_or_insep q g g' m m' ?_ hg hg'

Goal state after:
case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m)) g = f
g' : F[X] := Classical.choose hf
hg' : (Classical.choose hf).Separable
m' : ℕ
hm' : (expand F (q ^ m')) (Classical.choose hf) = f
this : Fact (Nat.Prime q)
⊢ (expand F (q ^ m)) g = (expand F (q ^ m')) g'
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
hc : IsCoprime f g
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
⊢ False

Tactic:
obtain ⟨u, v, hfg⟩ := hc

Goal state after:
case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
u v : F[X]
hfg : u * f + v * g = 1
⊢ False
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ sepDegree F F = 1

Tactic:
by
  rw [sepDegree, Subsingleton.elim (separableClosure F F) ⊥, IntermediateField.rank_bot]

Goal state after:
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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
⊢ Nat.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Nat.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯

Tactic:
have h1 : p ≠ 0 := fun hp => by
    rw [hp, Polynomial.aroots_zero] at hx
    exact Multiset.notMem_zero x hx

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
⊢ Nat.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Nat.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree

Tactic:
rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
    ← Fintype.card_coe]

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ Fintype.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) } =
    Fintype.card ↥((minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯)).toFinset
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : SeparatelyContinuousMul G
U : OpenSubgroup G
⊢ IsClosed[inst✝¹] ↑U

Tactic:
have := QuotientGroup.discreteTopology U.isOpen
  exact QuotientGroup.t1Space_iff.mp inferInstance

Goal state after:
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
⊢ ∃ T ∈ 𝓝 1, W * T ⊆ W

Tactic:
apply WClopen.isClosed.isCompact.induction_on (p := fun S ↦ ∃ T ∈ 𝓝 (1 : G), S * T ⊆ W)
    ⟨Set.univ, by simp only [univ_mem, empty_mul, empty_subset, and_self]⟩
    (fun _ _ huv ⟨T, hT, mem⟩ ↦ ⟨T, hT, (mul_subset_mul_right huv).trans mem⟩)
    fun U V ⟨T₁, hT₁, mem1⟩ ⟨T₂, hT₂, mem2⟩ ↦ ⟨T₁ ∩ T₂, inter_mem hT₁ hT₂, by
      rw [union_mul]
      exact union_subset (mul_subset_mul_left inter_subset_left |>.trans mem1)
        (mul_subset_mul_left inter_subset_right |>.trans mem2) ⟩

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
⊢ ∀ x ∈ W, ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
⊢ finSepDegree F ↥⊥ ∣ finrank F ↥⊥

Tactic:
finSepDegree_bot,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
⊢ 1 ∣ finrank F ↥⊥
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
⊢ finSepDegree F ↥⊥ = finrank F ↥⊥

Tactic:
finSepDegree_bot,

Goal state after:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
⊢ 1 = finrank F ↥⊥
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✝ : Normal K L
s : Set Gal(L/K)
⊢ s ∈ 𝓝 1 ↔ ∃ E, FiniteDimensional K ↥E ∧ Normal K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
by
  rw [krullTopology_mem_nhds_one_iff]
  refine ⟨fun ⟨E, _, hE⟩ ↦ ?_, fun ⟨E, hE⟩ ↦ ⟨E, hE.1, hE.2.2⟩⟩
  use (IntermediateField.normalClosure K E L)
  simp only [normalClosure.is_finiteDimensional K E L, normalClosure.normal K E L, true_and]
  exact le_trans (E.fixingSubgroup_antitone E.le_normalClosure) hE

Goal state after:
Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup

Goal state before:
pp: G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : SeparatelyContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
⊢ IsOpen ↑H

Tactic:
rw [← QuotientGroup.t1Space_iff] at h

Goal state after:
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : SeparatelyContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : T1Space (G ⧸ H)
⊢ IsOpen ↑H
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
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)

Tactic:
let L := FractionRing S

Goal state after:
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
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
inst✝¹ : Algebra K S
inst✝ : IsScalarTower R K S
s : S
hs : IsIntegral R s
L : Type u_2 := FractionRing S
⊢ minpoly K s = map (algebraMap R K) (minpoly R s)
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
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
⊢ minpoly R s ∣ p

Tactic:
let L := FractionRing S

Goal state after:
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
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly R s ∣ p
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
⊢ minpoly R (r • s) = (minpoly R s).scaleRoots r

Tactic:
let L := FractionRing S

Goal state after:
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
⊢ minpoly R (r • s) = (minpoly R s).scaleRoots r
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: case intro.intro
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
this✝ : DecidableEq ι
this : DecidableEq κ
val✝¹ : Fintype ι
val✝ : Fintype κ
⊢ ∑ i, ((leftMulMatrix b) (∑ i, ((leftMulMatrix c) x).diag i)).diag i =
    ∑ x_1, ∑ y, ((leftMulMatrix (b.smulTower c)) x).diag (x_1, y)

Tactic:
refine Finset.sum_congr rfl fun i _ ↦ ?_

Goal state after:
case intro.intro
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
this✝ : DecidableEq ι
this : DecidableEq κ
val✝¹ : Fintype ι
val✝ : Fintype κ
i : ι
x✝ : i ∈ Finset.univ
⊢ ((leftMulMatrix b) (∑ i, ((leftMulMatrix c) x).diag i)).diag i = ∑ y, ((leftMulMatrix (b.smulTower c)) x).diag (i, y)
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: 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✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : IsTorsionFree A L
this✝¹ : Free A C
this✝ : IsNoetherian A C
this : IsLocalization (algebraMapSubmonoid C A⁰) L
⊢ finrank A C = finrank K L

Tactic:
let b := Basis.localizationLocalization K A⁰ L (Module.Free.chooseBasis A C)

Goal state after:
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✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : IsTorsionFree A L
this✝¹ : Free A C
this✝ : IsNoetherian A C
this : IsLocalization (algebraMapSubmonoid C A⁰) L
b : Basis (Free.ChooseBasisIndex A C) K L := Basis.localizationLocalization K A⁰ L (Free.chooseBasis A C)
⊢ finrank A C = finrank K L
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: 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 : Ideal A
Q : Ideal B
hP : Q.LiesOver P
hQ : Q.IsPrime
R : Ideal B
h : R ∈ P.primesOver B
this : R.IsPrime
⊢ R ∈ MulAction.orbit G Q

Tactic:
obtain ⟨g, hg⟩ := exists_smul_of_under_eq A B G Q R (hP.over.symm.trans h.2.over)

Goal state after:
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 : Ideal A
Q : Ideal B
hP : Q.LiesOver P
hQ : Q.IsPrime
R : Ideal B
h : R ∈ P.primesOver B
this : R.IsPrime
g : G
hg : R = g • Q
⊢ R ∈ MulAction.orbit G Q
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
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)

Tactic:
let P := Finset.inf {g : G | g • Q ≠ Q} (fun g ↦ g • Q)

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
⊢ ∃ a b,
    (∀ (g : G), g • a = a) ∧
      a ∉ Q ∧ ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
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 : b ∉ Q
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 b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ a - eval b r ∈ g • Q

Tactic:
← Ideal.neg_mem_iff,

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 : b ∉ Q
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 b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ -(a - eval b r) ∈ g • Q
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case neg
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
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
g : G
hb : (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
hg : ¬g • Q = Q
⊢ (algebraMap B (B ⧸ Q)) 0 * (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) 0

Tactic:
rw [map_zero, zero_mul]

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
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i : Fin pb.dim
⊢ ∀ (j : Fin pb.dim),
    ((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)))) (pb.basis j) =
      if j = i then 1 else 0

Tactic:
j

Goal state after:
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
pb : PowerBasis K L
i j : Fin pb.dim
⊢ ((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)))) (pb.basis j) =
    if j = i then 1 else 0
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case inl
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2 ∨ p ∣ m.natAbs

pp: case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
· apply Or.intro_left
    exact le_antisymm (Nat.le_of_dvd zero_lt_two hp2) (Nat.Prime.two_le hp)

Goal state after:
case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p = 2 ∨ p ∣ m.natAbs
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✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
b : B ⧸ Q
hx : ∀ (g : ↥(MulAction.stabilizer G Q)), ((Ideal.Quotient.stabilizerHom Q P G) g) b = b
⊢ f ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b

Tactic:
by
  cases nonempty_fintype G
  obtain ⟨b₀, rfl⟩ := Ideal.Quotient.mk_surjective b
  rw [← Ideal.Quotient.algebraMap_eq]
  obtain ⟨a, b, ha1, ha2, hb⟩ := fixed_of_fixed1_aux2 G Q b₀ (fun g hg ↦ hx ⟨g, hg⟩)
  obtain ⟨M, key⟩ := (mem_lifts _).mp (Algebra.IsInvariant.charpoly_mem_lifts A B G b)
  replace key := congrArg (map (algebraMap B (B ⧸ Q))) key
  rw [map_map, ← algebraMap_eq, algebraMap_eq A (A ⧸ P) (B ⧸ Q),
      ← map_map, MulSemiringAction.charpoly, Polynomial.map_prod] at key
  have key₀ : ∀ g : G, (X - C (g • b)).map (algebraMap B (B ⧸ Q)) =
      if g • Q = Q then X - C (algebraMap B (B ⧸ Q) (a * b₀)) else X := by
    intro g
    rw [Polynomial.map_sub, map_X, map_C, hb]
    split_ifs
    · rfl
    · rw [map_zero, map_zero, sub_zero]
  simp only [key₀, Finset.prod_ite, Finset.prod_const] at key
  replace key := congrArg (map (algebraMap (B ⧸ Q) L)) key
  rw [map_map, ← algebraMap_eq, algebraMap_eq (A ⧸ P) K L,
      ← map_map, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_pow, Polynomial.map_sub,
      map_X, map_C] at key
  replace key := fixed_of_fixed1_aux3 key f (Finset.card_ne_zero_of_mem
    (Finset.mem_filter.mpr ⟨Finset.mem_univ 1, one_smul G Q⟩))
  simp only [map_mul] at key
  obtain ⟨a, rfl⟩ := Algebra.IsInvariant.isInvariant (A := A) a ha1
  rwa [← algebraMap_apply A B (B ⧸ Q), algebraMap_apply A (A ⧸ P) (B ⧸ Q),
      ← algebraMap_apply, algebraMap_apply (A ⧸ P) K L, f.commutes, mul_right_inj'] at key
  rwa [← algebraMap_apply, algebraMap_apply (A ⧸ P) (B ⧸ Q) L,
      ← algebraMap_apply A (A ⧸ P) (B ⧸ Q), algebraMap_apply A B (B ⧸ Q),
      Ne, algebraMap_eq_zero_iff, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
⊢ (expand (ZMod p) p) f = f ^ p

Tactic:
have h := FiniteField.expand_card f; rwa [ZMod.card p] at h

Goal state after:
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
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)

Tactic:
let b := Module.Free.chooseBasis ℤ M

Goal state after:
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
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Goal state before:
pp: M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank ℤ ↥N = finrank ℤ M
⊢ Finite (M ⧸ N)

Tactic:
let b := Module.Free.chooseBasis ℤ M

Goal state after:
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Free ℤ M
inst✝ : Module.Finite ℤ M
N : Submodule ℤ M
h : finrank ℤ ↥N = finrank ℤ M
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
⊢ Finite (M ⧸ N)