mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h : Ideal.map (algebraMap R ↥R[x]) I ⊔ Ideal.span {⟨x, ⋯⟩} = ⊤
⊢ ∃ p, p.leadingCoeff - 1 ∈ I ∧ (aeval ⅟x) p = 0

Tactic:
rw [← Ideal.one_eq_top, ← Ideal.add_eq_sup, Ideal.add_eq_one_iff] at h

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h : ∃ i ∈ Ideal.map (algebraMap R ↥R[x]) I, ∃ j ∈ Ideal.span {⟨x, ⋯⟩}, i + j = 1
⊢ ∃ p, p.leadingCoeff - 1 ∈ I ∧ (aeval ⅟x) p = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
⊢ b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]

Tactic:
have H := pb.basis.sum_repr b

Goal state after:
case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : ∑ i, (pb.basis.repr b) i • pb.basis i = b
⊢ b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]
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
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i ⋯
⊢ f (⇑e ∘ ⇑σ) = (f ⇑e • e.det) (⇑e ∘ ⇑σ)

Tactic:
simp [AlternatingMap.map_perm, Basis.det_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b b' b'' : Basis ι A M
⊢ b.det ⇑b' * b'.det ⇑b'' = b.det ⇑b''

Tactic:
have : b'' = (b'.equiv b'' (Equiv.refl ι)).toLinearMap ∘ b' := by
    ext; simp
  conv_rhs =>
    rw [this, Basis.det_comp, det_basis, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: K : Type u_5
inst✝ : Field K
f : K[X]
⊢ finrank K (K[X] ⧸ span {f}) = f.natDegree

Tactic:
by_cases hf : f = 0
  · rw [hf, natDegree_zero,
      ((Submodule.quotEquivOfEqBot _ (by simp)).restrictScalars K).finrank_eq]
    exact finrank_of_not_finite Polynomial.not_finite
  rw [PowerBasis.finrank]
  exact AdjoinRoot.powerBasis_dim hf

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
this : ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
⊢ exp a = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i

Tactic:
by
    dsimp [exp]
    rw [h₁, this, add_zero]

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : L
⊢ -⁅z, ⁅x, y⁆⁆ = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆

Tactic:
rw [leibniz_lie, neg_lie, neg_lie, ← lie_skew x]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : L
⊢ -(⁅⁅z, x⁆, y⁆ + -⁅⁅z, y⁆, x⁆) = - -⁅⁅z, y⁆, x⁆ - - -⁅⁅z, x⁆, y⁆
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ (∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = m) → ∃ x n, ⁅↑x, ↑n⁆ = m

Tactic:
rintro ⟨t, ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩, h⟩

Goal state after:
case mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h : ↑(toModuleHom R L M) (↑(incl I) ⟨x, hx⟩ ⊗ₜ[R] ↑N.incl ⟨n, hn⟩) = m
⊢ ∃ x n, ⁅↑x, ↑n⁆ = m
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
a✝ b✝ : M
hm₁ : a✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
hm₂ : b✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
x : L
⊢ ⁅x, a✝ + b✝⁆ ∈ N

Tactic:
rw [lie_add]

Goal state after:
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
a✝ b✝ : M
hm₁ : a✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
hm₂ : b✝ ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
x : L
⊢ ⁅x, a✝⁆ + ⁅x, b✝⁆ ∈ N
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
k : ℕ
⊢ derivedSeries R L k = ⊥ → derivedSeries R L' k = ⊥

Tactic:
hk

Goal state after:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ derivedSeries R L' k = ⊥
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
⊢ derivedSeries R L' k = ⊥ → derivedSeries R L k = ⊥

Tactic:
hk

Goal state after:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ derivedSeries R L k = ⊥
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ LieIdeal.map f (derivedSeries R L' k) = ⊥

Tactic:
hk

Goal state after:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ LieIdeal.map f ⊥ = ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
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✝ : IsNilpotent L M
h : 1 < nilpotencyLength L M
hk : nilpotencyLength L M = 0
⊢ (match 0 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1

Tactic:
hk

Goal state after:
case zero
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✝ : IsNilpotent L M
h : 1 < 0
hk : nilpotencyLength L M = 0
⊢ (match 0 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1
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
inst✝ : IsNilpotent L M
h : 1 < nilpotencyLength L M
k : ℕ
hk : nilpotencyLength L M = k + 1
⊢ (match k + 1 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1

Tactic:
hk

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
inst✝ : IsNilpotent L M
k : ℕ
h : 1 < k + 1
hk : nilpotencyLength L M = k + 1
⊢ (match k + 1 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1
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✝¹ : LieModule R L M
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
hfg : ∀ (x : L) (m : ↥M₁), ⁅f x, g m⁆ = g ⁅x, m⁆
⊢ IsNilpotent L ↥M₁

Tactic:
exact (Submodule.inclusion_injective h₁).lieModuleIsNilpotent hfg

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝⁷ : Monoid M
G : Type u
inst✝⁶ : Group G
K : Type u_1
F : Type v
inst✝⁵ : Field F
inst✝⁴ : MulSemiringAction M F
inst✝³ : MulSemiringAction G F
m✝ : M
inst✝² : Field K
inst✝¹ : Algebra K F
inst✝ : SMulCommClass M K F
m : M
f : ↥(subfield M F)
f' : F
⊢ m • ↑f * m • f' = ↑f * m • f'

Tactic:
f.prop m

Goal state after:
M : Type u
inst✝⁷ : Monoid M
G : Type u
inst✝⁶ : Group G
K : Type u_1
F : Type v
inst✝⁵ : Field F
inst✝⁴ : MulSemiringAction M F
inst✝³ : MulSemiringAction G F
m✝ : M
inst✝² : Field K
inst✝¹ : Algebra K F
inst✝ : SMulCommClass M K F
m : M
f : ↥(subfield M F)
f' : F
⊢ ↑f * m • f' = ↑f * m • f'
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥

Tactic:
hk

Goal state after:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ LieIdeal.map f ⊥ = ⊥
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 • l x - l x) • (toFun G F) x) g'

Tactic:
Finset.sum_apply

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
| ∑ c ∈ s, ((g • l c - l c) • (toFun G F) c) g'
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
H : minpoly G F x = 1
this : Polynomial.eval₂ (subfield G F).subtype x (minpoly G F x) = 0
⊢ 1 = 0

Tactic:
by rwa [H, Polynomial.eval₂_one] at this

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
S T : IntermediateField F E
⊢ (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield

Tactic:
← S.toSubfield.closure_eq,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
⊢ (S ⊔ T).toSubfield = Subfield.closure ↑S.toSubfield ⊔ T.toSubfield
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ ∃ z, z ^ n = x

Tactic:
use z

Goal state after:
case h
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
n : ℕ
hn : 0 < n
this : (X ^ n - C x).degree ≠ 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ z ^ n = x
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
⊢ ∀ (a b : Lifts F E K),
    (∃ (h : a.carrier ≤ b.carrier), ∀ (x : ↥a.carrier), b.emb ((inclusion h) x) = a.emb x) →
      (∃ (h : b.carrier ≤ a.carrier), ∀ (x : ↥b.carrier), a.emb ((inclusion h) x) = b.emb x) → a = b

Tactic:
by
    rintro ⟨L₁, e₁⟩ ⟨L₂, e₂⟩ ⟨h₁₂, h₁₂'⟩ ⟨h₂₁, h₂₁'⟩
    obtain rfl : L₁ = L₂ := h₁₂.antisymm h₂₁
    congr
    exact AlgHom.ext h₂₁'

Goal state after:
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 : Lifts F E K
x : F
⊢ L.emb ((inclusion ⋯) ((botEquiv F E).symm x)) = (Algebra.ofId F K) ((botEquiv F E) ((botEquiv F E).symm x))

Tactic:
AlgEquiv.apply_symm_apply

Goal state after:
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 : Lifts F E K
x : F
⊢ L.emb ((inclusion ⋯) ((botEquiv F E).symm x)) = (Algebra.ofId F K) x
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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb

Tactic:
AlgHom.ext_iff

Goal state after:
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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), ∀ (x : ↥L₁.carrier), (L₂.emb.comp (inclusion ⋯)) x = L₁.emb x
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
h_ne : C k - p ≠ 0
lead_ne : (C k - p).leadingCoeff ≠ 0
lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))
p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p
r : 𝕜
r_mem : r ∈ σ a
r_ev : eval r (C k - p) = 0
⊢ k = (fun x ↦ eval x p) r

Tactic:
by simpa [eval_sub, eval_C, sub_eq_zero] using r_ev

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

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
⊢ (aeval 0) 0 = 0 ∧ (aeval 0) q = 0

Tactic:
h.right,

Goal state after:
case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
⊢ (aeval 0) 0 = 0 ∧ (aeval 0) 0 = 0
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case pos
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional K ↥E1
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2

pp: case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : ¬FiniteDimensional K ↥E1
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2

Tactic:
· have := E1.toSubalgebra.finrank_sup_le_of_free E2.toSubalgebra
    change _ ≤ finrank K E1 * finrank K E2 at this
    rwa [← sup_toSubalgebra_of_left] at this

Goal state after:
case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : ¬FiniteDimensional K ↥E1
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅-h, e⁆ = -(2 • e)

Tactic:
by rw [neg_lie, neg_inj, ht.lie_h_e_nsmul]

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

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.IsCartanSubalgebra → H.toLieSubmodule.IsUcsLimit

pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.toLieSubmodule.IsUcsLimit → H.IsCartanSubalgebra

Tactic:
· intro h
    have h₁ : LieRing.IsNilpotent H := by infer_instance
    obtain ⟨k, hk⟩ := H.toLieSubmodule.isNilpotent_iff_exists_self_le_ucs.mp h₁
    replace hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥ :=
      le_antisymm hk
        (LieSubmodule.ucs_le_of_normalizer_eq_self H.normalizer_eq_self_of_isCartanSubalgebra k)
    refine ⟨k, fun l hl => ?_⟩
    rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk,
      LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]

Goal state after:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.toLieSubmodule.IsUcsLimit → H.IsCartanSubalgebra
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case pos.add
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hy✝ : y✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hv : ⁅u, x✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hw : ⁅u, y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅u, x✝ + y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
rw [lie_add]

Goal state after:
case pos.add
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hy✝ : y✝ ∈ ⨆ i ∈ s, genWeightSpace M i
hv : ⁅u, x✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hw : ⁅u, y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅u, x✝⁆ + ⁅u, y✝⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case h
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
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0

Tactic:
hk

Goal state after:
case h
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
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case add
ι : 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 z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x u v : L
hx✝ : u ∈ lieSpan R L (range b.f)
hy✝ : v ∈ lieSpan R L (range b.f)
hu : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅b.e i, u + v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
rw [lie_add]

Goal state after:
case add
ι : 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 z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x u v : L
hx✝ : u ∈ lieSpan R L (range b.f)
hy✝ : v ∈ lieSpan R L (range b.f)
hu : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅b.e i, u⁆ + ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie
ι : 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 z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x u v : L
hu : u ∈ lieSpan R L (range b.f)
hv : v ∈ lieSpan R L (range b.f)
hu' : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv' : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
w₁ : L
hw₁ : w₁ ∈ H
w₂ : L
hw₂ : w₂ ∈ b.borelLower
hwu : w₁ + w₂ = ⁅b.e i, u⁆
w₃ : L
hw₃ : w₃ ∈ H
w₄ : L
hw₄ : w₄ ∈ b.borelLower
hwv : w₃ + w₄ = ⁅b.e i, v⁆
⊢ ⁅w₁, v⁆ + ⁅w₂, v⁆ + ⁅u, w₃⁆ + ⁅u, w₄⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
apply add_mem

Goal state after:
case lie.a
ι : 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 z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x u v : L
hu : u ∈ lieSpan R L (range b.f)
hv : v ∈ lieSpan R L (range b.f)
hu' : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv' : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
w₁ : L
hw₁ : w₁ ∈ H
w₂ : L
hw₂ : w₂ ∈ b.borelLower
hwu : w₁ + w₂ = ⁅b.e i, u⁆
w₃ : L
hw₃ : w₃ ∈ H
w₄ : L
hw₄ : w₄ ∈ b.borelLower
hwv : w₃ + w₄ = ⁅b.e i, v⁆
⊢ ⁅w₁, v⁆ + ⁅w₂, v⁆ + ⁅u, w₃⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

case lie.a
ι : 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 z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x u v : L
hu : u ∈ lieSpan R L (range b.f)
hv : v ∈ lieSpan R L (range b.f)
hu' : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv' : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
w₁ : L
hw₁ : w₁ ∈ H
w₂ : L
hw₂ : w₂ ∈ b.borelLower
hwu : w₁ + w₂ = ⁅b.e i, u⁆
w₃ : L
hw₃ : w₃ ∈ H
w₄ : L
hw₄ : w₄ ∈ b.borelLower
hwv : w₃ + w₄ = ⁅b.e i, v⁆
⊢ ⁅u, w₄⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ Disjoint (↑I) (Φ.orthogonal ↑I)

Tactic:
← orthogonal_toSubmodule _ hΦ_inv,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ Disjoint ↑I ↑(orthogonal Φ hΦ_inv I)