awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : Fintype n
inst_2 : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_3 : DecidableEq n
inst_4 : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
mp :
  B = B' →
    Eq (α := Matrix n n' R)
      (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
            (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
          B :
        Matrix n n' R)
      (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
            (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
          B' :
        Matrix n n' R)
⊢ B = B' ↔
    Eq (α := Matrix n n' R)
      (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
            (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
          B :
        Matrix n n' R)
      (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
            (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
          B' :
        Matrix n n' R)
have mpr : Eq (α := Matrix n n' R)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
          (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
        B :
      Matrix n n' R)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
          (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
        B' :
      Matrix n n' R) →
  B = B'
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : Fintype n
inst_2 : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_3 : DecidableEq n
inst_4 : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
h : B = B'
⊢ Eq (α := Matrix n n' R)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
          (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
        B :
      Matrix n n' R)
    (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
          (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
        B' :
      Matrix n n' R)
have mp : Eq (α := Matrix n n' R)
  (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
        (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
      B' :
    Matrix n n' R)
  (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
        (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
      B' :
    Matrix n n' R)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (hypothesis)
Goal:
R : Type u_1
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : Fintype n
inst_2 : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_3 : DecidableEq n
inst_4 : DecidableEq n'
⊢ Eq (α := (n → R) →ₗ[R] (n' → R) →ₗ[R] R)
      (((toLinearMap₂' R : Matrix n' n' R ≃ₗ[R] (n' → R) →ₗ[R] (n' → R) →ₗ[R] R) :
            (a : Matrix n' n' R) → (n' → R) →ₗ[R] (n' → R) →ₗ[R] R)
          J' ∘ₗ
        (toLin' : (a : Matrix n' n R) → (n → R) →ₗ[R] n' → R) A)
      (compl₂ (R₂ := R) (N := n → R) (σ₂₃ := RingHom.id R) (σ₄₂ := RingHom.id R)
        (((toLinearMap₂' R : Matrix n n R ≃ₗ[R] (n → R) →ₗ[R] (n → R) →ₗ[R] R) :
            (a : Matrix n n R) → (n → R) →ₗ[R] (n → R) →ₗ[R] R)
          J)
        ((toLin' : (a : Matrix n n' R) → (n' → R) →ₗ[R] n → R) A')) ↔
    J.IsAdjointPair J' A A'
have h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R),
  B = B' ↔
    Eq (α := Matrix n n' R)
      (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
            (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
          B :
        Matrix n n' R)
      (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
            (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
          B' :
        Matrix n n' R)
Tactic: have h :
    ∀ B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R,
      B = B' ↔ LinearMap.toMatrix₂' R B = LinearMap.toMatrix₂' R B' := by
    intro B B'
    constructor <;> intro h
    · rw [h]
    · exact (LinearMap.toMatrix₂' R).injective h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
n : Type u_11
n' : Type u_13
inst : CommRing R
inst_1 : Fintype n
inst_2 : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst_3 : DecidableEq n
inst_4 : DecidableEq n'
h :
  ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R),
    B = B' ↔
      Eq (α := Matrix n n' R)
        (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
              (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
            B :
          Matrix n n' R)
        (((toMatrix₂' R : ((n → R) →ₗ[R] (n' → R) →ₗ[R] R) ≃ₗ[R] Matrix n n' R) :
              (a : (n → R) →ₗ[R] (n' → R) →ₗ[R] R) → Matrix n n' R)
            B' :
          Matrix n n' R)
⊢ Eq (α := (n → R) →ₗ[R] (n' → R) →ₗ[R] R)
      (((toLinearMap₂' R : Matrix n' n' R ≃ₗ[R] (n' → R) →ₗ[R] (n' → R) →ₗ[R] R) :
            (a : Matrix n' n' R) → (n' → R) →ₗ[R] (n' → R) →ₗ[R] R)
          J' ∘ₗ
        (toLin' : (a : Matrix n' n R) → (n → R) →ₗ[R] n' → R) A)
      (compl₂ (R₂ := R) (N := n → R) (σ₂₃ := RingHom.id R) (σ₄₂ := RingHom.id R)
        (((toLinearMap₂' R : Matrix n n R ≃ₗ[R] (n → R) →ₗ[R] (n → R) →ₗ[R] R) :
            (a : Matrix n n R) → (n → R) →ₗ[R] (n → R) →ₗ[R] R)
          J)
        ((toLin' : (a : Matrix n n' R) → (n' → R) →ₗ[R] n → R) A')) ↔
    J.IsAdjointPair J' A A'
have simp_rw : Aᵀ * J' = J * A' ↔ J.IsAdjointPair J' A A'
Tactic: simp_rw [h, LinearMap.toMatrix₂'_comp, LinearMap.toMatrix₂'_compl₂,
    LinearMap.toMatrix'_toLin', LinearMap.toMatrix'_toLinearMap₂']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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'
⊢ 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'
have 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'
Tactic: rw [isAdjointPair_iff_comp_eq_compl₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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)
⊢ 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)
have 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'
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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'
⊢ 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)
have 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)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (hypothesis)
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'
⊢ 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'
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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)
⊢ 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'
have simp_rw : Aᵀ * J' = J * 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₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (hypothesis)
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
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
have h' : IsUnit P.det
Tactic: have h' : IsUnit P.det := P.isUnit_iff_isUnit_det.mp h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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)
⊢ A₁ᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A₂ ↔ (P * A₁ * P⁻¹)ᵀ * J = J * (P * A₂ * P⁻¹)
have simp : A₁ᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A₂ ↔ P⁻¹ᵀ * (A₁ᵀ * Pᵀ) * J = J * (P * A₂ * P⁻¹)
Tactic: simp only [Matrix.transpose_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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)
⊢ A₁ᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A₂ ↔ P⁻¹ᵀ * (A₁ᵀ * Pᵀ) * J = J * (P * A₂ * P⁻¹)
have simp : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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)
⊢ A₁ᵀ * Pᵀ * J * P = Pᵀ * J * P * A₂ ↔ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = J * P * A₂ * P⁻¹
have h₁ : Pᵀ * J * P * A₂ = (↑v : Matrix n n R) * y
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
⊢ A₁ᵀ * Pᵀ * J * P = Pᵀ * J * P * A₂ ↔ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = J * P * A₂ * P⁻¹
have h₂ : Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = (↑v⁻¹ : Matrix n n R) * x
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
have h₁ : Pᵀ * (J * P * A₂) = (↑v : Matrix n n R) * y
Tactic: rw [mul_assoc, mul_assoc, ← mul_assoc J]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
have h₁ : Pᵀ⁻¹ * (A₁ᵀ * Pᵀ * J) = (↑v⁻¹ : Matrix n n R) * x
Tactic: rw [mul_assoc, mul_assoc, ← mul_assoc _ _ J]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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₂
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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₂
⊢ x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x = y * (↑u⁻¹ : Matrix n n R)
have 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
Tactic: rw [Units.eq_mul_inv_iff_mul_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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₂
| (↑v⁻¹ : Matrix n n R) * x * (↑u : Matrix n n R) = y
have rw : (↑v⁻¹ : Matrix n n R) * (x * (↑u : Matrix n n R)) = y
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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₂
⊢ x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * x * (↑u : Matrix n n R) = y
have 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
Tactic: conv_rhs => rw [mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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₂
⊢ x * (↑u : Matrix n n R) = (↑v : Matrix n n R) * y ↔ (↑v⁻¹ : Matrix n n R) * (x * (↑u : Matrix n n R)) = y
have 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
Tactic: rw [v.inv_mul_eq_iff_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (selfAdjointMatricesSubmodule J) A₁ ↔ J.IsSelfAdjoint A₁
have rw : Membership.mem (γ := Submodule R (Matrix n n R)) (pairSelfAdjointMatricesSubmodule J J) A₁ ↔ J.IsSelfAdjoint A₁
Tactic: rw [selfAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule, Matrix.IsSelfAdjoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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₁
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (selfAdjointMatricesSubmodule J) A₁ ↔ J.IsSelfAdjoint A₁
have rw₁ : J.IsAdjointPair J A₁ A₁ ↔ J.IsSelfAdjoint A₁
Tactic: rw [selfAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule, Matrix.IsSelfAdjoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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₁
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (selfAdjointMatricesSubmodule J) A₁ ↔ J.IsSelfAdjoint A₁
have rw₂ : J.IsAdjointPair J A₁ A₁ ↔ J.IsAdjointPair J A₁ A₁
Tactic: rw [selfAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule, Matrix.IsSelfAdjoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J) A₁ ↔ J.IsSkewAdjoint A₁
have rw : (-J).IsAdjointPair J A₁ A₁ ↔ J.IsSkewAdjoint A₁
Tactic: rw [skewAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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
have 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
Tactic: refine ⟨fun h ↦ separatingLeft_def.mpr ?_, SeparatingLeft.toLinearMap₂'⟩