awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val : Invertible A
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
have obtain : ∀ (val : Invertible C), (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
Tactic: obtain ⟨_⟩ := hC.nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val : Invertible A
val_1 : Invertible C
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
have obtain : ∀ (iAC : Invertible (C⁻¹ + V * A⁻¹ * U)), (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
Tactic: obtain ⟨iAC⟩ := hAC.nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val : Invertible A
val_1 : Invertible C
iAC : Invertible (C⁻¹ + V * A⁻¹ * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
have simp : ∀
  (iAC :
    Invertible
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
        V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)),
  (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
Tactic: simp only [← invOf_eq_nonsing_inv] at iAC
Cleared hypotheses: iAC
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val : Invertible A
val_1 : Invertible C
iAC :
  Invertible
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
      V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul U C V
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
have simp : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A + U * C * V) _ =
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U *
          @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
            (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one C _ +
              V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U)
            _ *
        V *
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _
Tactic: simp only [← invOf_eq_nonsing_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
have obtain : ∀ (val : Invertible A), (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
Tactic: obtain ⟨_⟩ := hA.nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val : Invertible A
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
have obtain : ∀ (ih : Invertible (C + C * V * A⁻¹ * U * C)),
  (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
Tactic: obtain ⟨ih⟩ := h.nonempty_invertible
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val : Invertible A
ih : Invertible (C + C * V * A⁻¹ * U * C)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
have simp : ∀ (ih : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)),
  (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
Tactic: simp only [← invOf_eq_nonsing_inv] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
inst_3 : Fintype m
inst_4 : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val : Invertible A
ih : Invertible (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul' U C V
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
have simp : @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one (A + U * C * V) _ =
  @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ -
    @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one
              (C + C * V * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * U * C) _ *
          C *
        V *
      @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _
Tactic: simp only [← invOf_eq_nonsing_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
have pos : ∀ (h : IsUnit A.det), A⁻¹⁻¹⁻¹ = A⁻¹
Tactic: by_cases h : IsUnit A.det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
pos : ∀ (h : IsUnit A.det), A⁻¹⁻¹⁻¹ = A⁻¹
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
have neg : ∀ (h : ¬IsUnit A.det), A⁻¹⁻¹⁻¹ = A⁻¹
Tactic: by_cases h : IsUnit A.det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
have pos : A⁻¹ = A⁻¹
Tactic: rw [nonsing_inv_nonsing_inv _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
⊢ (A * B)⁻¹ = B⁻¹ * A⁻¹
have simp : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate
Tactic: simp only [inv_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate
have rw : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • (B.adjugate * A.det⁻¹ʳ • A.adjugate)
Tactic: rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
rw : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • (B.adjugate * A.det⁻¹ʳ • A.adjugate)
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate
have rw₁ : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • A.det⁻¹ʳ • (B.adjugate * A.adjugate)
Tactic: rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
rw : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • (B.adjugate * A.det⁻¹ʳ • A.adjugate)
rw₁ : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • A.det⁻¹ʳ • (B.adjugate * A.adjugate)
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate
have rw₂ : (A * B).det⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
Tactic: rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
rw : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • (B.adjugate * A.det⁻¹ʳ • A.adjugate)
rw₁ : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • A.det⁻¹ʳ • (B.adjugate * A.adjugate)
rw₂ : (A * B).det⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate
have rw₃ : (A.det * B.det)⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
Tactic: rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
rw : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • (B.adjugate * A.det⁻¹ʳ • A.adjugate)
rw₁ : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • A.det⁻¹ʳ • (B.adjugate * A.adjugate)
rw₂ : (A * B).det⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
rw₃ : (A.det * B.det)⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate
have rw₄ : (A.det * B.det)⁻¹ʳ • (B.adjugate * A.adjugate) = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
Tactic: rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
rw : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • (B.adjugate * A.det⁻¹ʳ • A.adjugate)
rw₁ : (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • A.det⁻¹ʳ • (B.adjugate * A.adjugate)
rw₂ : (A * B).det⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
rw₃ : (A.det * B.det)⁻¹ʳ • (A * B).adjugate = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
rw₄ : (A.det * B.det)⁻¹ʳ • (B.adjugate * A.adjugate) = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
⊢ (A * B).det⁻¹ʳ • (A * B).adjugate = B.det⁻¹ʳ • B.adjugate * A.det⁻¹ʳ • A.adjugate
have rw₅ : (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate) = (B.det⁻¹ʳ * A.det⁻¹ʳ) • (B.adjugate * A.adjugate)
Tactic: rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
⊢ Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv (List.reverse [])))
have rw : Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv []))
Tactic: rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
rw : Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv []))
⊢ Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv (List.reverse [])))
have rw₁ : Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod [])
Tactic: rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
rw : Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv []))
rw₁ : Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod [])
⊢ Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv (List.reverse [])))
have rw₂ : Eq (α := Matrix n n α) 1⁻¹ 1
Tactic: rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
rw : Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv []))
rw₁ : Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod [])
rw₂ : Eq (α := Matrix n n α) 1⁻¹ 1
⊢ Eq (α := Matrix n n α) (List.prod [])⁻¹ (List.prod (List.map Inv.inv (List.reverse [])))
have rw₃ : Eq (α := Matrix n n α) 1 1
Tactic: rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod
have rw : (A :: Xs).prod⁻¹ = (List.map Inv.inv (Xs.reverse.concat A)).prod
Tactic: rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
rw : (A :: Xs).prod⁻¹ = (List.map Inv.inv (Xs.reverse.concat A)).prod
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod
have rw₁ : (A :: Xs).prod⁻¹ = ((List.map Inv.inv Xs.reverse).concat A⁻¹).prod
Tactic: rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
rw : (A :: Xs).prod⁻¹ = (List.map Inv.inv (Xs.reverse.concat A)).prod
rw₁ : (A :: Xs).prod⁻¹ = ((List.map Inv.inv Xs.reverse).concat A⁻¹).prod
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod
have rw₂ : (A :: Xs).prod⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
Tactic: rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
rw : (A :: Xs).prod⁻¹ = (List.map Inv.inv (Xs.reverse.concat A)).prod
rw₁ : (A :: Xs).prod⁻¹ = ((List.map Inv.inv Xs.reverse).concat A⁻¹).prod
rw₂ : (A :: Xs).prod⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod
have rw₃ : (A * Xs.prod)⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
Tactic: rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
rw : (A :: Xs).prod⁻¹ = (List.map Inv.inv (Xs.reverse.concat A)).prod
rw₁ : (A :: Xs).prod⁻¹ = ((List.map Inv.inv Xs.reverse).concat A⁻¹).prod
rw₂ : (A :: Xs).prod⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
rw₃ : (A * Xs.prod)⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod
have rw₄ : Xs.prod⁻¹ * A⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
Tactic: rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
rw : (A :: Xs).prod⁻¹ = (List.map Inv.inv (Xs.reverse.concat A)).prod
rw₁ : (A :: Xs).prod⁻¹ = ((List.map Inv.inv Xs.reverse).concat A⁻¹).prod
rw₂ : (A :: Xs).prod⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
rw₃ : (A * Xs.prod)⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
rw₄ : Xs.prod⁻¹ * A⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod
have rw₅ : (List.map Inv.inv Xs.reverse).prod * A⁻¹ = (List.map Inv.inv Xs.reverse).prod * A⁻¹
Tactic: rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ A.det • A⁻¹ *ᵥ b = (A.cramer : (a : n → α) → n → α) b
have rw : A.det • A⁻¹ *ᵥ b = A.adjugate *ᵥ b
Tactic: rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul,
    h.mul_val_inv, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • A⁻¹ *ᵥ b = A.adjugate *ᵥ b
