mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h : finrank F F' = 2
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
have emb : E →ₐ[F] F' := lift

Goal state after:
F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h : finrank F F' = 2
emb : E →ₐ[F] F'
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
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), Module.rank F ↥F⟮x⟯ = 1
⊢ ⊥ = ⊤

Tactic:
ext y

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤
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

Goal state after:
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
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ minpoly F (AdjoinSimple.gen F α) = minpoly F α

Tactic:
← minpoly.algebraMap_eq (algebraMap F⟮α⟯ E).injective,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ minpoly F ((algebraMap (↥F⟮α⟯) E) (AdjoinSimple.gen F α)) = minpoly F α
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case neg
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
hl₀ : ((f - (algebraMap K (End K V)) μ') ^ l₀) (m μ') = 0
this :
  ((m.support.erase μ).erase μ').noncommProd (fun μ ↦ (f - (algebraMap K (End K V)) μ) ^ l₀) ⋯ *
      (f - (algebraMap K (End K V)) μ') ^ l₀ =
    g
⊢ (((m.support.erase μ).erase μ').noncommProd (fun μ ↦ (f - (algebraMap K (End K V)) μ) ^ l₀) ⋯) 0 = 0

Tactic:
_root_.map_zero

Goal state after:
case neg
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
hl₀ : ((f - (algebraMap K (End K V)) μ') ^ l₀) (m μ') = 0
this :
  ((m.support.erase μ).erase μ').noncommProd (fun μ ↦ (f - (algebraMap K (End K V)) μ) ^ l₀) ⋯ *
      (f - (algebraMap K (End K V)) μ') ^ l₀ =
    g
⊢ 0 = 0
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:
← biSup_adjoin_simple,

Goal state after:
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 ↥(⨆ x ∈ S, K⟮x⟯)
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
inst✝ : Finite ↑S
hS : ∀ x ∈ S, IsIntegral K x
⊢ FiniteDimensional K ↥(adjoin K S)

Tactic:
← biSup_adjoin_simple,

Goal state after:
K : Type u
inst✝³ : Field K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
S : Set L
inst✝ : Finite ↑S
hS : ∀ x ∈ S, IsIntegral K x
⊢ FiniteDimensional K ↥(⨆ x ∈ S, K⟮x⟯)
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem
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
t : IsSl2Triple h e f
x y u v : L
hu : u = e ∨ u = f ∨ u = h
hv : v = e ∨ v = f ∨ v = h
⊢ ⁅u, v⁆ ∈ span R {e, f, h}

Tactic:
rcases hu with rfl | rfl | rfl <;>
        rcases hv with rfl | rfl | rfl <;> (try simp only [lie_self, zero_mem])

Goal state after:
case mem.mem.inl.inr.inl
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 x y u v : L
t : IsSl2Triple h u v
__spread✝⁻⁰ : Submodule R L := span R {u, v, h}
⊢ ⁅u, v⁆ ∈ span R {u, v, h}

case mem.mem.inl.inr.inr
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
f x y u v : L
t : IsSl2Triple v u f
__spread✝⁻⁰ : Submodule R L := span R {u, f, v}
⊢ ⁅u, v⁆ ∈ span R {u, f, v}

case mem.mem.inr.inl.inl
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 x y u v : L
t : IsSl2Triple h v u
__spread✝⁻⁰ : Submodule R L := span R {v, u, h}
⊢ ⁅u, v⁆ ∈ span R {v, u, h}

case mem.mem.inr.inl.inr.inr
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
e x y u v : L
t : IsSl2Triple v e u
__spread✝⁻⁰ : Submodule R L := span R {e, u, v}
⊢ ⁅u, v⁆ ∈ span R {e, u, v}

case mem.mem.inr.inr.inl
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
f x y u v : L
t : IsSl2Triple u v f
__spread✝⁻⁰ : Submodule R L := span R {v, f, u}
⊢ ⁅u, v⁆ ∈ span R {v, f, u}

case mem.mem.inr.inr.inr.inl
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
e x y u v : L
t : IsSl2Triple u e v
__spread✝⁻⁰ : Submodule R L := span R {e, v, u}
⊢ ⁅u, v⁆ ∈ span R {e, v, u}
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case inr
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
⊢ IsCompl M₀ M₁

Tactic:
set M₁ₓ := posFittingCompOf R M x

Goal state after:
case inr
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
⊢ IsCompl M₀ M₁
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
⊢ LieSubmodule.map M₀ₓ.incl M₀ₓ₁ ⊔ M₁ₓ = M₁

Tactic:
apply le_antisymm <| sup_le_iff.mpr
        ⟨map_posFittingComp_le _, posFittingCompOf_le_posFittingComp R L M x⟩

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := ⋯
M₁ : LieSubmodule R L M := ⋯
x : L
M₀ₓ : LieSubmodule R L M := ⋯
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := ⋯
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := ⋯
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := ⋯
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
h₃ : LieSubmodule.map M₀ₓ.incl M₀ₓ₀ = M₀
⊢ posFittingComp R L M ≤ LieSubmodule.map M₀ₓ.incl (posFittingComp R L ↥M₀ₓ) ⊔ posFittingCompOf R M x
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem.inr
ι : 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 : L
j : ι
hij : i ≠ j
⊢ ⁅b.e i, b.f j⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
· simp [b.lie_e_f_ne _ _ hij]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : B z = 0
x : M
hx : x ∈ p
⊢ ((B.restrict p) ⟨z, hz⟩) ⟨x, hx⟩ = 0 ⟨x, hx⟩

Tactic:
simpa using LinearMap.congr_fun h x

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
hT : ∅ ⊆ S
ha : IsAtom (sSup ∅)
haS : sSup ∅ ≤ sSup S
⊢ sSup ∅ ∈ S

Tactic:
simp only [sSup_empty] at ha
    exact (ha.1 rfl).elim

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
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
⊢ B.orthogonal W = ⊥

Tactic:
rw [h, eq_bot_iff]

Goal state after:
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
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
⊢ B.orthogonal ⊤ ≤ ⊥
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 : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
⊢ ⁅a + b, ↑I.incl y⁆ ∈ (Submodule.map ↑I.incl ↑J).carrier

Tactic:
simp only [Submodule.carrier_eq_coe, add_lie, SetLike.mem_coe]

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 : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
⊢ ⁅a, ↑I.incl y⁆ + ⁅b, ↑I.incl y⁆ ∈ Submodule.map ↑I.incl ↑J
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m.prod = ∏ x, x.fst

Tactic:
congr
  simp

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m.prod = ∏ x ∈ m.toEnumFinset, x.1

Tactic:
congr
  simp

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

Goal state before:
pp: case inr.left
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := ⋯
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := ⋯
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := ⋯
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ z ∈ sSup ↑s'

Tactic:
simpa only [K, Finset.sup_id_eq_sSup] using hz

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Algebra R A
inst✝⁹ : Module R M₁
inst✝⁸ : Module A M₁
inst✝⁷ : Module R N₁
inst✝⁶ : Module A N₁
inst✝⁵ : SMulCommClass R A M₁
inst✝⁴ : IsScalarTower R A M₁
inst✝³ : SMulCommClass R A N₁
inst✝² : IsScalarTower R A N₁
inst✝¹ : Module R M₂
inst✝ : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ : ∀ (x y : M₁), (B₁ x) y = (B₁ y) x
hB₂ : ∀ (x y : M₂), (B₂ x) y = (B₂ y) x
⊢ ∀ (x y : M₁ ⊗[R] M₂), ((B₁.tmul B₂) x) y = ((B₁.tmul B₂) y) x

Tactic:
isSymm_iff_eq_flip

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Algebra R A
inst✝⁹ : Module R M₁
inst✝⁸ : Module A M₁
inst✝⁷ : Module R N₁
inst✝⁶ : Module A N₁
inst✝⁵ : SMulCommClass R A M₁
inst✝⁴ : IsScalarTower R A M₁
inst✝³ : SMulCommClass R A N₁
inst✝² : IsScalarTower R A N₁
inst✝¹ : Module R M₂
inst✝ : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ : ∀ (x y : M₁), (B₁ x) y = (B₁ y) x
hB₂ : ∀ (x y : M₂), (B₂ x) y = (B₂ y) x
⊢ B₁.tmul B₂ = flip (B₁.tmul B₂)
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
⊢ e.symm x' ∈ LinearMap.ker (killingForm R L)

Tactic:
ext y

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
y : L
⊢ ((killingForm R L) (e.symm x')) y = 0 y
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 : ↥H
hx : x ∈ corootSpace α
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) x) = 0

Tactic:
rw [LieAlgebra.mem_corootSpace'] at hx
  induction hx using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨y, hy, z, hz, hyz⟩ := hu
    let f : Module.End R (genWeightSpaceChain M α χ p q) :=
      { toFun := fun ⟨m, hm⟩ ↦ ⟨⁅(y : L), m⁆,
          lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right M α χ p q hq hy hm⟩
        map_add' := fun _ _ ↦ by simp
        map_smul' := fun t m ↦ by simp }
    let g : Module.End R (genWeightSpaceChain M α χ p q) :=
      { toFun := fun ⟨m, hm⟩ ↦ ⟨⁅(z : L), m⁆,
          lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left M α χ p q hp hz hm⟩
        map_add' := fun _ _ ↦ by simp
        map_smul' := fun t m ↦ by simp }
    have hfg : toEnd R H _ u = ⁅f, g⁆ := by
      ext
      rw [toEnd_apply_apply, LieSubmodule.coe_bracket, LieSubalgebra.coe_bracket_of_module, ← hyz]
      simp only [lie_lie, LieHom.lie_apply, LinearMap.coe_mk, AddHom.coe_mk, Module.End.lie_apply,
        AddSubgroupClass.coe_sub, f, g]
    simp [hfg]
  | zero => simp
  | add => simp_all
  | smul => simp_all

Goal state after:
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 : L
hx : x ∈ rootSpace H α
hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0
⊢ (killingForm K L) x = 0

Tactic:
ext y

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 : L
hx : x ∈ rootSpace H α
hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0
y : L
⊢ ((killingForm K L) x) y = 0 y
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)
⊢ (traceForm K (↥H) L) ⟨x, hx⟩ = 0

Tactic:
ext y

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)
y : ↥H
⊢ ((traceForm K (↥H) L) ⟨x, hx⟩) y = 0 y
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
inst✝³ : LieRing.IsNilpotent L
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hz : z ∈ lowerCentralSeries R L L 1
hzc : z ∈ LieAlgebra.center R L
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
this : (algebraMap R A) ((trace R M) (φ z ∘ₗ φ x)) = 0
⊢ (trace R M) (φ z ∘ₗ φ x) = 0

Tactic:
by
    have that : Module.IsTorsionFree R A := .trans_faithfulSMul R (FractionRing R) A
    rw [← map_zero (algebraMap R A)] at this
    exact FaithfulSMul.algebraMap_injective R A this

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
h : f x = 2
p : Submodule R M
hx : x ∈ p
this : ∀ y ∈ p, (reflection h) y ∈ p
y : M
hy : y ∈ p
⊢ y ∈ Submodule.comap (↑(reflection h)) p

Tactic:
simpa using this y hy

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : R
ht : t = f y * g x - 2
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval t (S R ((↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval t (S R k) ^ 2 + Polynomial.eval t (S R (k + 1)) ^ 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
⊢ (reflection hf * reflection hg * (reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)) *
            (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) *
          (Polynomial.eval t (S R (↑(m + 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)

Tactic:
LinearEquiv.mul_apply,

Goal state after:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
z : M
t : R
ht : t = f y * g x - 2
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ m) z =
    z +
        (Polynomial.eval t (S R ((↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval t (S R k) ^ 2 + Polynomial.eval t (S R (k + 1)) ^ 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
⊢ (reflection hf * reflection hg) (((reflection hf * reflection hg) ^ m) z) =
    z +
        (Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)) *
            (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 3) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑(m + 1) - 1) / 2)) *
          (Polynomial.eval t (S R (↑(m + 1) / 2)) + Polynomial.eval t (S R ((↑(m + 1) - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
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
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
this : h = ((killingForm K L) e) f' • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
⊢ ¬((killingForm K L) e) f' = 0 ∧ ¬α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) = 0

Tactic:
exact ⟨hf, root_apply_cartanEquivDual_symm_ne_zero hα⟩

Goal state after: