mathlib-initiative/mathlib-tactics huggingface dataset:
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
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∀ (i : ↑(insert ⊥ c)), (↑i).carrier ≤ ⨆ i, (↑i).carrier

Tactic:
rintro ⟨i, rfl | hi⟩

Goal state after:
case inl
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
⊢ (↑⟨⊥, ⋯⟩).carrier ≤ ⨆ i, (↑i).carrier

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
i : Lifts F E K
hi : i ∈ c
⊢ (↑⟨i, ⋯⟩).carrier ≤ ⨆ i, (↑i).carrier
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u
inst✝¹⁵ : Field K
L : Type v
M : Type w
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : Field M
inst✝¹¹ : Algebra K M
inst✝¹⁰ : IsAlgClosed M
inst✝⁹ : Algebra.IsAlgebraic K L
R : Type u
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type v
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
inst✝³ : Algebra R M
inst✝² : IsTorsionFree R S
inst✝¹ : IsTorsionFree R M
inst✝ : Algebra.IsAlgebraic R S
this✝² : IsDomain R := Function.Injective.isDomain (algebraMap R S) (FaithfulSMul.algebraMap_injective R S)
this✝¹ : Algebra (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
this✝ : IsScalarTower R (FractionRing R) (FractionRing S)
this : Algebra.IsAlgebraic R (FractionRing S)
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)

Tactic:
exact ⟨fun _ ↦ (IsFractionRing.isAlgebraic_iff R (FractionRing R) (FractionRing S)).1
    (Algebra.IsAlgebraic.isAlgebraic _)⟩

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
⊢ (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra

Tactic:
by
  cases isEmpty_or_nonempty ι
  · simp_rw [iSup_of_empty, bot_toSubalgebra]
  · exact SetLike.ext' ((coe_iSup_of_directed dir).trans (Subalgebra.coe_iSup_of_directed dir).symm)

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

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a (derivative f) + rootMultiplicity a g

Tactic:
have h0 : 0 < f.rootMultiplicity a := (rootMultiplicity_pos hf0).2 haf
    rw [derivative_rootMultiplicity_of_root haf]
    intro h
    calc rootMultiplicity a f
        = rootMultiplicity a f - 1 + 1 := (Nat.sub_add_cancel (Nat.succ_le_iff.1 h0)).symm
      _ ≤ rootMultiplicity a f - 1 + rootMultiplicity a g := add_le_add le_rfl (Nat.succ_le_iff.1
        ((rootMultiplicity_pos hg0).2 (h haf)))

Goal state after:
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
⊢ Module.rank (↥⊥) E = Module.rank F E

Tactic:
← rank_mul_rank F (⊥ : IntermediateField F E) E,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Module.rank (↥⊥) E = Module.rank F ↥⊥ * Module.rank (↥⊥) E
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
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this✝ : Fact (Irreducible (minpoly F α))
this : F⟮α⟯.toSubfield ≤ (F⟮α⟯.toSubfield.subtype.comp f).fieldRange
x : ↥F⟮α⟯
⊢ ∃ a, (AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯) a = x

Tactic:
obtain ⟨y, hy⟩ := this (Subtype.mem x)

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this✝ : Fact (Irreducible (minpoly F α))
this : F⟮α⟯.toSubfield ≤ (F⟮α⟯.toSubfield.subtype.comp f).fieldRange
x : ↥F⟮α⟯
y : AdjoinRoot (minpoly F α)
hy : (F⟮α⟯.toSubfield.subtype.comp f) y = ↑x
⊢ ∃ a, (AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯) a = x
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := ⋯
this : Fact (Irreducible (minpoly F α))
⊢ Function.Surjective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
suffices F⟮α⟯.toSubfield ≤ RingHom.fieldRange (F⟮α⟯.toSubfield.subtype.comp f) by
          intro x
          obtain ⟨y, hy⟩ := this (Subtype.mem x)
          exact ⟨y, Subtype.ext hy⟩

Goal state after:
case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (minpoly F α))
⊢ F⟮α⟯.toSubfield ≤ (F⟮α⟯.toSubfield.subtype.comp f).fieldRange
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (i j : ι) (φ : R), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
l : ι
χ : ι → R
x : M
hx : ∀ (i : ι), x ∈ (f i).maxGenEigenspace (χ i)
⊢ ∀ (i : ι), (f l) x ∈ (f i).maxGenEigenspace (χ i)

Tactic:
exact fun i ↦ h l i (χ i) (hx i)

