mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
x y : L
hx : x ∈ (Submodule.toAddSubmonoid 0).carrier
_hy : y ∈ (Submodule.toAddSubmonoid 0).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.toAddSubmonoid 0).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : A₁
x✝ : L₁
⊢ (AlgHom.id R A₁) ⁅x✝, x✝¹⁆ =
    ⁅{ toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
        x✝,
      (AlgHom.id R A₁) x✝¹⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' L'' : LieRinehartSubalgebra A L
h : (fun L' ↦ L'.carrier) L' = (fun L' ↦ L'.carrier) L''
⊢ L' = L''

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x y z : ↥L'
⊢ ⟨⁅↑(x + y), ↑z⁆, ⋯⟩ = ⟨⁅↑x, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑z⁆, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x y z : ↥L'
⊢ ⟨⁅↑x, ↑(y + z)⁆, ⋯⟩ = ⟨⁅↑x, ↑y⁆, ⋯⟩ + ⟨⁅↑x, ↑z⁆, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x : ↥L'
⊢ ⟨⁅↑x, ↑x⁆, ⋯⟩ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x y z : ↥L'
⊢ ⟨⁅↑x, ↑⟨⁅↑y, ↑z⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅↑⟨⁅↑x, ↑y⁆, ⋯⟩, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑⟨⁅↑x, ↑z⁆, ⋯⟩⁆, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
⊢ Function.Injective toSubmodule

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝⁴ : CommRing A
inst✝³ : LieRing L
inst✝² : Module A L
L' : LieRinehartSubalgebra A L
inst✝¹ : LieRingModule L A
inst✝ : LieRinehartRing A L
x✝² x✝¹ : ↥L'
x✝ : A
⊢ ⁅x✝², x✝ • x✝¹⁆ = x✝ • ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆ • x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁵ : LieRingModule L A
inst✝⁴ : LieRinehartRing A L
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R A
inst✝¹ : LieAlgebra R L
inst✝ : LieRinehartAlgebra R A L
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module A L
inst✝⁵ : LieRingModule L A
inst✝⁴ : LieRinehartRing A L
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R A
inst✝¹ : LieAlgebra R L
inst✝ : LieRinehartAlgebra R A L
L₁' L₂' : LieRinehartSubalgebra A L
h : (fun L' ↦ L'.toLieSubalgebra R) L₁' = (fun L' ↦ L'.toLieSubalgebra R) L₂'
⊢ L₁' = L₂'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : LieRing L
inst✝¹⁰ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁹ : LieRingModule L A
inst✝⁸ : LieRinehartRing A L
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R A
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRinehartAlgebra R A L
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L M
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : LieRing L
inst✝¹⁰ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁹ : LieRingModule L A
inst✝⁸ : LieRinehartRing A L
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R A
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRinehartAlgebra R A L
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L M
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
x✝ : m ∈ ↑p
⊢ 0 • m ∈ ↑p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
a : A
b : B
hm : m ∈ ↑p
⊢ a ⊗ₜ[R] b • m ∈ ↑p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : AddSubmonoid M
hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p
hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p
ab : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz : m ∈ ↑p → z • m ∈ ↑p
hw : m ∈ ↑p → w • m ∈ ↑p
hm : m ∈ ↑p
⊢ (z + w) • m ∈ ↑p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
this : a • m = a ⊗ₜ[R] 1 • m
⊢ a • m ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
this : b • m = 1 ⊗ₜ[R] b • m
⊢ b • m ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m ∈ p

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (A n).diag = 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ B n i i = 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ C n i i = 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ D n i i = 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ A n i j ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Card

Goal state before:
pp: R : Type u
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : Module.IsTorsionFree R E
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ B n i j ≤ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ C n i j ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ n - E.order + ↑k < n

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ D n i j ≤ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (A n)ᵀ = A n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
⊢ E.IsSolution (E.mkSol init)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
⊢ E.IsSolution (E.mkSol init)

Tactic:
by
  intro n
  rw [mkSol]
  simp

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

Goal state before:
pp: n : ℕ
⊢ (B n)ᵀ = C n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (C n)ᵀ = B n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
init : Fin E.order → R
⊢ ∀ (n : Fin E.order), E.mkSol init ↑n = init n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (D n)ᵀ = D n

Tactic:
by

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

Goal state before:
pp: ⊢ A 1 = !![2]

Tactic:
by

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

Goal state before:
pp: ⊢ A 2 = !![2, -1; -1, 2]

Tactic:
by

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

Goal state before:
pp: ⊢ A 3 = !![2, -1, 0; -1, 2, -1; 0, -1, 2]

Tactic:
by

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

Goal state before:
pp: ⊢ B 1 = A 1

Tactic:
by

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

Goal state before:
pp: ⊢ C 1 = A 1

Tactic:
by

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

Goal state before:
pp: ⊢ D 1 = A 1

Tactic:
by

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

Goal state before:
pp: ⊢ D 2 = !![2, 0; 0, 2]

Tactic:
by

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

Goal state before:
pp: ⊢ B 2 = !![2, -2; -1, 2]

Tactic:
by

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

Goal state before:
pp: ⊢ C 2 = !![2, -1; -2, 2]

Tactic:
by

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

Goal state before:
pp: ⊢ D 3 = !![2, -1, -1; -1, 2, 0; -1, 0, 2]

Tactic:
by

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

Goal state before:
pp: ⊢ (reindex ((↑[0, 1]).formPerm ⋯) ((↑[0, 1]).formPerm ⋯)) (D 3) = A 3

Tactic:
by

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

Goal state before:
pp: ⊢ D 4 = !![2, -1, 0, 0; -1, 2, -1, -1; 0, -1, 2, 0; 0, -1, 0, 2]

Tactic:
by

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

Goal state before:
pp: i : Fin 6
⊢ E₆ i i = 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
⊢ ∀ (n : ℕ), u n = E.mkSol init n

Tactic:
by

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

Goal state before:
pp: i : Fin 7
⊢ E₇ i i = 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ {u | E.IsSolution u}
hv : v ∈ {u | E.IsSolution u}
n : ℕ
⊢ (u + v) (n + E.order) = ∑ i, E.coeffs i * (u + v) (n + ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
n : ℕ
⊢ 0 (n + E.order) = ∑ i, E.coeffs i * 0 (n + ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
a : R
u : ℕ → R
hu : u ∈ {u | E.IsSolution u}
n : ℕ
⊢ (a • u) (n + E.order) = ∑ i, E.coeffs i * (a • u) (n + ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ↥E.solSpace
⊢ (fun x ↦ ↑(u + v) ↑x) = (fun x ↦ ↑u ↑x) + fun x ↦ ↑v ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
a : R
u : ↥E.solSpace
⊢ (fun x ↦ ↑(a • u) ↑x) = (RingHom.id R) a • fun x ↦ ↑u ↑x

Tactic:
by

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

Goal state before:
pp: i : Fin 8
⊢ E₈ i i = 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
⊢ (fun u ↦ ⟨E.mkSol u, ⋯⟩) ((fun u x ↦ ↑u ↑x) u) = u

Tactic:
by

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

Goal state before:
pp: i : Fin 4
⊢ F₄ i i = 2

Tactic:
by

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

Goal state before:
pp: i : Fin 2
⊢ G₂ i i = 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : E.IsSolution u
hv : E.IsSolution v
⊢ u = v ↔ Set.EqOn u v ↑(range E.order)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
⊢ (fun i ↦ if h : ↑i + 1 < E.order then (x + y) ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * (x + y) i) =
    (fun i ↦ if h : ↑i + 1 < E.order then x ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * x i) + fun i ↦
      if h : ↑i + 1 < E.order then y ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * y i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x✝¹ : R
y : Fin E.order → R
i : Fin E.order
h : ¬↑i + 1 < E.order
x : Fin E.order
x✝ : x ∈ univ
⊢ E.coeffs x * (x✝¹ * y x) = x✝¹ * (E.coeffs x * y x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
⊢ (fun i ↦ if h : ↑i + 1 < E.order then (x • y) ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * (x • y) i) =
    (RingHom.id R) x • fun i ↦ if h : ↑i + 1 < E.order then y ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * y i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
⊢ (fun i ↦ if h : ↑i + 1 < E.order then (x • y) ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * (x • y) i) =
    (RingHom.id R) x • fun i ↦ if h : ↑i + 1 < E.order then y ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * y i

Tactic:
by
    ext i
    split_ifs with h <;>
      simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, h, ↓reduceDIte, mul_sum]
    exact sum_congr rfl fun x _ ↦ by ac_rfl

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
E : LinearRecurrence R
⊢ Module.rank R ↥E.solSpace = ↑E.order

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ E.charPoly.degree = ↑E.order

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ ((monomial ↑x✝¹) (E.coeffs x✝¹)).degree < ↑E.order

Tactic:
degree_monomial_le

Goal state after:
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ ↑↑x✝¹ < ↑E.order
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
⊢ E.charPoly.Monic

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝ : H.IsCartanSubalgebra
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
⊢ corootSubmodule α ≤ LieSubmodule.restr I H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) → q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0

Tactic:
intro h
    simpa [sub_eq_zero] using h 0

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
y : L
hy : y ∈ rootSpace H γ
⊢ γ (coroot α) • y ∈ ↑I

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α : Weight K (↥H) L
hα : rootSpace H ⇑α ≤ LieSubmodule.restr I H
γ : ↥H → K
hγ_ne : γ (coroot α) ≠ 0
⊢ rootSpace H γ ≤ LieSubmodule.restr I H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
h : q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0
n : ℕ
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ q ^ n * (E.coeffs x✝¹ * q ^ ↑x✝¹) = E.coeffs x✝¹ * (q ^ n * q ^ ↑x✝¹)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥LieSubalgebra.root
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
h : ∀ (γ δ : ↥LieSubalgebra.root), δ ∈ I.rootSet → (S.reflectionPerm γ) δ ∈ I.rootSet
⊢ ((rootSystem H).reflectionPerm β) α ∈ I.rootSet ↔ α ∈ I.rootSet

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) ↔ E.charPoly.IsRoot q

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥LieSubalgebra.root
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H ⇑(S.root' γ) ≤ LieSubmodule.restr I H
⊢ S.pairing ((S.reflectionPerm γ) δ) γ ≠ 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥LieSubalgebra.root
⊢ ((rootSystem H).reflectionPerm β) α ∈ I.rootSet ↔ α ∈ I.rootSet

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ I.rootSpan ∈ (rootSystem H).invtRootSubmodule

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
⊢ ¬IsUnit p

Tactic:
by

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
h : ↥H
hI : ↑h ∈ I
β : ↥LieSubalgebra.root
hβ : ↑β h ≠ 0
y : L
hy : y ∈ rootSpace H ⇑↑β
⊢ ↑β h • y ∈ ↑I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
⊢ p ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = p * ↑ha.unit⁻¹

Tactic:
by

Goal state after: