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
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
p : Submodule R₁ M₁
x x_1 : ↥p
simp_rw :
  Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (↑x : M₁) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (↑x_1 : M₁) : M)
      (0 : M) →
    Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (↑x_1 : M₁) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (↑x : M₁) : M)
      (0 : M)
⊢ Eq.{u_5 + 1} (α := M)
      ((((B.domRestrict₁₂ p p : (a : ↥p) → ↥p →ₛₗ[I₂] M) x : LinearMap.{u_2, u_1, u_6, u_5} I₂ (↥p) M) : (a : ↥p) → M)
          x_1 :
        M)
      (0 : M) →
    Eq.{u_5 + 1} (α := M)
      ((((B.domRestrict₁₂ p p : (a : ↥p) → ↥p →ₛₗ[I₂] M) x_1 : LinearMap.{u_2, u_1, u_6, u_5} I₂ (↥p) M) : (a : ↥p) → M)
          x :
        M)
      (0 : M)

Tactic:
simp_rw [domRestrict₁₂_apply]

Premises used: LinearMap.domRestrict₁₂_apply
-- 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
p : Submodule R₁ M₁
x x_1 : ↥p
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (↑x : M₁) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (↑x_1 : M₁) : M)
      (0 : M) →
    Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (↑x_1 : M₁) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (↑x : M₁) : M)
      (0 : M)

Tactic:
H _ _
-- 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
p : Submodule R₁ M₁
x x_1 : ↥p
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (↑x : M₁) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (↑x_1 : M₁) : M)
      (0 : M) →
    Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (↑x_1 : M₁) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (↑x : M₁) : M)
      (0 : M)

Tactic:
exact H _ _
-- 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
⊢ B.flip.IsRefl ↔ B.IsRefl

Tactic:
forall_comm

Premises used: forall_comm, LinearMap.IsRefl
-- 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
h : ∀ (x : M₁), x ∈ B.flip.ker ↔ x ∈ B.ker
⊢ B.flip.ker = B.ker

Tactic:
ext x
-- 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 : M₁
⊢ x ∈ B.flip.ker ↔ x ∈ B.ker

Tactic:
simp [LinearMap.ext_iff, H.eq_iff]

Premises used: LinearMap.ext_iff, LinearMap.IsRefl.eq_iff
-- 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
h rwa rwa₁ rwa₂ rwa₃ : B.ker = ⊥
⊢ B.flip.ker = ⊥

Tactic:
rwa [H.ker_flip]

Premises used: LinearMap.IsRefl.ker_flip
-- 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
rwa : B.ker = ⊥ ↔ B.ker = ⊥
rwa₁ : B.IsRefl
rwa₂ : B.ker = ⊥ ↔ B.ker = ⊥
rwa₃ rwa₄ rwa₅ : B.IsRefl
⊢ B.ker = ⊥ ↔ B.flip.ker = ⊥

Tactic:
rwa [ker_flip]

