awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Preorder R
inst_4 : PosMulMono R
B : BilinForm R M
c : R
hB : B.IsPosSemidef
hc : 0 ≤ c
⊢ (c • B).IsPosSemidef

Tactic:
isPosSemidef_def.2 ⟨hB.isSymm.smul c, hB.isNonneg.smul hc⟩

Premises used: Iff.mpr, LinearMap.BilinForm.IsPosSemidef.isNonneg, LinearMap.BilinForm.isPosSemidef_def, LinearMap.BilinForm.IsPosSemidef.isSymm, LinearMap.BilinForm.IsSymm.smul, And.intro, LinearMap.BilinForm.IsNonneg.smul
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
H : B.IsAlt
x : M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)

Tactic:
LinearMap.IsAlt.self_eq_zero H x

Premises used: LinearMap.IsAlt.self_eq_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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₁
H : B₁.IsAlt
x y : M₁
⊢ Eq.{u_3 + 1} (α := R₁) (-(((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)
    ((((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) y : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) x : R₁)

Tactic:
LinearMap.IsAlt.neg H x y

Premises used: LinearMap.IsAlt.neg
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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₁
H : B₁.IsAlt
⊢ B₁.IsRefl

Tactic:
LinearMap.IsAlt.isRefl H

Premises used: LinearMap.BilinForm.IsRefl, LinearMap.IsAlt.isRefl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
inst_3 : IsCancelAdd R
a b c : M
H : B.IsAlt
hAdd : a + b + c = 0
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) a : M →ₗ[R] R) : (a : M) → R) b : R)
    ((((B : (a : M) → M →ₗ[R] R) b : M →ₗ[R] R) : (a : M) → R) c : R)

Tactic:
LinearMap.IsAlt.eq_of_add_add_eq_zero H hAdd

Premises used: LinearMap.IsAlt.eq_of_add_add_eq_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B₁ B₂ : BilinForm R M
hB₁ : B₁.IsAlt
hB₂ : B₂.IsAlt
⊢ (B₁ + B₂).IsAlt

Tactic:
fun x => (congr_arg₂ (· + ·) (hB₁ x) (hB₂ x) :).trans <| add_zero _

Premises used: LinearMap.BilinForm.IsAlt, HAdd.hAdd, LinearMap.IsAlt, add_zero, OfNat.ofNat, Eq.trans, congr_arg₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B₁ B₂ : BilinForm R₁ M₁
hB₁ : B₁.IsAlt
hB₂ : B₂.IsAlt
⊢ (B₁ - B₂).IsAlt

Tactic:
fun x => (congr_arg₂ Sub.sub (hB₁ x) (hB₂ x)).trans <| sub_zero _

Premises used: sub_zero, LinearMap.BilinForm.IsAlt, Sub.sub, LinearMap.IsAlt, OfNat.ofNat, Eq.trans, congr_arg₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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₁
hB : B.IsAlt
⊢ (-B).IsAlt

Tactic:
fun x =>
  neg_eq_zero.mpr <| hB x

Premises used: Iff.mpr, LinearMap.BilinForm.IsAlt, neg_eq_zero, LinearMap.IsAlt
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α R
inst_5 : SMulCommClass R α R
a : α
B : BilinForm R M
hB : B.IsAlt
⊢ (a • B).IsAlt

Tactic:
fun x =>
  (congr_arg (a • ·) (hB x)).trans <| smul_zero _

Premises used: LinearMap.BilinForm.IsAlt, smul_zero, congr_arg, HSMul.hSMul, LinearMap.IsAlt, Eq.trans
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsAlt.{u_1, u_2} (R := R) (M := M) 0

Tactic:
fun _ => rfl

Premises used: LinearMap.BilinForm.IsAlt, LinearMap.IsAlt, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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).IsAlt ↔ B.IsAlt

Tactic:
⟨fun h => neg_neg B ▸ h.neg, IsAlt.neg⟩

Premises used: Eq.rec, neg_neg, LinearMap.BilinForm.IsAlt.neg, Iff.intro
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
⊢ ¬Nondegenerate.{u_1, u_2} (R := R) (M := M) 0

Tactic:
let ⟨m, hm⟩ := exists_ne (0 : M)
  fun h => hm (h.1 m fun _ => rfl)

Premises used: exists_ne, _private.0.LinearMap.BilinForm.not_nondegenerate_zero.match_1, And.left, LinearMap.BilinForm.Nondegenerate, OfNat.ofNat, Not, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial M
B : BilinForm R M
h : B.Nondegenerate
⊢ B ≠ 0

Tactic:
fun h0 => not_nondegenerate_zero R M <| h0 ▸ h

Premises used: LinearMap.BilinForm.not_nondegenerate_zero, Eq.rec, Not
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : B.Nondegenerate
⊢ Nondegenerate.{u_1, u_8} (R := R) (M := M') ((BilinForm.congr e : (a : BilinForm R M) → BilinForm R M') B)

Tactic:
⟨h.1.congr e e, show (BilinForm.congr e (flip B)).SeparatingLeft from .congr e e h.2⟩

Premises used: And.right, And.left, And.intro, LinearMap.Nondegenerate, LinearMap.SeparatingLeft.congr
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : Nondegenerate.{u_1, u_8} (R := R) (M := M') ((congr e : (a : BilinForm R M) → BilinForm R M') B)
⊢ Nondegenerate.{u_1, u_2} (R := R) (M := M)
    ((congr e.symm : (a : BilinForm R M') → BilinForm R M) ((congr e : (a : BilinForm R M) → BilinForm R M') B))

Tactic:
h.congr e.symm

Premises used: LinearEquiv.symm, LinearMap.BilinForm.Nondegenerate.congr
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : Nondegenerate.{u_1, u_8} (R := R) (M := M') ((congr e : (a : BilinForm R M) → BilinForm R M') B)
h₁ : B = (congr e.symm : (a : BilinForm R M') → BilinForm R M) ((congr e : (a : BilinForm R M) → BilinForm R M') B)
⊢ B.Nondegenerate

Tactic:
convert! h.congr e.symm

Premises used: LinearEquiv.symm, LinearMap.BilinForm.Nondegenerate.congr
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : Nondegenerate.{u_1, u_8} (R := R) (M := M') ((congr e : (a : BilinForm R M) → BilinForm R M') B)
h₁ : B = (congr (e ≪≫ₗ e.symm) : (a : BilinForm R M) → BilinForm R M) B
h₂ : B = (congr (LinearEquiv.refl R M) : (a : BilinForm R M) → BilinForm R M) B
h₃ : B = (LinearEquiv.refl R (BilinForm R M) : (a : BilinForm R M) → BilinForm R M) B
h₄ h₅ : B = B
⊢ B = (congr e.symm : (a : BilinForm R M') → BilinForm R M) ((congr e : (a : BilinForm R M) → BilinForm R M') B)

Tactic:
rw [congr_congr, e.self_trans_symm, congr_refl, LinearEquiv.refl_apply]

Premises used: LinearMap.BilinForm.congr_refl, LinearMap.BilinForm.congr_congr, LinearEquiv.refl_apply, LinearEquiv.self_trans_symm
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
h : B.Nondegenerate
⊢ ker B = ⊥

Tactic:
LinearMap.separatingLeft_iff_ker_eq_bot.mp h.1

Premises used: And.left, Iff.mp, LinearMap.separatingLeft_iff_ker_eq_bot
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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 ψ
h₁ : ∀ (w : M₁), Eq (α := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)
⊢ φ = ψ

Tactic:
ext w
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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 : M₁
⊢ Eq (α := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)

Tactic:
eq_of_sub_eq_zero (b.1 _ ?_)

Premises used: eq_of_sub_eq_zero, And.left
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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 : M₁
h₁ :
  ∀ (y : M₁),
    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₁)
          y :
        R₁)
      (0 : R₁)
⊢ Eq (α := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)

Tactic:
refine eq_of_sub_eq_zero (b.1 _ ?_)

Premises used: eq_of_sub_eq_zero, And.left
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
h₅ h₆ : Eq.{u_3 + 1} (α := R₁) 0 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₁)

Tactic:
rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self]

Premises used: sub_self, LinearMap.BilinForm.sub_left, LinearMap.BilinForm.compLeft_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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₁)
rw₃ 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₁)
⊢ 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₁)

Tactic:
rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂]

Premises used: LinearMap.BilinForm.compLeft_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
hB : B.Nondegenerate
⊢ B.flip.Nondegenerate

Tactic:
⟨hB.2, hB.1⟩

Premises used: And.right, And.left, And.intro, LinearMap.Nondegenerate
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
⊢ B.flip.Nondegenerate ↔ B.Nondegenerate

Tactic:
⟨Nondegenerate.flip, Nondegenerate.flip⟩

Premises used: LinearMap.BilinForm.Nondegenerate.flip, Iff.intro
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
b : B.Nondegenerate
m n : V
⊢ Eq.{u_6 + 1} (α := K) ((((B.toDual b : (a : V) → Dual K V) m : Dual K V) : (a : V) → K) n : K)
    ((((B : (a : V) → V →ₗ[K] K) m : V →ₗ[K] K) : (a : V) → K) n : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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)
⊢ 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)

Tactic:
change B.toDual hB ((B.toDual hB).symm f) v = f v

Premises used: LinearEquiv.symm, LinearMap.BilinForm.toDual, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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.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:
simp only [LinearEquiv.apply_symm_apply]

Premises used: LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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 : ι
⊢ FiniteDimensional K V

Tactic:
have := b.finiteDimensional_of_finite
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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)
rw₅ 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)
⊢ 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)

Tactic:
rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
    Basis.dualBasis_repr, toDual_def]

Premises used: Module.Basis.map_repr, LinearEquiv.trans_apply, LinearMap.BilinForm.toDual_def, LinearEquiv.symm_symm, Module.Basis.dualBasis_repr, LinearMap.BilinForm.dualBasis
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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 : ι
⊢ FiniteDimensional K V

Tactic:
have := b.finiteDimensional_of_finite
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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)
rw₇ rw₈ : Eq.{u_6 + 1} (α := K) (if j = i then 1 else 0) (if j = i then 1 else 0)
⊢ 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)

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]

Premises used: Module.Basis.coe_dualBasis, LinearMap.BilinForm.toDual_def, Module.Basis.map_apply, LinearEquiv.apply_symm_apply, Finsupp.single_apply, LinearMap.BilinForm.dualBasis, Module.Basis.coord_apply, Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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)
rw₁ rw₂ : Eq.{u_6 + 1} (α := K) (if i = j then 1 else 0) (if i = j then 1 else 0)
⊢ 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)

Tactic:
rw [sym.eq, apply_dualBasis_left]

Premises used: LinearMap.BilinForm.apply_dualBasis_left, LinearMap.BilinForm.IsSymm.eq
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
a :
  ∀ (i : ι),
    Eq.{u_5 + 1} (α := V) ((B.dualBasis hB (B.flip.dualBasis ⋯ b) : (a : ι) → V) i : V) ((b : (a : ι) → V) i : V)
⊢ B.dualBasis hB (B.flip.dualBasis ⋯ b) = b

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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)

Tactic:
LinearMap.ker_eq_bot.mp hB.ker_eq_bot ((B.flip.dualBasis hB.flip b).ext (fun j ↦ ?_))

Premises used: LinearMap.ker_eq_bot, LinearMap.BilinForm.Nondegenerate.flip, Iff.mp, LinearMap.BilinForm.Nondegenerate.ker_eq_bot, LinearMap.BilinForm.flip, LinearMap.BilinForm.dualBasis, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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 : ι
a :
  ∀ (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)
⊢ Eq.{u_5 + 1} (α := V) ((B.dualBasis hB (B.flip.dualBasis ⋯ b) : (a : ι) → V) i : V) ((b : (a : ι) → V) i : V)

Tactic:
refine LinearMap.ker_eq_bot.mp hB.ker_eq_bot ((B.flip.dualBasis hB.flip b).ext (fun j ↦ ?_))

Premises used: LinearMap.ker_eq_bot, LinearMap.BilinForm.Nondegenerate.flip, Iff.mp, LinearMap.BilinForm.Nondegenerate.ker_eq_bot, LinearMap.BilinForm.flip, LinearMap.BilinForm.dualBasis, Module.Basis.ext