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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (M.mapEquiv f).Dep D ↔ M.Dep (⇑f.symm '' D)

Tactic:
rw [mapEquiv_eq_map, map_dep_iff]

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) ↔ M.Dep (⇑f.symm '' D)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E ↔ ∀ C ⊆ I, ¬M.IsCircuit C

Tactic:
and_iff_left hI

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ (∀ C ⊆ I, ¬M.IsCircuit C) ↔ ∀ C ⊆ I, ¬M.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
⊢ M.IsBasis I X

Tactic:
by
  obtain ⟨J, hJ⟩ := M.exists_isBasis (I ∩ M.E)
  have hIJ := hJ.subset.trans inter_subset_left
  rw [← closure_inter_ground] at hXI
  replace hXI := hXI.trans <| M.closure_subset_closure_of_subset_closure hJ.subset_closure
  have hJX := hJ.indep.isBasis_of_subset_of_subset_closure (hIJ.trans hIX) hXI
  rw [← hJX.encard_eq_eRk] at hI
  rwa [← Finite.eq_of_subset_of_encard_le (hX.finite_of_isBasis hJX) hIJ hI]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.cRk (X ∩ Y) + M.cRk (IX ∪ IY) ≤ M.cRk X + M.cRk Y

Tactic:
← hIi.cardinalMk_eq_cRk,

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ #↑Ii + M.cRk (IX ∪ IY) ≤ M.cRk X + M.cRk Y
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
⊢ AlgebraicIndependent R fun i ↦ x ↑i

Tactic:
suffices AlgebraicIndependent R fun i : ↥(t ∩ s ∪ t \ s) ↦ x i from
    this.comp (Equiv.setCongr (t.inter_union_sdiff s).symm) (Equiv.injective _)

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
⊢ AlgebraicIndependent R fun i ↦ x ↑i
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
E X : Set α
⊢ (loopyOn E).closure X = E

Tactic:
simp [loopyOn, restrict_closure_eq']

Goal state after:
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
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
⊢ trdeg R A' ≤ trdeg R A

Tactic:
by
  rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id]; exact lift_trdeg_le_of_surjective f hf

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

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (IsAlgebraic (↥(adjoin R B)) x ∧ ∀ x ∈ B, IsAlgebraic (↥(adjoin R B)) x) ↔ IsAlgebraic (↥(adjoin R B)) x

Tactic:
exact fun _ ↦ and_iff_left fun x hx ↦ isAlgebraic_algebraMap (⟨x, subset_adjoin hx⟩ : adjoin R B)

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

Goal state before:
pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
his : v i ∈ v '' s
k : ι
hkj : k ∉ {j}
hks : k ∈ s
⊢ v k ∈ v '' s \ {v j}

Tactic:
exact ⟨⟨k, hks, rfl⟩, inj.ne hks hj hkj⟩

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
inst✝¹ : IsGalois F E
inst✝ : Finite Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional F ↥K
h₂ : Nat.card Gal(E/F) < finrank F ↥K
⊢ False

Tactic:
let K' := normalClosure F K E

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : IsGalois F E
inst✝ : Finite Gal(E/F)
H : ¬FiniteDimensional F E
K : IntermediateField F E
h₁ : FiniteDimensional F ↥K
h₂ : Nat.card Gal(E/F) < finrank F ↥K
K' : IntermediateField F E := normalClosure F (↥K) E
⊢ False
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (Polynomial.map (algebraMap F E) (minpoly F x)).coeff 0 = (X.coeff 0 - (C x).coeff 0) ^ q ^ n
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
coeff_map,

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = (X.coeff 0 - (C x).coeff 0) ^ q ^ n
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ (minpoly F α).natSepDegree ∣ (minpoly F α).natDegree

Tactic:
exact (minpoly.irreducible halg.isIntegral).natSepDegree_dvd_natDegree

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

Goal state before:
pp: case left
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (T.rootSet ↥K) = ⊤
T' : (↥L)[X] := ⋯
⊢ (Polynomial.map (algebraMap (↥L) E) T').Splits

pp: case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (T.rootSet ↥K) = ⊤
T' : (↥L)[X] := ⋯
⊢ adjoin (↥L) (T'.rootSet E) = ⊤

Tactic:
· rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
    exact Polynomial.Splits.of_algHom hT₂.1 (IsScalarTower.toAlgHom _ _ _)

Goal state after:
case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (T.rootSet ↥K) = ⊤
T' : (↥L)[X] := ⋯
⊢ adjoin (↥L) (T'.rootSet E) = ⊤
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable (↥F⟮x⟯) y
⊢ Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)

Tactic:
rw [← isSeparable_adjoin_simple_iff_isSeparable] at hx hy

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y : E
hx : Algebra.IsSeparable F ↥F⟮x⟯
hy : Algebra.IsSeparable ↥F⟮x⟯ ↥(↥F⟮x⟯)⟮y⟯
⊢ Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
p : R[X]
hp : p.Monic
he :
  eval₂ ((algebraMap K g.SplittingField).comp (algebraMap R K)) ((map (algebraMap K g.SplittingField) g).coeff n) p = 0
⊢ eval₂ (algebraMap R K) (g.coeff n) p = 0

Tactic:
coeff_map,

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
p : R[X]
hp : p.Monic
he : eval₂ ((algebraMap K g.SplittingField).comp (algebraMap R K)) ((algebraMap K g.SplittingField) (g.coeff n)) p = 0
⊢ eval₂ (algebraMap R K) (g.coeff n) p = 0
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: 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
j : ℕ
hj : j ∈ Set.Iio i
⊢ (fun x_1 ↦ x ^ x_1 * x) j ∈ (fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1)

Tactic:
Set.mem_Iio

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
j : ℕ
hj : j < i
⊢ (fun x_1 ↦ x ^ x_1 * x) j ∈ (fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1)
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: 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))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)

Tactic:
refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span hx ?_)

Goal state after:
case a.ind.refine_1
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))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i) ≤ Submodule.span R (Set.range (minpolyDiv R x).coeff)

case a.ind.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
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))
hi' : i ∈ Set.Iio (minpoly R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ i ≤ (minpolyDiv R x).natDegree
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case a.ind.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
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))
hi' : i < (minpolyDiv R x).natDegree + 1
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ i ≤ (minpolyDiv R x).natDegree

Tactic:
Nat.lt_succ_iff

Goal state after:
case a.ind.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
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))
hi' : i ≤ (minpolyDiv R x).natDegree
this : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) ∈ Submodule.span R (Set.range (minpolyDiv R x).coeff)
⊢ i ≤ (minpolyDiv R x).natDegree
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
h : n = 0
⊢ False

Tactic:
by
    rw [h, Nat.cast_zero] at hn
    exact hn.out 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 ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ∈ R⁰
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
⊢ IsUnit a ∨ IsUnit b

Tactic:
mem_nonZeroDivisors_iff_ne_zero

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
⊢ IsUnit a ∨ IsUnit b
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
⊢ ∀ (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

Tactic:
intro F

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 : Type v
⊢ ∀ (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.RingTheory.Trace.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
i✝ j✝ : Fin h.dim
⊢ (LinearMap.BilinForm.toMatrix h.basis) (traceForm R S) i✝ j✝ = of (fun i j ↦ (trace R S) (h.gen ^ (↑i + ↑j))) i✝ j✝

Tactic:
traceForm_toMatrix,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
i✝ j✝ : Fin h.dim
⊢ (trace R S) (h.basis i✝ * h.basis j✝) = of (fun i j ↦ (trace R S) (h.gen ^ (↑i + ↑j))) i✝ j✝
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
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
x : B
h : ∀ (g : G), g • x = x
a : A
hb : (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) x
⊢ (algebraMap A B) a = x

Tactic:
rwa [hc, IsFractionRing.coe_inj] at hb

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

Goal state before:
pp: A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))

Tactic:
← Algebra.trace_eq_of_ringEquiv e₁ he,

Goal state after:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
this : Algebra A₁ B₂ := ((↑e₂).comp (algebraMap A₁ B₁)).toAlgebra
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ (trace A₁ B₁) x = e₁.symm (e₁ ((trace A₁ B₂) (e₂ x)))
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
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : IsSeparable K x
⊢ (trace K L) x = 0 x

pp: case neg
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
⊢ (trace K L) x = 0 x

Tactic:
· lift x to separableClosure K L using hx
    rw [← IntermediateField.algebraMap_apply, ← trace_trace (S := separableClosure K L),
      trace_algebraMap]
    obtain ⟨n, hn⟩ := IsPurelyInseparable.finrank_eq_pow (separableClosure K L) L p
    cases n with
    | zero =>
      rw [pow_zero, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn
      cases H hn
    | succ n =>
      cases hp with
      | zero =>
        rw [one_pow, IntermediateField.finrank_eq_one_iff_eq_top, separableClosure.eq_top_iff] at hn
        cases H hn
      | prime hprime =>
        rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]

Goal state after:
case neg
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
⊢ (trace K L) x = 0 x
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 ι
b : Basis ι A B
z : B
i : ι
| ∑ x, b.equivFun z x • (b i * b x)

Tactic:
congr
    rfl
    ext
    rw [← mul_smul_comm]

Goal state after:
case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i x✝ : ι
| b i * b.equivFun z x✝ • b x✝
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
hF : FixedPoints.intermediateField ↥H = F
⊢ IsGaloisGroup (↥H) (↥F) L

Tactic:
rw [eq_comm] at hF
  convert! IsGaloisGroup.subgroup G K L H

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
tfae_1_to_3 : Algebra.IsSeparable K L → (traceForm K L).Nondegenerate
H₁ : (traceForm K L).Nondegenerate
H₂ : Algebra.trace K L = 0
⊢ traceForm K L = 0

Tactic:
by ext; simp [H₂]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i

Tactic:
obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
  rw [← Nat.card_eq_fintype_card, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx,
    orderOf_dvd_iff_pow_eq_one]
  constructor
  · intro h; apply h
  · intro h y
    simp_rw [← mem_powers_iff_mem_zpowers] at hx
    rcases hx y with ⟨j, rfl⟩
    rw [← pow_mul, mul_comm, pow_mul, h, one_pow]

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

Goal state before:
pp: K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : CommRing R
inst✝ : Algebra K R
x✝¹ x✝ : R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    obtain ⟨p, _, _, hp, card_eq⟩ := card' K
    nontriviality R
    have : CharP R p := charP_of_injective_algebraMap' K p
    have : ExpChar R p := .prime hp
    simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, powMonoidHom_apply, card_eq]
    exact add_pow_expChar_pow ..

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : 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)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ (piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) ((quotientPiLift p (fun i ↦ (p i).mkQ) ⋯) (Quotient.mk x')) =
    Quotient.mk x'

Tactic:
quotientPiLift_mk p,

Goal state after:
ι : 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)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ ((piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) fun i ↦ (p i).mkQ (x' i)) = Quotient.mk x'