R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ comp (↑toLinearMap₂' J') (↑toLin' A) = compl₂ (↑toLinearMap₂' J) (↑toLin' A') ↔ Matrix.IsAdjointPair J J' A A'
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ LinearMap.IsAdjointPair (↑toLinearMap₂' J) (↑toLinearMap₂' J') (↑toLin' A) (↑toLin' A') ↔
    Matrix.IsAdjointPair J J' A A'
rw [isAdjointPair_iff_comp_eq_compl₂]
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ ↑toMatrix₂' B = ↑toMatrix₂' B'
⊢ Aᵀ ⬝ J' = J ⬝ A' ↔ Matrix.IsAdjointPair J J' A A'
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ ↑toMatrix₂' B = ↑toMatrix₂' B'
⊢ comp (↑toLinearMap₂' J') (↑toLin' A) = compl₂ (↑toLinearMap₂' J) (↑toLin' A') ↔ Matrix.IsAdjointPair J J' A A'
simp_rw [h, LinearMap.toMatrix₂'_comp, LinearMap.toMatrix₂'_compl₂, LinearMap.toMatrix'_toLin',
  LinearMap.toMatrix'_toLinearMap₂']
no goals
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ ↑toMatrix₂' B = ↑toMatrix₂' B'
⊢ Aᵀ ⬝ J' = J ⬝ A' ↔ Matrix.IsAdjointPair J J' A A'
rfl
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
⊢ B = B' ↔ ↑toMatrix₂' B = ↑toMatrix₂' B'
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ ↑toMatrix₂' B = ↑toMatrix₂' B'
intro B B'
case mp
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
h : B = B'
⊢ ↑toMatrix₂' B = ↑toMatrix₂' B'

case mpr
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
h : ↑toMatrix₂' B = ↑toMatrix₂' B'
⊢ B = B'
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
⊢ B = B' ↔ ↑toMatrix₂' B = ↑toMatrix₂' B'
constructor <;> intro h
no goals
case mp
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
h : B = B'
⊢ ↑toMatrix₂' B = ↑toMatrix₂' B'
rw [h]
no goals
case mpr
R : Type u_1
R₁ : Type ?u.2034253
R₂ : Type ?u.2034256
M : Type ?u.2034259
M₁ : Type ?u.2034262
M₂ : Type ?u.2034265
M₁' : Type ?u.2034268
M₂' : Type ?u.2034271
n : Type u_2
m : Type ?u.2034277
n' : Type u_3
m' : Type ?u.2034283
ι : Type ?u.2034286
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
h : ↑toMatrix₂' B = ↑toMatrix₂' B'
⊢ B = B'
exact LinearMap.toMatrix₂'.injective h