l : Type ?u.57544
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A ⬝ B = 1
this : Invertible (det B) := detInvertibleOfLeftInverse B A h
⊢ B ⬝ A = 1
l : Type ?u.57544
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A ⬝ B = 1
⊢ B ⬝ A = 1
letI : Invertible B.det := detInvertibleOfLeftInverse _ _ h
l : Type ?u.57544
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A ⬝ B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B ⬝ A = 1
l : Type ?u.57544
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A ⬝ B = 1
this : Invertible (det B) := detInvertibleOfLeftInverse B A h
⊢ B ⬝ A = 1
letI : Invertible B := invertibleOfDetInvertible B
no goals
l : Type ?u.57544
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A ⬝ B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B ⬝ A = 1
calc
  B ⬝ A = B ⬝ A ⬝ (B ⬝ ⅟ B) := by rw [Matrix.mul_invOf_self, Matrix.mul_one]
  _ = B ⬝ (A ⬝ B ⬝ ⅟ B) := by simp only [Matrix.mul_assoc]
  _ = B ⬝ ⅟ B := by rw [h, Matrix.one_mul]
  _ = 1 := Matrix.mul_invOf_self B
no goals
l : Type ?u.57544
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A ⬝ B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B ⬝ A = B ⬝ A ⬝ (B ⬝ ⅟B)
rw [Matrix.mul_invOf_self, Matrix.mul_one]
no goals
l : Type ?u.57544
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A ⬝ B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B ⬝ A ⬝ (B ⬝ ⅟B) = B ⬝ (A ⬝ B ⬝ ⅟B)
simp only [Matrix.mul_assoc]
no goals
l : Type ?u.57544
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A ⬝ B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B ⬝ (A ⬝ B ⬝ ⅟B) = B ⬝ ⅟B
rw [h, Matrix.one_mul]