mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
⊢ ↑(chainBotCoeff i j) = sSup {k | P.root j - k • P.root i ∈ range ⇑P.root}

Tactic:
setOfPred_root_sub_zsmul_mem_eq_Icc h

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
⊢ ↑(chainBotCoeff i j) = sSup (Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j))
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
this : InvolutiveNeg ι := P.indexNeg
z : ℤ
⊢ z ∈ Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j) ↔ z ∈ Icc (-↑(chainBotCoeff (-i) j)) ↑(chainTopCoeff (-i) j)

Tactic:
rw [P.chainCoeff_reflectionPerm_left_aux]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
k : ι
hk : P.root k = P.root j + P.root i
h' : LinearIndependent R ![P.root i, P.root k]
this :
  {z | P.root k - z • P.root i ∈ range ⇑P.root} =
    ⇑(OrderIso.addRight 1) '' {n | P.root j - n • P.root i ∈ range ⇑P.root}
⊢ BddAbove {z | P.root j - z • P.root i ∈ range ⇑P.root}

Tactic:
setOfPred_root_sub_zsmul_mem_eq_Icc h

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
k : ι
hk : P.root k = P.root j + P.root i
h' : LinearIndependent R ![P.root i, P.root k]
this :
  {z | P.root k - z • P.root i ∈ range ⇑P.root} =
    ⇑(OrderIso.addRight 1) '' {n | P.root j - n • P.root i ∈ range ⇑P.root}
⊢ BddAbove (Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j))
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case pos
ι : 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✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
h : ∀ (i j : ι), (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)
i j : ι
this : P.pairing i j * (B.form (P.root j)) (P.root j) = P.pairing j i * (B.form (P.root i)) (P.root i)
⊢ P.pairing i j = P.pairing j i

Tactic:
rwa [h i j, mul_left_inj' (B.ne_zero j)] at this

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

Goal state before:
pp: R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R₁
⊢ (toBilin' M).IsSymm ↔ M.IsSymm

Tactic:
simp [← M.toBilin'.isSymm_toMatrix'_iff_isSymm]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
K : α
K0 : K > 0
i : ℕ
H : ∀ j ≥ i, K ≤ abv (↑f j)
j : ℕ
ij : j ≥ i
⊢ abv (↑(f.inv hf * f - 1) j) < ε

Tactic:
by simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
K : α
K0 : K > 0
i : ℕ
H : ∀ j ≥ i, K ≤ abv (↑f j)
j : ℕ
ij : j ≥ i
⊢ abv (↑(f * f.inv hf - 1) j) < ε

Tactic:
by simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ j ≥ i, ↑(↑f j) ≤ x
⊢ -x ≤ mk (-f)

Tactic:
exact le_mk_of_forall_le ⟨i, fun j ij => by simp [H _ ij]⟩

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
obtain ha | ha := ha

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
⊢ a ⊔ b ≤ c

case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≤ c
ha : a ≈ c
⊢ a ⊔ b ≤ c
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
hb : b ≤ c
ha : a ≈ c
⊢ a ⊔ b ≤ c

Tactic:
replace hb := le_of_le_of_eq hb (Setoid.symm ha)

Goal state after:
case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≤ c
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
⊢ A.vec = B.vec ↔ A = B

Tactic:
by
  simp_rw [← Matrix.ext_iff, funext_iff, Prod.forall, @forall_comm m n, vec]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
f : n ≃ m
⊢ ((reindex f f) A).IsHermitian ↔ A.IsHermitian

Tactic:
refine ⟨fun h ↦ ?_, (·.reindex f)⟩

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
f : n ≃ m
h : ((reindex f f) A).IsHermitian
⊢ A.IsHermitian
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
⊢ Commute A (B ^ m)

Tactic:
by
  rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)
  · refine SemiconjBy.zpow_right ?_ ?_ h _ <;> exact isUnit_det_of_left_inverse hB
  · cases m
    · simpa using h.pow_right _
    · simp [← inv_pow', hB]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
e : m → n
he : Function.Injective e
⊢ (M.submatrix e e).PosDef

Tactic:
by
  refine ⟨hM.1.submatrix _, fun x hx ↦ ?_⟩
  simpa [Finsupp.sum_mapDomain_index, add_mul, mul_add] using
    hM.2 <| Finsupp.mapDomain_injective he |>.ne_iff' Finsupp.mapDomain_zero |>.2 hx

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
⊢ 0 < x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * diagonal d i j * xj

Tactic:
refine Finsupp.sum_pos' (fun _ _ ↦ Finsupp.sum_nonneg ?_) ?_
    · simp +contextual [diagonal, apply_ite, star_left_conjugate_nonneg (h _).le]
    obtain ⟨i, hxi⟩ := by simpa [Finsupp.ext_iff] using hx
    refine ⟨i, ?_, Finsupp.sum_pos' ?_ ⟨i, ?_, ?_⟩⟩ <;> simp +contextual [diagonal,
      apply_ite, star_left_conjugate_nonneg (h _).le,
      star_left_conjugate_pos (h i), IsRegular.of_ne_zero hxi, Finsupp.mem_support_iff.mpr hxi]

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

Goal state before:
pp: n : ℕ
⊢ 1 = n.ascFactorial 0

Tactic:
Nat.ascFactorial_zero

Goal state after:
n : ℕ
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

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
S : Type u_5
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra S R
P✝ : RootPairing ι R M N
inst✝¹⁵ : P✝.IsValuedIn S
b✝ : P✝.Base
inst✝¹⁴ : P✝.IsCrystallographic
inst✝¹³ : CharZero R
inst✝¹² : IsDomain R
inst✝¹¹ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R M₂
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : Module R N₂
P : RootPairing ι R M N
inst✝⁶ : P.IsRootSystem
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝³ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
inst✝² : Finite ι₂
inst✝¹ : P₂.IsRootSystem
inst✝ : P₂.IsReduced
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
f : M ≃ₗ[R] M₂ := b.toWeightBasis.equiv b₂.toWeightBasis e
⊢ ∀ (m : M), f m ∈ range ⇑P₂.root ↔ m ∈ range ⇑P.root

Tactic:
refine fun m ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
ι : 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
S : Type u_5
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra S R
P✝ : RootPairing ι R M N
inst✝¹⁵ : P✝.IsValuedIn S
b✝ : P✝.Base
inst✝¹⁴ : P✝.IsCrystallographic
inst✝¹³ : CharZero R
inst✝¹² : IsDomain R
inst✝¹¹ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R M₂
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : Module R N₂
P : RootPairing ι R M N
inst✝⁶ : P.IsRootSystem
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝³ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
inst✝² : Finite ι₂
inst✝¹ : P₂.IsRootSystem
inst✝ : P₂.IsReduced
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
f : M ≃ₗ[R] M₂ := b.toWeightBasis.equiv b₂.toWeightBasis e
m : M
h : f m ∈ range ⇑P₂.root
⊢ m ∈ range ⇑P.root

case refine_2
ι : 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
S : Type u_5
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra S R
P✝ : RootPairing ι R M N
inst✝¹⁵ : P✝.IsValuedIn S
b✝ : P✝.Base
inst✝¹⁴ : P✝.IsCrystallographic
inst✝¹³ : CharZero R
inst✝¹² : IsDomain R
inst✝¹¹ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R M₂
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : Module R N₂
P : RootPairing ι R M N
inst✝⁶ : P.IsRootSystem
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝³ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
inst✝² : Finite ι₂
inst✝¹ : P₂.IsRootSystem
inst✝ : P₂.IsReduced
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
f : M ≃ₗ[R] M₂ := b.toWeightBasis.equiv b₂.toWeightBasis e
m : M
h : m ∈ range ⇑P.root
⊢ f m ∈ range ⇑P₂.root
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
⊢ eval (-↑k) (ascPochhammer R (n + 1)) = 0

Tactic:
ascPochhammer_succ_eval

Goal state after:
case succ
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ.inl
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : k < n
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

pp: case succ.inr.inl
R : Type u
inst✝ : Ring R
k : ℕ
ih : k < k → eval (-↑k) (ascPochhammer R k) = 0
h : k < k + 1
⊢ eval (-↑k) (ascPochhammer R k) * (-↑k + ↑k) = 0

pp: case succ.inr.inr
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : n < k
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

Tactic:
· simp [ih hkn]

Goal state after:
case succ.inr.inl
R : Type u
inst✝ : Ring R
k : ℕ
ih : k < k → eval (-↑k) (ascPochhammer R k) = 0
h : k < k + 1
⊢ eval (-↑k) (ascPochhammer R k) * (-↑k + ↑k) = 0

case succ.inr.inr
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : n < k
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
⊢ projVandermonde v w i = Pi.single (last n) (v i ^ n)

Tactic:
ext j
  obtain rfl | hlt := j.le_last.eq_or_lt
  · simp [projVandermonde_apply]
  rw [projVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]
  simpa [Nat.sub_eq_zero_iff_le] using! hlt

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i j : ι
hij : i ≠ j
⊢ Lagrange.basis {i, j} v j = basisDivisor (v j) (v i)

Tactic:
rw [pair_comm]
  exact basis_pair_left hij.symm

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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹⁰ : Finite ι₁
inst✝⁹ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁸ : LieRing L₁
inst✝⁷ : LieRing L₂
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieAlgebra K L₁
inst✝³ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝² : LieAlgebra K L₂
inst✝¹ : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
⊢ False

Tactic:
let f : H₁ × H₂ →ₗ[K] prodCartan eι b₁ b₂ :=
    { toFun x := ⟨⟨⟨x.fst, x.snd⟩, by simp [contra]⟩, this x _⟩
      map_add' := by simp
      map_smul' := by simp }

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹⁰ : Finite ι₁
inst✝⁹ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁸ : LieRing L₁
inst✝⁷ : LieRing L₂
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieAlgebra K L₁
inst✝³ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝² : LieAlgebra K L₂
inst✝¹ : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
f : ↥H₁ × ↥H₂ →ₗ[K] ↥(prodCartan eι b₁ b₂) := { toFun := fun x ↦ ⟨⟨(↑x.1, ↑x.2), ⋯⟩, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
⊢ False
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
hP : P.degree < ↑(#s)
⊢ P.coeff (#s - 1) = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
by
  nth_rewrite 1 [eq_interpolate hvs hP, interpolate_apply, finsetSum_coeff]
  congr! with i hi
  rw [coeff_C_mul, ← natDegree_basis hvs hi, ← leadingCoeff, leadingCoeff_basis hvs hi]
  field_simp

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

Goal state before:
pp: L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
h₁ : ∀ (i j : I), ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j)
h₂ : ∀ (i j : I), ⁅y, v.end (i, j)⁆ = (fμ i - fμ j) • v.end (i, j)
r : K[X]
hr : ∀ (i j : I), Polynomial.eval (μ i - μ j) r = (algebraMap ℚ K) (↑f ⟨μ i, ⋯⟩) - (algebraMap ℚ K) (↑f ⟨μ j, ⋯⟩)
x✝ : I × I
i j : I
⊢ ((aeval ((ad K (End K M)) s)) r) (v.end (i, j)) = ⁅y, v.end (i, j)⁆

Tactic:
aeval_apply_of_mem_apply_eq_smul (h₁ i j),

Goal state after:
L : Type u_2
M : Type u_3
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : IsAlgClosed K
inst✝³ : LieAlgebra K L
inst✝² : Module K M
inst✝¹ : LieModule K L M
inst✝ : FiniteDimensional K M
h : traceForm K L M = 0
φ : L →ₗ⁅K⁆ End K M := toEnd K L M
x : L
hx : x ∈ derivedSeries K L 1
n : End K M
hn_adj : n ∈ K[φ x]
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : φ x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top (eigenspaces_iSupIndep s)
    (IsSemisimple.iSup_eigenspace_eq_top hs_ss)
I : Type (max u_4 0) := (ν : K) × Fin (finrank K ↥(s.eigenspace ν))
v : Basis I K M := eigenDecomp.collectedBasis fun μ ↦ finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst
hsv : ∀ (i : I), s (v i) = μ i • v i
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : I → K := fun i ↦ ↑(f ⟨μ i, ⋯⟩)
y : End K M := (Matrix.toLin v v) (Matrix.diagonal fμ)
hyv : ∀ (i : I), y (v i) = fμ i • v i
z : End K M
hz : z ∈ φ.range
h₁ : ∀ (i j : I), ⁅s, v.end (i, j)⁆ = (μ i - μ j) • v.end (i, j)
h₂ : ∀ (i j : I), ⁅y, v.end (i, j)⁆ = (fμ i - fμ j) • v.end (i, j)
r : K[X]
hr : ∀ (i j : I), Polynomial.eval (μ i - μ j) r = (algebraMap ℚ K) (↑f ⟨μ i, ⋯⟩) - (algebraMap ℚ K) (↑f ⟨μ j, ⋯⟩)
x✝ : I × I
i j : I
⊢ Polynomial.eval (μ i - μ j) r • v.end (i, j) = ⁅y, v.end (i, j)⁆
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R (M₁ × M₂) := b₁.prod b₂
⊢ (f₁.prodMap f₂).charpoly = f₁.charpoly * f₂.charpoly

Tactic:
rw [← charpoly_toMatrix f₁ b₁, ← charpoly_toMatrix f₂ b₂, ← charpoly_toMatrix (f₁.prodMap f₂) b,
    toMatrix_prodMap b₁ b₂ f₁ f₂, Matrix.charpoly_fromBlocks_zero₁₂]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)), _root_.IsNilpotent ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)) x)
