awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i_1 : m,
      ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) : (a : n) → R)
            i' :
          R) •>
        ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                (a : m) → R)
              i_1 :
            R) •>
          ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) i_1 : M₂) :
            R))
    (∑ x : m,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                (a : n) → R)
              i' :
            R)
          ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) x : M₂) :
            R))
        ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
              (a : m) → R)
            x :
          R))
have a : ∀ (x : m),
  Membership.mem (γ := Finset m) univ x →
    ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) : (a : n) → R)
            i' :
          R) •>
        ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                (a : m) → R)
              x :
            R) •>
          ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) x : M₂) :
            R) =
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                (a : n) → R)
              i' :
            R)
          ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i') : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) x : M₂) :
            R))
        ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
              (a : m) → R)
            x :
          R)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
b₁' : Basis n' R M₁'
inst_11 : Fintype n'
inst_12 : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₁' →ₗ[R] M₁
⊢ (toMatrix₂ b₁' b₂ : (a : M₁' →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m R) (B ∘ₗ f) =
    HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) f)ᵀ
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
have rw : HMul.hMul (β := Matrix m m R)
    (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) f)ᵀ
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
    ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) id : Matrix m m R) =
  HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) f)ᵀ
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
Tactic: rw [← LinearMap.compl₂_id (B.comp f), ← LinearMap.compl₁₂, LinearMap.toMatrix₂_compl₁₂ b₁ b₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
m' : Type u_14
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₂'
inst_10 : Module R M₂'
b₂' : Basis m' R M₂'
inst_11 : Fintype m'
inst_12 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₂' →ₗ[R] M₂
⊢ (toMatrix₂ b₁ b₂' : (a : M₁ →ₗ[R] M₂' →ₗ[R] R) → Matrix n m' R) (B.compl₂ f) =
    HMul.hMul (α := Matrix n m R) (β := Matrix m m' R)
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
      ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) f : Matrix m m' R)
have rw : HMul.hMul (β := Matrix m m' R)
    (HMul.hMul (α := Matrix n n R) (β := Matrix n m R) ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id)ᵀ
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
    ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) f : Matrix m m' R) =
  HMul.hMul (α := Matrix n m R) (β := Matrix m m' R)
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) (B ∘ₗ id) : Matrix n m R)
    ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) f : Matrix m m' R)
Tactic: rw [← LinearMap.comp_id B, ← LinearMap.compl₁₂, LinearMap.toMatrix₂_compl₁₂ b₁ b₂]
-- 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
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : Fintype n'
inst_10 : Fintype m'
inst_11 : DecidableEq n'
inst_12 : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ HMul.hMul (β := Matrix m m' R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) (b₁.toMatrix (⇑c₁ : (a : n') → M₁))ᵀ
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
      (b₂.toMatrix (⇑c₂ : (a : m') → M₂)) =
    (toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) B
have simp_rw : HMul.hMul (β := Matrix m m' R)
    (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix c₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n' R) id)ᵀ
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
    ((toMatrix c₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m' R) id : Matrix m m' R) =
  (toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) B
Tactic: simp_rw [← LinearMap.toMatrix_id_eq_basis_toMatrix]
-- 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
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : Fintype n'
inst_10 : Fintype m'
inst_11 : DecidableEq n'
inst_12 : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ HMul.hMul (β := Matrix m m' R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix c₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n' R) id)ᵀ
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
      ((toMatrix c₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m' R) id : Matrix m m' R) =
    (toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) B
have rw : Eq (α := Matrix n' m' R)
  ((toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) (B.compl₁₂ id id) : Matrix n' m' R)
  ((toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) B : Matrix n' m' R)
Tactic: rw [← LinearMap.toMatrix₂_compl₁₂, LinearMap.compl₁₂_id_id]
-- 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
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : Fintype n'
inst_10 : Fintype m'
inst_11 : DecidableEq n'
inst_12 : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
rw :
  Eq (α := Matrix n' m' R)
    ((toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) (B.compl₁₂ id id) : Matrix n' m' R)
    ((toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) B : Matrix n' m' R)
⊢ HMul.hMul (β := Matrix m m' R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R) ((toMatrix c₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n' R) id)ᵀ
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
      ((toMatrix c₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m' R) id : Matrix m m' R) =
    (toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) B
have rw₁ : Eq (α := Matrix n' m' R) ((toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) B : Matrix n' m' R)
  ((toMatrix₂ c₁ c₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m' R) B : Matrix n' m' R)
Tactic: rw [← LinearMap.toMatrix₂_compl₁₂, LinearMap.compl₁₂_id_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix n' n R
N : Matrix m m' R
⊢ HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) * N =
    (toMatrix₂ b₁' b₂' : (a : M₁' →ₗ[R] M₂' →ₗ[R] R) → Matrix n' m' R)
      (B.compl₁₂ ((toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ)
        ((toLin b₂' b₂ : (a : Matrix m m' R) → M₂' →ₗ[R] M₂) N))
have simp_rw : HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) * N =
  HMul.hMul (β := Matrix m m' R)
    (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R)
      ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) ((toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ))ᵀ
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
    ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) ((toLin b₂' b₂ : (a : Matrix m m' R) → M₂' →ₗ[R] M₂) N) :
      Matrix m m' R)
Tactic: simp_rw [LinearMap.toMatrix₂_compl₁₂ b₁ b₂, toMatrix_toLin, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix n' n R
N : Matrix m m' R
simp_rw :
  HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) * N =
    HMul.hMul (β := Matrix m m' R)
      (HMul.hMul (α := Matrix n' n R) (β := Matrix n m R)
        ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R)
            ((toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ))ᵀ
        ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R))
      ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) ((toLin b₂' b₂ : (a : Matrix m m' R) → M₂' →ₗ[R] M₂) N) :
        Matrix m m' R)
⊢ HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) * N =
    (toMatrix₂ b₁' b₂' : (a : M₁' →ₗ[R] M₂' →ₗ[R] R) → Matrix n' m' R)
      (B.compl₁₂ ((toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ)
        ((toLin b₂' b₂ : (a : Matrix m m' R) → M₂' →ₗ[R] M₂) N))
have simp_rw₁ : HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) * N =
  HMul.hMul (β := Matrix n m R) Mᵀᵀ ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) * N
Tactic: simp_rw [LinearMap.toMatrix₂_compl₁₂ b₁ b₂, toMatrix_toLin, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
b₁' : Basis n' R M₁'
inst_11 : Fintype n'
inst_12 : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix n' n R
⊢ HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) =
    (toMatrix₂ b₁' b₂ : (a : M₁' →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m R)
      (B ∘ₗ (toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ)
have rw : HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) =
  HMul.hMul (α := Matrix n' n R) (β := Matrix n m R)
    ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) ((toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ))ᵀ
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
Tactic: rw [LinearMap.toMatrix₂_comp b₁, toMatrix_toLin, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
b₁' : Basis n' R M₁'
inst_11 : Fintype n'
inst_12 : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix n' n R
rw :
  HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) =
    HMul.hMul (α := Matrix n' n R) (β := Matrix n m R)
      ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) ((toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ))ᵀ
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
⊢ HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) =
    (toMatrix₂ b₁' b₂ : (a : M₁' →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m R)
      (B ∘ₗ (toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ)
have rw₁ : HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) =
  HMul.hMul (β := Matrix n m R) Mᵀᵀ ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
Tactic: rw [LinearMap.toMatrix₂_comp b₁, toMatrix_toLin, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
b₁' : Basis n' R M₁'
inst_11 : Fintype n'
inst_12 : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix n' n R
rw :
  HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) =
    HMul.hMul (α := Matrix n' n R) (β := Matrix n m R)
      ((toMatrix b₁' b₁ : (a : M₁' →ₗ[R] M₁) → Matrix n n' R) ((toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ))ᵀ
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
rw₁ :
  HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) =
    HMul.hMul (β := Matrix n m R) Mᵀᵀ ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
⊢ HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) =
    (toMatrix₂ b₁' b₂ : (a : M₁' →ₗ[R] M₂ →ₗ[R] R) → Matrix n' m R)
      (B ∘ₗ (toLin b₁' b₁ : (a : Matrix n n' R) → M₁' →ₗ[R] M₁) Mᵀ)
have rw₂ : HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) =
  HMul.hMul (β := Matrix n m R) M ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
Tactic: rw [LinearMap.toMatrix₂_comp b₁, toMatrix_toLin, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
m' : Type u_14
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₂'
inst_10 : Module R M₂'
b₂' : Basis m' R M₂'
inst_11 : Fintype m'
inst_12 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix m m' R
⊢ HMul.hMul (α := Matrix n m R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) M =
    (toMatrix₂ b₁ b₂' : (a : M₁ →ₗ[R] M₂' →ₗ[R] R) → Matrix n m' R)
      (B.compl₂ (σ₄₂ := RingHom.id R) ((toLin b₂' b₂ : (a : Matrix m m' R) → M₂' →ₗ[R] M₂) M))
have rw : HMul.hMul (α := Matrix n m R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) M =
  HMul.hMul (α := Matrix n m R) (β := Matrix m m' R)
    ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
    ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) ((toLin b₂' b₂ : (a : Matrix m m' R) → M₂' →ₗ[R] M₂) M) :
      Matrix m m' R)
Tactic: rw [LinearMap.toMatrix₂_compl₂ b₁ b₂, toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
m' : Type u_14
inst : CommSemiring 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 m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₂'
inst_10 : Module R M₂'
b₂' : Basis m' R M₂'
inst_11 : Fintype m'
inst_12 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix m m' R
rw :
  HMul.hMul (α := Matrix n m R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) M =
    HMul.hMul (α := Matrix n m R) (β := Matrix m m' R)
      ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R)
      ((toMatrix b₂' b₂ : (a : M₂' →ₗ[R] M₂) → Matrix m m' R) ((toLin b₂' b₂ : (a : Matrix m m' R) → M₂' →ₗ[R] M₂) M) :
        Matrix m m' R)
⊢ HMul.hMul (α := Matrix n m R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) M =
    (toMatrix₂ b₁ b₂' : (a : M₁ →ₗ[R] M₂' →ₗ[R] R) → Matrix n m' R)
      (B.compl₂ (σ₄₂ := RingHom.id R) ((toLin b₂' b₂ : (a : Matrix m m' R) → M₂' →ₗ[R] M₂) M))
have rw₁ : HMul.hMul (α := Matrix n m R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) M =
  HMul.hMul (α := Matrix n m R) ((toMatrix₂ b₁ b₂ : (a : M₁ →ₗ[R] M₂ →ₗ[R] R) → Matrix n m R) B : Matrix n m R) M
Tactic: rw [LinearMap.toMatrix₂_compl₂ b₁ b₂, toMatrix_toLin]
-- 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'
⊢ LinearMap.IsAdjointPair (R := R) (M := n → R) (M₁ := n' → R) (M₃ := R) (I := 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)
      (((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 : (n → R) →ₗ[R] n' → R) : (a : n → R) → n' → R)
      (⇑((toLin' : (a : Matrix n n' R) → (n' → R) →ₗ[R] n → R) A' : (n' → R) →ₗ[R] n → R) : (a : n' → R) → n → R) ↔
    J.IsAdjointPair J' A A'
have rw : 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'
Tactic: rw [isAdjointPair_iff_comp_eq_compl₂]
-- 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
⊢ 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 : 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: constructor