awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
b : B.IsRefl
⊢ N ≤ B.orthogonal (B.orthogonal N)

Tactic:
fun n hn _ hm => b _ _ (hm n hn)

Premises used: Set.Mem, setOf, LinearMap.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
hB : B.IsRefl
h : ∀ (x : M), x ∈ B.orthogonal ⊤ ↔ x ∈ ker B
⊢ B.orthogonal ⊤ = ker B

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
hB : B.IsRefl
x : M
⊢ x ∈ B.orthogonal ⊤ ↔ x ∈ ker B

Tactic:
simp [LinearMap.BilinForm.IsOrtho, LinearMap.ext_iff, hB.eq_iff]

Premises used: LinearMap.ext_iff, LinearMap.BilinForm.IsOrtho, LinearMap.IsRefl.eq_iff
-- 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
hB : B.Nondegenerate
x : M
hx : x ∈ B.orthogonal ⊤
⊢ ∀ (x_1 : M), Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x_1 : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)

Tactic:
simpa using hx
-- 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
⊢ K ∙ x ⊓ B.orthogonal (K ∙ x) = ⊥

Tactic:
LinearMap.span_singleton_inf_orthogonal_eq_bot B _ hx

Premises used: setOf, LinearMap.span_singleton_inf_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
B : BilinForm K V
x : V
⊢ B.orthogonal (K ∙ x) = (B.toLinHomAux₁ x).ker

Tactic:
LinearMap.orthogonal_span_singleton_eq_to_lin_ker ..

Premises used: LinearMap.BilinForm.toLinHomAux₁, LinearMap.BilinForm.orthogonal, LinearMap.orthogonal_span_singleton_eq_to_lin_ker
-- 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
⊢ K ∙ x ⊔ B.orthogonal (K ∙ x) = ⊤

Tactic:
LinearMap.span_singleton_sup_orthogonal_eq_top hx

Premises used: Set.Mem, LinearMap.span_singleton_sup_orthogonal_eq_top, setOf
-- 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
⊢ IsCompl (K ∙ x) (B.orthogonal (K ∙ x))

Tactic:
LinearMap.isCompl_span_singleton_orthogonal hx

Premises used: LinearMap.isCompl_span_singleton_orthogonal, LinearMap.BilinForm.orthogonal
-- 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₁
b : B.IsRefl
W : Submodule R₁ M₁
hW : Disjoint W (B.orthogonal W)
⊢ (B.restrict W).Nondegenerate

Tactic:
LinearMap.nondegenerate_restrict_of_disjoint_orthogonal b hW

Premises used: LinearMap.BilinForm.restrict, LinearMap.nondegenerate_restrict_of_disjoint_orthogonal
-- 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
inst_3 : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho.{w, u_1, u_2} (n := n) B (⇑v : (a : n) → M)
hB : B.Nondegenerate
i : n
⊢ ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
h.not_isOrtho_basis_self_of_separatingLeft hB.1 i

Premises used: LinearMap.BilinForm.IsOrtho, And.left, LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft
-- 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
inst_3 : Nontrivial R
inst_4 : IsDomain R
B : BilinForm R M
v : Basis n R M
hO : iIsOrtho.{w, u_1, u_2} (n := n) B (⇑v : (a : n) → M)
⊢ B.Nondegenerate ↔ ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
⟨hO.not_isOrtho_basis_self_of_nondegenerate, hO.nondegenerate_of_not_isOrtho_basis_self _⟩

Premises used: LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self, Iff.intro, LinearMap.BilinForm.iIsOrtho.not_isOrtho_basis_self_of_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
W : Subspace K V
h : ∀ (x : V), x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker ↔ x ∈ W ⊓ ker B
⊢ Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ ker B

Tactic:
ext x
-- 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
W : Subspace K V
x : V
h : x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker → x ∈ W ⊓ ker B
h₁ : x ∈ W ⊓ ker B → x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker
⊢ x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker ↔ x ∈ W ⊓ ker B

Tactic:
constructor
-- 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
W : Subspace K V
x : V
hx : x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker
h :
  ∀ (x : V) (hx : x ∈ W) (hker : Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx ∈ (↑(domRestrict B W).ker : Set ↥W)),
    Membership.mem (α := V) (W ⊓ ker B)
      ((Submodule.subtype W : (a : ↥W) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx) : V)
⊢ x ∈ W ⊓ ker B

Tactic:
rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩

Premises used: 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
W : Subspace K V
x : V
hx : x ∈ W
hker : Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx ∈ (↑(domRestrict B W).ker : Set ↥W)
h :
  Membership.mem (α := V) (↑W : Set V)
    ((Submodule.subtype W : (a : ↥W) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx) : V)
h₁ :
  Membership.mem (α := V) (↑(ker B) : Set V)
    ((Submodule.subtype W : (a : ↥W) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx) : V)
⊢ Membership.mem (α := V) (W ⊓ ker B)
    ((Submodule.subtype W : (a : ↥W) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx) : V)

Tactic:
constructor
-- 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
W : Subspace K V
x : V
hx : x ∈ W
hker : Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx ∈ (↑(domRestrict B W).ker : Set ↥W)
⊢ Membership.mem (α := V) (↑W : Set V)
    ((Submodule.subtype W : (a : ↥W) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx) : V)

Tactic:
simp [hx]
-- 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
W : Subspace K V
x : V
hx : x ∈ W
hker : Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx ∈ (↑(domRestrict B W).ker : Set ↥W)
⊢ Membership.mem (α := V) (↑(ker B) : Set V)
    ((Submodule.subtype W : (a : ↥W) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx) : V)

Tactic:
simpa
-- 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
W : Subspace K V
x : V
hx : x ∈ W ⊓ ker B
⊢ ∃ (y : ↥W),
    Eq (α := V →ₗ[K] K) ((domRestrict B W : (a : ↥W) → V →ₗ[K] K) y : V →ₗ[K] K) (0 : V →ₗ[K] K) ∧
      (Submodule.subtype W : (a : ↥W) → V) y = x

Tactic:
⟨⟨x, hx.1⟩, hx.right, rfl⟩

Premises used: Subtype.mk, And.right, And.left, And.intro, Exists.intro, 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
W : Subspace K V
x : V
hx : x ∈ W ⊓ ker B
⊢ ∃ (y : ↥W),
    Eq (α := V →ₗ[K] K) ((domRestrict B W : (a : ↥W) → V →ₗ[K] K) y : V →ₗ[K] K) (0 : V →ₗ[K] K) ∧
      (Submodule.subtype W : (a : ↥W) → V) y = x

Tactic:
exact ⟨⟨x, hx.1⟩, hx.right, 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
W : Subspace K V
b : B.IsRefl
rw : Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ ker B
⊢ Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ B.orthogonal ⊤

Tactic:
rw [orthogonal_top_eq_ker b]

Premises used: LinearMap.BilinForm.orthogonal_top_eq_ker
-- 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
W : Subspace K V
b : B.IsRefl
⊢ Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ ker B

Tactic:
toLin_restrict_ker_eq_inf_ker ..

Premises used: LinearMap.BilinForm.toLin_restrict_ker_eq_inf_ker
-- 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
W : Subspace K V
b : B.IsRefl
⊢ Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ ker B

Tactic:
exact toLin_restrict_ker_eq_inf_ker ..

Premises used: LinearMap.BilinForm.toLin_restrict_ker_eq_inf_ker
-- 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
W : Subspace K V
h : ∀ (x : V), x ∈ (domRestrict B W).range.dualCoannihilator ↔ x ∈ B.orthogonal W
⊢ (domRestrict B W).range.dualCoannihilator = B.orthogonal W

Tactic:
ext x
-- 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
W : Subspace K V
x : V
h : x ∈ (domRestrict B W).range.dualCoannihilator → x ∈ B.orthogonal W
h₁ : x ∈ B.orthogonal W → x ∈ (domRestrict B W).range.dualCoannihilator
⊢ x ∈ (domRestrict B W).range.dualCoannihilator ↔ x ∈ B.orthogonal W

Tactic:
constructor
-- 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
W : Subspace K V
x : V
h : x ∈ (domRestrict B W).range.dualCoannihilator → ∀ n ∈ W, B.IsOrtho n x
⊢ x ∈ (domRestrict B W).range.dualCoannihilator → x ∈ B.orthogonal W

Tactic:
rw [mem_orthogonal_iff]

Premises used: LinearMap.BilinForm.mem_orthogonal_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
B : BilinForm K V
W : Subspace K V
x : V
h : (∀ n ∈ W, B.IsOrtho n x) → x ∈ (domRestrict B W).range.dualCoannihilator
⊢ x ∈ B.orthogonal W → x ∈ (domRestrict B W).range.dualCoannihilator

Tactic:
rw [mem_orthogonal_iff]

Premises used: LinearMap.BilinForm.mem_orthogonal_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
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ (domRestrict B W).range.dualCoannihilator
y : V
hy : y ∈ W
h :
  ∀ (hx : ∀ φ ∈ (domRestrict B W).range, Eq.{u_6 + 1} (α := K) ((φ : (a : V) → K) x : K) (0 : K)) (y : V) (hy : y ∈ W),
    B.IsOrtho y x
⊢ B.IsOrtho y x

Tactic:
rw [Submodule.mem_dualCoannihilator] at hx

Premises used: Submodule.mem_dualCoannihilator
-- 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
W : Subspace K V
x : V
hx : ∀ φ ∈ (domRestrict B W).range, Eq.{u_6 + 1} (α := K) ((φ : (a : V) → K) x : K) (0 : K)
y : V
hy : y ∈ W
⊢ B.IsOrtho y x

Tactic:
hx (B.domRestrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩

Premises used: LinearMap.BilinForm.IsOrtho, Subtype.mk, LinearMap.domRestrict, Exists.intro, DFunLike.coe, 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
W : Subspace K V
x : V
hx : ∀ φ ∈ (domRestrict B W).range, Eq.{u_6 + 1} (α := K) ((φ : (a : V) → K) x : K) (0 : K)
y : V
hy : y ∈ W
⊢ B.IsOrtho y x

Tactic:
exact hx (B.domRestrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩

Premises used: Subtype.mk, LinearMap.domRestrict, Exists.intro, DFunLike.coe, 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
W : Subspace K V
x : V
hx : ∀ n ∈ W, B.IsOrtho n x
h : ∀ φ ∈ (domRestrict B W).range, Eq.{u_6 + 1} (α := K) ((φ : (a : V) → K) x : K) (0 : K)
⊢ x ∈ (domRestrict B W).range.dualCoannihilator

Tactic:
rw [Submodule.mem_dualCoannihilator]

Premises used: Submodule.mem_dualCoannihilator
-- 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
W : Subspace K V
x : V
hx : ∀ n ∈ W, B.IsOrtho n x
w : V
hw : w ∈ W
⊢ Eq.{u_6 + 1} (α := K)
    ((((domRestrict B W : (a : ↥W) → V →ₗ[K] K) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) w hw) : V →ₗ[K] K) : (a : V) → K)
        x :
      K)
    (0 : K)

Tactic:
hx w hw

Premises used: 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
W : Subspace K V
x : V
hx : ∀ n ∈ W, B.IsOrtho n x
w : V
hw : w ∈ W
⊢ Eq.{u_6 + 1} (α := K)
    ((((domRestrict B W : (a : ↥W) → V →ₗ[K] K) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) w hw) : V →ₗ[K] K) : (a : V) → K)
        x :
      K)
    (0 : K)

Tactic:
exact hx w hw
-- 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
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
h :
  ∀ (z : M) (hz : z ∈ p),
    Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz ∈ ker (B.restrict p) ↔
      Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz ∈ Submodule.comap p.subtype (ker B)
⊢ ker (B.restrict p) = Submodule.comap p.subtype (ker B)

Tactic:
ext ⟨z, hz⟩
-- 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
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
h :
  Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
      ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
        LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
      (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R) ↔
    Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz ∈ ker (B.restrict p) ↔
    Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz ∈ Submodule.comap p.subtype (ker B)

Tactic:
simp only [LinearMap.mem_ker, Submodule.mem_comap, Submodule.coe_subtype]

Premises used: Submodule.mem_comap, LinearMap.mem_ker, Submodule.coe_subtype
-- 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
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
      ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
        LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
      (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R) ↔
    Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) (0 : M →ₗ[R] R)

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

Premises used: Iff.intro
-- 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
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
h :
  ∀
    (h :
      Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
        ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
          LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
        (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)),
    Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) (0 : M →ₗ[R] R)
h₁ :
  ∀ (h : Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) (0 : M →ₗ[R] R)),
    Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
      ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
        LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
      (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
      ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
        LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
      (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R) ↔
    Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
h :
  Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
      LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
h₁ :
  ∀ (w : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) w : R) ((0 : (a : M) → R) w : R)
⊢ Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
ext w
-- 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
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
h :
  Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
      LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
w : M
h₁ :
  ∀ (x y : M) (hx : x ∈ p) (hy : y ∈ q),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) (x + y) : R)
      ((0 : (a : M) → R) (x + y) : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) w : R) ((0 : (a : M) → R) w : R)

Tactic:
obtain ⟨x, y, hx, hy, rfl⟩ := Submodule.codisjoint_iff_exists_add_eq.mp hpq w

Premises used: Submodule.codisjoint_iff_exists_add_eq, Iff.mp, rfl
-- 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
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
h :
  Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
      LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
x y : M
hx : x ∈ p
hy : y ∈ q
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) (x + y) : R)
    ((0 : (a : M) → R) (x + y) : R)

Tactic:
simpa [hB z hz y hy] using LinearMap.congr_fun h ⟨x, hx⟩

Premises used: Subtype.mk, LinearMap.congr_fun
-- 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
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
h : Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) (0 : M →ₗ[R] R)
h₁ :
  ∀ (x : M) (hx : x ∈ p),
    Eq.{u_1 + 1} (α := R)
      ((((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
              LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R) :
            (a : ↥p) → R)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) :
        R)
      ((0 : (a : ↥p) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : R)
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
      LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)

Tactic:
ext ⟨x, hx⟩
-- 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
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
h : Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) (0 : M →ₗ[R] R)
x : M
hx : x ∈ p
⊢ Eq.{u_1 + 1} (α := R)
    ((((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R) :
          (a : ↥p) → R)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) :
      R)
    ((0 : (a : ↥p) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : R)

Tactic:
simpa using LinearMap.congr_fun h x

Premises used: LinearMap.congr_fun
-- 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
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
simp :
  Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥W) R) (domRestrict ((B : (a : M) → M →ₗ[R] R) v) W) 0 ∧ v ∈ W
⊢ v ∈ Submodule.map W.subtype (ker (B.restrict W))

Tactic:
simp only [Submodule.mem_map, mem_ker, restrict_apply, Submodule.coe_subtype, Subtype.exists,
    exists_and_left, exists_prop, exists_eq_right_right]

Premises used: exists_eq_right_right, Submodule.mem_map, Subtype.exists, exists_and_left, exists_prop, LinearMap.mem_ker, Submodule.coe_subtype, LinearMap.BilinForm.restrict_apply
-- 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
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥W) R) (domRestrict ((B : (a : M) → M →ₗ[R] R) v) W) 0 ∧ v ∈ W

Tactic:
⟨?_, hv⟩

Premises used: And.intro