x : L
hx : x ∈ derivedSeries R L 1
⊢ 1 ⊗ₜ[R] x ∈ derivedSeries A (A ⊗[R] L) 1

Tactic:
derivedSeries_baseChange

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
inst✝³ : Module R M
inst✝² : LieModule R L M
inst✝¹ : IsNoetherian R M
inst✝ : Free R M
h : traceForm R L M = 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)), _root_.IsNilpotent ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)) x)
x : L
hx : x ∈ derivedSeries R L 1
⊢ 1 ⊗ₜ[R] x ∈ LieSubmodule.baseChange A (derivedSeries R L 1)
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : LieModule.traceForm R (↥DI) L = 0
⊢ IsSolvable ↥I

Tactic:
have module_nilp : LieModule.IsNilpotent (derivedSeries R DI 1) L :=
    LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero tf_eq_zero

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
I : LieIdeal R L
DI : LieIdeal R L := ⁅I, I⁆
h : ∀ x ∈ I, ∀ y ∈ DI, ((killingForm R L) x) y = 0
DDI : LieIdeal R L := ⁅DI, DI⁆
tf_eq_zero : LieModule.traceForm R (↥DI) L = 0
module_nilp : LieModule.IsNilpotent (↥(derivedSeries R (↥DI) 1)) L
⊢ IsSolvable ↥I
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst✝ : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
⊢ ↑n ≤ φ.support.sup fun s ↦ ↑((weight w) s)

Tactic:
· obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h
    simp only [← hφ hd]
    replace hd := Finsupp.mem_support_iff.mpr hd
    apply Finset.le_sup hd

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
h : ∀ (x y : L), y ∈ derivedSeries R L 1 → ((killingForm R L) x) y = 0
this : IsSolvable ↥⊤
⊢ IsSolvable L

Tactic:
← solvable_iff_equiv_solvable LieSubalgebra.topEquiv (R := R)

Goal state after:
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CharZero R
inst✝⁴ : IsDomain R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsNoetherian R L
inst✝ : Module.Free R L
h : ∀ (x y : L), y ∈ derivedSeries R L 1 → ((killingForm R L) x) y = 0
this : IsSolvable ↥⊤
⊢ IsSolvable ↥⊤