R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
⊢ (∃ y, IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) y ∧ ↑toMatrix' y = A₁) ↔
    Matrix.IsAdjointPair J J₂ A₁ A₁
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
⊢ A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ Matrix.IsAdjointPair J J₂ A₁ A₁
simp only [pairSelfAdjointMatricesSubmodule, LinearEquiv.coe_coe, LinearMap.toMatrix'_apply,
  Submodule.mem_map, mem_isPairSelfAdjointSubmodule]
case mp
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
⊢ (∃ y, IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) y ∧ ↑toMatrix' y = A₁) →
    Matrix.IsAdjointPair J J₂ A₁ A₁

case mpr
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
⊢ Matrix.IsAdjointPair J J₂ A₁ A₁ → ∃ y, IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) y ∧ ↑toMatrix' y = A₁
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
⊢ (∃ y, IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) y ∧ ↑toMatrix' y = A₁) ↔
    Matrix.IsAdjointPair J J₂ A₁ A₁
constructor
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
f : Module.End R (n → R)
hf : IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) f
hA : ↑toMatrix' f = A₁
⊢ Matrix.IsAdjointPair J J₂ A₁ A₁
case mp
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
⊢ (∃ y, IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) y ∧ ↑toMatrix' y = A₁) →
    Matrix.IsAdjointPair J J₂ A₁ A₁
rintro ⟨f, hf, hA⟩
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
f : Module.End R (n → R)
hf : IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) f
hA : ↑toMatrix' f = A₁
hf' : f = ↑toLin' A₁
⊢ Matrix.IsAdjointPair J J₂ A₁ A₁
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
f : Module.End R (n → R)
hf : IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) f
hA : ↑toMatrix' f = A₁
⊢ Matrix.IsAdjointPair J J₂ A₁ A₁
have hf' : f = toLin' A₁:= by rw [← hA, Matrix.toLin'_toMatrix']
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
f : Module.End R (n → R)
hf : IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) (↑toLin' A₁)
hA : ↑toMatrix' f = A₁
hf' : f = ↑toLin' A₁
⊢ Matrix.IsAdjointPair J J₂ A₁ A₁
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
f : Module.End R (n → R)
hf : IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) f
hA : ↑toMatrix' f = A₁
hf' : f = ↑toLin' A₁
⊢ Matrix.IsAdjointPair J J₂ A₁ A₁
rw [hf'] at hf
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
f : Module.End R (n → R)
hf : IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) (↑toLin' A₁)
hA : ↑toMatrix' f = A₁
hf' : f = ↑toLin' A₁
⊢ LinearMap.IsAdjointPair (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) (↑toLin' A₁) (↑toLin' A₁)
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
f : Module.End R (n → R)
hf : IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) (↑toLin' A₁)
hA : ↑toMatrix' f = A₁
hf' : f = ↑toLin' A₁
⊢ Matrix.IsAdjointPair J J₂ A₁ A₁
rw [← isAdjointPair_toLinearMap₂']
no goals
case mp.intro.intro
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
f : Module.End R (n → R)
hf : IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) (↑toLin' A₁)
hA : ↑toMatrix' f = A₁
hf' : f = ↑toLin' A₁
⊢ LinearMap.IsAdjointPair (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) (↑toLin' A₁) (↑toLin' A₁)
exact hf
no goals
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
f : Module.End R (n → R)
hf : IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) f
hA : ↑toMatrix' f = A₁
⊢ f = ↑toLin' A₁
rw [← hA, Matrix.toLin'_toMatrix']
case mpr
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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 : Matrix.IsAdjointPair J J₂ A₁ A₁
⊢ ∃ y, IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) y ∧ ↑toMatrix' y = A₁
case mpr
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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'
⊢ Matrix.IsAdjointPair J J₂ A₁ A₁ → ∃ y, IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) y ∧ ↑toMatrix' y = A₁
intro h
case mpr
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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 : Matrix.IsAdjointPair J J₂ A₁ A₁
⊢ IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) (↑toLin' A₁)
case mpr
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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 : Matrix.IsAdjointPair J J₂ A₁ A₁
⊢ ∃ y, IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) y ∧ ↑toMatrix' y = A₁
refine' ⟨toLin' A₁, _, LinearMap.toMatrix'_toLin' _⟩
no goals
case mpr
R : Type u_1
R₁ : Type ?u.2570704
R₂ : Type ?u.2570707
M : Type ?u.2570710
M₁ : Type ?u.2570713
M₂ : Type ?u.2570716
M₁' : Type ?u.2570719
M₂' : Type ?u.2570722
n : Type u_2
m : Type ?u.2570728
n' : Type ?u.2570731
m' : Type ?u.2570734
ι : Type ?u.2570737
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 : Matrix.IsAdjointPair J J₂ A₁ A₁
⊢ IsPairSelfAdjoint (↑toLinearMap₂' J) (↑toLinearMap₂' J₂) (↑toLin' A₁)
exact (isAdjointPair_toLinearMap₂' _ _ _ _).mpr h