awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = -B.flip
x : M₁
h' : Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R)
  ((((-B.flip : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R) :=
  ⋯
⊢ HAdd.hAdd (α := R) (β := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R)
      ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R) =
    0

Tactic:
simp only [neg_apply, flip_apply, ← add_eq_zero_iff_eq_neg] at h'

Premises used: LinearMap.neg_apply, add_eq_zero_iff_eq_neg, 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 = -B.flip
x : M₁
h' :
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R)
      ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R) =
    0
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R) (0 : R)

Tactic:
add_self_eq_zero.mp h'

Premises used: add_self_eq_zero, Iff.mp
-- 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 = -B.flip
x : M₁
h' :
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R)
      ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R) =
    0
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R) (0 : R)

Tactic:
exact add_self_eq_zero.mp h'

Premises used: add_self_eq_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
n_1 : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
N_1 L : Submodule R₁ M₁
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
N : Submodule R₁ M₁
a b : M₂
hx : Membership.mem (γ := Set M₂) {m : M₂ | ∀ n ∈ N, B.IsOrtho n m} a
hy : Membership.mem (γ := Set M₂) {m : M₂ | ∀ n ∈ N, B.IsOrtho n m} b
n : M₁
hn : n ∈ N
rw : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) n : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) (a + b) : M) (0 : M)
rw₁ :
  HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) n : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) a : M)
      ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) n : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) b : M) =
    0
rw₂ : HAdd.hAdd (α := M) (β := M) (0 : M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) n : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) b : M) = 0
rw₃ : HAdd.hAdd (α := M) 0 0 = 0
rw₄ rw₅ : Eq.{u_5 + 1} (α := M) 0 0
⊢ B.IsOrtho n (a + b)

Tactic:
rw [LinearMap.IsOrtho, map_add, show B n _ = 0 from hx n hn, show B n _ = 0 from hy n hn,
      zero_add]

Premises used: map_add, LinearMap.IsOrtho, zero_add
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
n_1 : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
N_1 L : Submodule R₁ M₁
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
N : Submodule R₁ M₁
c : R₂
x : M₂
hx : Membership.mem (γ := Set M₂) {m : M₂ | ∀ n ∈ N, B.IsOrtho n m} x
n : M₁
hn : n ∈ N
rw : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) n : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) (c • x) : M) (0 : M)
rw₁ :
  HSMul.hSMul.{u_1, u_5, u_5} (α := R) (β := M) ((I₂ : (a : R₂) → R) c : R)
      ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) n : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) x : M) =
    0
rw₂ : HSMul.hSMul.{u_1, u_5, u_5} (α := R) (β := M) ((I₂ : (a : R₂) → R) c : R) 0 = 0
rw₃ rw₄ : Eq.{u_5 + 1} (α := M) 0 0
⊢ B.IsOrtho n (c • x)

Tactic:
rw [LinearMap.IsOrtho, map_smulₛₗ, show B n x = 0 from hx n hn, smul_zero]

Premises used: smul_zero, MulActionSemiHomClass.map_smulₛₗ, LinearMap.IsOrtho
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
N : Submodule R₁ M₁
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
m : M₂
⊢ m ∈ orthogonalBilin B N ↔ ∀ n ∈ N, B.IsOrtho n m

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : CommSemiring R₂
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
N L : Submodule R₁ M₁
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : N ≤ L
⊢ orthogonalBilin B L ≤ orthogonalBilin B N

Tactic:
fun _ hn l hl ↦ hn l (h hl)

Premises used: Set.Mem, setOf
-- 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 : CommSemiring R₁
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
N : Submodule R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
b : B.IsRefl
⊢ N ≤ orthogonalBilin B (orthogonalBilin B N)

Tactic:
fun n hn _m hm ↦ b _ _ (hm n hn)

Premises used: Set.Mem, setOf, LinearMap.IsOrtho
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
rw : Submodule.span K₁ (↑{x} : Set V₁) ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ (↑{x} : Set V₁)) = ⊥
⊢ K₁ ∙ x ⊓ Submodule.orthogonalBilin B (K₁ ∙ x) = ⊥

Tactic:
rw [← Finset.coe_singleton]

Premises used: Finset.coe_singleton
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
⊢ Submodule.span K₁ (↑{x} : Set V₁) ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ (↑{x} : Set V₁)) = ⊥

Tactic:
eq_bot_iff.2 fun y h ↦ ?_

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
refine :
  ∀ (y : V₁)
    (h : y ∈ Submodule.span K₁ (↑{x} : Set V₁) ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ (↑{x} : Set V₁))),
    Membership.mem (γ := Submodule K₁ V₁) ⊥ y
⊢ Submodule.span K₁ (↑{x} : Set V₁) ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ (↑{x} : Set V₁)) = ⊥

Tactic:
refine eq_bot_iff.2 fun y h ↦ ?_

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
y : V₁
h : y ∈ Submodule.span K₁ (↑{x} : Set V₁) ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ (↑{x} : Set V₁))
obtain :
  ∀ (μ : V₁ → K₁)
    (h :
      ∑ a ∈ {x}, μ a • a ∈
        Submodule.span K₁ (↑{x} : Set V₁) ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ (↑{x} : Set V₁))),
    Membership.mem (γ := Submodule K₁ V₁) ⊥ (∑ a ∈ {x}, μ a • a)
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ y

Tactic:
obtain ⟨μ, -, rfl⟩ := Submodule.mem_span_finset.1 h.1

Premises used: Submodule.mem_span_finset, And.left, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h :
  ∑ a ∈ {x}, μ a • a ∈
    Submodule.span K₁ (↑{x} : Set V₁) ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ (↑{x} : Set V₁))
⊢ Membership.mem (γ := Submodule K₁ V₁) (Submodule.span K₁ (↑{x} : Set V₁)) x

Tactic:
simp [Submodule.mem_span]

Premises used: Submodule.mem_span
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h :
  ∑ a ∈ {x}, μ a • a ∈
    Submodule.span K₁ (↑{x} : Set V₁) ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ (↑{x} : Set V₁))
⊢ B.IsOrtho x (∑ a ∈ {x}, μ a • a)

Tactic:
replace h := h.2 x (by simp [Submodule.mem_span] : x ∈ Submodule.span K₁ ({x} : Finset V₁))
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (∑ a ∈ {x}, μ a • a)
rw : ∀ (h : B.IsOrtho x (μ x • x)), Membership.mem (γ := Submodule K₁ V₁) ⊥ (μ x • x)
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ (∑ a ∈ {x}, μ a • a)

Tactic:
rw [Finset.sum_singleton] at h ⊢

Premises used: Finset.sum_singleton
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (μ x • x)
hμzero : μ x = 0
rw : Membership.mem (γ := Submodule K₁ V₁) ⊥ (HSMul.hSMul.{u_14, u_17, u_17} (α := K₁) 0 x)
rw₁ : Membership.mem (γ := Submodule K₁ V₁) ⊥ 0
rw₂ rw₃ : Eq.{u_17 + 1} (α := V₁) 0 0
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ (μ x • x)

Tactic:
rw [hμzero, zero_smul, Submodule.mem_bot]

Premises used: Submodule.mem_bot, zero_smul
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (μ x • x)
suffices : μ x = 0
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ (μ x • x)

