awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
refine : ∀ (x : M) (hx : x ∈ W) (hx' : x ∈ B.ker), x = 0
⊢ Disjoint W B.ker

Tactic:
refine Submodule.disjoint_def.mpr fun x hx hx' ↦ ?_

Premises used: Iff.mpr, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
this : x' = 0
⊢ x = 0

Tactic:
simpa [x']
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
suffices : x' = 0
⊢ x = 0

Tactic:
suffices x' = 0 by simpa [x']
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
apply :
  ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) x' : LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)
⊢ x' = 0

Tactic:
apply hW.1 x'

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
simp_rw :
  ∀ (a : M) (b : a ∈ W),
    Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) (↑x' : M) : M →ₗ[R] M₁) : (a : M) → M₁) a : M₁) (0 : M₁)
⊢ ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) x' : LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)

Tactic:
simp_rw [Subtype.forall, domRestrict₁₂_apply]

Premises used: Subtype.forall, LinearMap.domRestrict₁₂_apply
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
y : M
hy : y ∈ W
rw :
  ∀ (hx' : Eq (α := M →ₗ[R] M₁) ((B : (a : M) → M →ₗ[R] M₁) x : M →ₗ[R] M₁) (0 : M →ₗ[R] M₁)),
    let x' := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx;
    ∀ (y : M) (hy : y ∈ W),
      Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) (↑x' : M) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
⊢ Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) (↑x' : M) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)

Tactic:
rw [mem_ker] at hx'

Premises used: LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : Eq (α := M →ₗ[R] M₁) ((B : (a : M) → M →ₗ[R] M₁) x : M →ₗ[R] M₁) (0 : M →ₗ[R] M₁)
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
y : M
hy : y ∈ W
⊢ Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) (↑x' : M) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)

Tactic:
simp [x', hx']
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
⊢ (B.domRestrict₁₂ W W).IsRefl

Tactic:
have hB' : (B.domRestrict₁₂ W W).IsRefl := fun x y ↦ hB.isRefl (W.subtype x) (W.subtype y)
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
rw : (B.domRestrict₁₂ W W).SeparatingLeft
⊢ (B.domRestrict₁₂ W W).Nondegenerate

Tactic:
rw [LinearMap.IsRefl.nondegenerate_iff_separatingLeft hB']

Premises used: LinearMap.IsRefl.nondegenerate_iff_separatingLeft
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' :
  ∀ (y : ↥W),
    Eq.{u_1 + 1} (α := R)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_1} (RingHom.id R) (↥W) R) :
            (a : ↥W) → R)
          y :
        R)
      (0 : R)
simp : x = 0
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx = 0

Tactic:
simp only [Submodule.mk_eq_zero]

Premises used: Submodule.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' :
  ∀ (y : ↥W),
    Eq.{u_1 + 1} (α := R)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_1} (RingHom.id R) (↥W) R) :
            (a : ↥W) → R)
          y :
        R)
      (0 : R)
⊢ ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
simpa [Subtype.forall] using hx'

Premises used: Subtype.forall
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' :
  ∀ (y : ↥W),
    Eq.{u_1 + 1} (α := R)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_1} (RingHom.id R) (↥W) R) :
            (a : ↥W) → R)
          y :
        R)
      (0 : R)
⊢ ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
replace hx' : ∀ y ∈ W, B x y = 0 := by simpa [Subtype.forall] using hx'
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ x ∈ W ⊓ B.ker

Tactic:
⟨hx, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
refine : x ∈ (↑B.ker : Set M)
⊢ x ∈ W ⊓ B.ker

Tactic:
refine ⟨hx, ?_⟩
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
h :
  ∀ (y : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) ((0 : (a : M) → R) y : R)
⊢ x ∈ (↑B.ker : Set M)

Tactic:
ext y
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
y : M
rw : Membership.mem (γ := Submodule R M) ⊤ y
⊢ ∃ u ∈ W, ∃ v ∈ B.ker, u + v = y

Tactic:
rw [← Submodule.mem_sup, hW.sup_eq_top]

Premises used: IsCompl.sup_eq_top, Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
y : M
⊢ Membership.mem (γ := Submodule R M) ⊤ y

Tactic:
Submodule.mem_top

Premises used: Set.Mem, Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
y : M
⊢ Membership.mem (γ := Submodule R M) ⊤ y

Tactic:
exact Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
y : M
h :
  ∀ (u : M) (hu : u ∈ W) (v : M) (hv : v ∈ B.ker),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (u + v) : R)
      ((0 : (a : M) → R) (u + v) : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) ((0 : (a : M) → R) y : R)

Tactic:
obtain ⟨u, hu, v, hv, rfl⟩ : ∃ u ∈ W, ∃ v ∈ ker B, u + v = y := by
      rw [← Submodule.mem_sup, hW.sup_eq_top]; exact Submodule.mem_top

Premises used: LinearMap.ker, rfl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
u : M
hu : u ∈ W
v : M
hv : v ∈ B.ker
this : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) u : R) (0 : R)
⊢ Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
rw [mem_ker] at hv

Premises used: LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
u : M
hu : u ∈ W
v : M
hv : v ∈ B.ker
this : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) u : R) (0 : R)
hv₁ : Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) u : R) (0 : R)

Tactic:
rw [mem_ker] at hv

Premises used: LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
u : M
hu : u ∈ W
v : M
hv : Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) (0 : M →ₗ[R] R)
this : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) u : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (u + v) : R)
    ((0 : (a : M) → R) (u + v) : R)

Tactic:
simpa [← hB.eq v, hv]

Premises used: LinearMap.IsSymm.eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
u : M
hu : u ∈ W
v : M
hv : v ∈ B.ker
h : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) u : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (u + v) : R)
    ((0 : (a : M) → R) (u + v) : R)

Tactic:
suffices B x u = 0 by rw [mem_ker] at hv; simpa [← hB.eq v, hv]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
u : M
hu : u ∈ W
v : M
hv : v ∈ B.ker
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) u : R) (0 : R)

Tactic:
hx' u hu
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
u : M
hu : u ∈ W
v : M
hv : v ∈ B.ker
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) u : R) (0 : R)

Tactic:
exact hx' u hu
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ x ∈ W ⊓ B.ker

Tactic:
replace hx' : x ∈ W ⊓ ker B := by
    refine ⟨hx, ?_⟩
    ext y
    obtain ⟨u, hu, v, hv, rfl⟩ : ∃ u ∈ W, ∃ v ∈ ker B, u + v = y := by
      rw [← Submodule.mem_sup, hW.sup_eq_top]; exact Submodule.mem_top
    suffices B x u = 0 by rw [mem_ker] at hv; simpa [← hB.eq v, hv]
    exact hx' u hu
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : x ∈ W ⊓ B.ker
⊢ x = 0

Tactic:
simpa [hW.inf_eq_bot] using hx'

Premises used: IsCompl.inf_eq_bot
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
rw : (B.domRestrict₁₂ W W).SeparatingLeft
⊢ (B.domRestrict₁₂ W W).Nondegenerate

Tactic:
rw [(hB.domRestrict W).nondegenerate_iff_separatingLeft]

Premises used: LinearMap.IsRefl.domRestrict, LinearMap.IsRefl.nondegenerate_iff_separatingLeft
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
b₁ :
  ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)
rw : Membership.mem (γ := Submodule R M) ⊥ x
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx = 0

Tactic:
rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R]

Premises used: Submodule.mem_bot, Submodule.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
b₁ :
  ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
hW.le_bot ⟨hx, fun y hy ↦ ?_⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
b₁ :
  ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)
refine : ∀ (y : M) (hy : y ∈ W), B.IsOrtho y x
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
refine hW.le_bot ⟨hx, fun y hy ↦ ?_⟩

Premises used: Disjoint.le_bot, And.intro
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
b₁ :
  ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)
y : M
hy : y ∈ W
⊢ Eq.{u_6 + 1} (α := M₁)
    ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
            LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
          (a : ↥W) → M₁)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ W) y hy) :
      M₁)
    (0 : M₁)

Tactic:
specialize b₁ ⟨y, hy⟩

Premises used: Subtype.mk
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) x : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
rw : B.IsOrtho x y
⊢ B.IsOrtho y x

Tactic:
rw [hB.ortho_comm]

Premises used: LinearMap.IsRefl.ortho_comm
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) x : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
⊢ B.IsOrtho x y

Tactic:
b₁

Premises used: LinearMap.IsOrtho
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) x : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
⊢ B.IsOrtho x y

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

Tactic:
v.ne_zero i (hB (v i) fun m ↦ ?_)

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

Tactic:
refine v.ne_zero i (hB (v i) fun m ↦ ?_)

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

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

Premises used: LinearEquiv.symm, LinearEquiv.surjective, Module.Basis.repr, rfl