mathlib-initiative/mathlib-tactics huggingface dataset:
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.natDegree ≤ q.natDegree

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
⊢ C f.leadingCoeff⁻¹ ≠ 0

Tactic:
· 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

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
⊢ C f.leadingCoeff⁻¹ ≠ 0
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}
hp₁ : p ∈ f.invtSubmodule
⊢ f x = 0 x

Tactic:
have hp₂ : Module.Finite R p := by
    let g : ℕ → M := fun i ↦ (f ^ i) x
    have hg : {(f ^ i) x | (i : ℕ) (_ : i ≤ k)} = g '' Iic k := by ext; simp [g]
    exact Module.Finite.span_of_finite _ <| hg ▸ toFinite (g '' Iic k)

Goal state after:
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}
hp₁ : p ∈ f.invtSubmodule
hp₂ : Module.Finite R ↥p
⊢ f x = 0 x
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
⊢ LinearMap.det e = LinearMap.det (e.restrict he) * LinearMap.det (W.mapQ W e he)

Tactic:
by
  let m := Module.Free.ChooseBasisIndex R W
  let bW : Basis m R W := Module.Free.chooseBasis R W
  let n := Module.Free.ChooseBasisIndex R (V ⧸ W)
  let bQ : Basis n R (V ⧸ W) := Module.Free.chooseBasis R (V ⧸ W)
  let b := sumQuot bW bQ
  let A : Matrix m m R := LinearMap.toMatrix bW bW (e.restrict he)
  let B : Matrix m n R := Matrix.of fun i l ↦
    ((sumQuot bW bQ).repr (e ((sumQuot bW bQ) (Sum.inr l)))) (Sum.inl i)
  let D : Matrix n n R := LinearMap.toMatrix bQ bQ (W.mapQ W e he)
  suffices LinearMap.toMatrix b b e = Matrix.fromBlocks A B 0 D by
    rw [← LinearMap.det_toMatrix b, this, ← LinearMap.det_toMatrix bW,
      ← LinearMap.det_toMatrix bQ, Matrix.det_fromBlocks_zero₂₁]
  ext u v
  cases u with
  | inl i =>
    cases v with
    | inl k =>
      simp only [b, sumQuot_inl, Matrix.fromBlocks_apply₁₁, A, LinearMap.toMatrix_apply]
      apply sumQuot_repr_inl_of_mem
    | inr l => simp [b, LinearMap.toMatrix_apply, Matrix.fromBlocks_apply₁₂, B]
  | inr j =>
    cases v with
    | inl k =>
      suffices W.mkQ (e (bW k)) = 0 by simp [LinearMap.toMatrix_apply, b, this]
      rw [← LinearMap.mem_ker, Submodule.ker_mkQ]
      exact he (Submodule.coe_mem (bW k))
    | inr l =>
      simp only [LinearMap.toMatrix_apply, sumQuot_repr_inr,
        Matrix.fromBlocks_apply₂₂, b, D]
      rw [← sumQuot_inr bW bQ l, W.mapQ_apply]
      simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: K : Type u_6
L : Type u_7
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
h2 : IsIntegral K (AdjoinRoot.root f)
h3 : f * C f.leadingCoeff⁻¹ ∣ Polynomial.map (algebraMap K L) (minpoly K (AdjoinRoot.root f))
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g

Tactic:
exact ⟨_, minpoly.monic h2, minpoly.irreducible h2, dvd_of_mul_right_dvd h3⟩

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

Goal state before:
pp: case inl
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)
s₁ :
  ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i =
    ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
h : N + 1 ≤ i.1
⊢ ((↑i.1!)⁻¹ * (↑i.2!)⁻¹) • (a ^ i.1 * b ^ i.2) = 0

Tactic:
rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]

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

Goal state before:
pp: case inl
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)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
h : N + 1 ≤ i.1
⊢ ((↑i.1!)⁻¹ * (↑i.2!)⁻¹) • (a ^ i.1 * b ^ i.2) = 0

