mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: 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
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this✝ : iSupIndep fun x ↦ (f.genEigenspace x) k
aux : ∀ μ' ∈ m.support.erase μ, (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k
this : Disjoint ((f.genEigenspace μ) k) ((m.support.erase μ).sup fun x ↦ (f.genEigenspace x) k)
μ' : K
hμ' : μ' ∈ m.support.erase μ
⊢ (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k

Tactic:
apply aux μ' hμ'

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case h
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
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this✝ : iSupIndep fun x ↦ (f.genEigenspace x) k
aux : ∀ μ' ∈ m.support.erase μ, (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k
this : (m.support.erase μ).SupIndep fun x ↦ (f.genEigenspace x) k
μ' : K
hμ' : μ' ∈ m.support.erase μ
⊢ (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k

Tactic:
apply aux μ' hμ'

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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hx : x ∈ ⨆ χ ∈ s, rootSpace H χ
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅x, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
by
  induction hx using LieSubmodule.iSup_induction' with
  | zero => simp
  | add _ _ _ _ hu hv => rw [add_lie]; exact add_mem hu hv
  | mem χ₁ u hu =>
    by_cases hχ₁ : χ₁ ∈ s; swap
    · simp_all
    replace hu : u ∈ rootSpace H χ₁ := by simpa [hχ₁] using hu
    induction hm using LieSubmodule.iSup_induction' with
    | zero => simp
    | add _ _ _ _ hv hw => rw [lie_add]; exact add_mem hv hw
    | mem χ₂ v hv =>
      by_cases hχ₂ : χ₂ ∈ s; swap
      · simp_all
      apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
      simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]

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
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : Nontrivial ↥H
⊢ Nontrivial ↥(genWeightSpace L 0)

Tactic:
by
  obtain ⟨⟨x, hx⟩, ⟨y, hy⟩, e⟩ := exists_pair_ne H
  exact ⟨⟨x, toLieSubmodule_le_rootSpace_zero R L H hx⟩,
    ⟨y, toLieSubmodule_le_rootSpace_zero R L H hy⟩, by simpa using e⟩

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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : ∀ (x : L), ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
x : L
h : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)
k : ℕ
hk : (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
this : f ((((toEnd R L M) x - χ x • 1) ^ k) m) = 0
⊢ (((toEnd R L M) x - χ x • 1) ^ k) m = 0

Tactic:
rw [← map_zero f] at this; exact hf 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
⊢ H.toSubmodule = Submodule.span R (range b.h)

Tactic:
conv_lhs => rw [b.cartan_eq_lieSpan]
  apply coe_lieSpan_eq_span_of_forall_lie_eq_zero
  rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩
  exact b.lie_h_h i j

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}
⊢ Disjoint I (sSup ({I | IsAtom I} \ {I}))

Tactic:
apply (orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI).mono_right

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}
⊢ sSup ({I | IsAtom I} \ {I}) ≤ orthogonal Φ hΦ_inv I
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (y : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) m) y = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ 0 + (B ↑m) z = 0

Tactic:
show B m z = 0 from hm ⟨z, hz⟩,

Goal state after:
case refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (y : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) m) y = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ 0 + 0 = 0
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
x : α
i : ℕ
⊢ (x, i) ∈ m.toFinset.disjiUnion (fun x ↦ Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (count x m))) ⋯ ↔
    (x, i) ∈ {p | p.2 < count p.1 m}

Tactic:
Finset.mem_disjiUnion,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
x : α
i : ℕ
⊢ (∃ a ∈ m.toFinset, (x, i) ∈ Finset.map { toFun := Prod.mk a, inj' := ⋯ } (Finset.range (count a m))) ↔
    (x, i) ∈ {p | p.2 < count p.1 m}
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), IsAtom I → ¬IsLieAbelian ↥I

Tactic:
intro I hI₁ hI₂

Goal state after:
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₁ : IsAtom I
hI₂ : IsLieAbelian ↥I
⊢ False
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M₂
inst✝² : Algebra R A
inst✝¹ : Module R M₂
inst✝ : FaithfulSMul R A
B : BilinForm R M₂
⊢ BilinForm.baseChange A B = 0 ↔ B = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  ext m m'
  simpa [← Algebra.algebraMap_eq_smul_one] using LinearMap.congr_fun₂ h (1 ⊗ₜ[R] m) (1 ⊗ₜ[R] m')

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

Goal state before:
pp: case lie.hx.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
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
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)
aux : yc + yl + yu = ⁅v, z⁆
⊢ ⁅u, yu⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
· rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| LieSubalgebra.lie_mem _ hyu hu

Goal state after:
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
inst✝ : Module.Finite R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈ Submodule.map (ad R L).range.subtype (LinearMap.ker (killingForm R ↥(ad R L).range))

Tactic:
rw [← killingForm_restrict_range_ad]
  exact LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict
    (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl ⟨by simp, ad_mem_orthogonal_of_mem_orthogonal hD x⟩

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

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
B : LinearMap.BilinForm R M
m₀ : M
hB : ∀ (x : L) (k : ℕ) (m n : M), (B m) ((φ x ^ k) n) = (-1) ^ k • (B ((φ x ^ k) m)) n
x : L
hm₀ : ∀ (x : L), ∃ k, (φ x ^ k) m₀ = 0
k : ℕ
hk : (φ x ^ k) m₀ = 0
m : M
hm₁ : (φ x ^ k) m ∈ posFittingCompOf R M x
⊢ (B m₀) ((φ x ^ k) m) = 0

Tactic:
simp [hB, hk]

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

Goal state before:
pp: case refine_4
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
k : ℕ
x : L
hk : 1 ≤ k
hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
t : R
u : L
x✝ : u ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}
hu : (trace R M) (φ u) = 0
⊢ (trace R M) (φ (t • u)) = 0

Tactic:
· simp [hu]

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x 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 : ℕ
S_eval_t_sub_two :
  ∀ (k : ℤ), Polynomial.eval t (S R (k - 2)) = t * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
S_eval_t_sq_add_S_eval_t_sq :
  ∀ (k : ℤ),
    Polynomial.eval t (S R k) ^ 2 + Polynomial.eval t (S R (k + 1)) ^ 2 -
        t * Polynomial.eval t (S R k) * Polynomial.eval t (S R (k + 1)) =
      1
k : ℤ := ↑m / 2
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 k) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        ((f y * g z - f z) • x - g z • y)
e : ℤ
he : e = 0 ∨ e = 1
⊢ -(f z * 1) - g z * -(f y * 1) +
        Polynomial.eval t (S R ((e - 2) / 2 + k)) *
            (Polynomial.eval t (S R ((e - 1) / 2 + k)) + Polynomial.eval t (S R ((e - 3) / 2 + k))) *
          ((g x * f z - g z) * (-(f y * 1) - 2 * -(f y * 1)) - f z * (1 - 2 * 1 - g x * -(f y * 1))) +
      Polynomial.eval t (S R ((e - 1) / 2 + k)) *
          (Polynomial.eval t (S R (e / 2 + k)) + Polynomial.eval t (S R ((e - 2) / 2 + k))) *
        ((f y * g z - f z) * (1 - 2 * 1 - g x * -(f y * 1)) - g z * (-(f y * 1) - 2 * -(f y * 1))) =
    Polynomial.eval t (S R ((e + 1 - 2) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 3) / 2 + k))) *
        -(f z * 1) +
      Polynomial.eval t (S R ((e + 1 - 1) / 2 + k)) *
          (Polynomial.eval t (S R ((e + 1) / 2 + k)) + Polynomial.eval t (S R ((e + 1 - 2) / 2 + k))) *
        ((f y * g z - f z) * 1)

Tactic:
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

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
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
this : ⁅⁅e, f'⁆, e⁆ = α h • e
⊢ 2 • e = 2 • e

Tactic:
two_smul,

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✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
this : ⁅⁅e, f'⁆, e⁆ = α h • e
⊢ e + e = 2 • e
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ (U R ↑n).degree < (2 * X * U R ↑(n + 1)).degree

Tactic:
rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X,
        degree_U_natCast R n, degree_U_natCast R (n + 1)]

Goal state after:
case more
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
this : leadingCoeff 2 = 2
n : ℕ
ih1 : (U R ↑n).leadingCoeff = 2 ^ n
ih2 : (U R (↑n + 1)).leadingCoeff = 2 ^ (n + 1)
⊢ ↑n < ↑(n + 1) + 1
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ C R (Int.negSucc 0) = X

Tactic:
rw [C]

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ X * C R (-↑0) - C R (-↑0 + 1) = X
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R
n : ℤ
⊢ (algebraMap R R') (eval x (S R n)) = eval ((algebraMap R R') x) (S R' n)

Tactic:
by
  rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_S]

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
inst✝¹ : Nonempty ι
inst✝ : NeZero 2
i : ι
hi : P.root i ≠ 0
⊢ Nontrivial M

Tactic:
exact ⟨P.root i, 0, hi⟩

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 : ι
⊢ (P.toLinearMap (P.root i - 2 • P.root i)) (P.coroot j) = -P.pairing i j

Tactic:
two_smul,

Goal state after:
ι : 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 : ι
⊢ (P.toLinearMap (P.root i - (P.root i + P.root i))) (P.coroot j) = -P.pairing i j
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 : ι
⊢ (P.root' i) (P.coroot j - 2 • P.coroot j) = -P.pairing i j

Tactic:
two_smul,

Goal state after:
ι : 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 : ι
⊢ (P.root' i) (P.coroot j - (P.coroot j + P.coroot j)) = -P.pairing i j
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 : ι
h : P.IsOrthogonal i j
⊢ Commute (P.reflection i) (P.reflection j)

Tactic:
rw [commute_iff_eq]

Goal state after:
ι : 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 : ι
h : P.IsOrthogonal i j
⊢ P.reflection i * P.reflection j = P.reflection j * P.reflection i
Module: Mathlib.RingTheory.Polynomial.Chebyshev

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

Tactic:
case succ k ih =>
    push_cast at ih ⊢
    rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 1),
      mul_assoc, iterate_derivative_T_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self]

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

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

Tactic:
rw [eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),
    mul_comm, iterate_derivative_U_eval_one]

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
N : Submodule R M
⊢ length R ↥N = Order.height N

Tactic:
by
  apply WithBot.coe_injective
  rw [Order.height_eq_krullDim_Iic, coe_length, Order.krullDim_eq_of_orderIso (Submodule.mapIic _)]

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
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
p : Submodule R M
h : p ≠ ⊥
⊢ Module.length R (M ⧸ p) < Module.length R M

Tactic:
rw [Module.length_quotient, Module.length, WithBot.lt_unbot_iff, ← Order.coheight_bot_eq_krullDim,
    WithBot.coe_lt_coe]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
p : Submodule R M
h : p ≠ ⊥
⊢ Order.coheight p < Order.coheight ⊥
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: 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
x : O
hvx : v ((algebraMap O F) x) = 1
⊢ IsUnit x

Tactic:
refine isUnit_of_one hv (IsUnit.mk0 _ ?_) hvx
  simp only [← v.ne_zero_iff, hvx, ne_eq, one_ne_zero, not_false_eq_true]

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

Goal state before:
pp: 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
x y : O
⊢ DvdNotUnit x y ↔ v ((algebraMap O F) y) < v ((algebraMap O F) x)

Tactic:
by
  rw [lt_iff_le_not_ge, hv.le_iff_dvd, hv.le_iff_dvd]
  refine ⟨?_, And.elim dvdNotUnit_of_dvd_of_not_dvd⟩
  rintro ⟨hx0, d, hdu, rfl⟩
  refine ⟨⟨d, rfl⟩, ?_⟩
  rw [hv.isUnit_iff_valuation_eq_one, ← ne_eq, ne_iff_lt_iff_le.mpr (hv.map_le_one d)] at hdu
  rw [dvd_iff_le hv]
  simp only [map_mul, not_le]
  contrapose! hdu
  refine one_le_of_le_mul_left₀ ?_ hdu
  simp [hv.valuation_pos_iff_ne_zero, hx0]

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

Goal state before:
pp: case neg.inl
A : Type u
inst✝² : CommRing A
inst✝¹ : Nontrivial A
inst✝ : PreValuationRing A
α β : Ideal A
a : A
h₁ : a ∈ α
h₂ : a ∉ β
b : A
hb : b ∈ β
c : A
h : a * c = b
⊢ b ∈ α

Tactic:
rw [← h]
    exact Ideal.mul_mem_right _ _ h₁

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : KrullDimLE 0 R
⊢ minimalPrimes R = {I | I.IsPrime}

Tactic:
ext
  exact Ideal.mem_minimalPrimes_iff_isPrime

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝⁴ : Ring R
inst✝³ : LinearOrderedCommMonoidWithZero Γ₀
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
⊢ 1 x ≤ 1

Tactic:
rw [one_apply_def]
  split_ifs <;> simp_all

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

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ₀
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors R
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : Nontrivial Γ₀
x : R
⊢ 1 x < 1 ↔ x = 0

Tactic:
rw [one_apply_def]
  split_ifs <;> simp_all

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = ⊤
hx : ¬x = 0
hy : y = 0
⊢ False

Tactic:
exact hx (addVal_eq_top_iff.mp h)

Goal state after: