-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem isAdjointPair_toLinearMap₂' :
    LinearMap.IsAdjointPair (Matrix.toLinearMap₂' R J) (Matrix.toLinearMap₂' R J')
        (Matrix.toLin' A) (Matrix.toLin' A') ↔
      Matrix.IsAdjointPair J J' A A'

Proof state:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'

case mpr
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'
⊢ B = B'

Proof state:
case mpr
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'
⊢ B = B'

Tactic:
exact (LinearMap.toMatrix₂' R).injective h

Result:
no goals

Proof state:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ ((toLinearMap₂' R) J).IsAdjointPair ((toLinearMap₂' R) J') ⇑(toLin' A) ⇑(toLin' A') ↔ J.IsAdjointPair J' A A'

Tactic:
rw [isAdjointPair_iff_comp_eq_compl₂]

Result:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ (toLinearMap₂' R) J' ∘ₗ toLin' A = ((toLinearMap₂' R) J).compl₂ (toLin' A') ↔ J.IsAdjointPair J' A A'

Proof state:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'

Tactic:
intro B B'

Result:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'

Proof state:
case mp
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'

Tactic:
rw [h]

Result:
no goals

Proof state:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'
⊢ Aᵀ * J' = J * A' ↔ J.IsAdjointPair J' A A'

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'
⊢ (toLinearMap₂' R) J' ∘ₗ toLin' A = ((toLinearMap₂' R) J).compl₂ (toLin' A') ↔ J.IsAdjointPair J' A A'

Tactic:
simp_rw [h, LinearMap.toMatrix₂'_comp, LinearMap.toMatrix₂'_compl₂,
  LinearMap.toMatrix'_toLin', LinearMap.toMatrix'_toLinearMap₂']

Result:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : 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₂' R) B = (toMatrix₂' R) B'
⊢ Aᵀ * J' = J * A' ↔ J.IsAdjointPair J' A A'