mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
this : ⇑H.subtype '' s = {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
⊢ x ∈ corootSpace α ↔ H.subtype x ∈ ⇑H.subtype '' ↑(Submodule.span R s)

Tactic:
rw [mem_image]

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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
this : ⇑H.subtype '' s = {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
⊢ x ∈ corootSpace α ↔ ∃ x_1 ∈ ↑(Submodule.span R s), H.subtype x_1 = H.subtype x
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✝ : IsNilpotent L M
⊢ posFittingComp R L M = ⊥

Tactic:
simp [posFittingComp]

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
⊢ IsLieAbelian ↥H

Tactic:
by
  rw [b.cartan_eq_lieSpan, isLieAbelian_lieSpan_iff]
  rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩
  exact b.lie_h_h i j

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
i j : ι
⊢ - -0 = 0

Tactic:
neg_neg

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
i j : ι
⊢ 0 = 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
i j : ι
⊢ - -(b.A i j • b.f i) = b.A i j • b.f i

Tactic:
neg_neg

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
i j : ι
⊢ b.A i j • b.f i = b.A i j • b.f i
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ (G (a • x)) y = 0 ↔ (G x) y = 0

Tactic:
map_smul

Goal state after:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ (a • G x) y = 0 ↔ (G x) y = 0
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ (G x) (a • y) = 0 ↔ (G x) y = 0

Tactic:
map_smul

Goal state after:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ a • (G x) y = 0 ↔ (G x) y = 0
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ S ⊆ {a | IsAtom a}

Tactic:
exact hS.isAtom

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

Goal state before:
pp: k : Type u_1
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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
t : R
x : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) (t • x) =
    t • (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x

Tactic:
map_smul

Goal state after:
k : Type u_1
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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
t : R
x : L
⊢ t • (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    t • (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: case non_abelian_of_isAtom
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
I : LieIdeal R L
hI₁ : I = ⊤
hI₂ : IsLieAbelian ↥I
⊢ IsLieAbelian L

Tactic:
rwa [hI₁, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI₂

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

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
change algebraMap k _ _ = _; simp_rw [NNRat.cast_def, map_div₀, map_natCast]

Goal state after:
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
inst✝⁵ : IsKilling R L
inst✝⁴ : Module.Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
I : LieIdeal R L
inst✝ : IsLieAbelian ↥I
⊢ I ≤ ⊥

Tactic:
← killingCompl_top_eq_bot

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : IsKilling R L
inst✝⁴ : Module.Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
I : LieIdeal R L
inst✝ : IsLieAbelian ↥I
⊢ I ≤ LieIdeal.killingCompl R L ⊤
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
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
h₁ : MapsTo ⇑g ↑p ↑p
h₂ : MapsTo ⇑(g - (algebraMap R (End R M)) μ) ↑p ↑p
h₃ : MapsTo ⇑(f - g) ↑p ↑p
h₄ : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑p ↑p
hfg : Commute (f - (algebraMap R (End R M)) μ) (f - g)
this : IsNilpotent (LinearMap.restrict (g - (algebraMap R (End R M)) μ) h₂)
⊢ IsFinitelySemisimple (LinearMap.restrict g h₁ - (algebraMap R (End R ↥p)) μ)

Tactic:
simpa using hss.restrict _

Goal state after:
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 : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
⊢ (f.genEigenspace μ) k = f.eigenspace μ

Tactic:
refine le_antisymm (fun m hm ↦ mem_eigenspace_iff.mpr ?_) (f.genEigenspace μ |>.mono ?_)
  · apply apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hm rfl hf
    simp
  · exact Order.one_le_iff_pos.mpr hk

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hp : genWeightSpace M (p • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : y ∈ genWeightSpaceChain M α χ p q
⊢ genWeightSpace M (- -(p • α) + χ) = ⊥

Tactic:
neg_neg

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hp : genWeightSpace M (p • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : y ∈ genWeightSpaceChain M α χ p q
⊢ genWeightSpace M (p • α + χ) = ⊥
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainTopCoeff (- -α) β = chainTopCoeff α β

Tactic:
neg_neg

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainTopCoeff α β = chainTopCoeff α β
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✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
have h₂ : χ x • d • χ y = d • (χ x * χ y) := by
    simpa [nsmul_eq_mul, smul_eq_mul] using mul_left_comm (χ x) d (χ y)

Goal state after:
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✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)
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
hm : m ∈ ⨆ χ, genWeightSpace M ⇑χ
⊢ ∃ n, ((toEnd K L M) x ^ n) m = 0

Tactic:
induction hm using LieSubmodule.iSup_induction' with

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✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
⊢ coroot (-α) = -coroot α

Tactic:
by
  simp [coroot]

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✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = α x • e
heα : e ∈ rootSpace H ⇑α
f : L
hfα : f ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f ≠ 0
⊢ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈ corootSpace ⇑α

Tactic:
suffices ⁅e, f⁆ = killingForm K L e f • ((cartanEquivDual H).symm α : L) from
    (mem_corootSpace α).mpr <| Submodule.subset_span ⟨(killingForm K L e f)⁻¹ • e,
      Submodule.smul_mem _ _ heα, f, hfα, by simpa [inv_smul_eq_iff₀ hf]⟩

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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = α x • e
heα : e ∈ rootSpace H ⇑α
f : L
hfα : f ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f ≠ 0
⊢ ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.a.a.a.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
x yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
hx✝ : yc + yl + yu ∈ lieSpan R L (range b.e ∪ range b.f)
hu : yc + yl + yu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
zc : L
hzc : zc ∈ H
zl : L
hzl : zl ∈ lieSpan R L (range b.f)
zu : L
hzu : zu ∈ lieSpan R L (range b.e)
hy✝ : zc + zl + zu ∈ lieSpan R L (range b.e ∪ range b.f)
hv : zc + zl + zu ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
⊢ ⁅yu, zl⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
exact b.iSup_cartan_borelLower_borelUpper_eq_top_aux hyu hzl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
n : ℤ
h : motive (-n)
⊢ n = - -n

Tactic:
neg_neg

Goal state after:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
n : ℤ
h : motive (-n)
⊢ n = n
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ), motive (-n) → motive n
⊢ ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)

Tactic:
intro n

Goal state after:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ), motive (-n) → motive n
n : ℕ
⊢ motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)
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)
⊢ ((reflection hf * reflection hg) ^ (m + 1)) 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:
have S_eval_t_sub_two (k : ℤ) :
        (S R (k - 2)).eval t = t * (S R (k - 1)).eval t - (S R k).eval t := by
      simp [S_sub_two]
    have S_eval_t_sq_add_S_eval_t_sq (k : ℤ) :
        (S R k).eval t ^ 2 + (S R (k + 1)).eval t ^ 2 - t * (S R k).eval t * (S R (k + 1)).eval t
        = 1 := by
      simpa using congr_arg (Polynomial.eval t) (S_sq_add_S_sq R k)
    -- Apply the inductive hypothesis.
    rw [pow_succ', LinearEquiv.mul_apply, ih, LinearEquiv.mul_apply]
    -- Expand out all the reflections and use `hf`, `hg`.
    simp only [reflection_apply, map_add, map_sub, map_smul, hf, hg]
    -- `m` can be written in the form `2 * k + e`, where `e` is `0` or `1`.
    push_cast
    rw [← Int.mul_ediv_add_emod m 2]
    set k : ℤ := m / 2
    set e : ℤ := m % 2
    simp_rw [add_assoc (2 * k), add_sub_assoc (2 * k), add_comm (2 * k),
      add_mul_ediv_left _ k (by simp : (2 : ℤ) ≠ 0)]
    have he : e = 0 ∨ e = 1 := by lia
    clear_value e
    /- Now, equate the coefficients on both sides. These linear combinations were
    found using `polyrith`. -/
    match_scalars
    · rfl
    · linear_combination (norm := skip) (-g z * f y * (S R (e - 1 + k)).eval t +
          f z * (S R (e - 1 + k)).eval t) * S_eval_t_sub_two (e + k) +
          (-g z * f y + f z) * S_eval_t_sq_add_S_eval_t_sq (k - 1)
      subst ht
      obtain rfl | rfl : e = 0 ∨ e = 1 := he <;> ring_nf
    · linear_combination (norm := skip)
          g z * (S R (e - 1 + k)).eval t * S_eval_t_sub_two (e + k) +
          g z * S_eval_t_sq_add_S_eval_t_sq (k - 1)
      subst ht
      obtain rfl | rfl : e = 0 ∨ e = 1 := he <;> ring_nf

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 ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
⊢ iSupIndep ![rootSpace H 0, U, V]

Tactic:
set sV : Set (H → R) := {f | ∃ n : ι → ℕ, n ≠ 0 ∧ f = ∑ i, n i • b.baseSupp i} with hsV

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
inst✝ : IsTorsionFree R L
this : IsLieAbelian ↥H := isLieAbelian_cartan b
U : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
hU : U = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i))
V : LieSubmodule R (↥H) L := ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
hV : V = ⨆ n, ⨆ (_ : n ≠ 0), rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
s0 : Set (↥H → R) := {0}
hs0 : s0 = {0}
sU : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
hsU : sU = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • (-b.baseSupp) i)}
sV : Set (↥H → R) := {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hsV : sV = {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
⊢ iSupIndep ![rootSpace H 0, U, V]
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
have := congr_arg (·.comp (Polynomial.C ⅟2 * X)) (S_comp_two_mul_X R n)

Goal state after:
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)
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 k l : ι
h : P.root k = P.root i + P.root j
⊢ P.pairing k l = P.pairing i l + P.pairing j l

Tactic:
simp only [← root_coroot_eq_pairing, h, map_add, LinearMap.add_apply]

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
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
⊢ ∀ (n : ℕ), ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x

Tactic:
intro n

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : span R Φ = ⊤
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : ↑u = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
⊢ ↑(u ^ n) = LinearMap.id + ↑n • LinearMap.smulRight (f - g) x
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: case calc_3
ι : 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.pairing i j • (P.toLinearMap x) (P.coroot i)) • P.root j =
    (P.toLinearMap x) (P.pairing i j • P.coroot i) • P.root j

Tactic:
map_smul

Goal state after:
case calc_3
ι : 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ (P.pairing i j • (P.toLinearMap x) (P.coroot i)) • P.root j =
    (P.pairing i j • (P.toLinearMap x) (P.coroot i)) • P.root j
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ :
  (0 - ↑2 * X ^ (2 - 1)) * derivative (T R n) + (1 - X ^ 2) * derivative (derivative (T R n)) =
    0 * (T R (n - 1) - X * T R n) + ↑n * (derivative (T R (n - 1)) - (1 * T R n + X * derivative (T R n)))
h₂ :
  (↑(n - 1) + 1) * ↑(n - 1) * T R (n - 1 + 1) =
    ↑(n - 1) * X * derivative (T R (n - 1 + 1)) - (↑(n - 1) + 1) * derivative (T R (n - 1))
⊢ (1 - X ^ 2) * (⇑derivative)^[2] (T R n) = X * derivative (T R n) - ↑n ^ 2 * T R n

Tactic:
Function.iterate_succ,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
h₁ :
  (0 - ↑2 * X ^ (2 - 1)) * derivative (T R n) + (1 - X ^ 2) * derivative (derivative (T R n)) =
    0 * (T R (n - 1) - X * T R n) + ↑n * (derivative (T R (n - 1)) - (1 * T R n + X * derivative (T R n)))
h₂ :
  (↑(n - 1) + 1) * ↑(n - 1) * T R (n - 1 + 1) =
    ↑(n - 1) * X * derivative (T R (n - 1 + 1)) - (↑(n - 1) + 1) * derivative (T R (n - 1))
⊢ (1 - X ^ 2) * ((⇑derivative)^[1] ∘ ⇑derivative) (T R n) = X * derivative (T R n) - ↑n ^ 2 * T R n