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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
hx : x ∈ (↑(rootSpace H 0)).carrier
hy : y ∈ (↑(rootSpace H 0)).carrier
⊢ ⁅x, y⁆ ∈ (↑(rootSpace H 0)).carrier

Tactic:
let xy : rootSpace H 0 ⊗[R] rootSpace H 0 := ⟨x, hx⟩ ⊗ₜ ⟨y, hy⟩
      suffices (rootSpaceProduct R L H 0 0 0 (add_zero 0) xy : L) ∈ rootSpace H 0 by
        rwa [rootSpaceProduct_tmul, Subtype.coe_mk, Subtype.coe_mk] at this
      exact (rootSpaceProduct R L H 0 0 0 (add_zero 0) xy).property

Goal state after:
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 α ↔ ↑x ∈ Submodule.map H.subtype (Submodule.span R s)

Tactic:
Submodule.map_span,

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 ∈ Submodule.span R (⇑H.subtype '' s)
Module: Mathlib.LinearAlgebra.BilinearForm.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective ⇑l
hᵣ : Function.Surjective ⇑r
⊢ B₁.comp l r = B₂.comp l r ↔ B₁ = B₂

Tactic:
by
  constructor <;> intro h
  · -- B₁.comp l r = B₂.comp l r → B₁ = B₂
    ext x y
    obtain ⟨x', rfl⟩ := hₗ x
    obtain ⟨y', rfl⟩ := hᵣ y
    rw [← comp_apply, ← comp_apply, h]
  · -- B₁ = B₂ → B₁.comp l r = B₂.comp l r
    rw [h]

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

Goal state before:
pp: L : Type u_2
inst✝⁵ : LieRing L
K : Type u_4
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), rootSpace H ⇑α = ⊤

Tactic:
rw [eq_top_iff, ← LieModule.iSup_genWeightSpace_eq_top', iSup_le_iff]

Goal state after:
L : Type u_2
inst✝⁵ : LieRing L
K : Type u_4
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ ∀ (i : Weight K (↥H) L), genWeightSpace L ⇑i ≤ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), rootSpace H ⇑α
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
x : V
i : ι
⊢ ((B.dualBasis hB b).repr x) i = (B x) (b i)

Tactic:
by
  have := b.finiteDimensional_of_finite
  rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    Basis.dualBasis_repr, toDual_def]

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 : ι
this : FiniteDimensional K V
⊢ (B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0

Tactic:
rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB,
    LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
H : ∀ n ∈ N, (Φ n) y = 0
a : M
ha : a ∈ N
⊢ (Φ ⁅x, a⁆) y = 0

Tactic:
exact H _ <| N.lie_mem ha

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
B : BilinForm K V
x : V
hx₁ : (B x) x ≠ 0
⊢ x ≠ 0

Tactic:
by_contra

Goal state after:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
x : V
hx₁ : (B x) x ≠ 0
this : x = 0
⊢ False
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
a : α
ha : IsAtom a
haS : a ≤ sSup S
⊢ a ∈ S

Tactic:
obtain ⟨T, hT, rfl⟩ := hS.atomistic a haS
  obtain rfl | ⟨a, haT⟩ := T.eq_empty_or_nonempty
  · simp only [sSup_empty] at ha
    exact (ha.1 rfl).elim
  suffices sSup T = a from this ▸ hT haT
  have : a ≤ sSup T := le_sSup haT
  rwa [ha.le_iff_eq, eq_comm] at this
  exact (hS.isAtom a (hT haT)).1

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst ≠ v
⊢ consEquiv x = some ⟨x.fst, Fin.cast ⋯ x.snd⟩

Tactic:
simp [consEquiv, hx]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst ≠ v
⊢ some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩ = some ⟨x.fst, Fin.cast ⋯ x.snd⟩
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')
B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f
aux : ∀ (i : ι), B i i ≠ 0 → i ∈ Set.range ⇑snf.f
⊢ ∀ x ∈ Finset.univ, B x x ≠ 0 → x ∈ Set.range ⇑snf.f

Tactic:
simpa using aux

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

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(toSplittingField s)) (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          map (↑(toSplittingField s)) (∏ i, (X - C (MvPolynomial.X ⟨f, i⟩)))).coeff
      n =
    0

