awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
rw :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      (((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
        (HSMul.hSMul.{u_20, u_21, u_21} (α := R) (β := M) ((vi : (a : n) → R) x : R) ((v : (a : n) → M) x : M)))
    0
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
        ((v.repr.symm : (a : n →₀ R) → M) vi : M) :
      M₁)
    (0 : M₁)

Tactic:
rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, map_sum]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, map_sum, Module.Basis.repr_symm_apply
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
h₁ :
  ∀ x ∈ vi.support,
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
          (HSMul.hSMul.{u_20, u_21, u_21} (α := R) (β := M) ((vi : (a : n) → R) x : R) ((v : (a : n) → M) x : M)) :
        M₁)
      (0 : M₁)
⊢ Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      (((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
        (HSMul.hSMul.{u_20, u_21, u_21} (α := R) (β := M) ((vi : (a : n) → R) x : R) ((v : (a : n) → M) x : M)))
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
j : n
h₁ :
  HSMul.hSMul (α := R) (β := M₁) ((I' : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
        M₁) =
    0
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
        (HSMul.hSMul.{u_20, u_21, u_21} (α := R) (β := M) ((vi : (a : n) → R) j : R) ((v : (a : n) → M) j : M)) :
      M₁)
    (0 : M₁)

Tactic:
rw [map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
j : n
this :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
      M₁)
    (0 : M₁)
rw : HSMul.hSMul (α := R) (β := M₁) ((I' : (a : R) → R) ((vi : (a : n) → R) j : R) : R) 0 = 0
rw₁ rw₂ : Eq.{u_22 + 1} (α := M₁) 0 0
⊢ HSMul.hSMul (α := R) (β := M₁) ((I' : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
        M₁) =
    0

Tactic:
rw [this, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
j : n
h₁ :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
      M₁)
    (0 : M₁)
⊢ HSMul.hSMul (α := R) (β := M₁) ((I' : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
        M₁) =
    0

Tactic:
suffices B (v i) (v j) = 0 by rw [this, smul_zero]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
j : n
h₁ :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
      M₁)
    (0 : M₁)
h₂ :
  ∀ (hij : i ≠ j),
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
        M₁)
      (0 : M₁)
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
      M₁)
    (0 : M₁)

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
      M₁)
    (0 : M₁)

Tactic:
ho

Premises used: LinearMap.IsOrtho
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
      M₁)
    (0 : M₁)

Tactic:
exact ho
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
j : n
hij : i ≠ j
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
      M₁)
    (0 : M₁)

Tactic:
h hij

Premises used: LinearMap.IsOrtho
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
j : n
hij : i ≠ j
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
      M₁)
    (0 : M₁)

Tactic:
exact h hij
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingRight
i : n
rw :
  ∀ (h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)) (hB : B.SeparatingRight) (i : n),
    ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
⊢ ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
rw [isOrthoᵢ_flip] at h

Premises used: LinearMap.isOrthoᵢ_flip
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
hB : B.SeparatingRight
i : n
rw : ¬B.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
⊢ ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
rw [isOrtho_flip]

Premises used: LinearMap.isOrtho_flip
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
hB : B.SeparatingRight
i : n
⊢ ¬B.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
h.not_isOrtho_basis_self_of_separatingLeft (flip_separatingLeft.mpr hB) i

Premises used: Iff.mpr, LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft, LinearMap.flip_separatingLeft
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
hB : B.SeparatingRight
i : n
⊢ ¬B.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
exact h.not_isOrtho_basis_self_of_separatingLeft (flip_separatingLeft.mpr hB) i

Premises used: Iff.mpr, LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft, LinearMap.flip_separatingLeft
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
m : M
hB : ∀ (y : M), Eq.{u_22 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) m : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
obtain :
  ∀ (vi : n →₀ R)
    (hB :
      ∀ (y : M),
        Eq.{u_22 + 1} (α := M₁)
          ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁)
          (0 : M₁)),
    Eq.{u_21 + 1} (α := M) ((v.repr.symm : (a : n →₀ R) → M) vi : M) (0 : M)
⊢ m = 0

Tactic:
obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m

Premises used: LinearEquiv.symm, LinearEquiv.surjective, Module.Basis.repr, rfl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
hB :
  ∀ (y : M),
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
rw : vi = 0
⊢ Eq.{u_21 + 1} (α := M) ((v.repr.symm : (a : n →₀ R) → M) vi : M) (0 : M)

Tactic:
rw [LinearEquiv.map_eq_zero_iff]

Premises used: LinearEquiv.map_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
hB :
  ∀ (y : M),
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
h₁ : ∀ (i : n), Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) ((0 : (a : n) → R) i : R)
⊢ vi = 0

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
hB :
  ∀ (y : M),
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
i : n
h₁ : Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) ((0 : (a : n) → R) i : R)

Tactic:
rw [Finsupp.zero_apply]

Premises used: Finsupp.zero_apply
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
hB :
  ∀ (y : M),
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
i : n
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁)
        ((v : (a : n) → M) i : M) :
      M₁)
    (0 : M₁)

Tactic:
specialize hB (v i)

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁)
        ((v : (a : n) → M) i : M) :
      M₁)
    (0 : M₁)
⊢ Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0

Tactic:
simp_rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂,
           map_smulₛₗ₂] at hB

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, LinearMap.map_sum₂, Module.Basis.repr_symm_apply, LinearMap.map_smulₛₗ₂
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
h₁ :
  ∀
    (hB :
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
          ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
            M₁) =
        0),
    Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
h₂ :
  ∀ b ∈ vi.support,
    b ≠ i →
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) b : R) : R)
          ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) b) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
            M₁) =
        0
h₃ :
  i ∉ vi.support →
    HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁) =
      0
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)

Tactic:
rw [Finset.sum_eq_single i] at hB

Premises used: Finset.sum_eq_single
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)

Tactic:
(smul_eq_zero.mp hB).elim _root_.id (h i).elim

Premises used: id, Not.elim, Iff.mp, Or.elim, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)

Tactic:
exact (smul_eq_zero.mp hB).elim _root_.id (h i).elim

Premises used: id, Not.elim, Iff.mp, Or.elim, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
j : n
_hj : j ∈ vi.support
hij : j ≠ i
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) : M₁)
    (0 : M₁)

Tactic:
replace hij : B (v j) (v i) = 0 := hO hij
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
j : n
_hj : j ∈ vi.support
hij :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) : M₁)
    (0 : M₁)
h₁ : HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) j : R) : R) 0 = 0
h₂ : HSMul.hSMul.{u_20, u_22, u_22} (α := R) (β := M₁) ((vi : (a : n) → R) j : R) 0 = 0
h₃ h₄ : Eq.{u_22 + 1} (α := M₁) 0 0
⊢ HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0

Tactic:
rw [hij, RingHom.id_apply, smul_zero]

Premises used: RingHom.id_apply, smul_zero