⊢ A.det • A⁻¹ *ᵥ b = (A.cramer : (a : n → α) → n → α) b
have rw₁ : A.det • ((↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
Tactic: rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul,
    h.mul_val_inv, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • A⁻¹ *ᵥ b = A.adjugate *ᵥ b
rw₁ : A.det • ((↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
⊢ A.det • A⁻¹ *ᵥ b = (A.cramer : (a : n → α) → n → α) b
have rw₂ : (A.det • (↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
Tactic: rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul,
    h.mul_val_inv, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • A⁻¹ *ᵥ b = A.adjugate *ᵥ b
rw₁ : A.det • ((↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
rw₂ : (A.det • (↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
⊢ A.det • A⁻¹ *ᵥ b = (A.cramer : (a : n → α) → n → α) b
have rw₃ : ((A.det * (↑h.unit⁻¹ : α)) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
Tactic: rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul,
    h.mul_val_inv, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • A⁻¹ *ᵥ b = A.adjugate *ᵥ b
rw₁ : A.det • ((↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
rw₂ : (A.det • (↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
rw₃ : ((A.det * (↑h.unit⁻¹ : α)) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
⊢ A.det • A⁻¹ *ᵥ b = (A.cramer : (a : n → α) → n → α) b
have rw₄ : HSMul.hSMul (α := α) 1 A.adjugate *ᵥ b = A.adjugate *ᵥ b
Tactic: rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul,
    h.mul_val_inv, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • A⁻¹ *ᵥ b = A.adjugate *ᵥ b
rw₁ : A.det • ((↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
rw₂ : (A.det • (↑h.unit⁻¹ : α) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
rw₃ : ((A.det * (↑h.unit⁻¹ : α)) • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
rw₄ : HSMul.hSMul (α := α) 1 A.adjugate *ᵥ b = A.adjugate *ᵥ b
⊢ A.det • A⁻¹ *ᵥ b = (A.cramer : (a : n → α) → n → α) b
have rw₅ : A.adjugate *ᵥ b = A.adjugate *ᵥ b
Tactic: rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul,
    h.mul_val_inv, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ A.det • b ᵥ* A⁻¹ = (Aᵀ.cramer : (a : n → α) → n → α) b
have rw : A.det • b ᵥ* A⁻¹ᵀᵀ = (Aᵀ.cramer : (a : n → α) → n → α) b
Tactic: rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
    Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • b ᵥ* A⁻¹ᵀᵀ = (Aᵀ.cramer : (a : n → α) → n → α) b
⊢ A.det • b ᵥ* A⁻¹ = (Aᵀ.cramer : (a : n → α) → n → α) b
have rw₁ : A.det • A⁻¹ᵀ *ᵥ b = (Aᵀ.cramer : (a : n → α) → n → α) b
Tactic: rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
    Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • b ᵥ* A⁻¹ᵀᵀ = (Aᵀ.cramer : (a : n → α) → n → α) b
rw₁ : A.det • A⁻¹ᵀ *ᵥ b = (Aᵀ.cramer : (a : n → α) → n → α) b
⊢ A.det • b ᵥ* A⁻¹ = (Aᵀ.cramer : (a : n → α) → n → α) b
have rw₂ : A.det • Aᵀ⁻¹ *ᵥ b = (Aᵀ.cramer : (a : n → α) → n → α) b
Tactic: rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
    Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
rw : A.det • b ᵥ* A⁻¹ᵀᵀ = (Aᵀ.cramer : (a : n → α) → n → α) b
rw₁ : A.det • A⁻¹ᵀ *ᵥ b = (Aᵀ.cramer : (a : n → α) → n → α) b
rw₂ : A.det • Aᵀ⁻¹ *ᵥ b = (Aᵀ.cramer : (a : n → α) → n → α) b
⊢ A.det • b ᵥ* A⁻¹ = (Aᵀ.cramer : (a : n → α) → n → α) b
have rw₃ : Aᵀ.det • Aᵀ⁻¹ *ᵥ b = (Aᵀ.cramer : (a : n → α) → n → α) b
Tactic: rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
    Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]