mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y : L ⧸ I
⊢ ∀ (a₁ a₂ b₁ b₂ : L), (↑I).quotientRel a₁ b₁ → (↑I).quotientRel a₂ b₂ → mk ⁅a₁, a₂⁆ = mk ⁅b₁, b₂⁆

Tactic:
intro x₁ x₂ y₁ y₂ h₁ h₂

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y : L ⧸ I
x₁ x₂ y₁ y₂ : L
h₁ : (↑I).quotientRel x₁ y₁
h₂ : (↑I).quotientRel x₂ y₂
⊢ mk ⁅x₁, x₂⁆ = mk ⁅y₁, y₂⁆
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
⊢ IsSolvable ↥(radical R L)

Tactic:
refine hwf { I : LieIdeal R L | IsSolvable I } ⟨⊥, ?_⟩ fun I hI J hJ => ?_

Goal state after:
case refine_1
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
⊢ ⊥ ∈ {I | IsSolvable ↥I}

case refine_2
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
I : LieSubmodule R L L
hI : I ∈ {I | IsSolvable ↥I}
J : LieSubmodule R L L
hJ : J ∈ {I | IsSolvable ↥I}
⊢ I ⊔ J ∈ {I | IsSolvable ↥I}
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : 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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
⊢ baseChange A ⁅I, N⁆ = ⁅baseChange A I, baseChange A N⁆

Tactic:
set s : Set (A ⊗[R] M) := { m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ ⁅x, n⁆ = m}
  have : (TensorProduct.mk R A M 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s := by ext; simp [s]
  rw [← toSubmodule_inj, coe_baseChange, lieIdeal_oper_eq_linear_span',
    Submodule.baseChange_span, this, lieIdeal_oper_eq_linear_span']
  refine le_antisymm (Submodule.span_mono ?_) (Submodule.span_le.mpr ?_)
  · rintro - ⟨x, hx, m, hm, rfl⟩
    exact ⟨1 ⊗ₜ x, tmul_mem_baseChange_of_mem 1 hx,
           1 ⊗ₜ m, tmul_mem_baseChange_of_mem 1 hm, by simp⟩
  · rintro - ⟨x, hx, m, hm, rfl⟩
    rw [mem_baseChange_iff] at hx hm
    refine Submodule.span_induction₂ (p := fun x m _ _ ↦ ⁅x, m⁆ ∈ Submodule.span A s)
      ?_ (by simp) (by simp) ?_ ?_ ?_ ?_ hx hm
    · rintro - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩; exact Submodule.subset_span ⟨x, hx, y, hy, by simp⟩
    all_goals { intros; simp [add_mem, Submodule.smul_mem, *] }

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

Goal state before:
pp: 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
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k ⊥ ≤ N₁

Tactic:
by
  rw [← ucs_eq_self_of_normalizer_eq_self h k]
  gcongr
  simp

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent ((ad R ↥L') ↑x)
⊢ ↑K.toLieSubmodule ≤ Submodule.comap ((ad R ↥L') ↑x) ↑K.toLieSubmodule

Tactic:
intro X

Goal state after:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent ((ad R ↥L') ↑x)
X : ↥L'
⊢ X ∈ ↑K.toLieSubmodule → X ∈ Submodule.comap ((ad R ↥L') ↑x) ↑K.toLieSubmodule
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case adjoin_rootSet'
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 g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L) ⊤)
        ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤

Tactic:
Algebra.map_top,

Goal state after:
case adjoin_rootSet'
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 g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin ↥(IsScalarTower.toAlgHom F K L).range
        ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
x : F
⊢ (algebraMap F E) x ∈ ↑S ∪ ↑T

Tactic:
exact Set.mem_union_left _ (algebraMap_mem S x)

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ restrictScalars F (extendScalars h) = restrictScalars F (adjoin (↥K) S)

Tactic:
rw [extendScalars_restrictScalars, restrictScalars_adjoin]
  exact le_antisymm (adjoin.mono F S _ Set.subset_union_right) <| adjoin_le_iff.2 <|
    Set.union_subset h (subset_adjoin F S)

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
⊢ (fun x ↦ eval x p) '' σ a ⊆ σ ((aeval a) p)

Tactic:
rintro _ ⟨k, hk, rfl⟩
  let q := C (eval k p) - p
  have hroot : IsRoot q k := by simp only [q, eval_C, eval_sub, sub_self, IsRoot.def]
  rw [← mul_div_eq_iff_isRoot, ← neg_mul_neg, neg_sub] at hroot
  have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by
    simp only [q, aeval_C, map_sub]
  rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]
  have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a : 𝕜[X] →ₐ[𝕜] A)
  apply mt fun h => (hcomm.isUnit_mul_iff.mp h).1
  simpa only [aeval_X, aeval_C, map_sub] using! hk

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
μ : ι → R
i : ι
h✝ : ∀ (j : ι), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace (μ i)) ↑((f i).maxGenEigenspace (μ i))
this : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo ⇑(f j) ↑p ↑p
⊢ Submodule.map ((f i).maxGenEigenspace (μ i)).subtype
      (⨅ j, (fun j ↦ maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) =
    ⨅ j, (f j).maxGenEigenspace (μ j)

Tactic:
have : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j) := by
    refine le_antisymm ?_ inf_le_right
    simpa only [le_inf_iff, le_refl, and_true] using iInf_le _ _

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
μ : ι → R
i : ι
h✝ : ∀ (j : ι), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace (μ i)) ↑((f i).maxGenEigenspace (μ i))
this✝ : Nonempty ι
p : Submodule R M := (f i).maxGenEigenspace (μ i)
h : ∀ (j : ι), MapsTo ⇑(f j) ↑p ↑p
this : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j)
⊢ Submodule.map ((f i).maxGenEigenspace (μ i)).subtype
      (⨅ j, (fun j ↦ maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) =
    ⨅ j, (f j).maxGenEigenspace (μ j)
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
⊢ (aeval (AdjoinSimple.gen F α)) (minpoly F α) = 0

Tactic:
ext
  convert! minpoly.aeval F α
  conv in aeval α => rw [← AdjoinSimple.algebraMap_gen F α]
  exact (aeval_algebraMap_apply E (AdjoinSimple.gen F α) _).symm

Goal state after:
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
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
⊢ ((f - (algebraMap K (End K V)) μ') ^ l₀) (m μ') = 0

Tactic:
← LinearMap.mem_ker,

Goal state after:
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
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
⊢ m μ' ∈ LinearMap.ker ((f - (algebraMap K (End K V)) μ') ^ 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
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
⊢ Function.Bijective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
set f := AdjoinRoot.lift _ _ (aeval_gen_minpoly F α :)
      have := Fact.mk (minpoly.irreducible h)
      constructor
      · exact RingHom.injective f
      · suffices F⟮α⟯.toSubfield ≤ RingHom.fieldRange (F⟮α⟯.toSubfield.subtype.comp f) by
          intro x
          obtain ⟨y, hy⟩ := this (Subtype.mem x)
          exact ⟨y, Subtype.ext hy⟩
        refine Subfield.closure_le.mpr (Set.union_subset (fun x hx => ?_) ?_)
        · obtain ⟨y, hy⟩ := hx
          refine ⟨y, ?_⟩
          rw [RingHom.comp_apply]
          dsimp only [coe_type_toSubfield]
          rw [AdjoinRoot.lift_of (aeval_gen_minpoly F α)]
          exact hy
        · refine Set.singleton_subset_iff.mpr ⟨AdjoinRoot.root (minpoly F α), ?_⟩
          rw [RingHom.comp_apply]
          dsimp only [coe_type_toSubfield]
          rw [AdjoinRoot.lift_root (aeval_gen_minpoly F α)]
          rfl

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

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
key₂' : finrank (↥K⟮(aeval (root p)) g⟯) Kx = g.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree

Tactic:
have := Module.finrank_mul_finrank K K⟮aeval (root p) g⟯ Kx

Goal state after:
K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝¹ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this✝ : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
key₂' : finrank (↥K⟮(aeval (root p)) g⟯) Kx = g.natDegree
this : finrank K ↥K⟮(aeval (root p)) g⟯ * finrank (↥K⟮(aeval (root p)) g⟯) Kx = finrank K Kx
⊢ p.natDegree = f.natDegree * g.natDegree
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case h
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
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 φ)
φ : K
⊢ ∀ (i_1 j : ι) (φ_1 : K),
    MapsTo ⇑(LinearMap.restrict (f i_1) ⋯) ↑(maxGenEigenspace (LinearMap.restrict (f j) ⋯) φ_1)
      ↑(maxGenEigenspace (LinearMap.restrict (f j) ⋯) φ_1)

Tactic:
intro j k μ

Goal state after:
case h
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
ih :
  ∀ m < n,
    ∀ {M : Type u_4} [inst : AddCommGroup M] [inst_1 : Module K M] [FiniteDimensional K M] (f : ι → End K M),
      (∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)) →
        (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → finrank K M = m → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
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 φ)
φ : K
j k : ι
μ : K
⊢ MapsTo ⇑(LinearMap.restrict (f j) ⋯) ↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) μ)
    ↑(maxGenEigenspace (LinearMap.restrict (f k) ⋯) μ)
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
inst✝² : LieRing.IsNilpotent ↥H
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ ↑x ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
⊢ ↑x ∈
      ↑(LieSubmodule.map H.toLieSubmodule.incl
          (LieSubmodule.map
            (LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯))
              ⋯)
            ⊤)) ↔
    ↑x ∈ Submodule.span R {x | ∃ y ∈ ↑(rootSpace H α), ∃ z ∈ ↑(rootSpace H (-α)), ⁅y, z⁆ = x}

