mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∀ (x : ↥⊥), (algebraMap (↥⊥) E) x = (algebraMap F E) ((algebraMap (↥⊥) F) x)

Tactic:
intro x
      obtain ⟨y, rfl⟩ := (botEquiv F E).symm.surjective x
      rw [coe_algebraMap_over_bot, (botEquiv F E).apply_symm_apply, botEquiv_symm,
        IsScalarTower.algebraMap_apply F (⊥ : IntermediateField F E) E]

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

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
⊢ ∃ z, x = z * z

Tactic:
rcases exists_pow_nat_eq x zero_lt_two with ⟨z, rfl⟩

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case h.succ
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ μ, f.maxGenEigenspace μ
hES : ES ≤ ⨆ μ, f.maxGenEigenspace μ
h_disjoint : Disjoint ER ES
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
change ⨆ (μ : K), f.maxGenEigenspace μ = ⊤

Goal state after:
case h.succ
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ μ, f.maxGenEigenspace μ
hES : ES ≤ ⨆ μ, f.maxGenEigenspace μ
h_disjoint : Disjoint ER ES
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝ : SMul ↥L ↥φ.carrier := this✝¹.toSMul
this : IsScalarTower (↥L) (↥φ.carrier) E
⊢ s ∈ ↑(extendScalars ⋯)

Tactic:
have := φ.exists_lift_of_splits' (hK s h).1.tower_top ((hK s h).1.minpoly_splits_tower_top' ?_)

Goal state after:
case refine_2
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝² : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝¹ : SMul ↥L ↥φ.carrier := this✝².toSMul
this✝ : IsScalarTower (↥L) (↥φ.carrier) E
this : ∃ y, φ ≤ y ∧ s ∈ y.carrier
⊢ s ∈ ↑(extendScalars ⋯)

case refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝ : SMul ↥L ↥φ.carrier := this✝¹.toSMul
this : IsScalarTower (↥L) (↥φ.carrier) E
⊢ (Polynomial.map (φ.emb.comp (algebraMap ↥L ↥φ.carrier)) (minpoly (↥L) s)).Splits
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
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
⊢ Algebra.IsAlgebraic K ↥(adjoin K S)

Tactic:
by
  rw [← biSup_adjoin_simple, ← iSup_subtype'']
  exact isAlgebraic_iSup fun x ↦ isAlgebraic_adjoin_simple (hS x x.2)

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 := ⋯
this : Module.Finite K (AdjoinRoot p) := ⋯
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)
⊢ (minpoly (↥K⟮(aeval (root p)) g⟯) (root p)).natDegree = g.natDegree

Tactic:
simp [← key₂]

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
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
this✝ : ∃ n, ((toEnd R L M) f ^ n) m = 0
n : ℕ
hn₁ : ¬((toEnd R L M) f ^ n) m = 0
hn₂ : ((toEnd R L M) f ^ (n + 1)) m = 0
this : 0 = ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m
⊢ μ = ↑n

Tactic:
eq_comm,

Goal state after:
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
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
this✝ : ∃ n, ((toEnd R L M) f ^ n) m = 0
n : ℕ
hn₁ : ¬((toEnd R L M) f ^ n) m = 0
hn₂ : ((toEnd R L M) f ^ (n + 1)) m = 0
this : ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m = 0
⊢ μ = ↑n
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₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : ∀ (x : L), ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
x : L
h : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
k : ℕ
hk : (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
this : f ((((toEnd R L M) x - χ x • 1) ^ k) m) = 0
⊢ (((toEnd R L M) x - χ x • 1) ^ k) m = 0

Tactic:
← map_zero f

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₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : ∀ (x : L), ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
x : L
h : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
k : ℕ
hk : (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
this : f ((((toEnd R L M) x - χ x • 1) ^ k) m) = f 0
⊢ (((toEnd R L M) x - χ x • 1) ^ k) m = 0
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h : ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : ↑ty ⊆ Set.range ⇑b
hy : ∑ a ∈ ty, fy a • a = y
⊢ ∑ x ∈ ty, ∑ i ∈ tx, fy x * (fx i * (B i) x) = ∑ x ∈ tx, ∑ i ∈ ty, fx x * (fy i * (B i) x)

Tactic:
Finset.sum_comm

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h : ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : ↑ty ⊆ Set.range ⇑b
hy : ∑ a ∈ ty, fy a • a = y
⊢ ∑ y ∈ tx, ∑ x ∈ ty, fy x * (fx y * (B y) x) = ∑ x ∈ tx, ∑ i ∈ ty, fx x * (fy i * (B i) x)
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: case e'_9
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι K V
⊢ B = B.flip

Tactic:
eq_comm,

Goal state after:
case e'_9
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι K V
⊢ B.flip = B
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
this : (∀ n ∈ N, (Φ n) y = 0) → ∀ n ∈ N, (Φ n) ⁅x, y⁆ = 0
⊢ y ∈ (Φ.orthogonal ↑N).carrier → ⁅x, y⁆ ∈ (Φ.orthogonal ↑N).carrier

Tactic:
simpa only [
        AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
        LinearMap.BilinForm.mem_orthogonal_iff, LieSubmodule.mem_toSubmodule]

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
N : LieSubmodule K L M
| LieSubmodule.map N.incl ⊤

Tactic:
← iSup_genWeightSpace_eq_top' K L N,

Goal state after:
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
N : LieSubmodule K L M
| LieSubmodule.map N.incl (⨆ χ, genWeightSpace ↥N ⇑χ)
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
s : Finset α
hs₁ : ↑s ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ ↑t ⊆ S

Tactic:
refine Set.Subset.trans ?_ hs₁

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
s : Finset α
hs₁ : ↑s ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ ↑t ⊆ ↑s
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
⊢ Nontrivial L

Tactic:
← not_subsingleton_iff_nontrivial

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
⊢ ¬Subsingleton L
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
x : α
i : ℕ
hi : i < count x m
⊢ ∀ ⦃a₂ : m.ToType⦄, (fun x ↦ (x.fst, ↑x.snd)) ⟨x, ⟨i, hi⟩⟩ = (fun x ↦ (x.fst, ↑x.snd)) a₂ → ⟨x, ⟨i, hi⟩⟩ = a₂

Tactic:
⟨y, j, hj⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
x : α
i : ℕ
hi : i < count x m
y : α
j : ℕ
hj : j < count y m
⊢ (fun x ↦ (x.fst, ↑x.snd)) ⟨x, ⟨i, hi⟩⟩ = (fun x ↦ (x.fst, ↑x.snd)) ⟨y, ⟨j, hj⟩⟩ → ⟨x, ⟨i, hi⟩⟩ = ⟨y, ⟨j, hj⟩⟩
Module: Mathlib.Algebra.Lie.Weights.Linear

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
χ : L → R
inst✝ : LinearWeights R L M
x : L
⊢ (toEnd R L ↥(shiftedGenWeightSpace R L M χ)) x =
    (shift R L M χ).conj ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id)

Tactic:
by
  tauto

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
⊢ ∃ yc ∈ H, ∃ yl ∈ lieSpan R L (range b.f), ∃ yu ∈ lieSpan R L (range b.e), yc + yl + yu = ⁅v, z⁆

Tactic:
simpa [LieSubmodule.mem_sup] using! hv' hz

Goal state after:
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
h : f.natDegree = 0
⊢ False

Tactic:
rw [h] at 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 : 0 = n.succ
h : f.natDegree = 0
⊢ False
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
⊢ IsNilpotent A ↔ ∀ (i : ι), ∃ n, (A ^ n).row i = 0

Tactic:
by
  rw [← isNilpotent_transpose_iff, isNilpotent_iff]
  refine ⟨fun h i ↦ ?_, fun h v ↦ ?_⟩
  · obtain ⟨n, hn⟩ := h (Pi.single i 1)
    exact ⟨n, by simpa [← transpose_pow] using hn⟩
  · choose n hn using h
    suffices ∀ i, (A ^ ⨆ j, n j) i = 0 from ⟨⨆ j, n j, by simp [mulVec_eq_sum, this]⟩
    exact fun i ↦ pow_row_eq_zero_of_le (hn i) (Finite.le_ciSup n i)

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
inst✝⁴ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun k ↦ k • χ₁ + χ₂
⊢ Injective f

Tactic:
intro k l hkl

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
inst✝⁴ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun k ↦ k • χ₁ + χ₂
k l : ℕ
hkl : f k = f l
⊢ k = l
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
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ ↑⁅u, x✝⁆ = ↑(⁅f, g⁆ x✝)

Tactic:
LieSubmodule.coe_bracket,

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
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ ⁅u, ↑x✝⁆ = ↑(⁅f, g⁆ x✝)
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
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
x y z : L
⊢ (⁅x, traceForm R L M⁆ y) z = (0 y) z

Tactic:
rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
    LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]

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
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : genWeightSpace M α ≠ ⊥
e : (chainTop α β).IsZero
⊢ genWeightSpace M α = ⊥

Tactic:
← add_zero (α : L → R),

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
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
hα' : genWeightSpace M α ≠ ⊥
e : (chainTop α β).IsZero
⊢ genWeightSpace M (α + 0) = ⊥
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ ↦ α + (β + γ)
⊢ ((killingForm K L) x) y = 0

Tactic:
have hσ : ∀ γ, σ γ ≠ γ := fun γ ↦ by simpa only [σ, ← add_assoc] using add_ne_right.mpr hαβ

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : ↥H → K
x y : L
hx : x ∈ rootSpace H α
hy : y ∈ rootSpace H β
hαβ : α + β ≠ 0
σ : (↥H → K) → ↥H → K := fun γ ↦ α + (β + γ)
hσ : ∀ (γ : ↥H → K), σ γ ≠ γ
⊢ ((killingForm K L) x) y = 0
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : (P.leadingCoeff • u • ↑S P.natDegree).degree = ↑P.natDegree
⊢ tail.degree < ↑n

Tactic:
eq_comm,

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m_1 < n, ∀ ⦃P : R[X]⦄, P ∈ degreeLT R m → P.natDegree = m_1 → P ∈ span R (↑S '' Set.Iio m)
P : R[X]
hP : P ∈ degreeLT R m
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (↑S '' Set.Iio m)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : ↑P.natDegree = (P.leadingCoeff • u • ↑S P.natDegree).degree
⊢ tail.degree < ↑n
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent ((ad K L) x)
this : ⟨x, hx⟩ ∈ LinearMap.ker (traceForm K (↥H) L)
⊢ x = 0

Tactic:
simp only [ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.mem_bot] at this

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent ((ad K L) x)
this : ⟨x, hx⟩ = 0
⊢ x = 0