Tactic:
Polynomial.map_prod,

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(toSplittingField s)) (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          ∏ i, map (↑(toSplittingField s)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff
      n =
    0
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
⊢ m ∈ Submodule.span R ↑S

Tactic:
simp [hS]

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
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
this : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q
⊢ genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • χ₁ + χ₂)

Tactic:
simp_rw [genWeightSpaceChain_def, this]

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : IsReflexive R N
⊢ e.flip.flip = e

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Polynomial.Sequence

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i ≤ m, IsUnit (↑S i).leadingCoeff
⊢ span R (↑S '' Set.Iic m) = degreeLE R ↑m

Tactic:
← Set.Iio_succ_eq_Iic,

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i ≤ m, IsUnit (↑S i).leadingCoeff
⊢ span R (↑S '' Set.Iio (Order.succ m)) = degreeLE R ↑m
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✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
⊢ ((ad K L) x).IsSemisimple

Tactic:
have h_der (y z : L) (α β : H → K) (hy : y ∈ rootSpace H α) (hz : z ∈ rootSpace H β) :
      S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆ := by
    have hyz : ⁅y, z⁆ ∈ rootSpace H (α + β) :=
      mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α β hy hz
    rw [aux hy, aux hz, aux hyz, smul_lie, lie_smul, ← add_smul, ← Pi.add_apply]

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✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
h_der : ∀ (y z : L) (α β : ↥H → K), y ∈ rootSpace H α → z ∈ rootSpace H β → S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆
⊢ ((ad K L) x).IsSemisimple
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : ⟨x, hx⟩ ∈ ↑(corootSpace ⇑α)
this :
  {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x} ⊆
    ↑(K ∙ ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))
⊢ ⟨x, hx⟩ ∈ K ∙ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)

Tactic:
simp only [LieSubmodule.mem_toSubmodule, mem_corootSpace] at hx'

Goal state after:
case refine_1
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✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
this :
  {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x} ⊆
    ↑(K ∙ ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
⊢ ⟨x, hx⟩ ∈ K ∙ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)
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
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
⊢ x = 0

Tactic:
rcases eq_or_ne α 0 with rfl | hα

Goal state after:
case inl
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
x : ↥H
hαx : 0 x = 0
hx : x ∈ corootSpace 0
⊢ x = 0

case inr
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
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
⊢ 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
hα : α.IsNonZero
⊢ ∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)

Tactic:
obtain ⟨e, heα : e ∈ rootSpace H α, he₀ : e ≠ 0⟩ := α.exists_ne_zero
  obtain ⟨f', hfα, hf⟩ : ∃ f ∈ rootSpace H (-α), killingForm K L e f ≠ 0 := by
    contrapose! he₀
    simpa using mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H heα he₀
  have hef := lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα
  let h : H := ⟨⁅e, f'⁆, hef ▸ Submodule.smul_mem _ _ (Submodule.coe_mem _)⟩
  have hh : α h ≠ 0 := by
    have : h = killingForm K L e f' • (cartanEquivDual H).symm α := by
      simp only [h, Subtype.ext_iff, hef]
      rw [Submodule.coe_smul_of_tower]
    rw [this, map_smul, smul_eq_mul, ne_eq, mul_eq_zero, not_or]
    exact ⟨hf, root_apply_cartanEquivDual_symm_ne_zero hα⟩
  let f := (2 * (α h)⁻¹) • f'
  replace hef : ⁅⁅e, f⁆, e⁆ = 2 • e := by
    have : ⁅⁅e, f'⁆, e⁆ = α h • e := lie_eq_smul_of_mem_rootSpace heα h
    rw [lie_smul, smul_lie, this, ← smul_assoc, smul_eq_mul, mul_assoc, inv_mul_cancel₀ hh,
      mul_one, two_smul, two_smul]
  refine ⟨⁅e, f⁆, e, f, ⟨fun contra ↦ ?_, rfl, hef, ?_⟩, heα, Submodule.smul_mem _ _ hfα⟩
  · rw [contra] at hef
    have : IsAddTorsionFree L := .of_isTorsionFree K L
    simp only [zero_lie, eq_comm (a := (0 : L)), smul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hef
    contradiction
  · have : ⁅⁅e, f'⁆, f'⁆ = - α h • f' := lie_eq_smul_of_mem_rootSpace hfα h
    rw [lie_smul, lie_smul, smul_lie, this]
    simp [← smul_assoc, f, hh, mul_comm _ (2 * (α h)⁻¹)]

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

Goal state before:
pp: case more
R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ eval (-x) (U R ↑(n + 2)) = ↑↑(↑(n + 2)).negOnePow * eval x (U R ↑(n + 2))

Tactic:
trans (n + 2 : ℤ).negOnePow * (2 * x * (U R (n + 1)).eval x - (U R n).eval x)

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ eval (-x) (U R ↑(n + 2)) = ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n))

