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

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q)ᵀ * f ((fromBlocks 1 0 0 0).submatrix ⇑s ⇑s) = f ((fromBlocks 1 0 0 0).submatrix ⇑s ⇑s)ᵀ * f Q
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0

Tactic:
← (f Q).fromBlocks_toBlocks,

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 :
  (fromBlocks (f Q).toBlocks₁₁ (f Q).toBlocks₁₂ (f Q).toBlocks₂₁ (f Q).toBlocks₂₂)ᵀ *
      f ((fromBlocks 1 0 0 0).submatrix ⇑s ⇑s) =
    f ((fromBlocks 1 0 0 0).submatrix ⇑s ⇑s)ᵀ *
      fromBlocks (f Q).toBlocks₁₁ (f Q).toBlocks₁₂ (f Q).toBlocks₂₁ (f Q).toBlocks₂₂
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
i✝ j✝ : m
⊢ (if i✝ = j✝ then if D i✝ = 0 then D j✝ else (D i✝)⁻¹ * D j✝ else 0) = if i✝ = j✝ then if D i✝ = 0 then 0 else 1 else 0

Tactic:
split_ifs with h1 h2 <;> first | rw [← h1, h2] | rw [← h1, inv_mul_cancel₀ h2] | rfl

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

Goal state before:
pp: case mp
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ⇑g ∘ ⇑(ι R) = ⇑f → (lift R).symm g = f

pp: case mpr
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ (lift R).symm g = f → ⇑g ∘ ⇑(ι R) = ⇑f

Tactic:
<;>

Goal state after:
case mp
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ⇑g ∘ ⇑(ι R) = ⇑f → (lift R).symm g = f

case mpr
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ (lift R).symm g = f → ⇑g ∘ ⇑(ι R) = ⇑f
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case e_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ f (Multiplicative.toAdd 1) = 0

pp: case e_4.e_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ (fun x ↦ x ∈ gradeBy R (⇑f) (f (Multiplicative.toAdd 1))) = fun x ↦ x ∈ gradeBy R (⇑f) 0

pp: case e_4.e_4
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ ⋯ ≍ ⋯

Tactic:
<;>

Goal state after:
case e_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ f (Multiplicative.toAdd 1) = 0

case e_4.e_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ (fun x ↦ x ∈ gradeBy R (⇑f) (f (Multiplicative.toAdd 1))) = fun x ↦ x ∈ gradeBy R (⇑f) 0

case e_4.e_4
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ ⋯ ≍ ⋯
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
hn✝ : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ 0) x = (p.cycleOf x ^ m) x → 0 = m

pp: case neg.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ m) x → n + 1 = m

Tactic:
<;>

Goal state after:
case neg.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
hn✝ : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ 0) x = (p.cycleOf x ^ m) x → 0 = m

case neg.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
⊢ (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ m) x → n + 1 = m
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : f x = x
hy : f y = y
⊢ s = s

pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : f x = x
hy : ¬f y = y
⊢ ↑(f.toList y) = ↑(f.toList y)

pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : f y = y
⊢ ↑(f.toList x) = ↑(f.toList x)

pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : ¬f y = y
⊢ ↑(f.toList x) = ↑(f.toList y)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : f x = x
hy : f y = y
⊢ s = s

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : f x = x
hy : ¬f y = y
⊢ ↑(f.toList y) = ↑(f.toList y)

case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : f y = y
⊢ ↑(f.toList x) = ↑(f.toList x)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : ¬f y = y
⊢ ↑(f.toList x) = ↑(f.toList y)
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ x ∈ f.toCycle hf → f x ≠ x

pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ f x ≠ x → x ∈ f.toCycle hf

Tactic:
· have ⟨l, hl⟩ := exists_toCycle_toList f hf
    simp only [hl, Cycle.mem_coe_iff, ne_eq]
    intro h
    have ⟨h1, h2⟩ := mem_toList_iff.mp h
    exact ((isCycle_iff_sameCycle (mem_support.mp h2)).mp (y := x) hf).mp h1

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ f x ≠ x → x ∈ f.toCycle hf
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x : L
⊢ E.proj (s₁ x - s₂ x) = 0

Tactic:
rw [map_sub, sub_eq_zero, hs₁, hs₂]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s, (↑s).formPerm ⋯ = f

Tactic:
by
  obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.existsUnique_cycle
  refine ⟨⟨s, hs⟩, rfl, ?_⟩
  rintro ⟨t, ht⟩ ht'
  simpa using hs' _ ⟨ht, ht'⟩

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝ : i = j
⊢ 2 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i
⊢ -1 ≤ 0

pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : ¬(↑i + 1 = ↑j ∨ ↑j + 1 = ↑i)
⊢ 0 ≤ 0

Tactic:
<;>

Goal state after:
case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝ : i = j
⊢ 2 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i
⊢ -1 ≤ 0

case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : ¬(↑i + 1 = ↑j ∨ ↑j + 1 = ↑i)
⊢ 0 ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝ : i = j
⊢ 2 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ↑i + 1 = ↑j
h✝ : ↑j = n - 1
⊢ -2 ≤ 0

pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ↑i + 1 = ↑j
h✝ : ¬↑j = n - 1
⊢ -1 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬↑i + 1 = ↑j
h✝ : ↑j + 1 = ↑i
⊢ -1 ≤ 0

pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬↑i + 1 = ↑j
h✝ : ¬↑j + 1 = ↑i
⊢ 0 ≤ 0

Tactic:
<;>

Goal state after:
case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝ : i = j
⊢ 2 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ↑i + 1 = ↑j
h✝ : ↑j = n - 1
⊢ -2 ≤ 0

case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ↑i + 1 = ↑j
h✝ : ¬↑j = n - 1
⊢ -1 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬↑i + 1 = ↑j
h✝ : ↑j + 1 = ↑i
⊢ -1 ≤ 0

case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬↑i + 1 = ↑j
h✝ : ¬↑j + 1 = ↑i
⊢ 0 ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝ : i = j
⊢ 2 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : ↑i + 1 = ↑j
⊢ -1 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝³ : ¬i = j
h✝² : ¬↑i + 1 = ↑j
h✝¹ : ↑j + 1 = ↑i
h✝ : ↑i = n - 1
⊢ -2 ≤ 0

pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝³ : ¬i = j
h✝² : ¬↑i + 1 = ↑j
h✝¹ : ↑j + 1 = ↑i
h✝ : ¬↑i = n - 1
⊢ -1 ≤ 0

pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬↑i + 1 = ↑j
h✝ : ¬↑j + 1 = ↑i
⊢ 0 ≤ 0

Tactic:
<;>

Goal state after:
case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝ : i = j
⊢ 2 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : ↑i + 1 = ↑j
⊢ -1 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝³ : ¬i = j
h✝² : ¬↑i + 1 = ↑j
h✝¹ : ↑j + 1 = ↑i
h✝ : ↑i = n - 1
⊢ -2 ≤ 0

case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝³ : ¬i = j
h✝² : ¬↑i + 1 = ↑j
h✝¹ : ↑j + 1 = ↑i
h✝ : ¬↑i = n - 1
⊢ -1 ≤ 0

case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬↑i + 1 = ↑j
h✝ : ¬↑j + 1 = ↑i
⊢ 0 ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝ : i = j
⊢ 2 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : n ≤ 2
⊢ 0 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬n ≤ 2
h✝ : ↑i + 1 = ↑j ∧ ↑j + 2 < n
⊢ -1 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝³ : ¬i = j
h✝² : ¬n ≤ 2
h✝¹ : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝ : ↑j + 1 = ↑i ∧ ↑i + 2 < n
⊢ -1 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝⁴ : ¬i = j
h✝³ : ¬n ≤ 2
h✝² : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝¹ : ¬(↑j + 1 = ↑i ∧ ↑i + 2 < n)
h✝ : ↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n)
⊢ -1 ≤ 0

pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝⁵ : ¬i = j
h✝⁴ : ¬n ≤ 2
h✝³ : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝² : ¬(↑j + 1 = ↑i ∧ ↑i + 2 < n)
h✝¹ : ¬(↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n))
h✝ : ↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n)
⊢ -1 ≤ 0

pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝⁵ : ¬i = j
h✝⁴ : ¬n ≤ 2
h✝³ : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝² : ¬(↑j + 1 = ↑i ∧ ↑i + 2 < n)
h✝¹ : ¬(↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n))
h✝ : ¬(↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n))
⊢ 0 ≤ 0

Tactic:
<;>

Goal state after:
case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝ : i = j
⊢ 2 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : n ≤ 2
⊢ 0 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬n ≤ 2
h✝ : ↑i + 1 = ↑j ∧ ↑j + 2 < n
⊢ -1 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝³ : ¬i = j
h✝² : ¬n ≤ 2
h✝¹ : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝ : ↑j + 1 = ↑i ∧ ↑i + 2 < n
⊢ -1 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝⁴ : ¬i = j
h✝³ : ¬n ≤ 2
h✝² : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝¹ : ¬(↑j + 1 = ↑i ∧ ↑i + 2 < n)
h✝ : ↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n)
⊢ -1 ≤ 0

case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝⁵ : ¬i = j
h✝⁴ : ¬n ≤ 2
h✝³ : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝² : ¬(↑j + 1 = ↑i ∧ ↑i + 2 < n)
h✝¹ : ¬(↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n))
h✝ : ↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n)
⊢ -1 ≤ 0

case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝⁵ : ¬i = j
h✝⁴ : ¬n ≤ 2
h✝³ : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝² : ¬(↑j + 1 = ↑i ∧ ↑i + 2 < n)
h✝¹ : ¬(↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n))
h✝ : ¬(↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n))
⊢ 0 ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

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

Tactic:
ext; simp only [A, transpose_apply, of_apply]; grind

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:
intro n
  rw [mkSol]
  simp only [n.is_lt, dif_pos, Fin.mk_val]

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

Goal state before:
pp: case «0»
⊢ E₆ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

pp: case «1»
⊢ E₆ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

pp: case «2»
⊢ E₆ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

pp: case «3»
⊢ E₆ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

pp: case «4»
⊢ E₆ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

pp: case «5»
⊢ E₆ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

Tactic:
<;>

Goal state after:
case «0»
⊢ E₆ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ E₆ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

case «2»
⊢ E₆ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

case «3»
⊢ E₆ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

case «4»
⊢ E₆ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

case «5»
⊢ E₆ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

pp: case «1»
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

pp: case «2»
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

pp: case «3»
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

pp: case «4»
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

pp: case «5»
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

pp: case «6»
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) = 2

Tactic:
<;>

Goal state after:
case «0»
⊢ E₇ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ E₇ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

case «2»
⊢ E₇ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

case «3»
⊢ E₇ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

case «4»
⊢ E₇ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

case «5»
⊢ E₇ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

case «6»
⊢ E₇ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

pp: case «1»
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

pp: case «2»
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

pp: case «3»
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

pp: case «4»
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

pp: case «5»
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

pp: case «6»
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) = 2

pp: case «7»
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) = 2

Tactic:
<;>

Goal state after:
case «0»
⊢ E₈ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ E₈ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

case «2»
⊢ E₈ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

case «3»
⊢ E₈ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

case «4»
⊢ E₈ ((fun i ↦ i) ⟨4, ⋯⟩) ((fun i ↦ i) ⟨4, ⋯⟩) = 2

case «5»
⊢ E₈ ((fun i ↦ i) ⟨5, ⋯⟩) ((fun i ↦ i) ⟨5, ⋯⟩) = 2

case «6»
⊢ E₈ ((fun i ↦ i) ⟨6, ⋯⟩) ((fun i ↦ i) ⟨6, ⋯⟩) = 2

case «7»
⊢ E₈ ((fun i ↦ i) ⟨7, ⋯⟩) ((fun i ↦ i) ⟨7, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

pp: case «1»
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

pp: case «2»
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

pp: case «3»
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2

Tactic:
<;>

Goal state after:
case «0»
⊢ F₄ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

case «2»
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = 2

case «3»
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

pp: case «1»
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2

Tactic:
<;>

Goal state after:
case «0»
⊢ G₂ ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 2

case «1»
⊢ G₂ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 2
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «0»
j : Fin 6
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

pp: case «1»
j : Fin 6
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

pp: case «2»
j : Fin 6
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

pp: case «3»
j : Fin 6
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

pp: case «4»
j : Fin 6
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

pp: case «5»
j : Fin 6
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0

Tactic:
<;>

Goal state after:
case «0»
j : Fin 6
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨0, ⋯⟩) j ≤ 0

case «1»
j : Fin 6
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨1, ⋯⟩) j ≤ 0

case «2»
j : Fin 6
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨2, ⋯⟩) j ≤ 0

case «3»
j : Fin 6
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨3, ⋯⟩) j ≤ 0

case «4»
j : Fin 6
h : (fun i ↦ i) ⟨4, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨4, ⋯⟩) j ≤ 0

case «5»
j : Fin 6
h : (fun i ↦ i) ⟨5, ⋯⟩ ≠ j
⊢ E₆ ((fun i ↦ i) ⟨5, ⋯⟩) j ≤ 0
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
i : Fin E.order
h : ↑i + 1 < E.order
⊢ (x + y) ⟨↑i + 1, h⟩ =
    ((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)
      i

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ 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)
      i

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
i : Fin E.order
h : ↑i + 1 < E.order
⊢ (x + y) ⟨↑i + 1, h⟩ =
    ((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)
      i

case neg
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ 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)
      i
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case pos
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 • y) ⟨↑i + 1, h⟩ =
    ((RingHom.id R) x • fun i ↦ if h : ↑i + 1 < E.order then y ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * y i) i

pp: case neg
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
⊢ ∑ 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) i

Tactic:
<;>

Goal state after:
case pos
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 • y) ⟨↑i + 1, h⟩ =
    ((RingHom.id R) x • fun i ↦ if h : ↑i + 1 < E.order then y ⟨↑i + 1, h⟩ else ∑ i, E.coeffs i * y i) i

case neg
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
⊢ ∑ 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) i
Module: Mathlib.Algebra.LinearRecurrence

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

pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ((monomial E.order) 1).degree

Tactic:
<;>

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ ((monomial E.order) 1).degree = ↑E.order

R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (E.coeffs i)).degree < ((monomial E.order) 1).degree