mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
h : M.eRk I = I.encard
⊢ M.Indep I

Tactic:
obtain hfin | hinf := I.finite_or_infinite

Goal state after:
case inl
α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
h : M.eRk I = I.encard
hfin : I.Finite
⊢ M.Indep I

case inr
α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
h : M.eRk I = I.encard
hinf : I.Infinite
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
x✝ : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X ∪ K)
hC : M.IsCircuit C
heC : e ∈ C
⊢ e ∈ M.closure X

Tactic:
← singleton_union,

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
x✝ : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ {e} ∪ (M.closure X ∪ K)
hC : M.IsCircuit C
heC : e ∈ C
⊢ e ∈ M.closure X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
X : Set α
⊢ M.closure (insert e (M.closure X)) = M.closure (insert e X)

Tactic:
← singleton_union,

Goal state after:
α : Type u_2
M : Matroid α
e : α
X : Set α
⊢ M.closure ({e} ∪ M.closure X) = M.closure ({e} ∪ X)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
obtain rfl | hne := eq_or_ne e f

Goal state after:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.closure (I \ {e}) ∨ e ∈ I

case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case pos
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Finite
⊢ ↑(B \ B').ncard ≤ ↑(B' \ B).ncard

pp: case pos
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Finite
⊢ (B \ B').Finite

Tactic:
hB.ncard_sdiff_comm hB'

Goal state after:
case pos
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Finite
⊢ ↑(B' \ B).ncard ≤ ↑(B' \ B).ncard

case pos
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : (B' \ B).Finite
⊢ (B \ B').Finite
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case inl
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hIs : X ⊆ insert f (J \ {e})
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ X ⊆ J

Tactic:
← singleton_union,

Goal state after:
case inl
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hIs : X ⊆ {f} ∪ J \ {e}
hX' : X ∈ Js
hfX : f ∉ X
hd : M.Dep (insert e X)
⊢ X ⊆ J
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
⊢ f ∈ M.fundCircuit e B

Tactic:
obtain rfl | hne := eq_or_ne e f

Goal state after:
case inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e : α
he : e ∈ M.fundCocircuit e B
⊢ e ∈ M.fundCircuit e B

case inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
⊢ f ∈ M.fundCircuit e B
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I J B B' X Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
⊢ (M.map f hf).InvariantCardinalRank

Tactic:
by
  refine ⟨fun I J X hI hJ ↦ ?_⟩
  obtain ⟨I, X, hIX, rfl, rfl⟩ := map_isBasis_iff'.1 hI
  obtain ⟨J, X', hJX, rfl, h'⟩ := map_isBasis_iff'.1 hJ
  obtain rfl : X = X' := by
    rwa [InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground] at h'
  have hcard := hIX.cardinalMk_sdiff_comm hJX
  rwa [← lift_inj.{u, v},
    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hIX.indep.sdiff _).subset_ground)),
    ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hJX.indep.sdiff _).subset_ground)),
    lift_inj, (hf.mono hIX.indep.subset_ground).image_sdiff,
    (hf.mono hJX.indep.subset_ground).image_sdiff, inter_comm,
    hf.image_inter hJX.indep.subset_ground hIX.indep.subset_ground,
    sdiff_inter_self_eq_sdiff, sdiff_self_inter] at hcard

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure (X ∩ f '' M.E) = f '' M.closure I

Tactic:
← aux hI.indep,

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure (X ∩ f '' M.E) = (M.map f hf).closure (f '' I)
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ ∀ (i : ↑s), AlgebraicIndependent R Subtype.val

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
⊢ AlgebraicIndepOn R _root_.id w → range x ⊆ w → range x = w

Tactic:
i'

Goal state after:
case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndepOn R _root_.id w
⊢ range x ⊆ w → range x = w
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f g : F[X]
q : ℕ
inst✝ : ExpChar F q
h1 : g.Separable
m : ℕ
h2 : (expand F (q ^ m)) g = f
⊢ f.natSepDegree = g.natDegree

Tactic:
rw [← h2, natSepDegree_expand, h1.natSepDegree_eq_natDegree]

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
h1 : p ≠ 0
⊢ minpoly K x ∣ Polynomial.map (algebraMap F K) p

Tactic:
apply minpoly.dvd

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
⊢ (Polynomial.aeval x) (Polynomial.map (algebraMap F K) p) = 0
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case succ.refine_2
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
apply SetLike.le_def.mp ?_
        (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi))
          (Submodule.mem_span_singleton_self x))

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i) * (R ∙ x) ≤
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
⊢ i ∈ Set.Iio (minpoly R x).natDegree →
    i ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))

Tactic:
induction i using Nat.strongRecOn with | ind i hi => ?_

Goal state after:
case a.ind
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (minpoly R x).natDegree →
      m ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
⊢ i ∈ Set.Iio (minpoly R x).natDegree →
    i ∈ (fun x_1 ↦ x ^ x_1) ⁻¹' ↑(Submodule.span R (Set.range (minpolyDiv R x).coeff))
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
⊢ g * map (algebraMap R K) f ∈ lifts (algebraMap R K) ↔ g ∈ lifts (algebraMap R K)

Tactic:
hf.mul_map_mem_lifts_iff

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
f : R[X]
hf : f.IsPrimitive
g : K[X]
⊢ g ∈ lifts (algebraMap R K) ↔ g ∈ lifts (algebraMap R K)
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
b : B
h : ∀ (g : G), g • b = b
a : A
ha : (algebraMap A B) a = b
⊢ (algebraMap A' B) (e a) = b

Tactic:
rw [he, ha]

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
a : A
⊢ (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)

Tactic:
simp_rw [← IsScalarTower.algebraMap_apply]

Goal state after:
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✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
⊢ ∃ g ∈ ⊤, Q ≤ g • P

Tactic:
rw [← Ideal.subset_union_prime 1 1 (fun _ _ _ _ ↦ hP.smul _)]

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✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
⊢ ↑Q ⊆ ⋃ i ∈ ↑⊤, ↑(i • P)
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : ¬(algebraMap B (B ⧸ Q)) b = 0
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr : map (algebraMap B (B ⧸ Q)) r = q
hf : (algebraMap B (B ⧸ Q)) (eval b f) = (algebraMap B (B ⧸ Q)) 0
⊢ (algebraMap B (B ⧸ Q)) (eval b r) = 0

Tactic:
← Polynomial.eval₂_at_apply,

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : ¬(algebraMap B (B ⧸ Q)) b = 0
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr : map (algebraMap B (B ⧸ Q)) r = q
hf : eval₂ (algebraMap B (B ⧸ Q)) ((algebraMap B (B ⧸ Q)) b) f = (algebraMap B (B ⧸ Q)) 0
⊢ eval₂ (algebraMap B (B ⧸ Q)) ((algebraMap B (B ⧸ Q)) b) r = 0
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case refine_1
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
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
⊢ ¬q.coeff 0 = 0

Tactic:
← Polynomial.X_dvd_iff

Goal state after:
case refine_1
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
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
⊢ ¬X ∣ q
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case pos
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
hr' : ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q
h : G
hh : h⁻¹ • Q = Q
⊢ a - eval b r - h⁻¹ • a ∈ h⁻¹ • Q

Tactic:
rwa [ha, sub_sub_cancel_left, hh, Q.neg_mem_iff]

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

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis κ A B
⊢ traceMatrix A ⇑b = (LinearMap.BilinForm.toMatrix b) (traceForm A B)

Tactic:
ext (i j)

Goal state after:
κ : Type w
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis κ A B
i j : κ
⊢ traceMatrix A (⇑b) i j = (LinearMap.BilinForm.toMatrix b) (traceForm A B) i j
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
κ : Type w
E : Type z
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
b : κ → L
⊢ (traceMatrix K b).map ⇑(algebraMap K E) = embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ

Tactic:
ext (i j)

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
κ : Type w
E : Type z
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
b : κ → L
i j : κ
⊢ (traceMatrix K b).map (⇑(algebraMap K E)) i j = (embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ) i j
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - C x
⊢ Fintype.card (ZMod p) % 2 = 1

Tactic:
rw [ZMod.card, hp_odd]

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

Goal state before:
pp: x n : ℕ
h : x.Coprime n
⊢ x ^ φ n ≡ 1 [MOD n]

Tactic:
by
  rw [← ZMod.natCast_eq_natCast_iff]
  let x' : Units (ZMod n) := ZMod.unitOfCoprime _ h
  have := ZMod.pow_totient x'
  apply_fun ((fun (x : Units (ZMod n)) => (x : ZMod n)) : Units (ZMod n) → ZMod n) at this
  simpa only [Nat.succ_eq_add_one, Nat.cast_pow, Units.val_one, Nat.cast_one,
    coe_unitOfCoprime, Units.val_pow_eq_pow_val]

Goal state after:
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
⊢ i ∉ Finset.univ → ((p i).mapQ q (f i) ⋯) (Pi.single i x i) = 0

Tactic:
intros
    have := Finset.mem_univ i
    contradiction

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : Algebra A L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : MulSemiringAction G B
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hAB : Algebra.IsInvariant A B G
inst✝¹ : SMulCommClass G A B
inst✝ : Algebra.IsIntegral A B
x : L
h : ∀ (g : G), g • x = x
a : A
⊢ (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)

Tactic:
simp_rw [← IsScalarTower.algebraMap_apply]

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
pb : PowerBasis R S
⊢ ((leftMulMatrix pb.basis) pb.gen).det = (-1) ^ pb.dim * (minpoly R pb.gen).coeff 0

Tactic:
det_eq_sign_charpoly_coeff,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
pb : PowerBasis R S
⊢ (-1) ^ Fintype.card (Fin pb.dim) * ((leftMulMatrix pb.basis) pb.gen).charpoly.coeff 0 =
    (-1) ^ pb.dim * (minpoly R pb.gen).coeff 0
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ (norm R) x = 0 → x = 0

Tactic:
let decEq := Classical.decEq (Module.Free.ChooseBasisIndex R S)

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Free R S
inst✝ : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ (norm R) x = 0 → x = 0