mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: 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
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Nontrivial M
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : IsTriangularizable R L M
t : IsSl2Triple h e f
⊢ ∃ μ m, m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ

Tactic:
obtain ⟨μ₀, hμ₀⟩ := IsTriangularizable.exists_hasEigenvalue R L M h
  obtain ⟨m₀, hm₀⟩ := hμ₀.exists_hasEigenvector
  let evals (n : ℕ) : R := μ₀ + 2 * (n : R)
  let e_vecs (n : ℕ) : M := ((toEnd R L M e) ^ n) m₀
  have h_exists_zero : ∃ k, e_vecs k = 0 := by
    by_contra! contra
    have h_inj : Function.Injective evals := fun a b hab ↦ by
      simpa [evals, add_right_inj, mul_eq_mul_left_iff, Nat.cast_inj] using hab
    have aux (μ : range evals) : (toEnd R L M h).HasEigenvector μ (e_vecs μ.property.choose) := by
      set n := μ.property.choose
      refine ⟨?_, contra n⟩
      rw [Module.End.mem_eigenspace_iff, toEnd_apply_apply, ← μ.property.choose_spec]
      exact t.lie_h_pow_toEnd_e hm₀.apply_eq_smul n
    have _i := ((toEnd R L M h).eigenvectors_linearIndependent (range evals) _ aux).finite
    exact (Set.infinite_range_of_injective h_inj) (Set.toFinite _)
  obtain ⟨n, hn_ne, hn_zero⟩ := Nat.exists_not_and_succ_of_not_zero_of_exists hm₀.2 h_exists_zero
  exact ⟨evals n, e_vecs n, hn_ne,
    { ne_zero := hn_ne
      lie_h := t.lie_h_pow_toEnd_e hm₀.apply_eq_smul n
      lie_e := by rwa [lie_e_pow_toEnd_e n] }⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ flipHom ≪≫ₗ flipHom = LinearEquiv.refl R (BilinForm R M)

Tactic:
ext A

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : BilinForm R M
x✝ y✝ : M
⊢ (((flipHom ≪≫ₗ flipHom) A) x✝) y✝ = (((LinearEquiv.refl R (BilinForm R M)) A) x✝) y✝
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
⊢ φ = ψ

Tactic:
ext w
  refine eq_of_sub_eq_zero (b.1 _ ?_)
  intro v
  rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self]

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
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
⊢ IsCompl (genWeightSpace M 0) (posFittingComp R L M)

Tactic:
by
  set M₀ := genWeightSpace M (0 : L → R)
  set M₁ := posFittingComp R L M
  rcases forall_or_exists_not (fun (x : L) ↦ genWeightSpaceOf M (0 : R) x = ⊤)
    with h | ⟨x, hx : genWeightSpaceOf M (0 : R) x ≠ ⊤⟩
  · suffices IsNilpotent L M by simp [M₀, M₁, isCompl_top_bot]
    replace h : M₀ = ⊤ := by simpa [M₀, genWeightSpace]
    rw [← LieModule.isNilpotent_of_top_iff' (R := R), ← h]
    infer_instance
  · set M₀ₓ := genWeightSpaceOf M (0 : R) x
    set M₁ₓ := posFittingCompOf R M x
    set M₀ₓ₀ := genWeightSpace M₀ₓ (0 : L → R)
    set M₀ₓ₁ := posFittingComp R L M₀ₓ
    have h₁ : IsCompl M₀ₓ M₁ₓ := isCompl_genWeightSpaceOf_zero_posFittingCompOf R L M x
    have h₂ : IsCompl M₀ₓ₀ M₀ₓ₁ := h M₀ₓ hx.lt_top
    have h₃ : M₀ₓ₀.map M₀ₓ.incl = M₀ := by
      rw [map_genWeightSpace_eq_of_injective M₀ₓ.injective_incl, inf_eq_left,
        LieSubmodule.range_incl]
      exact iInf_le _ x
    have h₄ : M₀ₓ₁.map M₀ₓ.incl ⊔ M₁ₓ = M₁ := by
      apply le_antisymm <| sup_le_iff.mpr
        ⟨map_posFittingComp_le _, posFittingCompOf_le_posFittingComp R L M x⟩
      rw [← posFittingComp_map_incl_sup_of_codisjoint h₁.codisjoint]
      exact sup_le_sup_left LieSubmodule.map_incl_le _
    rw [← h₃, ← h₄]
    apply Disjoint.isCompl_sup_right_of_isCompl_sup_left
    · rw [disjoint_iff, ← LieSubmodule.map_inf M₀ₓ.injective_incl, h₂.inf_eq_bot,
        LieSubmodule.map_bot]
    · rwa [← LieSubmodule.map_sup, h₂.sup_eq_top, LieModuleHom.map_top, LieSubmodule.range_incl]

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

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
⊢ ∀ (b : LieIdeal K L), IsAtom b → ¬b = I → b ≤ orthogonal Φ hΦ_inv I

Tactic:
intro J

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
⊢ IsAtom J → ¬J = I → J ≤ orthogonal Φ hΦ_inv I
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
⊢ J ≤ orthogonal Φ hΦ_inv I

Tactic:
rw [← lie_eq_self_of_isAtom_of_nonabelian J hJ (hL J hJ), lieIdeal_oper_eq_span, lieSpan_le]

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑(orthogonal Φ hΦ_inv I)
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
⊢ ∀ (I_1 : LieIdeal R ↥I), I_1 = ⊥ ∨ I_1 = ⊤

Tactic:
intro J

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
⊢ J = ⊥ ∨ J = ⊤
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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
x y : L
⊢ ⁅(toEnd R L M) x, (toEnd R L M) y⁆ = 0

Tactic:
← LieHom.map_lie,

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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
x y : L
⊢ (toEnd R L M) ⁅x, y⁆ = 0
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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
h : ∀ (x y : L), Commute ((toEnd R L M) x) ((toEnd R L M) y)
χ : L → R
x y : L
hχ : ¬↑(⨅ x, { toSubmodule := ((toEnd R L M) x).maxGenEigenspace (χ x), lie_mem := ⋯ }) = ↑⊥
⊢ χ (x + y) = χ x + χ y

Tactic:
LieSubmodule.iInf_toSubmodule,

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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
h : ∀ (x y : L), Commute ((toEnd R L M) x) ((toEnd R L M) y)
χ : L → R
x y : L
hχ : ¬⨅ i, ((toEnd R L M) i).maxGenEigenspace (χ i) = ↑⊥
⊢ χ (x + y) = χ x + χ y
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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
t : R
x : L
hχ : ¬↑(⨅ x, { toSubmodule := ((toEnd R L M) x).maxGenEigenspace (χ x), lie_mem := ⋯ }) = ↑⊥
⊢ χ (t • x) = t • χ x

Tactic:
LieSubmodule.iInf_toSubmodule,

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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
t : R
x : L
hχ : ¬⨅ i, ((toEnd R L M) i).maxGenEigenspace (χ i) = ↑⊥
⊢ χ (t • x) = t • χ x
Module: Mathlib.Algebra.Lie.Weights.Linear

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✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
hχ : 0 < ↑(finrank R ↥(genWeightSpace M χ))
⊢ 0 < finrank R ↥(genWeightSpace M χ)

Tactic:
Nat.cast_pos

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✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
hχ : 0 < finrank R ↥(genWeightSpace M χ)
⊢ 0 < finrank R ↥(genWeightSpace M χ)
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h : ¬(x.fst = v ∧ ↑x.snd = count v m)
hv : ¬x.fst = v
⊢ ↑x.snd < count x.fst m

Tactic:
convert! x.2.2 using 1
      exact (count_cons_of_ne hv _).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
⊢ Function.LeftInverse (fun x ↦ x.elim ⟨v, ⟨count v m, ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩) fun x ↦
    if h : x.fst = v ∧ ↑x.snd = count v m then none else some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩

Tactic:
by
    rintro ⟨x, hx⟩
    dsimp only
    split
    · rename_i h
      obtain ⟨rfl, h2⟩ := h
      simp [← h2]
    · simp

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

Goal state before:
pp: case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (Ideal.Quotient.mk (maxIdeal k)) X) -
      eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi))
        (C ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨fi.fst, fi.snd⟩))) =
    0

Tactic:
erw [eval_C]

Goal state after:
case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (Ideal.Quotient.mk (maxIdeal k)) X) -
      (Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨fi.fst, fi.snd⟩) =
    0
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule =
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
⊢ ⁅x, D⁆ ∈ ((killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule).carrier

Tactic:
change ⁅x, D⁆ ∈ 𝕀ᗮ

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule =
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
⊢ ⁅x, D⁆ ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
v : ι → R
n : ι → ℕ
hn : ∀ (i : ι), (A ^ n i).row i = 0
⊢ ∃ n, Aᵀ ^ n *ᵥ v = 0

Tactic:
suffices ∀ i, (A ^ ⨆ j, n j) i = 0 from ⟨⨆ j, n j, by simp [mulVec_eq_sum, this]⟩

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
v : ι → R
n : ι → ℕ
hn : ∀ (i : ι), (A ^ n i).row i = 0
⊢ ∀ (i : ι), (A ^ ⨆ j, n j) i = 0
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent ((ad K L) x)
y : ↥H
⊢ ⁅(toEnd K (↥H) L) ⟨x, hx⟩, (toEnd K (↥H) L) y⁆ = 0

Tactic:
← LieHom.map_lie,

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
⊢ (toEnd K (↥H) L) ⁅⟨x, hx⟩, y⁆ = 0
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : T R (-(↑n + 1)) = T R (↑n + 1)
ih2 : T R (-↑n) = T R ↑n
h₁ : T R (↑n + 2) = 2 * X * T R (↑n + 1) - T R ↑n
⊢ T R (-(↑n + 2)) = T R (↑n + 2)

Tactic:
have h₂ := T_sub_two R (-n)

Goal state after:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : T R (-(↑n + 1)) = T R (↑n + 1)
ih2 : T R (-↑n) = T R ↑n
h₁ : T R (↑n + 2) = 2 * X * T R (↑n + 1) - T R ↑n
h₂ : T R (-↑n - 2) = 2 * X * T R (-↑n - 1) - T R (-↑n)
⊢ T R (-(↑n + 2)) = T R (↑n + 2)
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✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
x : ↥H
hx : ∀ n ∈ K ∙ coroot α, ((traceForm K (↥H) L) n) x = 0
⊢ x ∈ Weight.ker

Tactic:
specialize hx (coroot α) (Submodule.mem_span_singleton_self _)

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✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
x : ↥H
hx : ((traceForm K (↥H) L) (coroot α)) x = 0
⊢ x ∈ Weight.ker
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
x : R
⊢ eval (-x) (T R n) = ↑↑n.negOnePow * eval x (T R n)

Tactic:
by
  induction n using Chebyshev.induct' with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    trans (n + 2 : ℤ).negOnePow * (2 * x * (T R (n + 1)).eval x - (T R n).eval x)
    · simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, ih1, Int.negOnePow_add,
        Int.negOnePow_one, Units.val_neg, Int.cast_neg, ih2, Int.negOnePow_even 2 even_two]
      ring_nf
    · simp
  | neg n ih => simp [ih]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : ((C R n).comp (2 * X)).comp (Polynomial.C ⅟2 * X) = (2 * T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T 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, map_ofNat] at this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
n : ℤ
this : C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)
⊢ C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
⊢ (2 * ↑k + 1) * eval 1 ((⇑derivative)^[k + 1] (T R n)) = (↑n ^ 2 - ↑k ^ 2) * eval 1 ((⇑derivative)^[k] (T R n))

Tactic:
have h := one_sub_X_sq_mul_iterate_derivative_T_eval (R := R) n k 1
  rw [one_pow, sub_self, zero_mul, mul_one] at h
  exact sub_eq_zero.mp h.symm

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
⊢ ⊤ ≤ span L (Set.range Subtype.val)

Tactic:
by rw [← hv₂, Subtype.range_coe_subtype, Set.ofPred_mem_eq]

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

Goal state before:
pp: case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : 2 * T R m * T R (-↑k) = T R (m + -↑k) + T R (m - -↑k)
ih2 : 2 * T R m * T R (-↑k + 1) = T R (m + (-↑k + 1)) + T R (m - (-↑k + 1))
h₁ : T R (m + (-↑k - 1) + 2) = 2 * X * T R (m + (-↑k - 1) + 1) - T R (m + (-↑k - 1))
⊢ 2 * T R m * T R (-↑k - 1) = T R (m + (-↑k - 1)) + T R (m - (-↑k - 1))

Tactic:
have h₂ := T_sub_two R (m - (-k - 1))

Goal state after:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
m : ℤ
k : ℕ
ih1 : 2 * T R m * T R (-↑k) = T R (m + -↑k) + T R (m - -↑k)
ih2 : 2 * T R m * T R (-↑k + 1) = T R (m + (-↑k + 1)) + T R (m - (-↑k + 1))
h₁ : T R (m + (-↑k - 1) + 2) = 2 * X * T R (m + (-↑k - 1) + 1) - T R (m + (-↑k - 1))
h₂ : T R (m - (-↑k - 1) - 2) = 2 * X * T R (m - (-↑k - 1) - 1) - T R (m - (-↑k - 1))
⊢ 2 * T R m * T R (-↑k - 1) = T R (m + (-↑k - 1)) + T R (m - (-↑k - 1))
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
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
⊢ length R M = length R N + length R P

Tactic:
by_cases hP : IsFiniteLength R P

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : IsFiniteLength R P
⊢ length R M = length R N + length R P

case neg
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
H : Function.Exact ⇑f ⇑g
hP : ¬IsFiniteLength R P
⊢ length R M = length R N + length R P
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
⊢ b⁻¹ • a⁻¹ = (b • a)⁻¹

Tactic:
rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv,
          map_units_inv]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
⊢ v ((algebraMap O R) x * ↑u⁻¹) ≤ v ((algebraMap O R) x)

Tactic:
← hu,

Goal state after:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
⊢ v (↑u * ↑u⁻¹) ≤ v ↑u
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : Γ₀
hx : IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x
⊢ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

pp: case mpr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
⊢ ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x

Tactic:
· obtain ⟨a, ha, rfl⟩ : ∃ a ∈ I, (v ∘ algebraMap O F) a = x := by simpa using hx.left
    refine ⟨a, ?_⟩
    ext b
    simp only [SetLike.mem_coe, mem_ofPred_eq]
    constructor <;> intro h
    · exact hx.right (Set.mem_image_of_mem _ h)
    · rw [le_iff_dvd hv] at h
      exact Ideal.mem_of_dvd I h ha

Goal state after:
case mpr
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
⊢ ∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
ha : Irreducible a
hb : Irreducible b
⊢ Associated a b

Tactic:
by
  rw [irreducible_iff_uniformizer] at ha hb
  rw [← span_singleton_eq_span_singleton, ← ha, hb]

Goal state after: