awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
mp :
  (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) →
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)
mpr :
  (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) →
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)
⊢ (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) ↔
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) →
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)

Tactic:
fun h i j hij ↦ h j i hij.symm

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) →
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)

Tactic:
exact fun h i j hij ↦ h j i hij.symm
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) →
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)

Tactic:
fun h i j hij ↦ h j i hij.symm

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) →
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)

Tactic:
exact fun h i j hij ↦ h j i hij.symm
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
mp :
  Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V) →
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
mpr :
  Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V) →
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V) ↔
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
mp :
  HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) a : K)
      ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) =
    0
mp₁ : HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) a : K) 0 = 0
mp₂ mp₃ : Eq.{u_16 + 1} (α := V) 0 0
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)

Tactic:
rw [map_smulₛₗ₂, H, smul_zero]

Premises used: smul_zero, LinearMap.map_smulₛₗ₂
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K) ∨
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)

Tactic:
rw [map_smulₛₗ₂, smul_eq_zero] at H

Premises used: LinearMap.map_smulₛₗ₂, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H :
  Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K) ∨
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
mpr :
  ∀ (H : Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K)),
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
mpr₁ :
  ∀ (H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)),
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)

Tactic:
rcases H with H | H
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K)
⊢ a = 0

Tactic:
rw [map_eq_zero I₁] at H

Premises used: map_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : a = 0
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)

Tactic:
trivial
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)

Tactic:
H
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)

Tactic:
exact H
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₂
ha : a ≠ 0
⊢ B.IsOrtho x y ↔ B.IsOrtho x (a • y)

Tactic:
simp_all [IsOrtho]

Premises used: LinearMap.IsOrtho
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw : ∀ (s : Finset n) (g : n → K₁), Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
⊢ LinearIndependent K₁ v

Tactic:
rw [linearIndependent_iff']

Premises used: linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
rw : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) 0 : (a : V₁) → V) (v i) : V) (0 : V)
rw₁ : Eq.{u_16 + 1} (α := V) ((0 : (a : V₁) → V) (v i) : V) (0 : V)
rw₂ rw₃ : Eq.{u_16 + 1} (α := V) 0 0
⊢ Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)

Tactic:
rw [hs, map_zero, zero_apply]

Premises used: LinearMap.zero_apply, map_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
⊢ Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)

Tactic:
have : B (s.sum fun i : n ↦ w i • v i) (v i) = 0 := by rw [hs, map_zero, zero_apply]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
apply :
  ∀ b ∈ s,
    b ≠ i →
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w b) : K)
          ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v b) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
        0
⊢ ∑ j ∈ s,
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)

Tactic:
apply Finset.sum_eq_single_of_mem i hi

Premises used: Finset.sum_eq_single_of_mem
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
j : n
_hj : j ∈ s
hij : j ≠ i
rw : HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K) 0 = 0
rw₁ rw₂ : Eq.{u_16 + 1} (α := V) 0 0
⊢ HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    0

Tactic:
rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]

Premises used: smul_zero, LinearMap.isOrthoᵢ_def, Iff.mp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
⊢ ∑ j ∈ s,
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)

Tactic:
have hsum : (s.sum fun j : n ↦ I₁ (w j) • B (v j) (v i)) = I₁ (w i) • B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _hj hij
      rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
hsum :
  ∑ j ∈ s,
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)
⊢ HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    0

Tactic:
simp_rw [B.map_sum₂, map_smulₛₗ₂, hsum] at this

Premises used: LinearMap.map_sum₂, LinearMap.map_smulₛₗ₂
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
hsum :
  ∑ j ∈ s,
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)
this :
  HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    0
apply : Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) (w i) : K) (0 : K)
⊢ w i = 0

Tactic:
apply (map_eq_zero I₁).mp

Premises used: map_eq_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
hsum :
  ∑ j ∈ s,
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)
this :
  HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    0
⊢ Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) (w i) : K) (0 : K)

Tactic:
(smul_eq_zero.mp this).elim _root_.id (hv₂ i · |>.elim)

Premises used: False.elim, id, Iff.mp, Or.elim, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
hsum :
  ∑ j ∈ s,
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)
this :
  HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    0
⊢ Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) (w i) : K) (0 : K)

Tactic:
exact (smul_eq_zero.mp this).elim _root_.id (hv₂ i · |>.elim)

Premises used: False.elim, id, Iff.mp, Or.elim, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ ∀ {x y : M₁},
    Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M) →
      Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) y : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) x : M) (0 : M)

Tactic:
fun {x y} ↦ H x y
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
x y : M₁
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M) ↔
    Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) y : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) x : M) (0 : M)

Tactic:
⟨H x y, H y x⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
x y : M₁
⊢ B.IsOrtho x y ↔ B.IsOrtho y x

Tactic:
⟨eq_zero H, eq_zero H⟩

Premises used: LinearMap.IsRefl.eq_zero, Iff.intro