Tactic:
LieSubmodule.toSubmodule_map,

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
H : LieSubalgebra R L
inst✝² : LieRing.IsNilpotent ↥H
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ ↑x ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
⊢ ↑x ∈
      Submodule.map (↑H.toLieSubmodule.incl)
        (Submodule.map
          ↑(LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯)) ⋯)
          ↑⊤) ↔
    ↑x ∈ Submodule.span R {x | ∃ y ∈ ↑(rootSpace H α), ∃ z ∈ ↑(rootSpace H (-α)), ⁅y, z⁆ = x}
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁
hψ₁ : IsAdjointPair B B ⇑ψ₁ ⇑φ
hψ₂ : IsAdjointPair B B ⇑ψ₂ ⇑φ
v w : M₁
⊢ ((B.compLeft ψ₁) v) w = ((B.compLeft ψ₂) v) w

Tactic:
by rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂]

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
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
this : IsCompl (genWeightSpace (↥(LieSubmodule.map N.incl N')) 0) (posFittingComp R L ↥(LieSubmodule.map N.incl N'))
⊢ IsCompl (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')

Tactic:
let e := LieSubmodule.equivMapOfInjective N' N.injective_incl
    rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e] at this
    exact (LieSubmodule.orderIsoMapComap e).isCompl_iff.mpr this

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
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
x : L
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint (genWeightSpaceOf M φ₁ x) (genWeightSpaceOf M φ₂ x)

Tactic:
rw [← LieSubmodule.disjoint_toSubmodule]

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✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
x : L
φ₁ φ₂ : R
h : φ₁ ≠ φ₂
⊢ Disjoint ↑(genWeightSpaceOf M φ₁ x) ↑(genWeightSpaceOf M φ₂ x)
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
b : α
⊢ IsCompactElement b → b ≤ sSup S → ∃ T ⊆ S, b = sSup T

Tactic:
hb

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
b : α
hb : IsCompactElement b
⊢ b ≤ sSup S → ∃ T ⊆ S, b = sSup T
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
a : α
ha : IsAtom a
haS : a ≤ sSup S
⊢ a ∈ S

Tactic:
by
  obtain ⟨T, hT, rfl⟩ := hS.atomistic a haS
  obtain rfl | ⟨a, haT⟩ := T.eq_empty_or_nonempty
  · simp only [sSup_empty] at ha
    exact (ha.1 rfl).elim
  suffices sSup T = a from this ▸ hT haT
  have : a ≤ sSup T := le_sSup haT
  rwa [ha.le_iff_eq, eq_comm] at this
  exact (hS.isAtom a (hT haT)).1

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ≤ sSup T₂

Tactic:
· exact (_root_.le_sSup hI).trans (hX'.ge.trans inf_le_right)

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
hχ : genWeightSpace M χ ≠ ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
⊢ 0 < b

Tactic:
replace hχ : Nontrivial (genWeightSpace M χ) := by rwa [LieSubmodule.nontrivial_iff_ne_bot]

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
inst✝⁶ : H.IsCartanSubalgebra
inst✝⁵ : IsNoetherian R L
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : CharZero R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hα : α ≠ 0
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥(genWeightSpace M (i • α + χ))
hχ : Nontrivial ↥(genWeightSpace M χ)
⊢ 0 < b