mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
⊢ LinearMap.det x✝ = (if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1) x✝

Tactic:
rw [LinearMap.det_def]

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
⊢ (if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1) x✝ =
    (if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1) x✝
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : IsCoprime (map ((Ideal.Quotient.mk m).comp f) p) (derivative (map ((Ideal.Quotient.mk m).comp f) p))
⊢ p.Separable

Tactic:
derivative_map,

Goal state after:
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : IsCoprime (map ((Ideal.Quotient.mk m).comp f) p) (map ((Ideal.Quotient.mk m).comp f) (derivative p))
⊢ p.Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : derivative f = 0
hp : p > 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F p) g = f

Tactic:
have := isLocalHom_expand F hp

Goal state after:
case inr
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : derivative f = 0
hp : p > 0
this : IsLocalHom (expand F p)
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F p) g = f
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
x : M
⊢ ((toLin v' v) ((toMatrix v v') f)⁻¹) (f x) = ((toLin v v) (((toMatrix v v') f)⁻¹ * (toMatrix v v') f)) x

Tactic:
toLin_mul v v' v,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
x : M
⊢ ((toLin v' v) ((toMatrix v v') f)⁻¹) (f x) =
    ((toLin v' v) ((toMatrix v v') f)⁻¹ ∘ₗ (toLin v v') ((toMatrix v v') f)) x
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
f✝ g✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
⊢ Polynomial.map g q ∣ Polynomial.map (g.comp f) p

Tactic:
by simpa [Polynomial.map_map] using Polynomial.map_dvd g hf

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
⊢ (b.map f).det v = b.det (⇑f.symm ∘ v)

Tactic:
by
  rw [det_apply, toMatrix_map, det_apply]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ ↑(f * C f.leadingCoeff⁻¹).natDegree ≤ q.degree

Tactic:
degree_eq_natDegree q_monic.ne_zero,

Goal state after:
case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ ↑(f * C f.leadingCoeff⁻¹).natDegree ≤ ↑q.natDegree
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ minpoly K (root f) = f * C f.leadingCoeff⁻¹

Tactic:
by
  have f'_monic : Monic _ := monic_mul_leadingCoeff_inv hf
  refine (minpoly.unique K _ f'_monic ?_ ?_).symm
  · rw [map_mul, aeval_eq, mk_self, zero_mul]
  intro q q_monic q_aeval
  have commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f := by
    ext
    · simp only [RingHom.comp_apply, mk_C, lift_of]
      rfl
    · simp only [RingHom.comp_apply, mk_X, lift_root]
  rw [degree_eq_natDegree f'_monic.ne_zero, degree_eq_natDegree q_monic.ne_zero,
    Nat.cast_le, natDegree_mul hf, natDegree_C, add_zero]
  · apply natDegree_le_of_dvd
    · have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, map_zero]
      exact mk_eq_zero.1 this
    · exact q_monic.ne_zero
  · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}
i : ℕ
hi : i ≤ k
hik : i < k
⊢ (f ^ (i + 1)) x = f ((f ^ i) x)

Tactic:
by simpa [Module.End.pow_apply] using iterate_succ_apply' f i x

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case e'_4
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
this : IsUnit ((aeval (P.newtonMap^[n] x)) (derivative P))
⊢ (aeval (P.newtonMap^[n] x)) P +
      eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
        (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) =
    0

Tactic:
derivative_map,

Goal state after:
case e'_4
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
this : IsUnit ((aeval (P.newtonMap^[n] x)) (derivative P))
⊢ (aeval (P.newtonMap^[n] x)) P +
      eval (P.newtonMap^[n] x) (map (algebraMap R S) (derivative P)) *
        (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) =
    0
Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
n' : Module.End K (Module.End K V)
hn'_adj : n' ∈ K[(ad K (Module.End K V)) (n + s)]
s' : Module.End K (Module.End K V)
hs'_adj : s' ∈ K[(ad K (Module.End K V)) (n + s)]
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V)) (n + s) = n' + s'
hc' : Commute n' s'
hs_eq : s' = (ad K (Module.End K V)) s
⊢ (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]

Tactic:
hs_eq

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
n' : Module.End K (Module.End K V)
hn'_adj : n' ∈ K[(ad K (Module.End K V)) (n + s)]
s' : Module.End K (Module.End K V)
hs'_adj : (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V)) (n + s) = n' + s'
hc' : Commute n' s'
hs_eq : s' = (ad K (Module.End K V)) s
⊢ (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ (derivative (map (algebraMap R S) P)) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))
⊢ r₁ = r₂

Tactic:
derivative_map,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ (map (algebraMap R S) (derivative P)) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))
⊢ r₁ = r₂
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
this : hasBracketAux x ∘ₗ hasBracketAux y = hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x
⊢ (hasBracketAux x) ((hasBracketAux y) t) = (hasBracketAux ⁅x, y⁆) t + (hasBracketAux y) ((hasBracketAux x) t)

Tactic:
by
      rw [← LinearMap.comp_apply, this]; rfl

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

Goal state before:
pp: case refine_2
R✝ : Type u_1
A✝ : Type u_2
L✝ : Type u_3
M : Type u_4
inst✝¹⁷ : CommRing R✝
inst✝¹⁶ : CommRing A✝
inst✝¹⁵ : Algebra R✝ A✝
inst✝¹⁴ : LieRing L✝
inst✝¹³ : LieAlgebra R✝ L✝
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R✝ M
inst✝¹⁰ : LieRingModule L✝ M
inst✝⁹ : LieModule R✝ L✝ M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y x✝ y✝ : A ⊗[R] L
⊢ (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x✝) y) =
      ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x✝))
        ((TensorProduct.map f.toLinearMap ↑g) y) →
    (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y✝) y) =
        ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y✝))
          ((TensorProduct.map f.toLinearMap ↑g) y) →
      (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ + y✝)) y) =
        ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ + y✝)))
          ((TensorProduct.map f.toLinearMap ↑g) y)

Tactic:
refine y.induction_on (by simp) (fun _ _ h ↦ by simp [h]) (by simp_all)

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case f
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
his : i ∈ s
g g' : G
x✝ : F
| ((g • l x✝ - l x✝) • (toFun G F) x✝) g'

Tactic:
rw [Pi.smul_apply, sub_smul, smul_eq_mul]

Goal state after:
case f
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
his : i ∈ s
g g' : G
x✝ : F
| g • l x✝ * (toFun G F) x✝ g' - l x✝ • (toFun G F) x✝ g'
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: case mp
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Finset E
hs : adjoin F ↑s = ⊤
this✝ : Algebra.FiniteType F ↥(Algebra.adjoin F ↑s)
this : Algebra.EssFiniteType ↥(Algebra.adjoin F ↑s) ↥(adjoin F ↑s)
⊢ Algebra.EssFiniteType F E

Tactic:
have : Algebra.EssFiniteType F (adjoin F (s : Set E)) :=
      .comp _ (Algebra.adjoin F (s : Set E)) _

Goal state after:
case mp
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Finset E
hs : adjoin F ↑s = ⊤
this✝¹ : Algebra.FiniteType F ↥(Algebra.adjoin F ↑s)
this✝ : Algebra.EssFiniteType ↥(Algebra.adjoin F ↑s) ↥(adjoin F ↑s)
this : Algebra.EssFiniteType F ↥(adjoin F ↑s)
⊢ Algebra.EssFiniteType F E
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: case mp
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ⊤.FG → Algebra.EssFiniteType F E

pp: case mpr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Algebra.EssFiniteType F E → ⊤.FG

Tactic:
· intro ⟨s, hs⟩
    have : Algebra.FiniteType F (Algebra.adjoin F (s : Set E)) := .adjoin_of_finite s.finite_toSet
    have : Algebra.EssFiniteType (Algebra.adjoin F (s : Set E)) (adjoin F (s : Set E)) :=
      .of_isLocalization _ (nonZeroDivisors _)
    have : Algebra.EssFiniteType F (adjoin F (s : Set E)) :=
      .comp _ (Algebra.adjoin F (s : Set E)) _
    rw [hs] at this
    exact .of_surjective IntermediateField.topEquiv.toAlgHom IntermediateField.topEquiv.surjective

Goal state after:
case mpr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Algebra.EssFiniteType F E → ⊤.FG
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
a✝ : Algebra.EssFiniteType F E
⊢ adjoin F ↑(Algebra.EssFiniteType.finset F E) = ⊤