R : Type u_1
inst✝ : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R ↑n) = ↑↑(↑n).negOnePow * eval x (U R ↑n)
ih2 : eval (-x) (U R ↑(n + 1)) = ↑↑(↑(n + 1)).negOnePow * eval x (U R ↑(n + 1))
⊢ ↑↑(↑n + 2).negOnePow * (2 * x * eval x (U R (↑n + 1)) - eval x (U R ↑n)) =
    ↑↑(↑(n + 2)).negOnePow * eval x (U R ↑(n + 2))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R (n + 1) = X * S R n - S R (n - 1)

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 1)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R (n - 1) = X * S R n - S R (n + 1)

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 1)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R (-n - 2) = -S R n

Tactic:
by
  simpa [sub_eq_add_neg, add_comm] using S_neg R (n + 2)

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

Goal state before:
pp: case refine_1.refine_3
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
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ c₃ • ⁅e, f⁆ ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α

Tactic:
suffices ∃ y ∈ corootSpace α, H.subtype y = c₃ • h' from
        mem_sup_right <| by simpa [ht.lie_e_f, -Subtype.exists]
      refine ⟨c₃ • coroot α, smul_mem _ _ <| by simp, ?_⟩
      rw [IsSl2Triple.h_eq_coroot hα ht heα hfα, map_smul, subtype_apply]

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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
this : 2 • (P.toLinearMap x) (P.coroot i) • P.root i = 2 • (P.toLinearMap x) (P.coroot j) • P.root j
⊢ (2 • ⇑(P.reflection i)) x = (2 • ⇑(P.reflection j)) x

Tactic:
by
    simpa [reflection_apply, smul_sub]

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

Goal state before:
pp: case e'_5
ι : 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)}
hs0' : rootSpace H 0 = ⨆ i ∈ s0, LieModule.genWeightSpace L i
hsU' : U = ⨆ i ∈ sU, LieModule.genWeightSpace L i
hsV' : V = ⨆ i ∈ sV, LieModule.genWeightSpace L i
hU0 : Disjoint s0 sU
hV0 : Disjoint s0 sV
hUV : Disjoint sU sV
key : iSupIndep fun χ ↦ LieModule.genWeightSpace L χ
⊢ U ⊔ V = ⨆ i ∈ sU ∪ sV, LieModule.genWeightSpace L i

Tactic:
rw [iSup_union, hsU', hsV']

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := ⋯
hv' : LinearIndependent (ι := ↑v) K v'
this : span K v = M'
⊢ Submodule.map M'.subtype (span K (Set.range v')) = Submodule.map M'.subtype ⊤

Tactic:
Submodule.map_span,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
this : span K v = M'
⊢ span K (⇑M'.subtype '' Set.range v') = Submodule.map M'.subtype ⊤
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ (algebraMap A K) (num A x) / (algebraMap A K) ↑(den A x) = x

Tactic:
by
  rw [← mk'_eq_div]
  apply mk'_num_den

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
⊢ ↑(∏ l ∈ Finset.range k, (2 * l + 3)) * eval 1 ((⇑derivative)^[k] (U R n)) =
    ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1)

Tactic:
by
  induction k
  case zero => simp
  case succ k ih =>
    push_cast at ih ⊢
    rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 3),
      mul_assoc, iterate_derivative_U_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
hb : (factorPow I ⋯) a * b = 1
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
⊢ IsUnit a

Tactic:
← hb',

Goal state after:
R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb : (factorPow I ⋯) a * (factor ⋯) b' = 1
hb' : (factor ⋯) b' = b
⊢ IsUnit a
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c d e : ℕ
h : c = b + a
h' : e = d + c
⊢ factorPow I M ⋯ ∘ₗ powSMulQuotInclusion I M ⋯ ⊤ = powSMulQuotInclusion I M h ⊤ ∘ₗ factorPow I ↥(I ^ a • ⊤) ⋯

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
P : Type u_4
inst✝¹ : AddCommGroup P
inst✝ : Module R P
g : M →ₗ[R] P
hg : Function.Surjective ⇑g
⊢ length R P ≤ length R M

Tactic:
by
  rw [Module.length_eq_add_of_exact (LinearMap.ker g).subtype g (Submodule.subtype_injective _) hg
    (LinearMap.exact_subtype_ker_map g)]
  exact le_add_self

Goal state after: