awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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.coord i : (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)
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)
rw₄ : Eq.{u_6 + 1} (α := K) ((b.coord i : (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.repr : (a : V) → ι →₀ K) ((b : (a : ι) → V) j) : ι →₀ K) : (a : ι) → K) i : 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)
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)
rw₄ : Eq.{u_6 + 1} (α := K) ((b.coord i : (a : V) → K) ((b : (a : ι) → V) j : V) : K) (if j = i then 1 else 0 : K)
rw₅ :
  Eq.{u_6 + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) ((b : (a : ι) → V) j) : ι →₀ K) : (a : ι) → K) i : 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) ((Finsupp.single j 1 : (a : ι) → K) i : 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)
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)
rw₄ : Eq.{u_6 + 1} (α := K) ((b.coord i : (a : V) → K) ((b : (a : ι) → V) j : V) : K) (if j = i then 1 else 0 : K)
rw₅ :
  Eq.{u_6 + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) ((b : (a : ι) → V) j) : ι →₀ K) : (a : ι) → K) i : K)
    (if j = i then 1 else 0 : K)
rw₆ : Eq.{u_6 + 1} (α := K) ((Finsupp.single j 1 : (a : ι) → K) i : 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) (if j = i then 1 else 0) (if j = i then 1 else 0)
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
sym : B.IsSymm
b : Basis ι K V
i j : ι
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.dualBasis hB b : (a : ι) → V) j : V) :
      K)
    (if i = j then 1 else 0 : K)
have rw : Eq.{u_6 + 1} (α := K)
  ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) j) : V →ₗ[K] K) : (a : V) → K)
      ((b : (a : ι) → V) i : V) :
    K)
  (if i = j then 1 else 0 : K)
Tactic: rw [sym.eq, apply_dualBasis_left]
-- 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
sym : B.IsSymm
b : Basis ι K V
i j : ι
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) j) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) i : V) :
      K)
    (if i = j then 1 else 0 : K)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.dualBasis hB b : (a : ι) → V) j : V) :
      K)
    (if i = j then 1 else 0 : K)
have rw₁ : Eq.{u_6 + 1} (α := K) (if i = j then 1 else 0) (if i = j then 1 else 0)
Tactic: rw [sym.eq, apply_dualBasis_left]
-- 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
⊢ B.dualBasis hB (B.flip.dualBasis ⋯ b) = b
have a : ∀ (i : ι), Eq.{u_5 + 1} (α := V) ((B.dualBasis hB (B.flip.dualBasis sorry b) : (a : ι) → V) i : V) ((b : (a : ι) → V) i : V)
Tactic: ext i
-- 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 : ι
⊢ Eq.{u_5 + 1} (α := V) ((B.dualBasis hB (B.flip.dualBasis ⋯ b) : (a : ι) → V) i : V) ((b : (a : ι) → V) i : V)
have a : ∀ (j : ι),
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB (B.flip.dualBasis sorry b) : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis sorry b : (a : ι) → V) j : V) :
      K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis sorry b : (a : ι) → V) j : V) :
      K)
Tactic: refine LinearMap.ker_eq_bot.mp hB.ker_eq_bot ((B.flip.dualBasis hB.flip b).ext (fun j ↦ ?_))
-- 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 : ι
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB (B.flip.dualBasis ⋯ b) : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
have a : Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0 : K)
  ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
      ((B.flip.dualBasis sorry b : (a : ι) → V) j : V) :
    K)
Tactic: simp_rw [apply_dualBasis_left, ← B.flip_apply, apply_dualBasis_left, @eq_comm _ i j]
-- 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 : ι
a :
  Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0 : K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB (B.flip.dualBasis ⋯ b) : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
have a₁ : Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0 : K)
  ((((((flipHom : (a : BilinForm K V) → BilinForm K V) B : BilinForm K V) : (a : V) → V →ₗ[K] K)
            ((B.flip.dualBasis sorry b : (a : ι) → V) j) :
          V →ₗ[K] K) :
        (a : V) → K)
      ((b : (a : ι) → V) i : V) :
    K)
Tactic: simp_rw [apply_dualBasis_left, ← B.flip_apply, apply_dualBasis_left, @eq_comm _ i j]
-- 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 : ι
a :
  Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0 : K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
a₁ :
  Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0 : K)
    ((((((flipHom : (a : BilinForm K V) → BilinForm K V) B : BilinForm K V) : (a : V) → V →ₗ[K] K)
              ((B.flip.dualBasis ⋯ b : (a : ι) → V) j) :
            V →ₗ[K] K) :
          (a : V) → K)
        ((b : (a : ι) → V) i : V) :
      K)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB (B.flip.dualBasis ⋯ b) : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
    ((((B : (a : V) → V →ₗ[K] K) ((b : (a : ι) → V) i) : V →ₗ[K] K) : (a : V) → K)
        ((B.flip.dualBasis ⋯ b : (a : ι) → V) j : V) :
      K)
have a₂ : Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0) (if i = j then 1 else 0)
Tactic: simp_rw [apply_dualBasis_left, ← B.flip_apply, apply_dualBasis_left, @eq_comm _ i j]
-- 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
hB' : B.IsSymm
b : Basis ι K V
⊢ B.dualBasis hB (B.dualBasis hB b) = b
have h : B = B.flip
Tactic: convert! dualBasis_dualBasis_flip hB.flip b
-- 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
hB' : B.IsSymm
b : Basis ι K V
⊢ B = B.flip
have h : B.flip = B
Tactic: rwa [eq_comm, ← isSymm_iff_flip]
-- 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
v : ι → V
h : (⇑(B.dualBasis hB b) : (a : ι) → V) = v
x x_1 : ι
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
    (if x_1 = x then 1 else 0 : K)
have rw : Eq.{u_6 + 1} (α := K)
  ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
      ((b : (a : ι) → V) x_1 : V) :
    K)
  (if x_1 = x then 1 else 0 : K)
Tactic: rw [← h, apply_dualBasis_left]
-- 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
v : ι → V
h : (⇑(B.dualBasis hB b) : (a : ι) → V) = v
x x_1 : ι
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) x_1 : V) :
      K)
    (if x_1 = x then 1 else 0 : K)
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
    (if x_1 = x then 1 else 0 : K)
have rw₁ : Eq.{u_6 + 1} (α := K) (if x_1 = x then 1 else 0) (if x_1 = x then 1 else 0)
Tactic: rw [← h, apply_dualBasis_left]
-- 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
v : ι → V
h :
  ∀ (i j : ι),
    Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) j : V) : K)
      (if j = i then 1 else 0 : K)
x x_1 : ι
⊢ Eq.{u_6 + 1} (α := K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) ((B.dualBasis hB b : (a : ι) → V) x) : ι →₀ K) : (a : ι) → K) x_1 :
      K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)
have rw : Eq.{u_6 + 1} (α := K)
  ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
      ((b : (a : ι) → V) x_1 : V) :
    K)
  (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)
Tactic: rw [dualBasis_repr_apply, dualBasis_repr_apply, apply_dualBasis_left, 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
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h :
  ∀ (i j : ι),
    Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) j : V) : K)
      (if j = i then 1 else 0 : K)
x x_1 : ι
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) x_1 : V) :
      K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)
⊢ Eq.{u_6 + 1} (α := K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) ((B.dualBasis hB b : (a : ι) → V) x) : ι →₀ K) : (a : ι) → K) x_1 :
      K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)
have rw₁ : Eq.{u_6 + 1} (α := K)
  ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
      ((b : (a : ι) → V) x_1 : V) :
    K)
  ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
Tactic: rw [dualBasis_repr_apply, dualBasis_repr_apply, apply_dualBasis_left, 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
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h :
  ∀ (i j : ι),
    Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) j : V) : K)
      (if j = i then 1 else 0 : K)
x x_1 : ι
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) x_1 : V) :
      K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) x_1 : V) :
      K)
    ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
⊢ Eq.{u_6 + 1} (α := K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) ((B.dualBasis hB b : (a : ι) → V) x) : ι →₀ K) : (a : ι) → K) x_1 :
      K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)
have rw₂ : Eq.{u_6 + 1} (α := K) (if x_1 = x then 1 else 0 : K)
  ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
Tactic: rw [dualBasis_repr_apply, dualBasis_repr_apply, apply_dualBasis_left, 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
ι : Type u_9
inst_3 : DecidableEq ι
inst_4 : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h :
  ∀ (i j : ι),
    Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) j : V) : K)
      (if j = i then 1 else 0 : K)
x x_1 : ι
rw :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) x_1 : V) :
      K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)
rw₁ :
  Eq.{u_6 + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) ((B.dualBasis hB b : (a : ι) → V) x) : V →ₗ[K] K) : (a : V) → K)
        ((b : (a : ι) → V) x_1 : V) :
      K)
    ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
rw₂ :
  Eq.{u_6 + 1} (α := K) (if x_1 = x then 1 else 0 : K)
    ((((B : (a : V) → V →ₗ[K] K) (v x) : V →ₗ[K] K) : (a : V) → K) ((b : (a : ι) → V) x_1 : V) : K)
⊢ Eq.{u_6 + 1} (α := K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) ((B.dualBasis hB b : (a : ι) → V) x) : ι →₀ K) : (a : ι) → K) x_1 :
      K)
    (((((B.dualBasis hB b).repr : (a : V) → ι →₀ K) (v x) : ι →₀ K) : (a : ι) → K) x_1 : K)
have rw₃ : Eq.{u_6 + 1} (α := K) (if x_1 = x then 1 else 0) (if x_1 = x then 1 else 0)
Tactic: rw [dualBasis_repr_apply, dualBasis_repr_apply, apply_dualBasis_left, 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₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ Eq (α := V →ₗ[K] K) ((B₂ : (a : V) → V →ₗ[K] K) ((B₁.symmCompOfNondegenerate B₂ b₂ : (a : V) → V) v) : V →ₗ[K] K)
    ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)
have rw : Eq (α := V →ₗ[K] K)
  ((B₂ : (a : V) → V →ₗ[K] K) (((↑(B₂.toDual b₂).symm : Dual K V →ₗ[K] V) ∘ₗ B₁ : (a : V) → V) v) : V →ₗ[K] K)
  ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)
Tactic: rw [symmCompOfNondegenerate]
-- 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₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ Eq (α := V →ₗ[K] K)
    ((B₂ : (a : V) → V →ₗ[K] K) (((↑(B₂.toDual b₂).symm : Dual K V →ₗ[K] V) ∘ₗ B₁ : (a : V) → V) v) : V →ₗ[K] K)
    ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)
have simp : Eq (α := V →ₗ[K] K)
  ((B₂ : (a : V) → V →ₗ[K] K) (((B₂.toDual b₂).symm : (a : Dual K V) → V) ((B₁ : (a : V) → Dual K V) v : Dual K V)) :
    V →ₗ[K] K)
  ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)
Tactic: simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_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
inst_3 : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ Eq (α := V →ₗ[K] K)
    ((B₂ : (a : V) → V →ₗ[K] K) (((B₂.toDual b₂).symm : (a : Dual K V) → V) ((B₁ : (a : V) → Dual K V) v : Dual K V)) :
      V →ₗ[K] K)
    ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)
have erw : Eq (α := V →ₗ[K] K) ((B₁ : (a : V) → Dual K V) v : Dual K V) ((B₁ : (a : V) → V →ₗ[K] K) v : V →ₗ[K] K)
Tactic: erw [LinearEquiv.apply_symm_apply (B₂.toDual b₂)]