Theorem: MatrixCookbook.eq_163 (MatrixCookbook/3Inverses.lean)

State before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
letI := hA.invertible
State after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this : Invertible A := hA.invertible
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A

State before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this : Invertible A := hA.invertible
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
letI := hB.invertible
State after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A

State before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
conv_lhs => rw [add_comm]
State after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (B⁻¹ + A⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A

State before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (B⁻¹ + A⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
rw [Matrix.inv_add_inv (iff_of_true hA hB), Matrix.inv_add_inv (iff_of_true hB hA)]
State after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (B⁻¹ * (B + A) * A⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ * (A + B) * B⁻¹)⁻¹ = B * (A + B)⁻¹ * A

State before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (B⁻¹ * (B + A) * A⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ * (A + B) * B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
simp_rw [Matrix.mul_inv_rev, Matrix.inv_inv_of_invertible, mul_assoc, add_comm]
State after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ True ∧ True

State before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ True ∧ True
Tactic:
simp
State after:
no goals