awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Fintype n
inst_6 : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_7 : DecidableEq n
inst_8 : DecidableEq n'
rw :
  Eq (α := M₁ →ₗ[R] M₂ →ₗ[R] R)
      ((toLinearMap₂ b₂ b₂ : (a : Matrix n' n' R) → M₂ →ₗ[R] M₂ →ₗ[R] R) J' ∘ₗ
        (toLin b₁ b₂ : (a : Matrix n' n R) → M₁ →ₗ[R] M₂) A)
      (compl₂ (R₂ := R) (N := M₁) (σ₂₃ := RingHom.id R) (σ₄₂ := RingHom.id R)
        ((toLinearMap₂ b₁ b₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁ →ₗ[R] R) J)
        ((toLin b₂ b₁ : (a : Matrix n n' R) → M₂ →ₗ[R] M₁) A')) ↔
    J.IsAdjointPair J' A A'
⊢ LinearMap.IsAdjointPair.{u_1, u_6, u_7, u_1} (R := R) (M := M₁) (M₁ := M₂) (M₃ := R) (I := RingHom.id R)
      ((toLinearMap₂ b₁ b₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁ →ₗ[R] R) J)
      ((toLinearMap₂ b₂ b₂ : (a : Matrix n' n' R) → M₂ →ₗ[R] M₂ →ₗ[R] R) J')
      (⇑((toLin b₁ b₂ : (a : Matrix n' n R) → M₁ →ₗ[R] M₂) A : M₁ →ₗ[R] M₂) : (a : M₁) → M₂)
      (⇑((toLin b₂ b₁ : (a : Matrix n n' R) → M₂ →ₗ[R] M₁) A' : M₂ →ₗ[R] M₁) : (a : M₂) → M₁) ↔
    J.IsAdjointPair J' A A'

Tactic:
rw [isAdjointPair_iff_comp_eq_compl₂]

Premises used: LinearMap.isAdjointPair_iff_comp_eq_compl₂
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Fintype n
inst_6 : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_7 : DecidableEq n
inst_8 : DecidableEq n'
B B' : M₁ →ₗ[R] M₂ →ₗ[R] R
mp :
  B = B' →
    Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B : Matrix n n' R)
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)
mpr :
  Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B : Matrix n n' R)
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R) →
    B = B'
⊢ B = B' ↔
    Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B : Matrix n n' R)
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Fintype n
inst_6 : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_7 : DecidableEq n
inst_8 : DecidableEq n'
B B' : M₁ →ₗ[R] M₂ →ₗ[R] R
h : B = B'
mp mp₁ :
  Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)
⊢ Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B : Matrix n n' R)
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Fintype n
inst_6 : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_7 : DecidableEq n
inst_8 : DecidableEq n'
B B' : M₁ →ₗ[R] M₂ →ₗ[R] R
h :
  Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B : Matrix n n' R)
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)
⊢ B = B'

Tactic:
(LinearMap.toMatrix₂ b₁ b₂).injective h

Premises used: LinearMap.toMatrix₂, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Fintype n
inst_6 : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_7 : DecidableEq n
inst_8 : DecidableEq n'
B B' : M₁ →ₗ[R] M₂ →ₗ[R] R
h :
  Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B : Matrix n n' R)
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)
⊢ B = B'

Tactic:
exact (LinearMap.toMatrix₂ b₁ b₂).injective h

Premises used: LinearMap.toMatrix₂, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Fintype n
inst_6 : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_7 : DecidableEq n
inst_8 : DecidableEq n'
⊢ ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R),
    B = B' ↔
      Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B : Matrix n n' R)
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)

Tactic:
have h :
    ∀ B B' : M₁ →ₗ[R] M₂ →ₗ[R] R,
      B = B' ↔ LinearMap.toMatrix₂ b₁ b₂ B = LinearMap.toMatrix₂ b₁ b₂ B' := by
    intro B B'
    constructor <;> intro h
    · rw [h]
    · exact (LinearMap.toMatrix₂ b₁ b₂).injective h
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Fintype n
inst_6 : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_7 : DecidableEq n
inst_8 : DecidableEq n'
h :
  ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R),
    B = B' ↔
      Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B : Matrix n n' R)
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)
simp_rw : Aᵀ * J' = J * A' ↔ J.IsAdjointPair J' A A'
⊢ Eq (α := M₁ →ₗ[R] M₂ →ₗ[R] R)
      ((toLinearMap₂ b₂ b₂ : (a : Matrix n' n' R) → M₂ →ₗ[R] M₂ →ₗ[R] R) J' ∘ₗ
        (toLin b₁ b₂ : (a : Matrix n' n R) → M₁ →ₗ[R] M₂) A)
      (compl₂ (R₂ := R) (N := M₁) (σ₂₃ := RingHom.id R) (σ₄₂ := RingHom.id R)
        ((toLinearMap₂ b₁ b₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁ →ₗ[R] R) J)
        ((toLin b₂ b₁ : (a : Matrix n n' R) → M₂ →ₗ[R] M₁) A')) ↔
    J.IsAdjointPair J' A A'

Tactic:
simp_rw [h, LinearMap.toMatrix₂_comp b₂ b₂, LinearMap.toMatrix₂_compl₂ b₁ b₁,
    LinearMap.toMatrix_toLin, LinearMap.toMatrix₂_toLinearMap₂]

Premises used: LinearMap.toMatrix₂_compl₂, LinearMap.toMatrix₂_comp, LinearMap.toMatrix₂_toLinearMap₂, LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Fintype n
inst_6 : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_7 : DecidableEq n
inst_8 : DecidableEq n'
h :
  ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R),
    B = B' ↔
      Eq (α := Matrix n n' R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B : Matrix n n' R)
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n n' R) B' : Matrix n n' R)
⊢ Aᵀ * J' = J * A' ↔ J.IsAdjointPair J' A A'

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
⊢ IsUnit P.det

Tactic:
have h' : IsUnit P.det := P.isUnit_iff_isUnit_det.mp h
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
simp : A₁ᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A₂ ↔ P⁻¹ᵀ * (A₁ᵀ * Pᵀ) * J = J * (P * A₂ * P⁻¹)
⊢ A₁ᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A₂ ↔ (P * A₁ * P⁻¹)ᵀ * J = J * (P * A₂ * P⁻¹)

Tactic:
simp only [Matrix.transpose_mul]

Premises used: Matrix.transpose_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
simp : A₁ᵀ * Pᵀ * J * P = Pᵀ * J * P * A₂ ↔ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = J * P * A₂ * P⁻¹
⊢ A₁ᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A₂ ↔ P⁻¹ᵀ * (A₁ᵀ * Pᵀ) * J = J * (P * A₂ * P⁻¹)

Tactic:
simp only [← mul_assoc, P.transpose_nonsing_inv]

Premises used: mul_assoc, Matrix.transpose_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
⊢ x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)

Tactic:
this
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
h₁ : Pᵀ * J * P * A₂ = (↑v : Matrix n n R) * y
h₂ : Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = (↑v⁻¹ : Matrix n n R) * x
⊢ A₁ᵀ * Pᵀ * J * P = Pᵀ * J * P * A₂ ↔ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = J * P * A₂ * P⁻¹

Tactic:
convert! this using 2
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
h₁ : Pᵀ * (J * P * A₂) = (↑v : Matrix n n R) * y
⊢ Pᵀ * J * P * A₂ = (↑v : Matrix n n R) * y

Tactic:
rw [mul_assoc, mul_assoc, ← mul_assoc J]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
⊢ Pᵀ * (J * P * A₂) = (↑v : Matrix n n R) * y

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
h₁ : Pᵀ⁻¹ * (A₁ᵀ * Pᵀ * J) = (↑v⁻¹ : Matrix n n R) * x
⊢ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = (↑v⁻¹ : Matrix n n R) * x

Tactic:
rw [mul_assoc, mul_assoc, ← mul_assoc _ _ J]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
⊢ Pᵀ⁻¹ * (A₁ᵀ * Pᵀ * J) = (↑v⁻¹ : Matrix n n R) * x

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
suffices : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)

Tactic:
suffices x * u = v * y ↔ v⁻¹ * x = y * u⁻¹ by
    dsimp only [Matrix.IsAdjointPair]
    simp only [Matrix.transpose_mul]
    simp only [← mul_assoc, P.transpose_nonsing_inv]
    convert! this using 2
    · rw [mul_assoc, mul_assoc, ← mul_assoc J]
      rfl
    · rw [mul_assoc, mul_assoc, ← mul_assoc _ _ J]
      rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
rw : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x * (↑u : Matrix n n R) = y
⊢ x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)

Tactic:
rw [Units.eq_mul_inv_iff_mul_eq]

Premises used: Units.eq_mul_inv_iff_mul_eq
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
rw : (↑v⁻¹ : Matrix n n R) * (x * (↑u : Matrix n n R)) = y
| (↑v⁻¹ : Matrix n n R) * x * (↑u : Matrix n n R) = y

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
conv_rhs : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * (x * (↑u : Matrix n n R)) = y
⊢ x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x * (↑u : Matrix n n R) = y

Tactic:
conv_rhs => rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ A₂ : Matrix n n R
inst_2 : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
rw rw₁ : x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y
⊢ x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * (x * (↑u : Matrix n n R)) = y

Tactic:
rw [v.inv_mul_eq_iff_eq_mul]

Premises used: Units.inv_mul_eq_iff_eq_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J J₂ A₁ : Matrix n n R
inst_2 : DecidableEq n
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (pairSelfAdjointMatricesSubmodule J J₂) A₁ ↔ J.IsAdjointPair J₂ A₁ A₁

Tactic:
simp only [pairSelfAdjointMatricesSubmodule, Submodule.mem_map_equiv,
    mem_isPairSelfAdjointSubmodule, toMatrix'_symm, ← isAdjointPair_toLinearMap₂',
    IsPairSelfAdjoint, toLin'_apply']

Premises used: LinearMap.mem_isPairSelfAdjointSubmodule, LinearMap.IsPairSelfAdjoint, LinearMap.toMatrix'_symm, isAdjointPair_toLinearMap₂', Matrix.toLin'_apply', pairSelfAdjointMatricesSubmodule, Submodule.mem_map_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ : Matrix n n R
inst_2 : DecidableEq n
rw : Membership.mem (γ := Submodule R (Matrix n n R)) (pairSelfAdjointMatricesSubmodule J J) A₁ ↔ J.IsSelfAdjoint A₁
rw₁ : J.IsAdjointPair J A₁ A₁ ↔ J.IsSelfAdjoint A₁
rw₂ rw₃ : J.IsAdjointPair J A₁ A₁ ↔ J.IsAdjointPair J A₁ A₁
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (selfAdjointMatricesSubmodule J) A₁ ↔ J.IsSelfAdjoint A₁

Tactic:
rw [selfAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule, Matrix.IsSelfAdjoint]

Premises used: mem_pairSelfAdjointMatricesSubmodule, selfAdjointMatricesSubmodule, Matrix.IsSelfAdjoint
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ : Matrix n n R
inst_2 : DecidableEq n
rw : (-J).IsAdjointPair J A₁ A₁ ↔ J.IsSkewAdjoint A₁
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J) A₁ ↔ J.IsSkewAdjoint A₁

Tactic:
rw [skewAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule]

Premises used: mem_pairSelfAdjointMatricesSubmodule, skewAdjointMatricesSubmodule
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
inst : CommRing R
inst_1 : Fintype n
J A₁ : Matrix n n R
inst_2 : DecidableEq n
⊢ (-J).IsAdjointPair J A₁ A₁ ↔ J.IsSkewAdjoint A₁

Tactic:
simp [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]

Premises used: Matrix.IsSkewAdjoint, Matrix.IsAdjointPair
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
h : M.SeparatingLeft
⊢ SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((Matrix.toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)

Tactic:
simpa [SeparatingLeft, toLinearMap₂'_apply', separatingLeft_def] using h

Premises used: Matrix.toLinearMap₂'_apply', Matrix.separatingLeft_def, LinearMap.SeparatingLeft
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
h : M.SeparatingRight
⊢ SeparatingRight (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((Matrix.toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)

Tactic:
simpa [SeparatingRight, toLinearMap₂'_apply', separatingRight_def] using h

Premises used: Matrix.toLinearMap₂'_apply', LinearMap.SeparatingRight, Matrix.separatingRight_def
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
h : M.Nondegenerate
⊢ Nondegenerate (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)

Tactic:
⟨h.1.toLinearMap₂', h.2.toLinearMap₂'⟩

Premises used: Matrix.Nondegenerate.separatingRight, Matrix.SeparatingLeft.toLinearMap₂', Matrix.SeparatingRight.toLinearMap₂', And.intro, Matrix.Nondegenerate.separatingLeft, LinearMap.Nondegenerate
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
⊢ SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.SeparatingLeft

Tactic:
⟨fun h ↦ separatingLeft_def.mpr ?_, SeparatingLeft.toLinearMap₂'⟩

Premises used: Iff.mpr, Matrix.SeparatingLeft.toLinearMap₂', Matrix.separatingLeft_def, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
refine :
  ∀
    (h :
      SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
        RingHom.id R)
        (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
            (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
          M))
    (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
⊢ SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R)
      (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
          (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
        M) ↔
    M.SeparatingLeft

Tactic:
refine ⟨fun h ↦ separatingLeft_def.mpr ?_, SeparatingLeft.toLinearMap₂'⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
n : Type u_11
m : Type u_12
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix m n R
h :
  SeparatingLeft (R := R) (R₁ := R) (R₂ := R) (M := R) (M₁ := m → R) (M₂ := n → R) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R)
    (((toLinearMap₂' R : Matrix m n R ≃ₗ[R] (m → R) →ₗ[R] (n → R) →ₗ[R] R) :
        (a : Matrix m n R) → (m → R) →ₗ[R] (n → R) →ₗ[R] R)
      M)
⊢ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0

Tactic:
fun v hv => h v fun w => (M.toLinearMap₂'_apply' _ _).trans <| hv w

Premises used: Matrix.toLinearMap₂'_apply', Eq.trans