-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem mem_pairSelfAdjointMatricesSubmodule :
    A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ Matrix.IsAdjointPair J J₂ A₁ A₁

Proof state:
case mp.intro.intro
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
f : Module.End R (n → R)
hf : ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑f
hA : toMatrix' f = A₁
hf' : f = toLin' A₁
⊢ J.IsAdjointPair J₂ A₁ A₁

Tactic:
rw [hf'] at hf

Result:
case mp.intro.intro
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
f : Module.End R (n → R)
hf : ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑(toLin' A₁)
hA : toMatrix' f = A₁
hf' : f = toLin' A₁
⊢ J.IsAdjointPair J₂ A₁ A₁

Proof state:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ (∃ y, ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑y ∧ toMatrix' y = A₁) ↔ J.IsAdjointPair J₂ A₁ A₁

Tactic:
constructor

Result:
case mp
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ (∃ y, ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑y ∧ toMatrix' y = A₁) → J.IsAdjointPair J₂ A₁ A₁

case mpr
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ J.IsAdjointPair J₂ A₁ A₁ → ∃ y, ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑y ∧ toMatrix' y = A₁

Proof state:
case mp.intro.intro
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
f : Module.End R (n → R)
hf : ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑f
hA : toMatrix' f = A₁
⊢ J.IsAdjointPair J₂ A₁ A₁

Tactic:
have hf' : f = toLin' A₁ := by rw [← hA, Matrix.toLin'_toMatrix']

Result:
case mp.intro.intro
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
f : Module.End R (n → R)
hf : ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑f
hA : toMatrix' f = A₁
hf' : f = toLin' A₁
⊢ J.IsAdjointPair J₂ A₁ A₁

Proof state:
case mpr
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ J.IsAdjointPair J₂ A₁ A₁ → ∃ y, ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑y ∧ toMatrix' y = A₁

Tactic:
intro h

Result:
case mpr
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
h : J.IsAdjointPair J₂ A₁ A₁
⊢ ∃ y, ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑y ∧ toMatrix' y = A₁

Proof state:
case mp
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ (∃ y, ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑y ∧ toMatrix' y = A₁) → J.IsAdjointPair J₂ A₁ A₁

Tactic:
rintro ⟨f, hf, hA⟩

Result:
case mp.intro.intro
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
f : Module.End R (n → R)
hf : ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑f
hA : toMatrix' f = A₁
⊢ J.IsAdjointPair J₂ A₁ A₁

Proof state:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
f : Module.End R (n → R)
hf : ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑f
hA : toMatrix' f = A₁
⊢ f = toLin' A₁

Tactic:
rw [← hA, Matrix.toLin'_toMatrix']

Result:
no goals

Proof state:
case mpr
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
h : J.IsAdjointPair J₂ A₁ A₁
⊢ ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑(toLin' A₁)

Tactic:
exact (isAdjointPair_toLinearMap₂' _ _ _ _).mpr h

Result:
no goals

Proof state:
case mpr
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
h : J.IsAdjointPair J₂ A₁ A₁
⊢ ∃ y, ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑y ∧ toMatrix' y = A₁

Tactic:
refine ⟨toLin' A₁, ?_, LinearMap.toMatrix'_toLin' _⟩

Result:
case mpr
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
h : J.IsAdjointPair J₂ A₁ A₁
⊢ ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑(toLin' A₁)

Proof state:
case mp.intro.intro
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
f : Module.End R (n → R)
hf : ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑(toLin' A₁)
hA : toMatrix' f = A₁
hf' : f = toLin' A₁
⊢ J.IsAdjointPair J₂ A₁ A₁

Tactic:
rw [← isAdjointPair_toLinearMap₂']

Result:
case mp.intro.intro
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
f : Module.End R (n → R)
hf : ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑(toLin' A₁)
hA : toMatrix' f = A₁
hf' : f = toLin' A₁
⊢ ((toLinearMap₂' R) J).IsAdjointPair ((toLinearMap₂' R) J₂) ⇑(toLin' A₁) ⇑(toLin' A₁)

Proof state:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ J.IsAdjointPair J₂ A₁ A₁

Tactic:
simp only [pairSelfAdjointMatricesSubmodule, LinearEquiv.coe_coe, LinearMap.toMatrix'_apply,
  Submodule.mem_map, mem_isPairSelfAdjointSubmodule]

Result:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ (∃ y, ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑y ∧ toMatrix' y = A₁) ↔ J.IsAdjointPair J₂ A₁ A₁

Proof state:
case mp.intro.intro
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J J₂ A₁ : Matrix n n R
inst✝ : DecidableEq n
f : Module.End R (n → R)
hf : ((toLinearMap₂' R) J).IsPairSelfAdjoint ((toLinearMap₂' R) J₂) ⇑(toLin' A₁)
hA : toMatrix' f = A₁
hf' : f = toLin' A₁
⊢ ((toLinearMap₂' R) J).IsAdjointPair ((toLinearMap₂' R) J₂) ⇑(toLin' A₁) ⇑(toLin' A₁)

Tactic:
exact hf

Result:
no goals