Tactic:
rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]

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
I J : LieIdeal R L
k l : ℕ
h₁ : I ≤ J
h₂ : l ≤ k
⊢ D k I ≤ D l J

Tactic:
induction k generalizing l with
  | zero => rw [le_zero_iff] at h₂; rw [h₂, derivedSeriesOfIdeal_zero]; exact h₁
  | succ k ih =>
    have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
    rcases h with h | h
    · rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
      exact LieSubmodule.mono_lie (ih (le_refl k)) (ih (le_refl k))
    · rw [derivedSeriesOfIdeal_succ]; exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ eval (m • x) (m • (C r * X ^ (n + 1))) = m • eval x (C r * X ^ (n + 1))

Tactic:
by
    rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : LieRing.IsNilpotent (L ⧸ I)
this : LieModule.IsNilpotent L (L ⧸ I)
⊢ LieRing.IsNilpotent L

Tactic:
exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this

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

Goal state before:
pp: case f
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
p : A[X]
⊢ ↑((AlgHom.restrictScalars A (ofId B C)).comp A[b].val) ⟨(aeval b) p, ⋯⟩ ∈ A[(algebraMap B C) b]

Tactic:
aesop (add norm [adjoin_singleton_eq_range_aeval, aeval_algebraMap_apply])

Goal state after:
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 : F
his : i ∈ s
g g' : G
⊢ ∑ x ∈ s, g • (fun y ↦ l y • (toFun G F) y) x (g⁻¹ * g') = ∑ x ∈ s, (fun y ↦ l y • (toFun G F) y) x g'

Tactic:
← smul_sum,

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
his : i ∈ s
g g' : G
⊢ g • ∑ x ∈ s, (fun y ↦ l y • (toFun G F) y) x (g⁻¹ * g') = ∑ x ∈ s, (fun y ↦ l y • (toFun G F) y) x g'
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case inl
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0
hf3 : f = minpoly G F x
⊢ g = 1

Tactic:
← mul_one (minpoly G F x),

Goal state after:
case inl
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x * 1
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0
hf3 : f = minpoly G F x
⊢ g = 1
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ Function.Bijective ⇑(Minpoly.toAdjoin F x)

Tactic:
refine ⟨(injective_iff_map_eq_zero _).2 fun P₁ hP₁ ↦ ?_, Minpoly.toAdjoin.surjective F x⟩
    obtain ⟨P, rfl⟩ := mk_surjective P₁
    refine AdjoinRoot.mk_eq_zero.mpr (minpoly.dvd F x ?_)
    simpa [← Subalgebra.coe_eq_zero, ← aeval_def] using hP₁

Goal state after:
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
p : K[X]
F : IntermediateField K L
h : (Polynomial.map (algebraMap K L) p).Splits
hF : ∀ x ∈ p.rootSet L, x ∈ F
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits

Tactic:
have := Splits.of_splits_map (f := p.map (algebraMap K F)) (algebraMap F L)

Goal state after:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : (Polynomial.map (algebraMap K L) p).Splits
hF : ∀ x ∈ p.rootSet L, x ∈ F
this :
  (Polynomial.map (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)).Splits →
    (∀ a ∈ (Polynomial.map (algebraMap (↥F) L) (Polynomial.map (algebraMap K ↥F) p)).roots,
        a ∈ (algebraMap (↥F) L).range) →
      (Polynomial.map (algebraMap K ↥F) p).Splits
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.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
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Injective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

pp: case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Surjective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
· exact RingHom.injective f

Goal state after:
case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Surjective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case right.refine_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ F⟮α⟯.toSubfield.subtype (f (AdjoinRoot.root (minpoly F α))) = α

Tactic:
rw [AdjoinRoot.lift_root (aeval_gen_minpoly F α)]

Goal state after:
case right.refine_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ F⟮α⟯.toSubfield.subtype (AdjoinSimple.gen F α) = α
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
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ (minpoly (↥K) α).natDegree = g.natDegree

Tactic:
natDegree_map

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ (minpoly (↥K) α).natDegree = (minpoly (↥K) α).natDegree
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 :
  ∀ (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
f : End R M
φ : R
k : ℕ
p : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
⊢ MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p

Tactic:
rw [Module.End.coe_pow]

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)))
χ₁ χ₂ : ι → 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
f : End R M
φ : R
k : ℕ
p : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
⊢ MapsTo (⇑(f - (algebraMap R (End R M)) φ))^[k] ↑p ↑p
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
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx✝ : x ∈ ⨆ i, t i
s : Finset ((i : ι) × ↥(t i))
hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯
this : ∀ (i : (i : ι) × ↥(t i)), FiniteDimensional K ↥K⟮↑i.snd⟯
⊢ IsAlgebraic K ⟨x, hx⟩

Tactic:
apply IsAlgebraic.of_finite

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case refine_2
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
⊢ ∀ (x_1 : ↥𝕎(M₁, χ₁, x)) (y : ↥𝕎(M₂, χ₂, x)),
    ∃ k,
      (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k)
          (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) (x_1 ⊗ₜ[R] y))) =
        0

Tactic:
rintro ⟨m₁, hm₁⟩ ⟨m₂, hm₂⟩

Goal state after:
case refine_2
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)
m₂ : M₂
hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)
⊢ ∃ k,
    (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k)
        (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) (⟨m₁, hm₁⟩ ⊗ₜ[R] ⟨m₂, hm₂⟩))) =
      0
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : Weight R L M
h : (fun χ ↦ χ.toFun) χ₁ = (fun χ ↦ χ.toFun) χ₂
⊢ χ₁ = χ₂

Tactic:
cases χ₁; cases χ₂; simp_all

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
m : M
hm : m ∈ (genWeightSpace M 0).normalizer
⊢ m ∈ genWeightSpace M 0

Tactic:
rw [LieSubmodule.mem_normalizer] at hm

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
m : M
hm : ∀ (x : L), ⁅x, m⁆ ∈ genWeightSpace M 0
⊢ m ∈ genWeightSpace M 0
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := ⋯
M₁ : LieSubmodule R L M := ⋯
x : L
M₀ₓ : LieSubmodule R L M := ⋯
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := ⋯
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := ⋯
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := ⋯
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
⊢ posFittingComp R L M ≤ LieSubmodule.map M₀ₓ.incl (posFittingComp R L ↥M₀ₓ) ⊔ posFittingCompOf R M x

Tactic:
rw [← posFittingComp_map_incl_sup_of_codisjoint h₁.codisjoint]

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
⊢ LieSubmodule.map M₀ₓ.incl (posFittingComp R L ↥M₀ₓ) ⊔ LieSubmodule.map M₁ₓ.incl (posFittingComp R L ↥M₁ₓ) ≤
    LieSubmodule.map M₀ₓ.incl (posFittingComp R L ↥M₀ₓ) ⊔ posFittingCompOf R M x
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
j : n
a✝ : j ∈ s
hij : j ≠ i
⊢ w j * (B (v j)) (v i) = 0

Tactic:
rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
⊢ x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker → x ∈ W ⊓ ker B

Tactic:
intro hx

Goal state after:
case mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker
⊢ x ∈ W ⊓ ker B
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
⊢ x ∈ W ⊓ ker B → x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker

Tactic:
intro hx

Goal state after:
case mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ W ⊓ ker B
⊢ x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
⊢ x ∈ (domRestrict B W).range.dualCoannihilator → ∀ n ∈ W, (B n) x = 0

Tactic:
intro hx

Goal state after:
case mp
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ (domRestrict B W).range.dualCoannihilator
⊢ ∀ n ∈ W, (B n) x = 0