Tactic:
refine top_le_iff.mp fun x _ ↦ ?_

Goal state after:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
a✝ : Algebra.EssFiniteType F E
x : E
x✝ : x ∈ ⊤
⊢ x ∈ adjoin F ↑(Algebra.EssFiniteType.finset F E)
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: F : Type u_5
E : Type u_6
K : Type u_7
inst✝⁹ : CommSemiring F
inst✝⁸ : StrongRankCondition F
inst✝⁷ : CommSemiring E
inst✝⁶ : StrongRankCondition E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Algebra F K
inst✝¹ : IsScalarTower F E K
L : Subalgebra F K
inst✝ : Module.Free F ↥L
⊢ Module.rank E ↥(Algebra.adjoin E ↑L) ≤ Module.rank F ↥L

Tactic:
by
  rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex F L,
    L.adjoin_eq_span_basis E (Module.Free.chooseBasis F L)]
  exact rank_span_le _ |>.trans Cardinal.mk_range_le

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

Goal state before:
pp: k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
x : k[X]
hu : x ∈ nonunits k[X]
h0 : x ≠ 0
w✝¹ w✝ : k[X]
h : ∀ (a : K), (aeval a) (x * w✝¹) ≠ 0 ∨ (aeval a) (x * w✝) ≠ 0
a : K
ha : eval a (map (algebraMap k K) x) = 0
⊢ (aeval a) x * (aeval a) w✝¹ = 0 ∧ (aeval a) x * (aeval a) w✝ = 0

Tactic:
← eval_map_algebraMap,

Goal state after:
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
x : k[X]
hu : x ∈ nonunits k[X]
h0 : x ≠ 0
w✝¹ w✝ : k[X]
h : ∀ (a : K), (aeval a) (x * w✝¹) ≠ 0 ∨ (aeval a) (x * w✝) ≠ 0
a : K
ha : eval a (map (algebraMap k K) x) = 0
⊢ eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w✝¹) = 0 ∧
    eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w✝) = 0
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
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ∀ i ∈ s, {↑i} ⊆ ↑(adjoin F (Subtype.val '' ↑s))

Tactic:
rintro _ h _ rfl

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
i✝ : ↑S
h : i✝ ∈ s
⊢ ↑i✝ ∈ ↑(adjoin F (Subtype.val '' ↑s))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ Module.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree

Tactic:
PowerBasis.finrank (adjoin.powerBasis hx :)

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (powerBasis hx).dim = (minpoly K x).natDegree
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case insert.refine_2
ι : 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)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
χ : ι → R
x✝ : χ ∈ s
u : M
hu : u ∈ ↑(⨅ i, (f i).maxGenEigenspace (χ i))
⊢ (g ^ k) u ∈ ⨅ i, (f i).maxGenEigenspace (χ i)

Tactic:
refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu

Goal state after:
case insert.refine_2
ι : 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)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
χ : ι → R
x✝ : χ ∈ s
u : M
hu : u ∈ ↑(⨅ i, (f i).maxGenEigenspace (χ i))
⊢ MapsTo ⇑(f l) ↑(⨅ i, (f i).maxGenEigenspace (χ i)) ↑(⨅ i, (f i).maxGenEigenspace (χ i))
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Tactic:
have := congr_arg (Submodule.comap p.subtype) (Submodule.eq_iSup_inf_genEigenspace k h h')
  have h_inj : Function.Injective p.subtype := Subtype.coe_injective
  simp_rw [Submodule.inf_genEigenspace f p h, Submodule.comap_subtype_self,
    ← Submodule.map_iSup, Submodule.comap_map_eq_of_injective h_inj] at this
  exact this.symm

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

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
this :
  ∀ (χ : ι → K),
    χ i = φ →
      ⨅ j, (f j).maxGenEigenspace (χ j) =
        Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
⊢ Submodule.map ((f i).maxGenEigenspace φ).subtype ⊤ = (f i).maxGenEigenspace φ

Tactic:
Submodule.map_top,

Goal state after:
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
this :
  ∀ (χ : ι → K),
    χ i = φ →
      ⨅ j, (f j).maxGenEigenspace (χ j) =
        Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j))
⊢ ((f i).maxGenEigenspace φ).subtype.range = (f i).maxGenEigenspace φ