mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', toLaurent f' = p * T ↑n) → (∃ n f', toLaurent f' = q * T ↑n) → ∃ n f', toLaurent f' = (p + q) * T ↑n

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
a : R
⊢ ∃ n_1 f', toLaurent f' = C a * T n * T ↑n_1

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', toLaurent f' = p * T ↑n) → (∃ n f', toLaurent f' = q * T ↑n) → ∃ n f', toLaurent f' = (p + q) * T ↑n

case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
a : R
⊢ ∃ n_1 f', toLaurent f' = C a * T n * T ↑n_1
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case map_add
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ ∀ (x y : n → α), A.cramerMap (x + y) = A.cramerMap x + A.cramerMap y

pp: case map_smul
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ ∀ (c : α) (x : n → α), A.cramerMap (c • x) = c • A.cramerMap x

Tactic:
<;>

Goal state after:
case map_add
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ ∀ (x y : n → α), A.cramerMap (x + y) = A.cramerMap x + A.cramerMap y

case map_smul
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ ∀ (c : α) (x : n → α), A.cramerMap (c • x) = c • A.cramerMap x
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case map_add
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
x✝ y✝ : n → α
⊢ A.cramerMap (x✝ + y✝) = A.cramerMap x✝ + A.cramerMap y✝

pp: case map_smul
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
c✝ : α
x✝ : n → α
⊢ A.cramerMap (c✝ • x✝) = c✝ • A.cramerMap x✝

Tactic:
<;>

Goal state after:
case map_add
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
x✝ y✝ : n → α
⊢ A.cramerMap (x✝ + y✝) = A.cramerMap x✝ + A.cramerMap y✝

case map_smul
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
c✝ : α
x✝ : n → α
⊢ A.cramerMap (c✝ • x✝) = c✝ • A.cramerMap x✝
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
M' : Submodule R M
⊢ lift.{max uR uM, uM} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max uR uM, uM} (Module.rank R M)

Tactic:
simp_rw [lift_add, ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalized R⁰) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalizedQuotient R⁰) le_rfl,
    ← IsLocalization.rank_eq (FractionRing R) R⁰ le_rfl,
    ← lift_add, rank_quotient_add_rank_of_divisionRing]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℤ
a : R
h : a = 0
⊢ (C a * T n).degree = ⊥

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℤ
a : R
h : ¬a = 0
⊢ (C a * T n).degree = ↑n

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℤ
a : R
h : a = 0
⊢ (C a * T n).degree = ⊥

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℤ
a : R
h : ¬a = 0
⊢ (C a * T n).degree = ↑n
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ (A.submatrix ⇑e ⇑e).adjugate i j = A.adjugate.submatrix (⇑e) (⇑e) i j

Tactic:
have : (fun j ↦ Pi.single i 1 <| e.symm j) = Pi.single (e i) 1 :=
    Function.update_comp_equiv (0 : n → α) e.symm i 1

Goal state after:
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
this : (fun j ↦ Pi.single i 1 (e.symm j)) = Pi.single (e i) 1
⊢ (A.submatrix ⇑e ⇑e).adjugate i j = A.adjugate.submatrix (⇑e) (⇑e) i j
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
a : R
h : a = 0
⊢ (C a).degree = ⊥

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
a : R
h : ¬a = 0
⊢ (C a).degree = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
a : R
h : a = 0
⊢ (C a).degree = ⊥

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
a : R
h : ¬a = 0
⊢ (C a).degree = 0
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝¹ : DecidableEq n
inst✝ : CommRing R
i j : n
⊢ transvection i j 0 = 1

Tactic:
simp [transvection]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
m : ℕ
hn : -↑m < 0
⊢ (eval₂ f x) (T (-↑m)) = ↑(x ^ (-↑m))

Tactic:
eval₂_T_neg_n,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
m : ℕ
hn : -↑m < 0
⊢ ↑x⁻¹ ^ m = ↑(x ^ (-↑m))
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case mk.inl
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
b : n ⊕ p
a : n
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) b =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) b

pp: case mk.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
b : n ⊕ p
a : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) b =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) b

Tactic:
<;>

Goal state after:
case mk.inl
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
b : n ⊕ p
a : n
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) b =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) b

case mk.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
b : n ⊕ p
a : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) b =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) b
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
r : R
n : ℕ
⊢ (eval₂ f x) (C r) * (eval₂ f x) (T (-↑n)) = f r * ↑x⁻¹ ^ n

Tactic:
eval₂_T_neg_n,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
r : R
n : ℕ
⊢ (eval₂ f x) (C r) * ↑x⁻¹ ^ n = f r * ↑x⁻¹ ^ n
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n
h : a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) (inl b)

pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n
h : ¬a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) (inl b)

Tactic:
<;>

Goal state after:
case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n
h : a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) (inl b)

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n
h : ¬a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) (inl b)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
h : a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)

pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
h : ¬a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)

Tactic:
<;>

Goal state after:
case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
h : a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
h : ¬a = b
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

Tactic:
<;>

Goal state after:
case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : e t_j = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : ¬e t_j = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : e t_j = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : ¬e t_j = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

Tactic:
<;>

Goal state after:
case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : e t_j = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : ¬e t_j = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : e t_j = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : ¬e t_j = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case «0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨0, ⋯⟩)) * (A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨1, ⋯⟩)) * (A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨0, ⋯⟩)) * (A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨1, ⋯⟩)) * (A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case «0».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨0, ⋯⟩) + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨1, ⋯⟩) + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨0, ⋯⟩) + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨1, ⋯⟩) + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨0, ⋯⟩) + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨1, ⋯⟩) + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨0, ⋯⟩) + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨1, ⋯⟩) + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case «0».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 0 2 * A 2 1 - A 0 1 * A 2 2 = -(A 0 1 * A 2 2) + A 0 2 * A 2 1

pp: case «1».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 1 2 * A 2 0 - A 1 0 * A 2 2 = -(A 1 0 * A 2 2) + A 1 2 * A 2 0

pp: case «1».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 3 * (A 0 0 * A 1 2 - A 0 2 * A 1 0) = -(A 0 0 * A 1 2) + A 0 2 * A 1 0

pp: case «2».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 3 * (A 0 0 * A 2 1 - A 0 1 * A 2 0) = -(A 0 0 * A 2 1) + A 0 1 * A 2 0

pp: case «2».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 4 * (A 0 0 * A 1 1 - A 0 1 * A 1 0) = A 0 0 * A 1 1 - A 0 1 * A 1 0

Tactic:
<;>

Goal state after:
case «0».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 0 2 * A 2 1 - A 0 1 * A 2 2 = -(A 0 1 * A 2 2) + A 0 2 * A 2 1

case «1».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 1 2 * A 2 0 - A 1 0 * A 2 2 = -(A 1 0 * A 2 2) + A 1 2 * A 2 0

case «1».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 3 * (A 0 0 * A 1 2 - A 0 2 * A 1 0) = -(A 0 0 * A 1 2) + A 0 2 * A 1 0

case «2».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 3 * (A 0 0 * A 2 1 - A 0 1 * A 2 0) = -(A 0 0 * A 2 1) + A 0 1 * A 2 0

case «2».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 4 * (A 0 0 * A 1 1 - A 0 1 * A 1 0) = A 0 0 * A 1 1 - A 0 1 * A 1 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A.adjugateᴴ = Aᴴ.adjugate

Tactic:
dsimp only [conjTranspose]

Goal state after:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A.adjugateᵀ.map star = (Aᵀ.map star).adjugate
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg.inr.hnc
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n + 1 ≤ ↑i

Tactic:
simpa only [not_le] using hi

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : SubNegZeroMonoid R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ (M - N) i j = 0

Tactic:
simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]

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

Goal state before:
pp: case inl.inl
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : m
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inl d) = 0

pp: case inl.inr
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : m
d : n
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inr d) = 0

pp: case inr.inl
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : n
d : m
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inl d) = 0

pp: case inr.inr
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : n
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inr d) = 0

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : m
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inl d) = 0

case inl.inr
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : m
d : n
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inr d) = 0

case inr.inl
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : n
d : m
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inl d) = 0

case inr.inr
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : n
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inr d) = 0