Premises used: LinearMap.IsRefl.ker_flip
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
⊢ B.IsSymm ↔
    ∀ (x y : M),
      Eq (α := R) ((I : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: LinearMap.IsSymm.mk, Iff.intro, _private.0.LinearMap.isSymm_def.match_1
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
H1 : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
rw : Eq (α := R) ((I : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)

Tactic:
rw [← H.eq]

Premises used: LinearMap.IsSymm.eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
H1 : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ Eq (α := R) ((I : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R) (0 : R)

Tactic:
simp [H1]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
⊢ B.IsOrtho x y ↔ B.IsOrtho y x

Tactic:
H.isRefl.ortho_comm

Premises used: LinearMap.IsRefl.ortho_comm, LinearMap.IsSymm.isRefl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
p : Submodule R M
x x_1 : ↥p
simp_rw :
  Eq (α := R) ((I : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x_1 : M) : R) : R)
    ((((B : (a : M) → M →ₗ[R] R) (↑x_1 : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
⊢ Eq (α := R)
    ((I : (a : R) → R)
        ((((B.domRestrict₁₂ p p : (a : ↥p) → ↥p →ₗ[R] R) x : LinearMap.{u_1, u_1, u_5, u_1} (RingHom.id R) (↥p) R) :
              (a : ↥p) → R)
            x_1 :
          R) :
      R)
    ((((B.domRestrict₁₂ p p : (a : ↥p) → ↥p →ₗ[R] R) x_1 : LinearMap.{u_1, u_1, u_5, u_1} (RingHom.id R) (↥p) R) :
          (a : ↥p) → R)
        x :
      R)

Tactic:
simp_rw [domRestrict₁₂_apply]

Premises used: LinearMap.domRestrict₁₂_apply
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
p : Submodule R M
x x_1 : ↥p
⊢ Eq (α := R) ((I : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x_1 : M) : R) : R)
    ((((B : (a : M) → M →ₗ[R] R) (↑x_1 : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)

Tactic:
H.eq _ _

Premises used: LinearMap.IsSymm.eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
p : Submodule R M
x x_1 : ↥p
⊢ Eq (α := R) ((I : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x_1 : M) : R) : R)
    ((((B : (a : M) → M →ₗ[R] R) (↑x_1 : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)

Tactic:
exact H.eq _ _

Premises used: LinearMap.IsSymm.eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
⊢ IsSymm.{u_1, u_5} (R := R) (M := M) (I := I) 0

Tactic:
⟨fun _ _ => map_zero _⟩

Premises used: map_zero, LinearMap.IsSymm.mk
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B C : M →ₛₗ[I] M →ₗ[R] R
hB : B.IsSymm
hC : C.IsSymm
x y : M
⊢ Eq (α := R) ((I : (a : R) → R) ((((B + C : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
    ((((B + C : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
simp [hB.eq, hC.eq]

Premises used: LinearMap.IsSymm.eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_20
inst_3 : AddCommMonoid N
inst_4 : Module R N
B : LinearMap.BilinMap R M N
⊢ (∀ (x y : M),
      Eq.{u_20 + 1} (α := N) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
        ((((B : (a : M) → M →ₗ[R] N) y : M →ₗ[R] N) : (a : M) → N) x : N)) ↔
    B = flip B

Tactic:
simp [LinearMap.ext_iff₂]

Premises used: LinearMap.ext_iff₂
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : LinearMap.BilinForm R M
⊢ IsSymm B ↔ B = flip B

Tactic:
isSymm_def.trans BilinMap.isSymm_iff_eq_flip

Premises used: LinearMap.isSymm_def, LinearMap.BilinMap.isSymm_iff_eq_flip, Iff.trans
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I₁ I₂ : R →+* R
inst_3 : LE R
B : M →ₛₗ[I₁] M →ₛₗ[I₂] R
⊢ B.IsNonneg ↔
    ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₛₗ[I₂] R) x : M →ₛₗ[I₂] R) : (a : M) → R) x : R)

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: LinearMap.IsNonneg.mk, Iff.intro, _private.0.LinearMap.isNonneg_def.match_1
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I₁ I₂ : R →+* R
inst_3 : Preorder R
⊢ IsNonneg.{u_1, u_5} (R := R) (M := M) (I₁ := I₁) (I₂ := I₂) 0

Tactic:
⟨fun _ ↦ le_rfl⟩

Premises used: le_rfl, LinearMap.IsNonneg.mk
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I₁ : R →+* R
inst_3 : LE R
B : M →ₛₗ[I₁] M →ₗ[R] R
⊢ B.IsPosSemidef ↔ B.IsSymm ∧ B.IsNonneg

Tactic:
⟨fun h ↦ ⟨h.isSymm, h.isNonneg⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩⟩

Premises used: LinearMap.IsPosSemidef.isNonneg, LinearMap.IsPosSemidef, _private.0.LinearMap.isPosSemidef_def.match_1, And.intro, LinearMap.IsPosSemidef.mk, LinearMap.IsPosSemidef.isSymm, Iff.intro
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I₁ : R →+* R
inst_3 : Preorder R
inst_4 : AddLeftMono R
B C : M →ₛₗ[I₁] M →ₗ[R] R
hB : B.IsPosSemidef
hC : C.IsPosSemidef
⊢ (B + C).IsPosSemidef

Tactic:
isPosSemidef_def.2 ⟨hB.isSymm.add hC.isSymm, hB.isNonneg.add hC.isNonneg⟩

Premises used: Iff.mpr, LinearMap.isPosSemidef_def, LinearMap.IsPosSemidef.isNonneg, LinearMap.IsNonneg.add, And.intro, LinearMap.IsPosSemidef.isSymm, LinearMap.IsSymm.add
-- 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.IsAlt
x : M₁
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) x : M) (0 : M)

Tactic:
H x
-- 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.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
simp_rw :
  (((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (a + b + c) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
simp_rw₁ :
  Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (a + b + c) : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (a + b + c) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
simp_rw₂ :
  Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) 0 : M)
    (((B : (a : M₁) → M₁ →ₛₗ[I₂] M) 0 : (a : M₁) → M) c : M)
simp_rw₃ : Eq.{u_5 + 1} (α := M) (0 : M) ((0 : (a : M₁) → M) c : M)
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) a : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)

Tactic:
simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, map_zero, map_add, LinearMap.map_add₂
-- 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.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) a : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)

Tactic:
have : B a a + B a b + B a c = B a c + B b c + B c c := by
    simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]
-- 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.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this :
  HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) a : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
⊢ HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M) =
    HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)

Tactic:
rw [H, H, zero_add, add_zero, add_comm] at this

Premises used: zero_add, add_comm, add_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.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this :
  HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M) =
    HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)

Tactic:
add_left_cancel this

Premises used: add_left_cancel
-- 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.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this :
  HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M) =
    HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)

Tactic:
exact add_left_cancel this

Premises used: add_left_cancel
-- 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 : AddCommGroup 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.IsAlt
x y : M₁
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (y + x) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (y + x) : M) (0 : M)

Tactic:
have H1 : B (y + x) (y + x) = 0 := self_eq_zero H (y + x)
-- 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 : AddCommGroup 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.IsAlt
x y : M₁
H1 : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (y + x) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (y + x) : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) (-(((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) y : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) x : M)

Tactic:
simpa [map_add, self_eq_zero H, add_eq_zero_iff_neg_eq] using H1

Premises used: map_add, add_eq_zero_iff_neg_eq, LinearMap.IsAlt.self_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 : AddCommGroup 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.IsAlt
x y : M₁
h : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M)
rw : Eq.{u_5 + 1} (α := M) (-(((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M)
rw₁ : Eq.{u_5 + 1} (α := M) (-0) 0
rw₂ rw₃ : Eq.{u_5 + 1} (α := M) 0 0
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) y : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) x : M) (0 : M)

Tactic:
rw [← neg H, h, neg_zero]

Premises used: neg_zero, LinearMap.IsAlt.neg
-- 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 : AddCommGroup 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.IsAlt
x y : M₁
⊢ B.IsOrtho x y ↔ B.IsOrtho y x

Tactic:
H.isRefl.ortho_comm

Premises used: LinearMap.IsRefl.ortho_comm, LinearMap.IsAlt.isRefl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst : CommRing R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
I : R₁ →+* R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
mp : B.IsAlt → B = -B.flip
mpr : B = -B.flip → B.IsAlt
⊢ B.IsAlt ↔ B = -B.flip

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst : CommRing R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
I : R₁ →+* R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B.IsAlt
mp :
  ∀ (x x_1 : M₁),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
      ((((-B.flip : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
⊢ B = -B.flip

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst : CommRing R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
I : R₁ →+* R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B.IsAlt
x x_1 : M₁
mp :
  Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
    (-(((B : (a : M₁) → M₁ →ₛₗ[I] R) x_1 : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
    ((((-B.flip : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)

Tactic:
simp_rw [neg_apply, flip_apply]

Premises used: LinearMap.neg_apply, LinearMap.flip_apply
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst : CommRing R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
I : R₁ →+* R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B.IsAlt
x x_1 : M₁
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
    (-(((B : (a : M₁) → M₁ →ₛₗ[I] R) x_1 : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R)

Tactic:
(h.neg _ _).symm

Premises used: Eq.symm, LinearMap.IsAlt.neg
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst : CommRing R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
I : R₁ →+* R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B.IsAlt
x x_1 : M₁
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
    (-(((B : (a : M₁) → M₁ →ₛₗ[I] R) x_1 : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R)

Tactic:
exact (h.neg _ _).symm

Premises used: Eq.symm, LinearMap.IsAlt.neg