-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)) :
    (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Proof state:
case intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
obtain ⟨iAC⟩ := hAC.nonempty_invertible

Result:
case intro.intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
iAC : Invertible (C⁻¹ + V * A⁻¹ * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Proof state:
case intro.intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
iAC : Invertible (⅟C + V * ⅟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

Tactic:
apply invOf_add_mul_mul

Result:
no goals

Proof state:
case intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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⁻¹

Tactic:
obtain ⟨_⟩ := hC.nonempty_invertible

Result:
case intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Proof state:
case intro.intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
iAC : Invertible (C⁻¹ + V * A⁻¹ * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
simp only [← invOf_eq_nonsing_inv] at iAC

Result:
case intro.intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
iAC : Invertible (⅟C + V * ⅟A * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Proof state:
case intro.intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
iAC : Invertible (⅟C + V * ⅟A * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
letI := invertibleAddMulMul A U C V

Result:
case intro.intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
iAC : Invertible (⅟C + V * ⅟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⁻¹

Proof state:
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
obtain ⟨_⟩ := hA.nonempty_invertible

Result:
case intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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⁻¹

Proof state:
case intro.intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
iAC : Invertible (⅟C + V * ⅟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⁻¹

Tactic:
simp only [← invOf_eq_nonsing_inv]

Result:
case intro.intro.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : 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✝ : Invertible C
iAC : Invertible (⅟C + V * ⅟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