Goal state after:
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₀) ⋯)
      (((f - (algebraMap K (End K V)) μ') ^ l₀) (m μ')) =
    0

Tactic:
hl₀,

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
⊢ (((m.support.erase μ).erase μ').noncommProd (fun μ ↦ (f - (algebraMap K (End K V)) μ) ^ l₀) ⋯) 0 = 0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case 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 : L
hy : y ∈ span R {e, f, h}
u : L
hu : u ∈ {e, f, h}
⊢ ⁅u, y⁆ ∈ span R {e, f, h}

Tactic:
induction hy using span_induction with

Goal state after:
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
x : L
⊢ posFittingCompOf R M x ≤ ⨆ x, posFittingCompOf R M x

Tactic:
exact le_iSup (posFittingCompOf R M) x

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

Goal state before:
pp: 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
b : Basis ι K V
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0

Tactic:
@eq_comm _ i j

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
b₁ : B.IsRefl
W : Submodule K V
⊢ finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)

Tactic:
rw [orthogonal_top_eq_ker b₁]
  exact finrank_add_finrank_orthogonal' _

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

Goal state before:
pp: case a
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⁆ ∈ Submodule.map ↑I.incl ↑J

Tactic:
simp only [Submodule.mem_map, LieSubmodule.mem_toSubmodule, Subtype.exists]
          erw [Submodule.coe_subtype]
          simp only [exists_and_right, exists_eq_right, ha, lie_mem_left, exists_true_left]
          exact lie_mem_right R I J ⟨a, ha⟩ y hy

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x ↦ a = x.1) s.val).card > 0
⊢ ∃ n ≥ (filter (fun x ↦ a = x.1) s.val).card - 1, (a, n) ∈ s

Tactic:
by_contra! h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x ↦ a = x.1) s.val).card > 0
h : ∀ n ≥ (filter (fun x ↦ a = x.1) s.val).card - 1, (a, n) ∉ s
⊢ False
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: case hΦ_refl
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : LieAlgebra K L
inst✝² : IsKilling R L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
⊢ (killingForm K L).IsRefl

pp: case hL
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : LieAlgebra K L
inst✝² : IsKilling R L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
⊢ ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I

Tactic:
· exact (LieModule.traceForm_isSymm K L L).isRefl

Goal state after:
case hL
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : LieAlgebra K L
inst✝² : IsKilling R L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
⊢ ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : ∃ l, ↑l ≤ k ∧ m ∈ ((f - μ • 1) ^ l).ker
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m

Tactic:
obtain ⟨l, -, hm⟩ := hm

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
hm : m ∈ ((f - μ • 1) ^ l).ker
⊢ g m = μ • m
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✝³ : Free R M
inst✝² : Module.Finite R M
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Algebra R A
x✝¹ x✝ : L
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry (traceForm A (A ⊗[R] L) (A ⊗[R] M))) 1) x✝¹))
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry (LinearMap.BilinForm.baseChange A (traceForm R L M))) 1) x✝¹))
        1)
      x✝

Tactic:
simp [traceForm_apply_apply, ← LinearMap.baseChange_comp, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: L : Type u_2
inst✝¹⁰ : LieRing L
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
K : Type u_4
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L
H : LieSubalgebra K L
inst✝⁴ : LieRing.IsNilpotent ↥H
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : IsTriangularizable K (↥H) M
inst✝ : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
⊢ ∃ n, ((toEnd K L M) x ^ n) m = 0

Tactic:
have hm : m ∈ ⨆ χ : LieModule.Weight K H M, genWeightSpace M χ := by
    simp [iSup_genWeightSpace_eq_top' K H M]

Goal state after:
L : Type u_2
inst✝¹⁰ : LieRing L
M : Type u_3
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
K : Type u_4
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieAlgebra K L
H : LieSubalgebra K L
inst✝⁴ : LieRing.IsNilpotent ↥H
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : IsTriangularizable K (↥H) M
inst✝ : FiniteDimensional K M
x : L
χ : ↥H → K
hχ : χ ≠ 0
hx : x ∈ rootSpace H χ
m : M
hm : m ∈ ⨆ χ, genWeightSpace M ⇑χ
⊢ ∃ n, ((toEnd K L M) x ^ n) m = 0
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✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' : ∀ m ∈ N, (φ x ∘ₗ φ y) m ∈ N
this : ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N
⊢ (trace R M) (φ x ∘ₗ φ y) = (trace R ↥N) ((φ x ∘ₗ φ y).restrict hy')

Tactic:
by
    have : (trace R { x // x ∈ N }) ((φ x ∘ₗ φ y).restrict _) = (trace R M) (φ x ∘ₗ φ y) :=
      (φ x ∘ₗ φ y).trace_restrict_eq_of_forall_mem _ this
    simp [this]

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
inst✝ : Fintype ι
i : ι
x : ↥H
⊢ (b.baseSupp i) x • b.e i = ⁅x, b.e i⁆

Tactic:
obtain ⟨x, hx⟩ := x
  simp only [coe_bracket_of_module]
  have hx' : x ∈ Submodule.span R (range b.h) := by
    rwa [← LieSubalgebra.mem_toSubmodule, b.coe_cartan_eq_span] at hx
  induction hx' using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨j, rfl⟩ := hu
    change b.baseSupp i (b.h' j) • _ = _
    simp [b.lie_h_e, Int.cast_smul_eq_zsmul]
  | zero => change b.baseSupp i 0 • _ = _; simp
  | add u v hu hv hu' hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu hv
    rw [← AddMemClass.mk_add_mk _ u v hu hv]
    simp only [map_add, add_smul, add_lie] at hu' hv' ⊢
    rw [hu', hv']
  | smul t u hu hv' =>
    rw [← coe_cartan_eq_span, LieSubalgebra.mem_toSubmodule] at hu
    rw [← SetLike.mk_smul_mk _ t u hu, map_smul, smul_assoc, hv', smul_lie]

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

Goal state before:
pp: case h
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 f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
hef₀ : ((killingForm K L) e) f ≠ 0
⊢ (2 • (α α')⁻¹ * ((((killingForm K L) e) f)⁻¹ * ((killingForm K L) e) f)) • α' = coroot α

Tactic:
inv_mul_cancel₀ hef₀,

Goal state after:
case h
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 f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
h : ↥H
ht : IsSl2Triple (↑h) e f
key : α h = 2
α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
hef : ⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
hα' : α' = (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
h_eq : h = ((killingForm K L) e) f • α'
hef₀ : ((killingForm K L) e) f ≠ 0
⊢ (2 • (α α')⁻¹ * 1) • α' = coroot α
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
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
hu : u ∈ ⨆ χ ∈ s, rootSpace H χ
⊢ v ∈ ⨆ χ ∈ s, rootSpace H χ

Tactic:
convert! hv

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
inst✝² : Fintype ι
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : IsLieAbelian ↥H := isLieAbelian_cartan b
x u v : L
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : v ∈ lieSpan R L (range b.e)
hv : v ∈ ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s : Set (↥H → R) := {χ | ∃ n, n ≠ 0 ∧ χ = ⇑(∑ i, n i • b.baseSupp i)}
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
e : ↑{n | n ≠ 0} ≃ ↑s := Equiv.ofBijective (fun n ↦ ⟨∑ i, ↑n i • ⇑(b.baseSupp i), ⋯⟩) ⋯
hu : u ∈ ⨆ χ ∈ s, rootSpace H χ
⊢ ⨆ χ ∈ s, rootSpace H χ = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case neg
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
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
⊢ 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)))) •
          ((f y * g z - f z) • x - g z • y) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((g x * f z - g z) • y - f z • x) =
    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)

Tactic:
add_right_comm z

Goal state after:
case neg
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
a✝ :
  ∀ (n : ℕ),
    ((reflection hf * reflection hg) ^ ↑n) z =
      z +
          (Polynomial.eval t (S R ((↑n - 2) / 2)) *
              (Polynomial.eval t (S R ((↑n - 1) / 2)) + Polynomial.eval t (S R ((↑n - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (S R ((↑n - 1) / 2)) *
            (Polynomial.eval t (S R (↑n / 2)) + Polynomial.eval t (S R ((↑n - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
m : ℕ
ht' : t = g x * f y - 2
⊢ z +
        (Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
          ((g x * f z - g z) • y - f z • x) +
      (Polynomial.eval t (S R ((↑m - 2) / 2)) *
          (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
        ((f y * g z - f z) • x - g z • y) =
    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)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : ((S R n).comp (2 * X)).comp (Polynomial.C ⅟2 * X) = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)

Tactic:
simp_rw [comp_assoc, mul_comp, ofNat_comp, X_comp, ← mul_assoc, ← C_eq_natCast, ← C_mul,
    Nat.cast_ofNat, mul_invOf_self', map_one, one_mul, comp_X] at this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : S R n = (U R n).comp (Polynomial.C ⅟2 * X)
⊢ S R n = (U R n).comp (Polynomial.C ⅟2 * X)
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 i : ι
⊢ (P.reflectionPerm ((P.reflectionPerm i) i)) ((P.reflectionPerm i) i) = i

Tactic:
by
    apply P.root.injective
    simp only [root_reflectionPerm, reflection_apply, LinearMap.flip_apply, root_coroot_eq_pairing,
      pairing_same, map_sub, coroot_reflectionPerm, coreflection_apply_self, map_neg, neg_smul,
      sub_neg_eq_add, map_smul, smul_add]
    module

Goal state after: