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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
h : Commute a b
⊢ (ad R A) a * (ad R A) b = (ad R A) b * (ad R A) a

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
h : Commute a b
⊢ (ad R A) a * (ad R A) b - (ad R A) b * (ad R A) a = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ eval₂ (ϕ.comp (of f)) (ϕ (root f)) f = 0

Tactic:
← map_zero ϕ.toRingHom,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ eval₂ (ϕ.comp (of f)) (ϕ (root f)) f = ϕ.toRingHom 0
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
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
G : Type u_5
inst✝² : Group G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
g : G
v : ι → M
⊢ ((g • e).toMatrix v).det = (e.toMatrix (g⁻¹ • v)).det

Tactic:
toMatrix_smul_left

Goal state after:
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
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f g : S[X]
hfg : f = g
⊢ Associated f g

Tactic:
by rw [hfg]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_2.h1
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 ∣ q

Tactic:
have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, map_zero]

Goal state after:
case refine_2.h1
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
this : (mk f) q = 0
⊢ f ∣ q
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
⊢ C f.leadingCoeff⁻¹ ≠ 0

Tactic:
· rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]

Goal state after:
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]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * C f.leadingCoeff⁻¹
⊢ C f.leadingCoeff⁻¹ ≠ 0

Tactic:
· rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
f : End K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
g : K[X]
k : ℕ
sep : Squarefree g
nil : minpoly K f ∣ g ^ k
⊢ ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
← PerfectField.separable_iff_squarefree

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
f : End K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
g : K[X]
k : ℕ
sep : g.Separable
nil : minpoly K f ∣ g ^ k
⊢ ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
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 : LieIdeal R L
k : ℕ
⊢ derivedSeries R (↥I) k = ⊥ ↔ derivedSeries R (↥I) k ≤ I.incl.ker

Tactic:
ker_incl,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedSeries R (↥I) k = ⊥ ↔ derivedSeries R (↥I) k ≤ ⊥
Module: Mathlib.Algebra.Lie.Normalizer

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
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅x, y⁆ ∈ H

Tactic:
rw [← lie_skew, neg_mem_iff (G := L)]
  exact hx ⟨y, hy⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
⊢ ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0

Tactic:
rintro ⟨x⟩ hx
    suffices x ∈ H by rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
      coe_toLieSubmodule, mem_toSubmodule]
    rw [← h, H.mem_normalizer_iff']
    intro y hy
    replace hx : ⁅_, LieSubmodule.Quotient.mk' _ x⁆ = 0 := hx ⟨y, hy⟩
    rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx

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
inst✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
⊢ ∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l

Tactic:
obtain ⟨n, hn : ∀ m, n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m⟩ :=
    h_wf.monotone_chain_condition ⟨_, antitone_lowerCentralSeries R L M⟩

Goal state after:
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✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
⊢ ∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: 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
⊢ lowerCentralSeries R L M (i + n) ≤ I.lcs M (j + 1)

Tactic:
suffices
    ∀ l,
      ((⊤ : LieIdeal R L).lcs M (i + l) : Submodule R M) ≤
        (I.lcs M j : Submodule R M).map (toEnd R L M x ^ l) ⊔
          (I.lcs M (j + 1) : Submodule R M)
    by simpa only [bot_sup_eq, LieIdeal.incl_coe, Submodule.map_zero, hxn] using! this n
  intro l
  induction l with
  | zero =>
    simp only [add_zero, LieIdeal.lcs_succ, pow_zero, Module.End.one_eq_id,
      Submodule.map_id]
    exact le_sup_of_le_left hIM
  | succ l ih =>
    simp only [LieIdeal.lcs_succ, i.add_succ l, lie_top_eq_of_span_sup_eq_top hxI, sup_le_iff]
    refine ⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩
    · rw [Submodule.map_sup, ← Submodule.map_comp, ← Module.End.mul_eq_comp, ← pow_succ', ←
        I.lcs_succ]
      grw [coe_map_toEnd_le]
    · norm_cast
      gcongr
      exact le_trans (antitone_lowerCentralSeries R L M le_self_add) hIM

Goal state after:
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
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ lcs (l + (k + 1)) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂

Tactic:
(by abel : l + (k + 1) = l + 1 + k),

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
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ lcs (l + 1 + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (k + 1) N₂
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case mpr
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₂
inst✝ : LieModule R L₂ M₂
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
h : LieModule.IsNilpotent L₂ M₂
hg : Surjective ⇑↑g.symm
x : L₂
m : M₂
⊢ g.symm (g ⁅f.symm x, g.symm m⁆) = g.symm ⁅x, m⁆

Tactic:
←
      hfg,

Goal state after:
case mpr
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₂
inst✝ : LieModule R L₂ M₂
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
h : LieModule.IsNilpotent L₂ M₂
hg : Surjective ⇑↑g.symm
x : L₂
m : M₂
⊢ g.symm ⁅f (f.symm x), g (g.symm m)⁆ = g.symm ⁅x, m⁆
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
k : ℕ
N : LieSubmodule R L M
inst✝¹ : LieModule R L M
inst✝ : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L M)
⊢ IsNilpotent L ↥(maxNilpotentSubmodule R L M)

Tactic:
refine hwf { N : LieSubmodule R L M | IsNilpotent L N } ⟨⊥, ?_⟩ fun N₁ h₁ N₂ h₂ => ?_ <;>
  simp_all <;> infer_instance

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
⊢ LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s

Tactic:
by
  classical
  have : IsEmpty ((∅ : Finset F) : Set F) := by simp
  refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
  rw [coe_insert] at hs ⊢
  rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
  rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
  rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
  rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
  suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
    replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
    simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
    refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
    change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
    exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa
  intro i his g
  refine
    eq_of_sub_eq_zero
      (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) ?_ ⟨i, his⟩
          (mem_attach _ _) :
        _)
  refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
  ext g'
  conv_lhs =>
    rw [Finset.sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
  rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
  conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
  change
    (∑ x ∈ s, g • (fun y => l y • MulAction.toFun G F y) x (g⁻¹ * g')) =
      ∑ x ∈ s, (fun y => l y • MulAction.toFun G F y) x g'
  rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]
  rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]

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
inst✝ : Fintype G
x : F
⊢ (minpoly G F x).Monic

Tactic:
by
  simp only [minpoly]
  rw [Polynomial.monic_toSubring]
  exact prodXSubSMul.monic G F x

Goal state after:
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
inst✝¹ : EssFiniteType F E
inst✝ : Algebra.IsAlgebraic F E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ Algebra.adjoin F ↑s = ⊤

Tactic:
← adjoin_toSubalgebra_of_isAlgebraic fun x hx ↦ Algebra.IsAlgebraic.isAlgebraic x

Goal state after:
case h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : EssFiniteType F E
inst✝ : Algebra.IsAlgebraic F E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ (adjoin F ↑s).toSubalgebra = ⊤
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
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E1 E2 : IntermediateField K L
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
⊢ FiniteDimensional K ↥(E1 ⊔ E2)

Tactic:
by
  let g := Algebra.TensorProduct.productMap E1.val E2.val
  suffices g.range = (E1 ⊔ E2).toSubalgebra by
    have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) :=
      g.toLinearMap.finiteDimensional_range
    rwa [this] at h
  rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]

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))
⊢ ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, (f j).maxGenEigenspace (χ j) = (f i).maxGenEigenspace φ

Tactic:
biSup_congr this,

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))
⊢ ⨆ i_1,
      ⨆ (_ : i_1 i = φ),
        Submodule.map ((f i).maxGenEigenspace φ).subtype (⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (i_1 j)) =
    (f i).maxGenEigenspace φ
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h e f x : L
t : IsSl2Triple h e f
⊢ x ∈ toLieSubalgebra R t ↔ ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

Tactic:
simp_rw [t.lie_e_f, toLieSubalgebra, ← LieSubalgebra.mem_toSubmodule, Submodule.mem_span_triple,
    eq_comm]

Goal state after:
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
⊢ x ∈ corootSpace α ↔ ↑x ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}

Tactic:
by
  have : x ∈ corootSpace α ↔
      (x : L) ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α) := by
    rw [corootSpace]
    simp only [rootSpaceProduct_def, LieModuleHom.mem_range, LieSubmodule.mem_map,
      LieSubmodule.incl_apply, SetLike.coe_eq_coe, exists_eq_right]
    rfl
  simp_rw [this, corootSpace, ← LieModuleHom.map_top, ← LieSubmodule.mem_toSubmodule,
    LieSubmodule.toSubmodule_map, LieSubmodule.top_toSubmodule, ← TensorProduct.span_tmul_eq_top,
    LinearMap.map_span, Set.image, Set.mem_ofPred_eq, exists_exists_exists_and_eq]
  change (x : L) ∈ Submodule.span R
    {x | ∃ (a : rootSpace H α) (b : rootSpace H (-α)), ⁅(a : L), (b : L)⁆ = x} ↔ _
  simp

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Nontrivial M
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ : ((toEnd R L M) h).HasEigenvalue μ₀
m₀ : M
hm₀ : ((toEnd R L M) h).HasEigenvector μ₀ m₀
evals : ℕ → R := fun n ↦ μ₀ + 2 * ↑n
e_vecs : ℕ → M := fun n ↦ ((toEnd R L M) e ^ n) m₀
h_exists_zero : ∃ k, e_vecs k = 0
n : ℕ
hn_ne : ¬e_vecs n = 0
hn_zero : e_vecs (n + 1) = 0
⊢ ⁅e, e_vecs n⁆ = 0

Tactic:
by rwa [lie_e_pow_toEnd_e n]

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

Goal state before:
pp: K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
⊢ ⨆ χ, genWeightSpace M ⇑χ = ⊤

Tactic:
by
  have := iSup_genWeightSpace_eq_top K L M
  erw [← iSup_ne_bot_subtype, ← (Weight.equivSetOfPred K L M).iSup_comp] at this
  exact this

Goal state after:
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
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
W : Submodule K V
⊢ finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W

Tactic:
by
  have := finrank_add_finrank_orthogonal' (B := B) W
  rw [hB.ker_eq_bot, inf_bot_eq, finrank_bot, add_zero] at this
  lia

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ ComplementedLattice α

Tactic:
let _i := hS.distribLatticeOfSSupEqTop h
  have _i₁ := isAtomistic_of_sSup_eq_top hS h
  apply complementedLattice_of_isAtomistic

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

Goal state before:
pp: k : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : LieRing L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieRing.IsNilpotent L
inst✝⁷ : Field k
inst✝⁶ : LieAlgebra k L
inst✝⁵ : Module k M
inst✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
⊢ Nonempty (Weight k L M)

Tactic:
by
    by_contra! contra
    simpa only [iSup_of_empty, bot_ne_top] using LieModule.iSup_genWeightSpace_eq_top' k L M

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
⊢ Irreducible f.factor

Tactic:
rw [factor]

Goal state after:
K : Type v
inst✝ : Field K
f : K[X]
⊢ Irreducible (if H : ∃ g, Irreducible g ∧ g ∣ f then Classical.choose H else X)
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: case pos
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ f.factor ∣ f

Tactic:
hf2

Goal state after:
case pos
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ factor 0 ∣ 0
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))) =
    ⊤

Tactic:
ih _ (natDegree_removeFactor' hfn),

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Subalgebra.restrictScalars K ⊤ = ⊤
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (Ideal.Quotient.mk (maxIdeal k)) (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f)).coeff n✝ =
    (map (Ideal.Quotient.mk (maxIdeal k)) (∏ i, (X - C (MvPolynomial.X ⟨f, i⟩)))).coeff n✝

Tactic:
← sub_eq_zero,

Goal state after:
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (Ideal.Quotient.mk (maxIdeal k)) (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f)).coeff n✝ -
      (map (Ideal.Quotient.mk (maxIdeal k)) (∏ i, (X - C (MvPolynomial.X ⟨f, i⟩)))).coeff n✝ =
    0
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
U : Submodule R M
⊢ p.IsPerfectCompl U ⊤ ↔ U = ⊤

Tactic:
rw [← IsPerfectCompl.flip_iff]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
U : Submodule R M
⊢ p.flip.IsPerfectCompl ⊤ U ↔ U = ⊤
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case h₂
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
P : R[X]
hP : P ∈ degreeLT R m
⊢ P ∈ span R (↑S '' Set.Iio m)

Tactic:
nontriviality R using Subsingleton.eq_zero P

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
P : R[X]
hP : P ∈ degreeLT R m
a✝ : Nontrivial R
⊢ P ∈ span R (↑S '' Set.Iio m)