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

Goal state before:
pp: case e'_3
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ single t.i t.j t.c = single t.i t.j t.c

Tactic:
]

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

Goal state before:
pp: case inr.inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
hjk : k ≠ j
⊢ 0 = 0

Tactic:
]

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
⊢ ↑x⁻¹ ^ m = ↑x⁻¹ ^ m

Tactic:
]

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

Goal state before:
pp: n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i (f 1) = ⇑f ∘ Pi.single i 1

Tactic:
]

Goal state after:
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i (f 1) = ⇑f ∘ Pi.single i 1
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
⊢ f r = f r

Tactic:
]

Goal state after:
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 : ℕ
⊢ f r * ↑x ^ n = f r * ↑x ^ n

Tactic:
]

Goal state after:
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 : ℕ
⊢ f r * ↑x⁻¹ ^ n = f r * ↑x⁻¹ ^ n

Tactic:
]

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

Goal state before:
pp: n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ⇑f ∘ Pi.single i 1
⊢ f (M.adjugate i k) = f (M.adjugate i k)

Tactic:
]

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

Goal state before:
pp: case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n = 0
this : IsEmpty n
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
n : ℤ
r : R
⊢ r • ↑(x ^ n) = r • ↑(x ^ n)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
r : R
⊢ r • 1 = r • 1

Tactic:
]

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
⊢ (MvPolynomial.aeval fun p ↦ A p.1 p.2) (A'.det ^ (Fintype.card n - 1)) =
    (MvPolynomial.aeval fun p ↦ A p.1 p.2) ((mvPolynomialX n n ℤ).det ^ (Fintype.card n - 1))

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : MulActionWithZero R S
inst✝ : Monoid S
n : ℤ
x : Sˣ
⊢ ↑(x ^ n) = ↑(x ^ n)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : MulActionWithZero R S
inst✝ : Monoid S
x : Sˣ
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : MulActionWithZero R S
inst✝ : Monoid S
x : Sˣ
⊢ smeval 1 x = 1

Tactic:
by
  rw [← T_zero, smeval_T_pow 0 x, zpow_zero, Units.val_eq_one]

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n = A'.det ^ Fintype.card n

Tactic:
]

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (C r * p).smeval x = r • p.smeval x
hq : (C r * q).smeval x = r • q.smeval x
⊢ r • p.smeval x + r • q.smeval x = r • p.smeval x + r • q.smeval x

Tactic:
]

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

Goal state before:
pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * (A.submatrix j.succAbove h.succAbove).det = 0

Tactic:
]

Goal state after:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * (A.submatrix j.succAbove h.succAbove).det = 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case C_mul_T
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
n : ℤ
s : R
⊢ r • s • ↑(x ^ n) = r • s • ↑(x ^ n)

Tactic:
]

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

Goal state before:
pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.refine_2
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝² : NoZeroDivisors R
h✝ : Nontrivial R
this✝¹ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this✝ : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝¹ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
x✝ : Field (FR ⊗[R] FT) := ⋯.toField
this : IsBaseChange FT (↑R g ∘ₗ g✝)
⊢ Cardinal.lift.{max uP uT, uM} (Module.rank R M) = Cardinal.lift.{max uP uT, uM} (Module.rank R M)

Tactic:
]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ B = B

Tactic:
]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A = A

Tactic:
]

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

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
h : ⅟C * A = B
⊢ A = A

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : ¬∀ (r : R) (s : ↥R⁰), ∃ r' s', ↑s' * r = r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : ¬∀ (r : R) (s : ↥R⁰), ∃ r' s', ↑s' * r = r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
h : A = C * B
⊢ B = B

Tactic:
]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
⊢ A = ⅟C * B ↔ A = ⅟C * B

Tactic:
]

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

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
h : A * ⅟C = B
⊢ A = A

Tactic:
]

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

Goal state before:
pp: case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
]

Goal state after:
case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
h : A = B * C
⊢ B = B

Tactic:
]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
⊢ A = B * ⅟C ↔ A = B * ⅟C

Tactic:
]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : StarRing α
A : Matrix n n α
inst✝ : Invertible Aᴴ
⊢ Invertible (star Aᴴ)

Tactic:
]

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : StarRing α
A : Matrix n n α
inst✝ : Invertible Aᴴ
⊢ Invertible (star Aᴴ)
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ (-1) ^ (↑j + ↑i) *
      (A.submatrix j.succAbove i.succAbove 0 0 * A.submatrix j.succAbove i.succAbove 1 1 -
        A.submatrix j.succAbove i.succAbove 0 1 * A.submatrix j.succAbove i.succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j

Tactic:
]

Goal state after:
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ (-1) ^ (↑j + ↑i) *
      (A.submatrix j.succAbove i.succAbove 0 0 * A.submatrix j.succAbove i.succAbove 1 1 -
        A.submatrix j.succAbove i.succAbove 0 1 * A.submatrix j.succAbove i.succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ (⅟Aᵀ)ᵀ * A = (⅟Aᵀ)ᵀ * A

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg : ∑ k ∈ Finset.range n, g (k + 1) • (r * ↑s ^ (k + 1 + x)) + g 0 • (r * ↑s ^ (0 + x)) = 0
i : ℕ
hin : i < n + 1
⊢ g i = 0

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg : ∑ k ∈ Finset.range n, g (k + 1) • (r * ↑s ^ (k + 1 + x)) + g 0 • (r * ↑s ^ (0 + x)) = 0
i : ℕ
hin : i < n + 1
⊢ g i = 0
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ A * (⅟Aᵀ)ᵀ = A * (⅟Aᵀ)ᵀ

Tactic:
]

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

Goal state before:
pp: case of_succ
𝕜 : 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⟩
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
]

Goal state after:
case of_succ
𝕜 : 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⟩
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
⊢ g i = 0

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
⊢ g i = 0
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : IsEmpty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ 1
⊢ False

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : IsEmpty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ 1
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 - U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A - U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)

Tactic:
]

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 - U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A - U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)
Module: Mathlib.LinearAlgebra.Matrix.Trace

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

Tactic:
]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (C * (A * B)).trace = (C * (A * B)).trace

Tactic:
]

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

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ a ⬝ᵥ b = a ⬝ᵥ b

Tactic:
]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

Tactic:
]

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

Goal state before:
pp: R : Type u_6
n : ℕ
inst✝ : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + ∑ i, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i, M.diag ((finSuccEquiv n).symm i)

Tactic:
]

Goal state after:
R : Type u_6
n : ℕ
inst✝ : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + ∑ i, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i, M.diag ((finSuccEquiv n).symm i)
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
R : Type u_6
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ N.trace = N.trace

Tactic:
]

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

Goal state before:
pp: R : Type u_6
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))

Tactic:
]

Goal state after:
R : Type u_6
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg
𝕜 : 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
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
]

Goal state after:
case neg
𝕜 : 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
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + U * C * V * ⅟A - U * C * V * ⅟A = 1

Tactic:
]

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + U * C * V * ⅟A - U * C * V * ⅟A = 1