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

Goal state before:
pp: K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ ↑n ≤ f.rank ↔ ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) ↦ f ↑x

Tactic:
simp only [le_rank_iff_exists_linearIndependent, Cardinal.lift_natCast, Cardinal.lift_eq_nat_iff,
    Cardinal.mk_set_eq_nat_iff_finset]

Goal state after:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s) ↔
    ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) ↦ f ↑x
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B ⇑f
hg : IsSkewAdjoint B ⇑g
⊢ IsAdjointPair B B ⇑(f * g) ⇑(-g * -f)

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B ⇑f
hg : IsSkewAdjoint B ⇑g
⊢ IsAdjointPair B B ⇑(f * g) ⇑(-g * -f)
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B ⇑f
hg : IsSkewAdjoint B ⇑g
hfg : IsAdjointPair B B ⇑(f * g) ⇑(g * f)
⊢ IsAdjointPair B B ⇑(g * f) ⇑(-f * -g)

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B ⇑f
hg : IsSkewAdjoint B ⇑g
hfg : IsAdjointPair B B ⇑(f * g) ⇑(g * f)
⊢ IsAdjointPair B B ⇑(g * f) ⇑(-f * -g)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
i : ChooseBasisIndex R L
⊢ (b.repr y) i * r + (b.repr x) i = (b.repr (r • y + x)) i

Tactic:
;

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
i : ChooseBasisIndex R L
⊢ (b.repr y) i * r + (b.repr x) i = (b.repr (r • y + x)) i
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B ⇑f
hg : IsSkewAdjoint B ⇑g
hfg : IsAdjointPair B B ⇑(f * g) ⇑(g * f)
hgf : IsAdjointPair B B ⇑(g * f) ⇑(f * g)
⊢ IsAdjointPair B B ⇑(f * g - g * f) ⇑(-(f * g - g * f))

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B ⇑f
hg : IsSkewAdjoint B ⇑g
hfg : IsAdjointPair B B ⇑(f * g) ⇑(g * f)
hgf : IsAdjointPair B B ⇑(g * f) ⇑(f * g)
⊢ IsAdjointPair B B ⇑(f * g - g * f) ⇑(-(f * g - g * f))
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y✝ : L
hyU : y✝ ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y✝, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
u : L
hu : u ∈ U
y : L
hy : y ∈ (engel K x).carrier
⊢ ⁅⟨u, hu⟩, y⁆ ∈ (engel K x).carrier

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y✝ : L
hyU : y✝ ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y✝, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
u : L
hu : u ∈ U
y : L
hy : y ∈ (engel K x).carrier
⊢ ⁅⟨u, hu⟩, y⁆ ∈ (engel K x).carrier
Module: Mathlib.LinearAlgebra.Matrix.Diagonal

Goal state before:
pp: m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ (fun i ↦ Submodule.map (toLin' (diagonal w)) (LinearMap.single K (fun a ↦ K) i).range) = fun i ↦
    ⨆ (_ : w i ≠ 0), (LinearMap.single K (fun x ↦ K) i).range

Tactic:
;

Goal state after:
m : Type u_1
inst✝² : Fintype m
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ (fun i ↦ Submodule.map (toLin' (diagonal w)) (LinearMap.single K (fun a ↦ K) i).range) = fun i ↦
    ⨆ (_ : w i ≠ 0), (LinearMap.single K (fun x ↦ K) i).range
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
this : χ = X ^ r
⊢ Ex ≤ Ey

Tactic:
apply_fun (fun p ↦ p.map (evalRingHom 1)) at this

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
this : Polynomial.map (evalRingHom 1) χ = Polynomial.map (evalRingHom 1) (X ^ r)
⊢ Ex ≤ Ey
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j k : n
r : R
⊢ ↑((singleSubSingle i j) r + (singleSubSingle j k) r) = ↑((singleSubSingle i k) r)

Tactic:
;

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j k : n
r : R
⊢ ↑((singleSubSingle i j) r + (singleSubSingle j k) r) = ↑((singleSubSingle i k) r)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j k : n
r : R
⊢ ↑((singleSubSingle i k) r - (singleSubSingle i j) r) = ↑((singleSubSingle j k) r)

Tactic:
;

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j k : n
r : R
⊢ ↑((singleSubSingle i k) r - (singleSubSingle i j) r) = ↑((singleSubSingle j k) r)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j k : n
r : R
⊢ ↑((singleSubSingle i k) r - (singleSubSingle j k) r) = ↑((singleSubSingle i j) r)

Tactic:
;

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j k : n
r : R
⊢ ↑((singleSubSingle i k) r - (singleSubSingle j k) r) = ↑((singleSubSingle i j) r)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
⊢ (Pso p q R i * Pso p q R (-i)) x y = 1 x y

Tactic:
;

Goal state after:
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
⊢ (Pso p q R i * Pso p q R (-i)) x y = 1 x y
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) x y = 1 x y

Tactic:
;

Goal state after:
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : p ⊕ q
⊢ ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i) x y = 1 x y
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) ↔
    A ∈ ↑(so (p ⊕ q) R)

Tactic:
;

Goal state after:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra ((Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i)) ↔
    A ∈ ↑(so (p ⊕ q) R)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra 1) ↔ A ∈ ↑(so (p ⊕ q) R)

Tactic:
;

Goal state after:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : Matrix (p ⊕ q) (p ⊕ q) R
⊢ A ∈ ↑(skewAdjointMatricesLieSubalgebra 1) ↔ A ∈ ↑(so (p ⊕ q) R)
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
x : n₀
⊢ ((A.submatrix r id).submatrix id c).col x ∈ range (A.submatrix r id).col

Tactic:
;

Goal state after:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
x : n₀
⊢ ((A.submatrix r id).submatrix id c).col x ∈ range (A.submatrix r id).col
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
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)

Tactic:
;

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
⊢ ∃ X, X.IsSymm ∧ IsUnit (A + X * C)
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).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ 0 = (f Q).toBlocks₁₂ ∧ (f Q).toBlocks₁₂ = 0
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0

Tactic:
;

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 : (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ 0 = (f Q).toBlocks₁₂ ∧ (f Q).toBlocks₁₂ = 0
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case refine_1
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).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
x : Fin (Fintype.card l - C.rank) → R
hx : (f Q).toBlocks₂₂ *ᵥ x = 0
⊢ fromBlocks (f Q).toBlocks₁₁ (f Q).toBlocks₁₂ (f Q).toBlocks₂₁ (f Q).toBlocks₂₂ • Sum.elim 0 x = 0

Tactic:
;

Goal state after:
case refine_1
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).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
x : Fin (Fintype.card l - C.rank) → R
hx : (f Q).toBlocks₂₂ *ᵥ x = 0
⊢ fromBlocks (f Q).toBlocks₁₁ (f Q).toBlocks₁₂ (f Q).toBlocks₂₁ (f Q).toBlocks₂₂ • Sum.elim 0 x = 0
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : oneCochain R L M
x x✝¹ x✝ : L
⊢ ⁅x, f x✝¹⁆ + ⁅x, f x✝⁆ - (⁅x✝¹, f x⁆ + ⁅x✝, f x⁆) - (f ⁅x, x✝¹⁆ + f ⁅x, x✝⁆) =
    ⁅x, f x✝¹⁆ - ⁅x✝¹, f x⁆ - f ⁅x, x✝¹⁆ + (⁅x, f x✝⁆ - ⁅x✝, f x⁆ - f ⁅x, x✝⁆)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : oneCochain R L M
