awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
h₁ :
  HSub.hSub (α := R₁) (β := R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((φ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
h₂ :
  HSub.hSub (α := R₁) (β := R₁) ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
h₃ :
  HSub.hSub (α := R₁) (β := R₁) ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B.compLeft ψ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
⊢ Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁)
              (HSub.hSub (α := M₁) (β := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)) :
            M₁ →ₗ[R₁] R₁) :
          (a : M₁) → R₁)
        v :
      R₁)
    (0 : R₁)
have h₄ : HSub.hSub (α := R₁) (β := R₁) ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
    ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
  0
Tactic: rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
h₁ :
  HSub.hSub (α := R₁) (β := R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((φ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
h₂ :
  HSub.hSub (α := R₁) (β := R₁) ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
h₃ :
  HSub.hSub (α := R₁) (β := R₁) ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B.compLeft ψ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
h₄ :
  HSub.hSub (α := R₁) (β := R₁) ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
⊢ Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁)
              (HSub.hSub (α := M₁) (β := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)) :
            M₁ →ₗ[R₁] R₁) :
          (a : M₁) → R₁)
        v :
      R₁)
    (0 : R₁)
have h₅ : Eq.{u_3 + 1} (α := R₁) 0 0
Tactic: rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁
hψ₁ : IsAdjointPair B B (⇑ψ₁ : (a : M₁) → M₁) (⇑φ : (a : M₁) → M₁)
hψ₂ : IsAdjointPair B B (⇑ψ₂ : (a : M₁) → M₁) (⇑φ : (a : M₁) → M₁)
v w : M₁
⊢ Eq.{u_3 + 1} (α := R₁) ((((B.compLeft ψ₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
    ((((B.compLeft ψ₂ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
have rw : Eq.{u_3 + 1} (α := R₁)
  ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₁ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
  ((((B.compLeft ψ₂ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
Tactic: rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁
hψ₁ : IsAdjointPair B B (⇑ψ₁ : (a : M₁) → M₁) (⇑φ : (a : M₁) → M₁)
hψ₂ : IsAdjointPair B B (⇑ψ₂ : (a : M₁) → M₁) (⇑φ : (a : M₁) → M₁)
v w : M₁
rw :
  Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₁ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
    ((((B.compLeft ψ₂ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
⊢ Eq.{u_3 + 1} (α := R₁) ((((B.compLeft ψ₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
    ((((B.compLeft ψ₂ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
have rw₁ : Eq.{u_3 + 1} (α := R₁)
  ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₁ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
  ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₂ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
Tactic: rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁
hψ₁ : IsAdjointPair B B (⇑ψ₁ : (a : M₁) → M₁) (⇑φ : (a : M₁) → M₁)
hψ₂ : IsAdjointPair B B (⇑ψ₂ : (a : M₁) → M₁) (⇑φ : (a : M₁) → M₁)
v w : M₁
rw :
  Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₁ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
    ((((B.compLeft ψ₂ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
rw₁ :
  Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₁ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₂ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
⊢ Eq.{u_3 + 1} (α := R₁) ((((B.compLeft ψ₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
    ((((B.compLeft ψ₂ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
have rw₂ : Eq.{u_3 + 1} (α := R₁)
  ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) ((φ : (a : M₁) → M₁) w : M₁) : R₁)
  ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₂ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
Tactic: rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁
hψ₁ : IsAdjointPair B B (⇑ψ₁ : (a : M₁) → M₁) (⇑φ : (a : M₁) → M₁)
hψ₂ : IsAdjointPair B B (⇑ψ₂ : (a : M₁) → M₁) (⇑φ : (a : M₁) → M₁)
v w : M₁
rw :
  Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₁ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
    ((((B.compLeft ψ₂ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
rw₁ :
  Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₁ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₂ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
rw₂ :
  Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) ((φ : (a : M₁) → M₁) w : M₁) : R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ₂ : (a : M₁) → M₁) v) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
⊢ Eq.{u_3 + 1} (α := R₁) ((((B.compLeft ψ₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
    ((((B.compLeft ψ₂ : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) w : R₁)
have rw₃ : Eq.{u_3 + 1} (α := R₁)
  ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) ((φ : (a : M₁) → M₁) w : M₁) : R₁)
  ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) v : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) ((φ : (a : M₁) → M₁) w : M₁) : R₁)
Tactic: rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
f : Dual K V
v : V
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) (((B.toDual hB).symm : (a : Dual K V) → V) f) : V →ₗ[K] K) : (a : V) → K) v : K)
    ((f : (a : V) → K) v : K)
have change : Eq.{u_6 + 1} (α := K)
  ((((B.toDual hB : (a : V) → Dual K V) (((B.toDual hB).symm : (a : Dual K V) → V) f) : Dual K V) : (a : V) → K) v : K)
  ((f : (a : V) → K) v : K)
Tactic: change B.toDual hB ((B.toDual hB).symm f) v = f v
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (hypothesis)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
⊢ Eq.{u_6 + 1} (α := K) (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
have this : FiniteDimensional K V
Tactic: have := b.finiteDimensional_of_finite
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
⊢ Eq.{u_6 + 1} (α := K) (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
have rw : Eq.{u_6 + 1} (α := K)
  (((((b.dualBasis.map (B.toDual hB).symm).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
  ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
Tactic: rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    Basis.dualBasis_repr, toDual_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
rw :
  Eq.{u_6 + 1} (α := K)
    (((((b.dualBasis.map (B.toDual hB).symm).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
⊢ Eq.{u_6 + 1} (α := K) (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
have rw₁ : Eq.{u_6 + 1} (α := K)
  (((((B.toDual hB).symm.symm ≪≫ₗ b.dualBasis.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
  ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
Tactic: rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    Basis.dualBasis_repr, toDual_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
rw :
  Eq.{u_6 + 1} (α := K)
    (((((b.dualBasis.map (B.toDual hB).symm).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    (((((B.toDual hB).symm.symm ≪≫ₗ b.dualBasis.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
⊢ Eq.{u_6 + 1} (α := K) (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
have rw₂ : Eq.{u_6 + 1} (α := K) ((((B.toDual hB ≪≫ₗ b.dualBasis.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
  ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
Tactic: rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    Basis.dualBasis_repr, toDual_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
rw :
  Eq.{u_6 + 1} (α := K)
    (((((b.dualBasis.map (B.toDual hB).symm).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    (((((B.toDual hB).symm.symm ≪≫ₗ b.dualBasis.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₂ :
  Eq.{u_6 + 1} (α := K) ((((B.toDual hB ≪≫ₗ b.dualBasis.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
⊢ Eq.{u_6 + 1} (α := K) (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
have rw₃ : Eq.{u_6 + 1} (α := K)
  ((((b.dualBasis.repr : (a : Dual K V) → ι →₀ K) ((B.toDual hB : (a : V) → Dual K V) x) : ι →₀ K) : (a : ι) → K) i : K)
  ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
Tactic: rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    Basis.dualBasis_repr, toDual_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
rw :
  Eq.{u_6 + 1} (α := K)
    (((((b.dualBasis.map (B.toDual hB).symm).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    (((((B.toDual hB).symm.symm ≪≫ₗ b.dualBasis.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₂ :
  Eq.{u_6 + 1} (α := K) ((((B.toDual hB ≪≫ₗ b.dualBasis.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₃ :
  Eq.{u_6 + 1} (α := K)
    ((((b.dualBasis.repr : (a : Dual K V) → ι →₀ K) ((B.toDual hB : (a : V) → Dual K V) x) : ι →₀ K) : (a : ι) → K) i :
      K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
⊢ Eq.{u_6 + 1} (α := K) (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
have rw₄ : Eq.{u_6 + 1} (α := K) ((((B.toDual hB : (a : V) → Dual K V) x : Dual K V) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
  ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
Tactic: rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    Basis.dualBasis_repr, toDual_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
rw :
  Eq.{u_6 + 1} (α := K)
    (((((b.dualBasis.map (B.toDual hB).symm).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    (((((B.toDual hB).symm.symm ≪≫ₗ b.dualBasis.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₂ :
  Eq.{u_6 + 1} (α := K) ((((B.toDual hB ≪≫ₗ b.dualBasis.repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₃ :
  Eq.{u_6 + 1} (α := K)
    ((((b.dualBasis.repr : (a : Dual K V) → ι →₀ K) ((B.toDual hB : (a : V) → Dual K V) x) : ι →₀ K) : (a : ι) → K) i :
      K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
rw₄ :
  Eq.{u_6 + 1} (α := K)
    ((((B.toDual hB : (a : V) → Dual K V) x : Dual K V) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
⊢ Eq.{u_6 + 1} (α := K) (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
have rw₅ : Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
  ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) i : V) : K)
Tactic: rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    Basis.dualBasis_repr, toDual_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (hypothesis)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
have this : FiniteDimensional K V
Tactic: have := b.finiteDimensional_of_finite
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
have rw : Eq.{u_6 + 1} (α := K)
  ((((B : (a : V) → V →ₗ[K] K) ((b.dualBasis.map (B.toDual hB).symm : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
      ((b : (a : ι) → V) j : V) :
    K)
  (if j = i then 1 else 0 : K)
Tactic: rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB,
    LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((b.dualBasis.map (B.toDual hB).symm : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
have rw₁ : Eq.{u_6 + 1} (α := K)
  ((((B : (a : V) → V →ₗ[K] K)
            (((B.toDual hB).symm : (a : Dual K V) → V) ((b.dualBasis : (a : ι) → Dual K V) i : Dual K V)) :
          V →ₗ[K] K) :
        (a : V) → K)
      ((b : (a : ι) → V) j : V) :
    K)
  (if j = i then 1 else 0 : K)
Tactic: rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB,
    LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((b.dualBasis.map (B.toDual hB).symm : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K)
              (((B.toDual hB).symm : (a : Dual K V) → V) ((b.dualBasis : (a : ι) → Dual K V) i : Dual K V)) :
            V →ₗ[K] K) :
          (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
have rw₂ : Eq.{u_6 + 1} (α := K)
  ((((B : (a : V) → V →ₗ[K] K) (((B.toDual hB).symm : (a : Dual K V) → V) (b.coord i)) : V →ₗ[K] K) : (a : V) → K)
      ((b : (a : ι) → V) j : V) :
    K)
  (if j = i then 1 else 0 : K)
Tactic: rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB,
    LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((b.dualBasis.map (B.toDual hB).symm : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K)
              (((B.toDual hB).symm : (a : Dual K V) → V) ((b.dualBasis : (a : ι) → Dual K V) i : Dual K V)) :
            V →ₗ[K] K) :
          (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
rw₂ :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) (((B.toDual hB).symm : (a : Dual K V) → V) (b.coord i)) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) j : V) :
      K)
    (if j = i then 1 else 0 : K)
have rw₃ : Eq.{u_6 + 1} (α := K)
  ((((B.toDual hB : (a : V) → Dual K V) (((B.toDual hB).symm : (a : Dual K V) → V) (b.coord i)) : Dual K V) :
        (a : V) → K)
      ((b : (a : ι) → V) j : V) :
    K)
  (if j = i then 1 else 0 : K)
Tactic: rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB,
    LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply]