awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.orthogonal W = ⊥
this : W ⊔ B.orthogonal W = ⊤
rwa : ∀ (this : W ⊔ ⊥ = ⊤), W = ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : W = ⊤), W = ⊤
⊢ W = ⊤

Tactic:
rwa [b₃, sup_bot_eq] at this

Premises used: sup_bot_eq
-- 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
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
⊢ B.orthogonal W = ⊥ ↔ W = ⊤

Tactic:
⟨eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot b₁ b₂, fun h ↦ ?_⟩

Premises used: Iff.intro, LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot
-- 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
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
refine : ∀ (h : W = ⊤), B.orthogonal W = ⊥
⊢ B.orthogonal W = ⊥ ↔ W = ⊤

Tactic:
refine ⟨eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot b₁ b₂, fun h ↦ ?_⟩
-- 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
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
rw : B.orthogonal ⊤ ≤ ⊥
⊢ B.orthogonal W = ⊥

Tactic:
rw [h, eq_bot_iff]

Premises used: eq_bot_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
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
x : V
hx : x ∈ B.orthogonal ⊤
y : V
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) y : V →ₗ[K] K) : (a : V) → K) x : K) (0 : K)

Tactic:
simpa using hx y
-- 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
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.Nondegenerate
h : W = ⊤
⊢ B.orthogonal ⊤ ≤ ⊥

Tactic:
exact fun x hx ↦ b₃.1 x fun y ↦ b₁ y x <| by simpa using hx y

Premises used: And.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
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
⊢ ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)

Tactic:
have (n : V) : n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x) :=
    (span_singleton_sup_orthogonal_eq_top hx).symm ▸ Submodule.mem_top
-- 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
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
⊢ Nondegenerate (M := ↥(B.orthogonal (K ∙ x))) (B.restrict (B.orthogonal (K ∙ x)))

Tactic:
⟨fun m hm => Submodule.coe_eq_zero.1 (b₁.1 m fun n ↦ ?_),
    fun m hm => Submodule.coe_eq_zero.1 (b₁.2 m fun n ↦ ?_)⟩

Premises used: And.right, And.left, And.intro, Iff.mp, Submodule.coe_eq_zero, Subtype.val, LinearMap.Nondegenerate
-- 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
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
refine_1 :
  ∀ (m : ↥(B.orthogonal (K ∙ x)))
    (hm :
      ∀ (y : ↥(B.orthogonal (K ∙ x))),
        Eq.{u_6 + 1} (α := K)
          ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
                  LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
                (a : ↥(B.orthogonal (K ∙ x))) → K)
              y :
            K)
          (0 : K))
    (n : V), Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) n : K) (0 : K)
refine_2 :
  ∀ (m : ↥(B.orthogonal (K ∙ x)))
    (hm :
      ∀ (x_1 : ↥(B.orthogonal (K ∙ x))),
        Eq.{u_6 + 1} (α := K)
          ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) x_1 :
                  LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
                (a : ↥(B.orthogonal (K ∙ x))) → K)
              m :
            K)
          (0 : K))
    (n : V), Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) n : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)
⊢ Nondegenerate (M := ↥(B.orthogonal (K ∙ x))) (B.restrict (B.orthogonal (K ∙ x)))

Tactic:
refine ⟨fun m hm => Submodule.coe_eq_zero.1 (b₁.1 m fun n ↦ ?_),
    fun m hm => Submodule.coe_eq_zero.1 (b₁.2 m fun n ↦ ?_)⟩
-- 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
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (y : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          y :
        K)
      (0 : K)
n : V
refine_1 :
  ∀ (y : V) (hy : Membership.mem (γ := Submodule K V) (K ∙ x) y) (z : V) (hz : z ∈ B.orthogonal (K ∙ x)),
    Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) (y + z) : K) (0 : K)
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) n : K) (0 : K)

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.1 <| this n

Premises used: Iff.mp, Submodule.mem_sup, rfl
-- 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
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (x_1 : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) x_1 :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          m :
        K)
      (0 : K)
n : V
refine_2 :
  ∀ (y : V) (hy : Membership.mem (γ := Submodule K V) (K ∙ x) y) (z : V) (hz : z ∈ B.orthogonal (K ∙ x)),
    Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (y + z) : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) n : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.1 <| this n

Premises used: Iff.mp, Submodule.mem_sup, rfl
-- 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
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (y : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          y :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
refine_1 :
  HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) y : K)
      ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) z : K) =
    0
refine_1₁ :
  HAdd.hAdd (α := K) (β := K) (0 : K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) z : K) = 0
refine_1₂ : HAdd.hAdd (α := K) 0 0 = 0
refine_1₃ refine_1₄ : Eq.{u_6 + 1} (α := K) 0 0
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) (y + z) : K) (0 : K)

Tactic:
rw [add_right, b₂ y m <| m.2 y hy, show B m z = 0 from hm ⟨z, hz⟩, add_zero]

Premises used: Subtype.mk, LinearMap.BilinForm.add_right, add_zero, Subtype.val, Subtype.property
-- 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
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (x_1 : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) x_1 :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          m :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
refine_2 :
  HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) y : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K)
      ((((B : (a : V) → V →ₗ[K] K) z : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) =
    0
refine_2₁ :
  HAdd.hAdd (α := K) (β := K) (0 : K) ((((B : (a : V) → V →ₗ[K] K) z : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) = 0
refine_2₂ : HAdd.hAdd (α := K) 0 0 = 0
refine_2₃ refine_2₄ : Eq.{u_6 + 1} (α := K) 0 0
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (y + z) : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)

Tactic:
rw [add_left, m.2 y hy, show B z m = 0 from hm ⟨z, hz⟩, add_zero]

Premises used: LinearMap.BilinForm.add_left, Subtype.mk, add_zero, Subtype.property
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
H : B.IsRefl
⊢ ∀ {x y : M},
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : 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:
fun {x y} => H x y
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
hB : B.IsRefl
⊢ (-B).IsRefl

Tactic:
fun x y =>
  neg_eq_zero.mpr ∘ hB x y ∘ neg_eq_zero.mp

Premises used: Iff.mpr, Function.comp, LinearMap.IsRefl, neg_eq_zero, Iff.mp, LinearMap.BilinForm.IsRefl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_8
inst_3 : Semiring α
inst_4 : IsDomain α
inst_5 : Module α R
inst_6 : SMulCommClass R α R
inst_7 : IsTorsionFree α R
a : α
B : BilinForm R M
hB : B.IsRefl
⊢ (a • B).IsRefl

Tactic:
fun _ _ h =>
  (smul_eq_zero.mp h).elim (fun ha => smul_eq_zero_of_left ha _) fun hBz =>
    smul_eq_zero_of_right _ (hB _ _ hBz)

Premises used: smul_eq_zero_of_left, LinearMap.IsRefl, Iff.mp, smul_eq_zero_of_right, LinearMap.BilinForm.IsRefl, Or.elim, DFunLike.coe, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_8
inst_3 : Group α
inst_4 : DistribMulAction α R
inst_5 : SMulCommClass R α R
a : α
B : BilinForm R M
hB : B.IsRefl
⊢ (a • B).IsRefl

Tactic:
fun x y =>
  (smul_eq_zero_iff_eq _).mpr ∘ hB x y ∘ (smul_eq_zero_iff_eq _).mp

Premises used: Iff.mpr, smul_eq_zero_iff_eq, Function.comp, LinearMap.IsRefl, Iff.mp, LinearMap.BilinForm.IsRefl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsRefl.{u_1, u_2} (R := R) (M := M) 0

Tactic:
fun _ _ _ => rfl

Premises used: LinearMap.IsRefl, LinearMap.BilinForm.IsRefl, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
⊢ (-B).IsRefl ↔ B.IsRefl

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

Premises used: Eq.rec, neg_neg, LinearMap.BilinForm.IsRefl.neg, Iff.intro
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
⊢ B.IsSymm ↔ LinearMap.IsSymm B

Tactic:
simp [isSymm_def, LinearMap.isSymm_def]

Premises used: LinearMap.isSymm_def, LinearMap.BilinForm.isSymm_def
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
H : B.IsSymm
⊢ B.IsRefl

Tactic:
fun x y H1 => H.eq x y ▸ H1

Premises used: LinearMap.BilinForm.IsSymm.eq, Eq.rec, LinearMap.IsRefl, LinearMap.BilinForm.IsRefl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B₁ B₂ : BilinForm R M
hB₁ : B₁.IsSymm
hB₂ : B₂.IsSymm
⊢ (B₁ + B₂).IsSymm

Tactic:
⟨fun x y => (congr_arg₂ (· + ·) (hB₁.eq x y) (hB₂.eq x y) :)⟩

Premises used: LinearMap.BilinForm.IsSymm.eq, LinearMap.BilinForm.IsSymm.mk, HAdd.hAdd, congr_arg₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B₁ B₂ : BilinForm R₁ M₁
hB₁ : B₁.IsSymm
hB₂ : B₂.IsSymm
⊢ (B₁ - B₂).IsSymm

Tactic:
⟨fun x y => (congr_arg₂ Sub.sub (hB₁.eq x y) (hB₂.eq x y) :)⟩

Premises used: LinearMap.BilinForm.IsSymm.eq, LinearMap.BilinForm.IsSymm.mk, Sub.sub, congr_arg₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
hB : B.IsSymm
⊢ (-B).IsSymm

Tactic:
⟨fun x y =>
  congr_arg Neg.neg (hB.eq x y)⟩

Premises used: LinearMap.BilinForm.IsSymm.eq, LinearMap.BilinForm.IsSymm.mk, congr_arg, Neg.neg
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_8
inst_3 : Monoid α
inst_4 : DistribMulAction α R
inst_5 : SMulCommClass R α R
a : α
B : BilinForm R M
hB : B.IsSymm
⊢ (a • B).IsSymm

Tactic:
⟨fun x y =>
  congr_arg (a • ·) (hB.eq x y)⟩

Premises used: LinearMap.BilinForm.IsSymm.eq, LinearMap.BilinForm.IsSymm.mk, congr_arg, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
b : B.IsSymm
W : Submodule R M
⊢ (B.restrict W).IsSymm

Tactic:
⟨fun x y => b.eq x y⟩

Premises used: LinearMap.BilinForm.IsSymm.eq, LinearMap.BilinForm.IsSymm.mk, Subtype.val
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsSymm.{u_1, u_2} (R := R) (M := M) 0

Tactic:
⟨fun _ _ => rfl⟩

Premises used: LinearMap.BilinForm.IsSymm.mk, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
⊢ (-B).IsSymm ↔ B.IsSymm

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

Premises used: Eq.rec, neg_neg, LinearMap.BilinForm.IsSymm.neg, Iff.intro
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
h_1 : B.IsSymm
h :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
H :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R)
      ((((((flipHom : (a : BilinForm R M) → BilinForm R M) B : BilinForm R M) : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) :
            (a : M) → R)
          y :
        R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ (flipHom : (a : BilinForm R M) → BilinForm R M) B = B

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
h_1 : B.IsSymm
h :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
⊢ Eq.{u_1 + 1} (α := R)
    ((((((flipHom : (a : BilinForm R M) → BilinForm R M) B : BilinForm R M) : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) :
          (a : M) → R)
        y :
      R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
h : (flipHom : (a : BilinForm R M) → BilinForm R M) B = B
x y : M
rw :
  Eq.{u_1 + 1} (α := R)
    ((((((flipHom : (a : BilinForm R M) → BilinForm R M) B : BilinForm R M) : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) :
          (a : M) → R)
        x :
      R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
rw [← flip_apply, h]

Premises used: LinearMap.BilinForm.flip_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
simp :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HSub.hSub (β := R)
        (HSub.hSub (β := R)
          (HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
              ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) +
            HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
              ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) /
      2
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HSub.hSub (β := R)
        (HSub.hSub (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (x + y) : M →ₗ[R] R) : (a : M) → R) (x + y) : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) /
      2

Tactic:
simp only [map_add, LinearMap.add_apply]

Premises used: LinearMap.add_apply, map_add
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
rw :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HSub.hSub (β := R)
        (HSub.hSub (β := R)
          (HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
              ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) +
            HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
              ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) /
      2
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HSub.hSub (β := R)
        (HSub.hSub (β := R)
          (HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
              ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) +
            HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
              ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) /
      2

Tactic:
rw [hB.eq y x]

Premises used: LinearMap.BilinForm.IsSymm.eq
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
ring_nf :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (2⁻¹ : R) * 2
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HSub.hSub (β := R)
        (HSub.hSub (β := R)
          (HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
              ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) +
            HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
              ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R))
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) /
      2

Tactic:
ring_nf
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
rw :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (HMul.hMul (α := R) 2⁻¹ 2)
rw₁ :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (1 : R)
rw₂ rw₃ :
  Eq.{u_8 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (2⁻¹ : R) * 2

Tactic:
rw [mul_assoc, inv_mul_cancel₀ two_ne_zero, mul_one]

Premises used: mul_assoc, two_ne_zero, mul_one, inv_mul_cancel₀
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B C : BilinForm R M
hB : B.IsSymm
hC : C.IsSymm
h :
  ∀ (x : M),
    Eq.{u_8 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((C : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
H :
  ∀ (x y : M),
    Eq.{u_8 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((C : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ B = C

Tactic:
ext x y