x x✝¹ x✝ : L
⊢ ⁅x, f x✝¹⁆ + ⁅x, f x✝⁆ - (⁅x✝¹, f x⁆ + ⁅x✝, f x⁆) - (f ⁅x, x✝¹⁆ + f ⁅x, x✝⁆) =
    ⁅x, f x✝¹⁆ - ⁅x✝¹, f x⁆ - f ⁅x, x✝¹⁆ + (⁅x, f x✝⁆ - ⁅x✝, f x⁆ - f ⁅x, x✝⁆)
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : oneCochain R L M
x✝² x✝¹ x✝ : L
⊢ { toFun := fun y ↦ ⁅x✝² + x✝¹, f y⁆ - ⁅y, f (x✝² + x✝¹)⁆ - f ⁅x✝² + x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ({ toFun := fun y ↦ ⁅x✝², f y⁆ - ⁅y, f x✝²⁆ - f ⁅x✝², y⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun y ↦ ⁅x✝¹, f y⁆ - ⁅y, f x✝¹⁆ - f ⁅x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ })
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : oneCochain R L M
x✝² x✝¹ x✝ : L
⊢ { toFun := fun y ↦ ⁅x✝² + x✝¹, f y⁆ - ⁅y, f (x✝² + x✝¹)⁆ - f ⁅x✝² + x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ({ toFun := fun y ↦ ⁅x✝², f y⁆ - ⁅y, f x✝²⁆ - f ⁅x✝², y⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun y ↦ ⁅x✝¹, f y⁆ - ⁅y, f x✝¹⁆ - f ⁅x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ })
      x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : oneCochain R L M
x✝² x✝¹ x✝ : L
⊢ ⁅x✝², f x✝⁆ + ⁅x✝¹, f x✝⁆ - (⁅x✝, f x✝²⁆ + ⁅x✝, f x✝¹⁆) - (f ⁅x✝², x✝⁆ + f ⁅x✝¹, x✝⁆) =
    ⁅x✝², f x✝⁆ - ⁅x✝, f x✝²⁆ - f ⁅x✝², x✝⁆ + (⁅x✝¹, f x✝⁆ - ⁅x✝, f x✝¹⁆ - f ⁅x✝¹, x✝⁆)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : oneCochain R L M
x✝² x✝¹ x✝ : L
⊢ ⁅x✝², f x✝⁆ + ⁅x✝¹, f x✝⁆ - (⁅x✝, f x✝²⁆ + ⁅x✝, f x✝¹⁆) - (f ⁅x✝², x✝⁆ + f ⁅x✝¹, x✝⁆) =
    ⁅x✝², f x✝⁆ - ⁅x✝, f x✝²⁆ - f ⁅x✝², x✝⁆ + (⁅x✝¹, f x✝⁆ - ⁅x✝, f x✝¹⁆ - f ⁅x✝¹, x✝⁆)
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : oneCochain R L M
x✝² : R
x✝¹ x✝ : L
⊢ { toFun := fun y ↦ ⁅x✝² • x✝¹, f y⁆ - ⁅y, f (x✝² • x✝¹)⁆ - f ⁅x✝² • x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ((RingHom.id R) x✝² • { toFun := fun y ↦ ⁅x✝¹, f y⁆ - ⁅y, f x✝¹⁆ - f ⁅x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ }) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : oneCochain R L M
x✝² : R
x✝¹ x✝ : L
⊢ { toFun := fun y ↦ ⁅x✝² • x✝¹, f y⁆ - ⁅y, f (x✝² • x✝¹)⁆ - f ⁅x✝² • x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    ((RingHom.id R) x✝² • { toFun := fun y ↦ ⁅x✝¹, f y⁆ - ⁅y, f x✝¹⁆ - f ⁅x✝¹, y⁆, map_add' := ⋯, map_smul' := ⋯ }) x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝³ x✝² : oneCochain R L M
x✝¹ x✝ : L
⊢ (↑⟨{
              toFun := fun x ↦
                { toFun := fun y ↦ ⁅x, (x✝³ + x✝²) y⁆ - ⁅y, (x✝³ + x✝²) x⁆ - (x✝³ + x✝²) ⁅x, y⁆, map_add' := ⋯,
                  map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ },
            ⋯⟩
        x✝¹)
      x✝ =
    (↑(⟨{ toFun := fun x ↦ { toFun := fun y ↦ ⁅x, x✝³ y⁆ - ⁅y, x✝³ x⁆ - x✝³ ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
              ⋯⟩ +
            ⟨{
                toFun := fun x ↦
                  { toFun := fun y ↦ ⁅x, x✝² y⁆ - ⁅y, x✝² x⁆ - x✝² ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
              ⋯⟩)
        x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝³ x✝² : oneCochain R L M
x✝¹ x✝ : L
⊢ (↑⟨{
              toFun := fun x ↦
                { toFun := fun y ↦ ⁅x, (x✝³ + x✝²) y⁆ - ⁅y, (x✝³ + x✝²) x⁆ - (x✝³ + x✝²) ⁅x, y⁆, map_add' := ⋯,
                  map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ },
            ⋯⟩
        x✝¹)
      x✝ =
    (↑(⟨{ toFun := fun x ↦ { toFun := fun y ↦ ⁅x, x✝³ y⁆ - ⁅y, x✝³ x⁆ - x✝³ ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
              ⋯⟩ +
            ⟨{
                toFun := fun x ↦
                  { toFun := fun y ↦ ⁅x, x✝² y⁆ - ⁅y, x✝² x⁆ - x✝² ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ },
              ⋯⟩)
        x✝¹)
      x✝
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝³ x✝² : oneCochain R L M
x✝¹ x✝ : L
⊢ ⁅x✝¹, x✝³ x✝⁆ + ⁅x✝¹, x✝² x✝⁆ - (⁅x✝, x✝³ x✝¹⁆ + ⁅x✝, x✝² x✝¹⁆) - (x✝³ ⁅x✝¹, x✝⁆ + x✝² ⁅x✝¹, x✝⁆) =
    ⁅x✝¹, x✝³ x✝⁆ - ⁅x✝, x✝³ x✝¹⁆ - x✝³ ⁅x✝¹, x✝⁆ + (⁅x✝¹, x✝² x✝⁆ - ⁅x✝, x✝² x✝¹⁆ - x✝² ⁅x✝¹, x✝⁆)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x✝³ x✝² : oneCochain R L M
x✝¹ x✝ : L
⊢ ⁅x✝¹, x✝³ x✝⁆ + ⁅x✝¹, x✝² x✝⁆ - (⁅x✝, x✝³ x✝¹⁆ + ⁅x✝, x✝² x✝¹⁆) - (x✝³ ⁅x✝¹, x✝⁆ + x✝² ⁅x✝¹, x✝⁆) =
    ⁅x✝¹, x✝³ x✝⁆ - ⁅x✝, x✝³ x✝¹⁆ - x✝³ ⁅x✝¹, x✝⁆ + (⁅x✝¹, x✝² x✝⁆ - ⁅x✝, x✝² x✝¹⁆ - x✝² ⁅x✝¹, x✝⁆)