Tactic:
suffices hμzero : μ x = 0 by rw [hμzero, zero_smul, Submodule.mem_bot]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h : B.IsOrtho x (μ x • x)
⊢ HSMul.hSMul.{u_13, u_18, u_18} (α := K) (β := V₂) ((J₁' : (a : K₁) → K) (μ x) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[J₁'] V₂) x : V₁ →ₛₗ[J₁'] V₂) : (a : V₁) → V₂) x : V₂) =
    0

Tactic:
rw [isOrtho_def, map_smulₛₗ] at h

Premises used: MulActionSemiHomClass.map_smulₛₗ, LinearMap.isOrtho_def
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h :
  HSMul.hSMul.{u_13, u_18, u_18} (α := K) (β := V₂) ((J₁' : (a : K₁) → K) (μ x) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[J₁'] V₂) x : V₁ →ₛₗ[J₁'] V₂) : (a : V₁) → V₂) x : V₂) =
    0
y : Eq.{u_13 + 1} (α := K) ((J₁' : (a : K₁) → K) (μ x) : K) (0 : K)
⊢ μ x = 0

Tactic:
simpa using y
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
K₁ : Type u_14
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : Field K₁
inst_2 : AddCommGroup V₁
inst_3 : Module K₁ V₁
inst_4 : AddCommGroup V₂
inst_5 : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : ¬B.IsOrtho x x
μ : V₁ → K₁
h :
  HSMul.hSMul.{u_13, u_18, u_18} (α := K) (β := V₂) ((J₁' : (a : K₁) → K) (μ x) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[J₁'] V₂) x : V₁ →ₛₗ[J₁'] V₂) : (a : V₁) → V₂) x : V₂) =
    0
⊢ μ x = 0

Tactic:
exact Or.elim (smul_eq_zero.mp h)
      (fun y ↦ by simpa using y)
      (fun hfalse ↦ False.elim <| hx hfalse)

Premises used: False.elim, Iff.mp, Or.elim, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x : V
h :
  ∀ (y : V),
    y ∈ Submodule.orthogonalBilin B (K ∙ x) ↔
      Membership.mem (γ := Submodule K V)
        (ker.{u_13, u_13, u_16, u_18} (R₂ := K) (M₂ := V₂) (τ₁₂ := J) ((B : (a : V) → V →ₛₗ[J] V₂) x)) y
⊢ Submodule.orthogonalBilin B (K ∙ x) =
    ker.{u_13, u_13, u_16, u_18} (R₂ := K) (M₂ := V₂) (τ₁₂ := J) ((B : (a : V) → V →ₛₗ[J] V₂) x)

Tactic:
ext y
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h :
  (∀ (n : V), (∃ (a : K), a • x = n) → B.IsOrtho n y) ↔
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
⊢ y ∈ Submodule.orthogonalBilin B (K ∙ x) ↔
    Membership.mem (γ := Submodule K V)
      (ker.{u_13, u_13, u_16, u_18} (R₂ := K) (M₂ := V₂) (τ₁₂ := J) ((B : (a : V) → V →ₛₗ[J] V₂) x)) y

Tactic:
simp_rw [Submodule.mem_orthogonalBilin_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton, LinearMap.mem_ker, Submodule.mem_orthogonalBilin_iff
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h :
  (∀ (n : V), (∃ (a : K), a • x = n) → B.IsOrtho n y) →
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
h₁ :
  Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂) →
    ∀ (n : V), (∃ (a : K), a • x = n) → B.IsOrtho n y
⊢ (∀ (n : V), (∃ (a : K), a • x = n) → B.IsOrtho n y) ↔
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ (a : K), a • x = n) → B.IsOrtho n y) →
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)

Tactic:
fun h ↦ h x ⟨1, one_smul _ _⟩

Premises used: LinearMap.IsOrtho, one_smul, Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ (a : K), a • x = n) → B.IsOrtho n y) →
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)

Tactic:
exact fun h ↦ h x ⟨1, one_smul _ _⟩
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
z : K
h₁ :
  Eq (α := K) ((RingHom.id K : (a : K) → K) z : K) (0 : K) ∨
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
⊢ B.IsOrtho (z • x) y

Tactic:
rw [isOrtho_def, map_smulₛₗ₂, smul_eq_zero]

Premises used: LinearMap.map_smulₛₗ₂, LinearMap.isOrtho_def, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
z : K
⊢ Eq (α := K) ((RingHom.id K : (a : K) → K) z : K) (0 : K) ∨
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)

Tactic:
Or.intro_right _ h

Premises used: Or.intro_right
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)
z : K
⊢ Eq (α := K) ((RingHom.id K : (a : K) → K) z : K) (0 : K) ∨
    Eq.{u_18 + 1} (α := V₂) ((((B : (a : V) → V →ₛₗ[J] V₂) x : V →ₛₗ[J] V₂) : (a : V) → V₂) y : V₂) (0 : V₂)

Tactic:
exact Or.intro_right _ h

Premises used: Or.intro_right
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬B.IsOrtho x x
rw : Eq (α := Submodule K V) (K ∙ x ⊔ ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K) ((B : (a : V) → V →ₗ[K] K) x)) ⊤
⊢ K ∙ x ⊔ Submodule.orthogonalBilin B (K ∙ x) = ⊤

Tactic:
rw [orthogonal_span_singleton_eq_to_lin_ker]

Premises used: LinearMap.orthogonal_span_singleton_eq_to_lin_ker
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬B.IsOrtho x x
⊢ Eq (α := Submodule K V) (K ∙ x ⊔ ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K) ((B : (a : V) → V →ₗ[K] K) x)) ⊤

Tactic:
(B x).span_singleton_sup_ker_eq_top hx

Premises used: Set.Mem, setOf, LinearMap.span_singleton_sup_ker_eq_top, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬B.IsOrtho x x
⊢ Eq (α := Submodule K V) (K ∙ x ⊔ ker (R₂ := K) (M₂ := K) (τ₁₂ := RingHom.id K) ((B : (a : V) → V →ₗ[K] K) x)) ⊤

Tactic:
exact (B x).span_singleton_sup_ker_eq_top hx

Premises used: LinearMap.span_singleton_sup_ker_eq_top, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
K : Type u_13
V : Type u_16
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬B.IsOrtho x x
⊢ IsCompl (K ∙ x) (Submodule.orthogonalBilin B (K ∙ x))

Tactic:
{ disjoint := disjoint_iff.2 <| span_singleton_inf_orthogonal_eq_bot B x hx
    codisjoint := codisjoint_iff.2 <| span_singleton_sup_orthogonal_eq_top hx }

Premises used: Iff.mpr, LinearMap.span_singleton_sup_orthogonal_eq_top, codisjoint_iff, disjoint_iff, LinearMap.span_singleton_inf_orthogonal_eq_bot, IsCompl.mk
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
mp : B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M) → B' ∘ₗ f = B.compl₂ g
mpr : B' ∘ₗ f = B.compl₂ g → B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M)
⊢ B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M) ↔ B' ∘ₗ f = B.compl₂ g

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M)
mp :
  ∀ (x : M) (y : M₁),
    Eq.{u_8 + 1} (α := M₃) ((((B' ∘ₗ f : (a : M) → M₁ →ₛₗ[I] M₃) x : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
      ((((B.compl₂ g : (a : M) → M₁ →ₛₗ[I] M₃) x : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
⊢ B' ∘ₗ f = B.compl₂ g

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M)
x : M
y : M₁
mp :
  Eq.{u_8 + 1} (α := M₃)
    ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) ((f : (a : M) → M₁) x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g : (a : M₁) → M) y : M) : M₃)
⊢ Eq.{u_8 + 1} (α := M₃) ((((B' ∘ₗ f : (a : M) → M₁ →ₛₗ[I] M₃) x : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
    ((((B.compl₂ g : (a : M) → M₁ →ₛₗ[I] M₃) x : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)

Tactic:
rw [comp_apply, compl₂_apply]

Premises used: LinearMap.compl₂_apply, LinearMap.comp_apply
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B.IsAdjointPair B' (⇑f : (a : M) → M₁) (⇑g : (a : M₁) → M)
x : M
y : M₁
⊢ Eq.{u_8 + 1} (α := M₃)
    ((((B' : (a : M₁) → M₁ →ₛₗ[I] M₃) ((f : (a : M) → M₁) x) : M₁ →ₛₗ[I] M₃) : (a : M₁) → M₃) y : M₃)
    ((((B : (a : M) → M →ₛₗ[I] M₃) x : M →ₛₗ[I] M₃) : (a : M) → M₃) ((g : (a : M₁) → M) y : M) : M₃)

Tactic:
h x y