mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑(cons a s ha)).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ Squarefree (f a * ∏ x ∈ s, f x)

Tactic:
squarefree_mul_iff

Goal state after:
case cons
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑(cons a s ha)).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ IsRelPrime (f a) (∏ x ∈ s, f x) ∧ Squarefree (f a) ∧ Squarefree (∏ x ∈ s, f x)
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this✝ : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
this : root g ^ p = (of g) a
⊢ a ^ (powerBasis ⋯).dim = a ^ g.natDegree

Tactic:
powerBasis_dim hg.ne_zero

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this✝ : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
this : root g ^ p = (of g) a
⊢ a ^ g.natDegree = a ^ g.natDegree
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : (Multiset.map (fun a ↦ X - C a) s).prod.Separable
⊢ s.Nodup

Tactic:
by
  rw [Multiset.nodup_iff_ne_cons_cons]
  rintro a t rfl
  refine not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs ?_)
  simpa only [Multiset.map_cons, Multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : p = 0
⊢ rootMultiplicity x p ≤ 1

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ rootMultiplicity x p ≤ 1
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ 0 = minpoly 𝕜 a

Tactic:
minpoly.eq_zero

Goal state after:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ 0 = 0

case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ ¬IsIntegral 𝕜 a
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case C
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S[X]
a : R
⊢ (algebraMap R (AdjoinRoot f)) a = (of f) ((algebraMap R S) a)

Tactic:
IsScalarTower.algebraMap_apply R S

Goal state after:
case C
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S[X]
a : R
⊢ (algebraMap S (AdjoinRoot f)) ((algebraMap R S) a) = (of f) ((algebraMap R S) a)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ (mk g) (∑ i_1, (monomial ↑i_1) (Pi.single i 1 i_1)) = root g ^ ↑i

Tactic:
rw [Finset.sum_eq_single i]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ (mk g) ((monomial ↑i) (Pi.single i 1 i)) = root g ^ ↑i

case h₀
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial ↑b) (Pi.single i 1 b) = 0

case h₁
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ i ∉ Finset.univ → (monomial ↑i) (Pi.single i 1 i) = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j : n
k : m
this : W.mkQ (e ↑(bW k)) = 0
⊢ (toMatrix b b) e (Sum.inr j) (Sum.inl k) = fromBlocks A B 0 D (Sum.inr j) (Sum.inl k)

Tactic:
simp [LinearMap.toMatrix_apply, b, this]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : (↑i !)⁻¹ * ↑(i.choose j) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹
⊢ i.choose j • (↑i !)⁻¹ • (a ^ j * b ^ (i - j)) = ↑(i.choose j) • (↑i !)⁻¹ • (a ^ j * b ^ (i - j))

Tactic:
norm_cast

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_3
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ (liftAlgHom q (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
          (1 ⊗ₜ[R] root p) ⋯).comp
      (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯) =
    AlgHom.id T (T ⊗[R] AdjoinRoot p)

Tactic:
ext : 3

Goal state after:
case refine_3.hAlg
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
x✝ : S
⊢ (((AlgHom.restrictScalars R
                ((liftAlgHom q
                      (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
                      (1 ⊗ₜ[R] root p) ⋯).comp
                  (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯))).comp
            includeRight).comp
        (ofAlgHom R p))
      x✝ =
    (((AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] AdjoinRoot p))).comp includeRight).comp (ofAlgHom R p)) x✝

case refine_3.hRoot
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ ((AlgHom.restrictScalars R
            ((liftAlgHom q
                  (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
                  (1 ⊗ₜ[R] root p) ⋯).comp
              (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯))).comp
        includeRight)
      (root p) =
    ((AlgHom.restrictScalars R (AlgHom.id T (T ⊗[R] AdjoinRoot p))).comp includeRight) (root p)
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent ↑D
_i : NonUnitalNonAssocRing L := LieRing.toNonUnitalNonAssocRing L
⊢ ∀ {x y : L}, (IsNilpotent.exp ↑D).toFun ⁅x, y⁆ = ⁅(IsNilpotent.exp ↑D).toFun x, (IsNilpotent.exp ↑D).toFun y⁆

Tactic:
have : SMulCommClass R L L := LieAlgebra.smulCommClass R L

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent ↑D
_i : NonUnitalNonAssocRing L := LieRing.toNonUnitalNonAssocRing L
this : SMulCommClass R L L
⊢ ∀ {x y : L}, (IsNilpotent.exp ↑D).toFun ⁅x, y⁆ = ⁅(IsNilpotent.exp ↑D).toFun x, (IsNilpotent.exp ↑D).toFun y⁆
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (ad R L).ker = LieAlgebra.center R L

Tactic:
by
  ext x
  rw [← LieAlgebra.self_module_ker_eq_center, LieHom.mem_ker, LieModule.mem_ker]
  simp [DFunLike.ext_iff]

Goal state after:
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ (hasBracketAux x) ((hasBracketAux y) t) = (hasBracketAux ⁅x, y⁆) t + (hasBracketAux y) ((hasBracketAux x) t)

Tactic:
suffices (hasBracketAux x).comp (hasBracketAux y) =
        hasBracketAux ⁅x, y⁆ + (hasBracketAux y).comp (hasBracketAux x) by
      rw [← LinearMap.comp_apply, this]; rfl
    ext m n
    simp only [hasBracketAux, AlgebraTensorModule.curry_apply, curry_apply, sub_tmul, tmul_sub,
      LinearMap.coe_restrictScalars, Function.comp_apply, LinearMap.coe_comp,
      LinearMap.rTensor_tmul, LieHom.map_lie, toEnd_apply_apply, LinearMap.add_apply,
      map_add, LieHom.lie_apply, Module.End.lie_apply, LinearMap.lTensor_tmul]
    abel

Goal state after:
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ IsSolvable L ↔ ∃ k, derivedSeries R L k = ⊥

Tactic:
simp [isSolvable_iff_int, SetLike.ext'_iff, LieIdeal.coe_derivedSeries_eq_int]

Goal state after:
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: case succ.refine_2
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ ↑⁅I, ⊤.lcs M (i + l)⁆ ≤ ↑⁅I, I.lcs M j⁆

Tactic:
norm_cast

Goal state after:
case succ.refine_2
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ ⁅I, ⊤.lcs M (i + l)⁆ ≤ ⁅I, I.lcs M j⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
y : L ⧸ f.ker
z✝ : L
⊢ (↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝, y⁆ =
    ⁅(↑f).quotKerEquivRange (Submodule.Quotient.mk z✝), (↑f).quotKerEquivRange y⁆

Tactic:
induction y using Submodule.Quotient.induction_on

Goal state after:
case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ (↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆ =
    ⁅(↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹), (↑f).quotKerEquivRange (Submodule.Quotient.mk z✝)⁆
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁴ : LieRing L₂
inst✝³ : LieAlgebra R L₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
⊢ ⇑g '' {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x} ⊆ ↑↑(lowerCentralSeries R L₂ M₂ (k + 1))

Tactic:
rintro m₂ ⟨m, ⟨x, n, m_n, ⟨h₁, h₂⟩⟩, rfl⟩

Goal state after:
case succ
R : Type u
L : Type v
M : Type w
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁴ : LieRing L₂
inst✝³ : LieAlgebra R L₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
m : M
x : L
n : x ∈ ⊤
m_n : M
h₁ : m_n ∈ lowerCentralSeries R L M k
h₂ : ⁅x, m_n⁆ = m
⊢ g m ∈ ↑↑(lowerCentralSeries R L₂ M₂ (k + 1))
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
⊢ ∀ i ∈ s, l i ∈ subfield G F

Tactic:
intro i

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
⊢ i ∈ s → l i ∈ subfield G F
Module: Mathlib.RingTheory.Adjoin.Singleton

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : CommSemiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
x : ↥A[b]
⊢ ↑((AlgHom.restrictScalars A (ofId B C)).comp A[b].val) x ∈ A[(algebraMap B C) b]

Tactic:
by induction x using adjoin_singleton_induction with
      | f p => aesop (add norm [adjoin_singleton_eq_range_aeval, aeval_algebraMap_apply])

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Singleton

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : CommSemiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra B C
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A B C
b : B
inst✝ : FaithfulSMul B C
y : ↥A[(algebraMap B C) b]
⊢ ∃! a, (adjoinAlgebraMap b) a = y

Tactic:
induction y using Algebra.adjoin_singleton_induction with | f p =>
  use ⟨p.aeval b, by simp⟩
  aesop (add norm [Polynomial.aeval_algebraMap_apply, Subtype.ext_iff])

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (prodXSubSMul G F x).Separable

Tactic:
exact Polynomial.separable_prod_X_sub_C_iff.2 (injective_ofQuotientStabilizer G x)

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = Subring.closure (Set.range ⇑(algebraMap F L) ∪ s)

Tactic:
rw [← Algebra.adjoin_eq_ring_closure, ← hs]

Goal state after:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = g.range.toSubring
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ ⊤ ≤ Subalgebra.restrictScalars F (Algebra.adjoin K ↑(Polynomial.map (algebraMap F L) f).roots.toFinset)

Tactic:
← adjoin_rootSet L f,

Goal state after:
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Algebra.adjoin F (f.rootSet L) ≤
    Subalgebra.restrictScalars F (Algebra.adjoin K ↑(Polynomial.map (algebraMap F L) f).roots.toFinset)
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : f.Splits
⊢ ⊤ ≤ ⊥

Tactic:
← adjoin_rootSet L f,

Goal state after:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : f.Splits
⊢ Algebra.adjoin K (f.rootSet L) ≤ ⊥
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α x : E
⊢ x ∈ F⟮α⟯ ↔ ∃ r s, x = (aeval α) r / (aeval α) s

Tactic:
simp only [mem_adjoin_iff_div, Algebra.adjoin_singleton_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case pos
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional K ↥E1
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2

Tactic:
have := E1.toSubalgebra.finrank_sup_le_of_free E2.toSubalgebra

Goal state after:
case pos
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional K ↥E1
this : finrank K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ finrank K ↥E1.toSubalgebra * finrank K ↥E2.toSubalgebra
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : Cardinal.aleph0 ≤ Module.rank K ↥E1
this :
  Module.rank K ↥(Subalgebra.toSubmodule E1.toSubalgebra) ≤
    Module.rank K ↥(Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra)
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2

Tactic:
rw [show finrank K E1 = 0 from Cardinal.toNat_apply_of_aleph0_le h,
    show finrank K ↥(E1 ⊔ E2) = 0 from Cardinal.toNat_apply_of_aleph0_le (h.trans this), zero_mul]

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
σ : Λ
⊢ ϕ.carrier < (L σ).carrier

Tactic:
simpa only [L, restrictScalars_adjoin_eq_sup, left_lt_sup, adjoin_simple_le_iff]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (i j : ι) (φ : R), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
⊢ iSupIndep fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)

Tactic:
replace h (l : ι) (χ : ι → R) :
      MapsTo (f l) (⨅ i, (f i).maxGenEigenspace (χ i)) (⨅ i, (f i).maxGenEigenspace (χ i)) := by
    intro x hx
    simp only [iInf_eq_iInter, mem_iInter, SetLike.mem_coe] at hx ⊢
    exact fun i ↦ h l i (χ i) (hx i)

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
⊢ iSupIndep fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : minpoly K x = minpoly K y
⊢ (algEquiv hx h_mp) (AdjoinSimple.gen K x) = AdjoinSimple.gen K y

Tactic:
have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩
  rw [algEquiv, trans_apply, ← adjoinRootEquivAdjoin_apply_root K hx.isIntegral,
    symm_apply_apply, trans_apply, AdjoinRoot.algEquivOfEq_root,
    adjoinRootEquivAdjoin_apply_root K hy.isIntegral]

Goal state after: