mathlib-initiative/mathlib-tactics huggingface dataset:
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:
[

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
⊢ A.vec = B.vec ↔ A = B
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: ι : Type u_2
m : Type u_3
n : Type u_4
R : Type u_1
inst✝ : AddCommMonoid R
s : Finset ι
A : ι → Matrix m n R
x✝ : n × m
⊢ (∑ i ∈ s, A i).vec x✝ = (∑ i ∈ s, (A i).vec) x✝

Tactic:
[

Goal state after:
ι : Type u_2
m : Type u_3
n : Type u_4
R : Type u_1
inst✝ : AddCommMonoid R
s : Finset ι
A : ι → Matrix m n R
x✝ : n × m
⊢ (∑ i ∈ s, A i).vec x✝ = (∑ i ∈ s, (A i).vec) x✝
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_1
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace

Tactic:
[

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_1
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Mul R
inst✝² : Star R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ star A.vec ⬝ᵥ B.vec = (Aᴴ * B).trace

Tactic:
[

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Mul R
inst✝² : Star R
inst✝¹ : Fintype m
inst✝ : Fintype n
A B : Matrix m n R
⊢ star A.vec ⬝ᵥ B.vec = (Aᴴ * B).trace
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
⊢ (A.map f).IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : A.IsHermitian
f : α → β
hf : Function.Semiconj f star star
⊢ (A.map f)ᴴ = A.map f
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
⊢ (A.map f).IsHermitian ↔ A.IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
⊢ (A.map f)ᴴ = A.map f ↔ A.IsHermitian
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
⊢ (A.map f)ᴴ = A.map f ↔ A.IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
f : α → β
hf : Function.Semiconj f star star
hinj : Function.Injective f
⊢ (A.map f)ᴴ = A.map f ↔ Aᴴ = A
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ Aᵀ.IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : A.IsHermitian
⊢ Aᵀᴴ = Aᵀ
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)

Tactic:
[

Goal state after:
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

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

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A)ᴴ = (comp m m n n α) A ↔ A.IsHermitian
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A)ᴴ = (comp m m n n α) A ↔ A.IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A)ᴴ = (comp m m n n α) A ↔ Aᴴ = A
Module: Mathlib.LinearAlgebra.Matrix.Vec

Goal state before:
pp: l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ (X.vec ᵥ* kroneckerMap (fun x1 x2 ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)

Tactic:
[

Goal state after:
l✝ : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m l✝ R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l✝), Commute (A i j) x
k : p
l : l✝
⊢ (X.vec ᵥ* kroneckerMap (fun x1 x2 ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝¹ : CommMonoid α
inst✝ : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
⊢ (A ⊙ B).IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
n : Type u_4
inst✝¹ : CommMonoid α
inst✝ : StarMul α
A B : Matrix n n α
hA : A.IsHermitian
hB : B.IsHermitian
⊢ (A ⊙ B)ᴴ = A ⊙ B
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
R : Type u_5
inst✝³ : Star R
inst✝² : Star α
inst✝¹ : SMul R α
inst✝ : StarModule R α
A : Matrix n n α
h : A.IsHermitian
k : R
hk : IsSelfAdjoint k
⊢ (k • A).IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
n : Type u_4
R : Type u_5
inst✝³ : Star R
inst✝² : Star α
inst✝¹ : SMul R α
inst✝ : StarModule R α
A : Matrix n n α
h : A.IsHermitian
k : R
hk : IsSelfAdjoint k
⊢ (k • A)ᴴ = k • A
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
R : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Star R
inst✝³ : Star α
inst✝² : MulAction R α
inst✝¹ : StarModule R α
A : Matrix n n α
k : R
inst✝ : Invertible k
h : (k • A).IsHermitian
hk : IsSelfAdjoint k
⊢ A.IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
n : Type u_4
R : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Star R
inst✝³ : Star α
inst✝² : MulAction R α
inst✝¹ : StarModule R α
A : Matrix n n α
k : R
inst✝ : Invertible k
h : (k • A)ᴴ = k • A
hk : IsSelfAdjoint k
⊢ A.IsHermitian
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : NonUnitalSemiring α
inst✝¹ : StarRing α
inst✝ : Fintype n
A : Matrix m n α
⊢ (A * Aᴴ).IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : NonUnitalSemiring α
inst✝¹ : StarRing α
inst✝ : Fintype n
A : Matrix m n α
⊢ (A * Aᴴ)ᴴ = A * Aᴴ
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : NonUnitalSemiring α
inst✝¹ : StarRing α
inst✝ : Fintype m
A : Matrix m n α
⊢ (Aᴴ * A).IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : NonUnitalSemiring α
inst✝¹ : StarRing α
inst✝ : Fintype m
A : Matrix m n α
⊢ (Aᴴ * A)ᴴ = Aᴴ * A
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
h : A.IsHermitian
k : ℤ
⊢ (A ^ k).IsHermitian

Tactic:
IsHermitian,

Goal state after:
α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
h : A.IsHermitian
k : ℤ
⊢ (A ^ k)ᴴ = A ^ k
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A ^ (-↑k + -↑l) = A ^ (-↑k) * A ^ (-↑l)

Tactic:
[

Goal state after:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A ^ (-↑k + -↑l) = A ^ (-↑k) * A ^ (-↑l)
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-↑(n + 1)) = A ^ (-↑(n + 2)) * A

Tactic:
[

Goal state after:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-↑(n + 1)) = A ^ (-↑(n + 2)) * A
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
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective (star ∘ (fun v ↦ v ᵥ* B) ∘ star)
⊢ (B * A * Bᴴ).PosDef

Tactic:
[

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : Fintype n
inst✝ : Fintype m
A : Matrix n n R
B : Matrix m n R
hA : A.PosDef
hB : Function.Injective (star ∘ (fun v ↦ v ᵥ* B) ∘ star)
⊢ (B * A * Bᴴ).PosDef
Module: Mathlib.Algebra.Lie.Prod

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f g : L₁ × L₂ →ₗ⁅R⁆ L
⊢ f = g ↔ f.comp (inl R L₁ L₂) = g.comp (inl R L₁ L₂) ∧ f.comp (inr R L₁ L₂) = g.comp (inr R L₁ L₂)

Tactic:
[

Goal state after:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f g : L₁ × L₂ →ₗ⁅R⁆ L
⊢ f = g ↔ f.comp (inl R L₁ L₂) = g.comp (inl R L₁ L₂) ∧ f.comp (inr R L₁ L₂) = g.comp (inr R L₁ L₂)
Module: Mathlib.Algebra.Lie.Prod

Goal state before:
pp: R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f g : L₁ × L₂ →ₗ⁅R⁆ L
h :
  ↑f = ↑g ↔
    ↑f ∘ₗ LinearMap.inl R L₁ L₂ = ↑g ∘ₗ LinearMap.inl R L₁ L₂ ∧
      ↑f ∘ₗ LinearMap.inr R L₁ L₂ = ↑g ∘ₗ LinearMap.inr R L₁ L₂
⊢ (∀ (x : L₁ × L₂), f x = g x) ↔
    (∀ (x : L₁), (f.comp (inl R L₁ L₂)) x = (g.comp (inl R L₁ L₂)) x) ∧
      ∀ (x : L₂), (f.comp (inr R L₁ L₂)) x = (g.comp (inr R L₁ L₂)) x

Tactic:
[

Goal state after:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f g : L₁ × L₂ →ₗ⁅R⁆ L
h :
  ↑f = ↑g ↔
    ↑f ∘ₗ LinearMap.inl R L₁ L₂ = ↑g ∘ₗ LinearMap.inl R L₁ L₂ ∧
      ↑f ∘ₗ LinearMap.inr R L₁ L₂ = ↑g ∘ₗ LinearMap.inr R L₁ L₂
⊢ (∀ (x : L₁ × L₂), f x = g x) ↔
    (∀ (x : L₁), (f.comp (inl R L₁ L₂)) x = (g.comp (inl R L₁ L₂)) x) ∧
      ∀ (x : L₂), (f.comp (inr R L₁ L₂)) x = (g.comp (inr R L₁ L₂)) x
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
P : RootPairing ι R M N
b : P.Base
inst✝³ : P.IsCrystallographic
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
⊢ b.cartanMatrix i j = 0 ↔ P.root ↑i + P.root ↑j ∉ range ⇑P.root

Tactic:
by
  rw [b.cartanMatrix_eq_neg_chainTopCoeff hij, neg_eq_zero, Int.natCast_eq_zero,
    P.chainTopCoeff_eq_zero_iff]
  replace hij := b.linearIndependent_pair_of_ne hij.symm
  tauto

Goal state after:
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
P : RootPairing ι R M N
b : P.Base
inst✝⁴ : P.IsCrystallographic
inst✝³ : CharZero R
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
i j : ↥b.support
⊢ (algebraMap ℤ R) (b.cartanMatrix i j) * (P.RootForm (P.root ↑j)) (P.root ↑j) =
    (algebraMap ℤ R) 2 * (P.RootForm ↑(b.toWeightBasisInt i)) ↑(b.toWeightBasisInt j)

Tactic:
simpa [← algebraMap_pairingIn P ℤ i j] using
    congr_fun₂ (cartanMatrixIn_mul_diagonal_eq ℤ P.toInvariantForm b) i j

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
χ : ↥root
this : H.IsCartanSubalgebra := isCartanSubalgebra b
n : ι → ℕ
⊢ ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

Tactic:
[

Goal state after:
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
χ : ↥root
this : H.IsCartanSubalgebra := isCartanSubalgebra b
n : ι → ℕ
⊢ ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
χ : ↥root
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
⊢ (rootSystem H).root χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp') ∨
    -(rootSystem H).root χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

Tactic:
have hs : ⨆ α ∈ s, rootSpace H α = ⊤ := by
    have := b.iSup_cartan_borelLower_borelUpper_eq_top
    rw [borelLower_eq, borelUpper_eq, b.cartan_eq] at this
    rw [iSup_union, iSup_union]
    simpa [iSup_and, iSup_comm (ι := H → K)] using this

Goal state after:
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
χ : ↥root
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
hs : ⨆ α ∈ s, rootSpace H α = ⊤
⊢ (rootSystem H).root χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp') ∨
    -(rootSystem H).root χ ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
Module: Mathlib.Data.Nat.Factorial.BigOperators

Goal state before:
pp: k : ℕ
n : ℤ
⊢ (∏ i ∈ range k, (n + ↑i) % ↑k !) % ↑k ! = 0

Tactic:
[

Goal state after:
k : ℕ
n : ℤ
⊢ (∏ i ∈ range k, (n + ↑i) % ↑k !) % ↑k ! = 0
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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
hk : k ∈ b.support
this : f k = g k
⊢ f k • P.root k = g k • P.root k

Tactic:
this

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
hk : k ∈ b.support
this : f k = g k
⊢ g k • P.root k = g k • P.root k
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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
⊢ ∀ (k : ι), P.pairingIn ℤ i k = ∑ l ∈ b.support, f l * P.pairingIn ℤ l k

Tactic:
refine fun k ↦ algebraMap_injective ℤ R ?_

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
⊢ (algebraMap ℤ R) (P.pairingIn ℤ i k) = (algebraMap ℤ R) (∑ l ∈ b.support, f l * P.pairingIn ℤ l k)
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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
⊢ (algebraMap ℤ R) (P.pairingIn ℤ i k) = (algebraMap ℤ R) (∑ l ∈ b.support, f l * P.pairingIn ℤ l k)

Tactic:
[

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
k : ι
⊢ (algebraMap ℤ R) (P.pairingIn ℤ i k) = (algebraMap ℤ R) (∑ l ∈ b.support, f l * P.pairingIn ℤ l k)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ n + (X + ↑n).natDegree = n + 1

pp: S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ ascPochhammer S n ≠ 0

Tactic:
this

Goal state after:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ n + 1 = n + 1

S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ ascPochhammer S n ≠ 0
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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
⊢ ∀ (k : ι), P.pairingIn ℤ j k = ∑ l ∈ b.support, g l * P.pairingIn ℤ l k

Tactic:
refine fun k ↦ algebraMap_injective ℤ R ?_

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
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
i j : ι
hij : (fun i k ↦ P.pairingIn ℤ i ↑k) i = (fun i k ↦ P.pairingIn ℤ i ↑k) j
f g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
f' : ↥b.support → ℤ := f ∘ Subtype.val
g' : ↥b.support → ℤ := g ∘ Subtype.val
hf : (fun k ↦ P.pairingIn ℤ i ↑k) = f' ᵥ* b.cartanMatrix
k : ι
⊢ (algebraMap ℤ R) (P.pairingIn ℤ j k) = (algebraMap ℤ R) (∑ l ∈ b.support, g l * P.pairingIn ℤ l k)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 1)) = ↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1))

Tactic:
[

Goal state after:
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 1)) = ↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1))