mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : CommRing M
inst✝³ : Algebra R K
inst✝² : Algebra R M
inst✝¹ : Algebra K M
inst✝ : IsScalarTower R K M
x : M
int : IsIntegral R x
f : K →+* L
h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits
⊢ Polynomial.map f (minpoly K x) ∣ Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)

Tactic:
rw [← map_map, map_dvd_map']

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : CommRing M
inst✝³ : Algebra R K
inst✝² : Algebra R M
inst✝¹ : Algebra K M
inst✝ : IsScalarTower R K M
x : M
int : IsIntegral R x
f : K →+* L
h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits
⊢ minpoly K x ∣ Polynomial.map (algebraMap R K) (minpoly R x)
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit ((aeval a) (Multiset.map (fun x ↦ X - C x) p.roots).prod)
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
rw [← Multiset.prod_toList, map_list_prod] at h

Goal state after:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (List.map (⇑(aeval a)) (Multiset.map (fun x ↦ X - C x) p.roots).toList).prod
⊢ ∃ k ∈ σ a, eval k p = 0
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: M : Type w
inst✝¹ : Field M
inst✝ : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x : M
⊢ ∃ a, (fun x ↦ eval x p) a = x

Tactic:
have ⟨y, hy⟩ := (IsAlgClosed.splits (p - C x)).exists_eval_eq_zero <| by
      simpa only [degree_sub_C hp] using hp.ne'

Goal state after:
M : Type w
inst✝¹ : Field M
inst✝ : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x y : M
hy : eval y (p - C x) = 0
⊢ ∃ a, (fun x ↦ eval x p) a = x
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case inr
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
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = adjoin F (↑(↑π).carrier ∪ ↑S)
π₁ π₂ : ↑c
this : ∀ (π₁ π₂ : ↑c), π₁ ≤ π₂ → (fun x1 x2 ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun x1 x2 ↦ x1 ≤ x2) (θ π₂) (θ π₁)
h : ¬π₁ ≤ π₂
⊢ (fun x1 x2 ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun x1 x2 ↦ x1 ≤ x2) (θ π₂) (θ π₁)

Tactic:
exact (this _ _ <| (hc.total π₁.2 π₂.2).resolve_left h).symm

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

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹⁵ : Field K
inst✝¹⁴ : Field J
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Field L
inst✝¹⁰ : Field M
inst✝⁹ : Algebra R M
inst✝⁸ : IsTorsionFree R M
inst✝⁷ : IsAlgClosure R M
inst✝⁶ : Algebra K M
inst✝⁵ : IsAlgClosure K M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
this✝⁵ : Algebra R S := hSR.symm.toRingHom.toAlgebra
this✝⁴ : Algebra S R := hSR.toRingHom.toAlgebra
this✝³ : Algebra R L := ((algebraMap S L).comp (algebraMap R S)).toAlgebra
this✝² : IsScalarTower R S L
this✝¹ : IsScalarTower S R L
this✝ : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
x : S
⊢ (equivOfAlgebraic' R S L M) ((algebraMap S L) x) = (algebraMap R M) (hSR x)

Tactic:
conv_lhs => rw [← hSR.symm_apply_apply x]

Goal state after:
k : Type u
inst✝¹⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝¹⁵ : Field K
inst✝¹⁴ : Field J
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Field L
inst✝¹⁰ : Field M
inst✝⁹ : Algebra R M
inst✝⁸ : IsTorsionFree R M
inst✝⁷ : IsAlgClosure R M
inst✝⁶ : Algebra K M
inst✝⁵ : IsAlgClosure K M
inst✝⁴ : Algebra S L
inst✝³ : IsTorsionFree S L
inst✝² : IsAlgClosure S L
inst✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
this✝⁵ : Algebra R S := hSR.symm.toRingHom.toAlgebra
this✝⁴ : Algebra S R := hSR.toRingHom.toAlgebra
this✝³ : Algebra R L := ((algebraMap S L).comp (algebraMap R S)).toAlgebra
this✝² : IsScalarTower R S L
this✝¹ : IsScalarTower S R L
this✝ : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
x : S
⊢ (equivOfAlgebraic' R S L M) ((algebraMap S L) (hSR.symm (hSR x))) = (algebraMap R M) (hSR 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
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
⊢ False

Tactic:
have := finiteDimensional_adjoin (S := {α}) fun _ _ ↦ ((alg.tower_top ϕ.carrier).isIntegral).1 _

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
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
⊢ False
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
h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1
⊢ ⊥ = ⊤

Tactic:
ext y
  rw [iff_true_right IntermediateField.mem_top]
  exact finrank_adjoin_simple_eq_one_iff.mp (h y)

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
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
⊢ InjOn ⇑g ↑((f.genEigenspace μ) k)

Tactic:
apply LinearMap.injOn_of_disjoint_ker subset_rfl

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₀ : ℕ := ⋯
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
⊢ Disjoint ((f.genEigenspace μ) k) (LinearMap.ker g)
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
this : Fact (Irreducible f)
e : g.natDegree = 0
⊢ minpoly K (root f) = f

Tactic:
AdjoinRoot.minpoly_root hf.ne_zero,

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
this : Fact (Irreducible f)
e : g.natDegree = 0
⊢ f * C f.leadingCoeff⁻¹ = f
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
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this : iSupIndep fun x ↦ (f.genEigenspace x) k
aux : ∀ μ' ∈ m.support.erase μ, (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k
⊢ Disjoint ((f.genEigenspace μ) k)
    ((m.support.erase μ).sup fun i ↦ LinearMap.ker ((f - (algebraMap K (End K V)) i) ^ l₀))

Tactic:
have := Finset.supIndep_iff_disjoint_erase.mp (this.supIndep' m.support) μ hμ

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
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this✝ : iSupIndep fun x ↦ (f.genEigenspace x) k
aux : ∀ μ' ∈ m.support.erase μ, (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k
this : Disjoint ((f.genEigenspace μ) k) ((m.support.erase μ).sup fun x ↦ (f.genEigenspace x) k)
⊢ Disjoint ((f.genEigenspace μ) k)
    ((m.support.erase μ).sup fun i ↦ LinearMap.ker ((f - (algebraMap K (End K V)) i) ^ l₀))
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
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
h_inj : Injective ⇑p.subtype
this : ⊤ = Submodule.comap p.subtype (Submodule.map p.subtype (⨆ i, (genEigenspace (LinearMap.restrict f h) i) k))
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤

Tactic:
Submodule.comap_map_eq_of_injective h_inj

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
k : ℕ∞
h : ∀ x ∈ p, f x ∈ p
h' : ⨆ μ, (f.genEigenspace μ) k = ⊤
h_inj : Injective ⇑p.subtype
this : ⊤ = ⨆ i, (genEigenspace (LinearMap.restrict f h) i) k
⊢ ⨆ μ, (genEigenspace (LinearMap.restrict f h) μ) k = ⊤
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : LieSubmodule.ucs (k + 1) ⊥ = H.toLieSubmodule
⊢ H.normalizer = H

Tactic:
rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : H.toLieSubmodule.normalizer = H.toLieSubmodule
⊢ H.normalizer = H
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
⊢ (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H

Tactic:
refine le_antisymm ?_ (LieSubalgebra.le_normalizer _)

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
⊢ (zeroRootSubalgebra R L H).normalizer ≤ zeroRootSubalgebra R L H
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
⊢ ∑ y ∈ tx, ∑ x ∈ ty, fy x * (fx y * (B y) x) = ∑ x ∈ tx, ∑ i ∈ ty, fx x * (fy i * (B i) x)

Tactic:
refine Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)

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
b₁ : M
h₁ : b₁ ∈ tx
b₂ : M
h₂ : b₂ ∈ ty
⊢ fy b₂ * (fx b₁ * (B b₁) b₂) = fx b₁ * (fy b₂ * (B b₂) b₁)
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
⊢ IsLieAbelian ↥(lieSpan R L (range b.h))

Tactic:
isLieAbelian_lieSpan_iff

Goal state after:
ι : 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
⊢ ∀ x ∈ range b.h, ∀ y ∈ range b.h, ⁅x, y⁆ = 0
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:
← add_assoc

Goal state after:
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
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
⊢ IsCompl I (orthogonal Φ hΦ_inv I)

Tactic:
rw [← LieSubmodule.isCompl_toSubmodule]

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
⊢ IsCompl ↑I ↑(orthogonal Φ hΦ_inv I)
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
⊢ IsCompl ↑I ↑(orthogonal Φ hΦ_inv I)

Tactic:
exact orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

Goal state after:
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
⊢ IsCompl (LieIdeal.toLieSubalgebra K L I).toSubmodule (Φ.orthogonal (LieIdeal.toLieSubalgebra K L I).toSubmodule)

Tactic:
exact orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

Goal state after:
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✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
⊢ ∀ (x m : ↥J), ⁅x, m⁆ = 0

Tactic:
intro x y

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
⊢ ⁅x, y⁆ = 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✝ : IsKilling K L
x : ↥H
hx : x ∈ corootSpace 0
⊢ x ∈ ⊥

Tactic:
suffices {x | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} = {0} by simpa [mem_corootSpace, this] using hx

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 : ↥H
hx : x ∈ corootSpace 0
⊢ {x | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} = {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✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
x y : ↥H
hx : x ∈ Weight.ker
hy : y ∈ K ∙ coroot α
⊢ ((traceForm K (↥H) L) x) y = 0

Tactic:
rw [← coe_corootSpace_eq_span_singleton, LieSubmodule.mem_toSubmodule, mem_corootSpace'] at hy

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
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
x y : ↥H
hx : x ∈ Weight.ker
hy : y ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = ↑x}
⊢ ((traceForm K (↥H) L) x) y = 0
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
⊢ iSup ![H.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤

Tactic:
suffices H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper = ⊤ by simpa
  refine eq_top_iff.mpr fun x hx ↦ ?_
  replace hx : x ∈ lieSpan R L (range b.e ∪ range b.f) := by simp [b.span_ef]
  induction hx using lieSpan_induction with
  | mem u hu =>
    rcases (mem_union _ _ _).mpr hu with hu | hu
    · exact LieSubmodule.mem_sup_right <| subset_lieSpan hu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| subset_lieSpan hu
  | zero => simp
  | add u v _ _ hu hv => exact add_mem hu hv
  | smul t u _ hu => exact SMulMemClass.smul_mem t hu
  | lie u v _ _ hu hv =>
    obtain ⟨yc, hyc, yl, hyl, yu, hyu, rfl⟩ :
        ∃ᵉ (yc ∈ H) (yl ∈ lieSpan R L (range b.f)) (yu ∈ lieSpan R L (range b.e)),
          yc + yl + yu = u := by simpa [LieSubmodule.mem_sup] using! hu
    obtain ⟨zc, hzc, zl, hzl, zu, hzu, rfl⟩ :
        ∃ᵉ (zc ∈ H) (zl ∈ lieSpan R L (range b.f)) (zu ∈ lieSpan R L (range b.e)),
          zc + zl + zu = v := by simpa [LieSubmodule.mem_sup] using! hv
    simp only [lie_add, add_lie, ← add_assoc]
    repeat apply add_mem
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_left <| lie_mem _ hyc hzc
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨zc, hzc⟩) hyl
    · rw [← lie_skew, neg_mem_iff]
      exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨zc, hzc⟩) hyu
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <|
        b.borelLower.lie_mem (x := ⟨yc, hyc⟩) hzl
    · exact LieSubmodule.mem_sup_left <| LieSubmodule.mem_sup_right <| lie_mem _ hyl hzl
    · exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl
    · exact LieSubmodule.mem_sup_right <| b.borelUpper.lie_mem (x := ⟨yc, hyc⟩) hzu
    · rw [← lie_skew, neg_mem_iff]
      exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hzu hyl
    · exact LieSubmodule.mem_sup_right <| lie_mem _ hyu hzu

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.reflectionPerm i) ((P.reflectionPerm i) j) = j

Tactic:
by
  apply P.root.injective
  simp only [root_reflectionPerm, reflection_same]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
j : ι
s : Set ι
hj : ∀ i ∈ s, P.IsOrthogonal j i
x : M
hx : x ∈ span R (⇑P.root '' s)
⊢ IsFixedPt (⇑(P.reflection j)) x

Tactic:
rw [IsFixedPt]
  induction hx using Submodule.span_induction with
  | zero => rw [map_zero]
  | add u v hu hv hu' hv' => rw [map_add, hu', hv']
  | smul t u hu hu' => rw [map_smul, hu']
  | mem u hu =>
      obtain ⟨i, his, rfl⟩ := hu
      exact IsOrthogonal.reflection_apply_right <| hj i his

Goal state after: