awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
n m : M₂
⊢ (f : (a : M₁) → M₂) ((↑f.symm : M₂ →ₗ[R] M₁).toFun n) = n

Tactic:
repeat exact f.toLinearEquiv.apply_symm_apply _

Premises used: LinearMap.BilinForm.IsometryEquiv.toLinearEquiv, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
n m : M₁
rw :
  Eq.{u_1 + 1} (α := R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun n) : M₃ →ₗ[R] R) :
          (a : M₃) → R)
        ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) :
      R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) n : M₂)) : M₃ →ₗ[R] R) : (a : M₃) → R)
        ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) m : M₂) : M₃) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun n) : M₃ →ₗ[R] R) :
          (a : M₃) → R)
        ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) :
      R)
    ((((B₁ : (a : M₁) → M₁ →ₗ[R] R) n : M₁ →ₗ[R] R) : (a : M₁) → R) m : R)

Tactic:
rw [← f.map_app, ← g.map_app]

Premises used: LinearMap.BilinForm.IsometryEquiv.map_app
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
n m : M₁
⊢ Eq.{u_1 + 1} (α := R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun n) : M₃ →ₗ[R] R) :
          (a : M₃) → R)
        ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv) : M₁ →ₗ[R] M₃).toFun m) :
      R)
    ((((B₃ : (a : M₃) → M₃ →ₗ[R] R) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) n : M₂)) : M₃ →ₗ[R] R) : (a : M₃) → R)
        ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) m : M₂) : M₃) :
      R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Q : LinearMap.BilinForm R M
⊢ Q.Equivalent Q

Tactic:
⟨IsometryEquiv.refl Q⟩

Premises used: LinearMap.BilinForm.IsometryEquiv.refl, LinearMap.BilinForm.Equivalent, Nonempty.intro
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
h : B₁.Equivalent B₂
⊢ B₂.Equivalent B₁

Tactic:
h.elim fun f => ⟨f.symm⟩

Premises used: Nonempty.elim, Nonempty.intro, LinearMap.BilinForm.IsometryEquiv.symm
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
h : B₁.Equivalent B₂
h' : B₂.Equivalent B₃
⊢ B₁.Equivalent B₃

Tactic:
h'.elim <| h.elim fun f g => ⟨f.trans g⟩

Premises used: Nonempty.elim, LinearMap.BilinForm.IsometryEquiv.trans, Nonempty.intro
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
B : LinearMap.BilinForm R M
f : M₁ ≃ₗ[R] M
n : M
_ :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := R)
      ((((B.comp (↑f : M₁ →ₗ[R] M) (↑f : M₁ →ₗ[R] M) : (a : M₁) → M₁ →ₗ[R] R) ((↑f.symm : M →ₗ[R] M₁).toFun n) :
              M₁ →ₗ[R] R) :
            (a : M₁) → R)
          ((↑f.symm : M →ₗ[R] M₁).toFun m) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) m : R)
⊢ ∀ (m : M),
    Eq.{u_1 + 1} (α := R)
      ((((B.comp (↑f : M₁ →ₗ[R] M) (↑f : M₁ →ₗ[R] M) : (a : M₁) → M₁ →ₗ[R] R) ((↑f.symm : M →ₗ[R] M₁).toFun n) :
              M₁ →ₗ[R] R) :
            (a : M₁) → R)
          ((↑f.symm : M →ₗ[R] M₁).toFun m) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) m : R)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
B : LinearMap.BilinForm R M
f : M₁ ≃ₗ[R] M
n m : M
⊢ Eq.{u_1 + 1} (α := R)
    ((((B.comp (↑f : M₁ →ₗ[R] M) (↑f : M₁ →ₗ[R] M) : (a : M₁) → M₁ →ₗ[R] R) ((↑f.symm : M →ₗ[R] M₁).toFun n) :
            M₁ →ₗ[R] R) :
          (a : M₁) → R)
        ((↑f.symm : M →ₗ[R] M₁).toFun m) :
      R)
    ((((B : (a : M) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) m : R)

Tactic:
simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe,
        f.apply_symm_apply]

Premises used: LinearEquiv.apply_symm_apply, LinearEquiv.toFun_eq_coe, LinearMap.BilinForm.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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
x y : M
⊢ B.IsOrtho x y ↔ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearMap.BilinForm.IsOrtho
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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
x : M
⊢ B.IsOrtho 0 x

Tactic:
LinearMap.isOrtho_zero_left B x

Premises used: LinearMap.BilinForm.IsOrtho, LinearMap.isOrtho_zero_left
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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
x : M
⊢ B.IsOrtho x 0

Tactic:
zero_right x

Premises used: LinearMap.BilinForm.zero_right, LinearMap.BilinForm.IsOrtho
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
x : V
hx₁ : ¬B.IsOrtho x x
⊢ x ≠ 0

Tactic:
fun hx₂ => hx₁ (hx₂.symm ▸ isOrtho_zero_left _)

Premises used: Eq.rec, LinearMap.BilinForm.isOrtho_zero_left, OfNat.ofNat, Eq.symm, Not
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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.IsRefl
x y : M
⊢ B.IsOrtho x y ↔ B.IsOrtho y x

Tactic:
⟨eq_zero H, eq_zero H⟩

Premises used: Iff.intro, LinearMap.BilinForm.IsRefl.eq_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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₁
⊢ B₁.IsOrtho x y ↔ B₁.IsOrtho y x

Tactic:
LinearMap.IsAlt.ortho_comm H

Premises used: LinearMap.BilinForm.IsOrtho, LinearMap.IsAlt.ortho_comm
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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.IsSymm
x y : M
⊢ B.IsOrtho x y ↔ B.IsOrtho y x

Tactic:
LinearMap.IsSymm.ortho_comm (isSymm_iff.1 H)

Premises used: LinearMap.IsSymm.ortho_comm, LinearMap.BilinForm.isSymm_iff, LinearMap.BilinForm.IsOrtho, Iff.mp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : Type w
B : BilinForm R M
v : n → M
⊢ B.iIsOrtho v ↔
    ∀ (i j : n),
      i ≠ j → Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearMap.IsOrtho, Pairwise, LinearMap.IsOrthoᵢ, LinearMap.BilinForm.iIsOrtho
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
rw :
  Eq.{u_7 + 1} (α := R₄)
      ((HSMul.hSMul (β := M₄ →ₗ[R₄] R₄) a ((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄)
      (0 : R₄) ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
⊢ Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) (a • x) : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄) ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)

Tactic:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
simp :
  a = 0 → Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
⊢ Eq.{u_7 + 1} (α := R₄)
      ((HSMul.hSMul (β := M₄ →ₗ[R₄] R₄) a ((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄)
      (0 : R₄) ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)

Tactic:
simp only [LinearMap.smul_apply, smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]

Premises used: LinearMap.smul_apply, mul_eq_zero, or_iff_right_iff_imp, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ a = 0 → Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)

Tactic:
fun a ↦ (ha a).elim

Premises used: False.elim
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ a = 0 → Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)

Tactic:
exact fun a ↦ (ha a).elim

Premises used: False.elim
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
rw :
  HSMul.hSMul (β := R₄) a ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) = 0 ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
⊢ Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) (a • y) : R₄) (0 : R₄) ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)

Tactic:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R₄ : Type u_7
M₄ : Type u_8
inst : CommRing R₄
inst_1 : IsDomain R₄
inst_2 : AddCommGroup M₄
inst_3 : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
simp :
  a = 0 → Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)
⊢ HSMul.hSMul (β := R₄) a ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) = 0 ↔
    Eq.{u_7 + 1} (α := R₄) ((((G : (a : M₄) → M₄ →ₗ[R₄] R₄) x : M₄ →ₗ[R₄] R₄) : (a : M₄) → R₄) y : R₄) (0 : R₄)

Tactic:
simp only [smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]

Premises used: mul_eq_zero, or_iff_right_iff_imp, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw : ∀ (s : Finset n) (g : n → K), Eq.{u_5 + 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.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
rw : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) 0 : (a : V) → K) (v i) : K) (0 : K)
rw₁ rw₂ : Eq.{u_6 + 1} (α := K) 0 0
⊢ Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)

Tactic:
rw [hs, zero_left]

Premises used: LinearMap.BilinForm.zero_left
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
⊢ Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)

Tactic:
have : B (s.sum fun i : n => w i • v i) (v i) = 0 := by rw [hs, zero_left]
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
apply :
  ∀ b ∈ s,
    b ≠ i → HMul.hMul (β := K) (w b) ((((B : (a : V) → V →ₗ[K] K) (v b) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0
⊢ ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
    HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)

Tactic:
apply Finset.sum_eq_single_of_mem i hi

Premises used: Finset.sum_eq_single_of_mem
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
j : n
_ :
  j ∈ s → j ≠ i → HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0
⊢ j ∈ s → j ≠ i → HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0

Tactic:
_
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
j : n
h : j ∈ s
hij : j ≠ i
rw : w j * 0 = 0
rw₁ rw₂ : Eq.{u_6 + 1} (α := K) 0 0
⊢ HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0

Tactic:
rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]

Premises used: MulZeroClass.mul_zero, Iff.mp, LinearMap.BilinForm.iIsOrtho_def
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
⊢ ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
    HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)

Tactic:
have hsum : (s.sum fun j : n => w j * B (v j) (v i)) = w i * B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _ hij
      rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
hsum :
  ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
    HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)
⊢ HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0

Tactic:
simp_rw [sum_left, smul_left, hsum] at this

Premises used: LinearMap.BilinForm.sum_left, LinearMap.BilinForm.smul_left
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
hsum :
  ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
    HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)
this : HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0
⊢ w i = 0

Tactic:
eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this

Premises used: eq_zero_of_ne_zero_of_mul_right_eq_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
hsum :
  ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
    HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)
this : HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0
⊢ w i = 0

Tactic:
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this

Premises used: eq_zero_of_ne_zero_of_mul_right_eq_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw rw₁ rw₂ rw₃ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s), w i = 0
rw₄ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)),
    w i = 0
rw₅ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K))
    (hsum :
      ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
        HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)),
    w i = 0
rw₆ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (hsum :
      ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
        HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K))
    (this : HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0),
    w i = 0
⊢ LinearIndependent K v

Tactic:
classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n => w i • v i) (v i) = 0 := by rw [hs, zero_left]
    have hsum : (s.sum fun j : n => w j * B (v j) (v i)) = w i * B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _ hij
      rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
    simp_rw [sum_left, smul_left, hsum] at this
    exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this

Premises used: LinearMap.BilinForm.sum_left, linearIndependent_iff', LinearMap.BilinForm.smul_left
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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
N : Submodule R M
m : M
⊢ m ∈ B.orthogonal N ↔ ∀ n ∈ N, B.IsOrtho n m

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, LinearMap.BilinForm.IsOrtho
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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 : ∀ (x : M), x ∈ B.orthogonal ⊥ ↔ Membership.mem (γ := Submodule R M) ⊤ x
⊢ B.orthogonal ⊥ = ⊤

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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
x : M
⊢ x ∈ B.orthogonal ⊥ ↔ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
simp [IsOrtho]

Premises used: LinearMap.BilinForm.IsOrtho
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
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
N L : Submodule R M
h : N ≤ L
⊢ B.orthogonal L ≤ B.orthogonal N

Tactic:
fun _ hn l hl => hn l (h hl)

Premises used: Set.Mem, setOf