awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
⊢ LinearIndependent K v
have rw : ∀ (s : Finset n) (g : n → K), Eq.{u_5 + 1} (α := V) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
Tactic: rw [linearIndependent_iff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
⊢ Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
have rw : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) 0 : (a : V) → K) (v i) : K) (0 : K)
Tactic: rw [hs, zero_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
rw : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) 0 : (a : V) → K) (v i) : K) (0 : K)
⊢ Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
have rw₁ : Eq.{u_6 + 1} (α := K) 0 0
Tactic: rw [hs, zero_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
⊢ w i = 0
have this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
Tactic: have : B (s.sum fun i : n => w i • v i) (v i) = 0 := by rw [hs, zero_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
⊢ ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
    HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)
have apply : ∀ b ∈ s, b ≠ i → HMul.hMul (β := K) (w b) ((((B : (a : V) → V →ₗ[K] K) (v b) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0
Tactic: apply Finset.sum_eq_single_of_mem i hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
j : n
h : j ∈ s
hij : j ≠ i
⊢ HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0
have rw : w j * 0 = 0
Tactic: rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
j : n
h : j ∈ s
hij : j ≠ i
rw : w j * 0 = 0
⊢ HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0
have rw₁ : Eq.{u_6 + 1} (α := K) 0 0
Tactic: rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
⊢ w i = 0
have hsum : ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
  HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)
Tactic: have hsum : (s.sum fun j : n => w j * B (v j) (v i)) = w i * B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _ hij
      rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K
hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)
hsum :
  ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
    HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)
⊢ w i = 0
have this₁ : HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0
Tactic: simp_rw [sum_left, smul_left, hsum] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
⊢ LinearIndependent K v
have rw : ∀ (s : Finset n) (g : n → K), Eq.{u_5 + 1} (α := V) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
Tactic: classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n => w i • v i) (v i) = 0 := by rw [hs, zero_left]
    have hsum : (s.sum fun j : n => w j * B (v j) (v i)) = w i * B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _ hij
      rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
    simp_rw [sum_left, smul_left, hsum] at this
    exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw rw₁ rw₂ rw₃ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s), w i = 0
⊢ LinearIndependent K v
have rw₄ : ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
  (this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)),
  w i = 0
Tactic: classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n => w i • v i) (v i) = 0 := by rw [hs, zero_left]
    have hsum : (s.sum fun j : n => w j * B (v j) (v i)) = w i * B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _ hij
      rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
    simp_rw [sum_left, smul_left, hsum] at this
    exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw rw₁ rw₂ rw₃ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s), w i = 0
rw₄ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)),
    w i = 0
⊢ LinearIndependent K v
have rw₅ : ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
  (this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K))
  (hsum :
    ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
      HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)),
  w i = 0
Tactic: classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n => w i • v i) (v i) = 0 := by rw [hs, zero_left]
    have hsum : (s.sum fun j : n => w j * B (v j) (v i)) = w i * B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _ hij
      rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
    simp_rw [sum_left, smul_left, hsum] at this
    exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw rw₁ rw₂ rw₃ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s), w i = 0
rw₄ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K)),
    w i = 0
rw₅ :
  ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this : Eq.{u_6 + 1} (α := K) (((B : (a : V) → V →ₗ[K] K) (∑ i ∈ s, w i • v i) : (a : V) → K) (v i) : K) (0 : K))
    (hsum :
      ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
        HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K)),
    w i = 0
⊢ LinearIndependent K v
have rw₆ : ∀ (s : Finset n) (w : n → K) (hs : Eq.{u_5 + 1} (α := V) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
  (hsum :
    ∑ j ∈ s, HMul.hMul (β := K) (w j) ((((B : (a : V) → V →ₗ[K] K) (v j) : V →ₗ[K] K) : (a : V) → K) (v i) : K) =
      HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K))
  (this : HMul.hMul (β := K) (w i) ((((B : (a : V) → V →ₗ[K] K) (v i) : V →ₗ[K] K) : (a : V) → K) (v i) : K) = 0),
  w i = 0
Tactic: classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n => w i • v i) (v i) = 0 := by rw [hs, zero_left]
    have hsum : (s.sum fun j : n => w j * B (v j) (v i)) = w i * B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _ hij
      rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
    simp_rw [sum_left, smul_left, hsum] at this
    exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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.orthogonal ⊥ = ⊤
have h : ∀ (x : M), x ∈ B.orthogonal ⊥ ↔ Membership.mem (γ := Submodule R M) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ B.orthogonal ⊤ = ker B
have h : ∀ (x : M), x ∈ B.orthogonal ⊤ ↔ x ∈ ker B
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ ker B
have h : ∀ (x : V), x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker ↔ x ∈ W ⊓ ker B
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker ↔ x ∈ W ⊓ ker B
have h : x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker → x ∈ W ⊓ ker B
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker ↔ x ∈ W ⊓ ker B
have h₁ : x ∈ W ⊓ ker B → x ∈ Submodule.map (Submodule.subtype W) (domRestrict B W).ker
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ x ∈ W ⊓ ker B
have 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)
Tactic: rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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 ⊓ ker B)
    ((Submodule.subtype W : (a : ↥W) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx) : V)
have h : Membership.mem (α := V) (↑W : Set V)
  ((Submodule.subtype W : (a : ↥W) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx) : V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
⊢ Membership.mem (α := V) (W ⊓ ker B)
    ((Submodule.subtype W : (a : ↥W) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx) : V)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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 ⊓ B.orthogonal ⊤
have rw : Submodule.map (Submodule.subtype W) (domRestrict B W).ker = W ⊓ ker B
Tactic: rw [orthogonal_top_eq_ker b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ (domRestrict B W).range.dualCoannihilator = B.orthogonal W
have h : ∀ (x : V), x ∈ (domRestrict B W).range.dualCoannihilator ↔ x ∈ B.orthogonal W
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ x ∈ (domRestrict B W).range.dualCoannihilator ↔ x ∈ B.orthogonal W
have h : x ∈ (domRestrict B W).range.dualCoannihilator → x ∈ B.orthogonal W
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ x ∈ (domRestrict B W).range.dualCoannihilator ↔ x ∈ B.orthogonal W
have h₁ : x ∈ B.orthogonal W → x ∈ (domRestrict B W).range.dualCoannihilator
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ x ∈ (domRestrict B W).range.dualCoannihilator → x ∈ B.orthogonal W
have h : x ∈ (domRestrict B W).range.dualCoannihilator → ∀ n ∈ W, B.IsOrtho n x
Tactic: rw [mem_orthogonal_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ x ∈ B.orthogonal W → x ∈ (domRestrict B W).range.dualCoannihilator
have h : (∀ n ∈ W, B.IsOrtho n x) → x ∈ (domRestrict B W).range.dualCoannihilator
Tactic: rw [mem_orthogonal_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ B.IsOrtho y x
have 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
Tactic: rw [Submodule.mem_dualCoannihilator] at hx
Cleared hypotheses: hx, y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ x ∈ (domRestrict B W).range.dualCoannihilator
have h : ∀ φ ∈ (domRestrict B W).range, Eq.{u_6 + 1} (α := K) ((φ : (a : V) → K) x : K) (0 : K)
Tactic: rw [Submodule.mem_dualCoannihilator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
⊢ ker (B.restrict p) = Submodule.comap p.subtype (ker B)
have 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)
Tactic: ext ⟨z, hz⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ 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)
have 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)
Tactic: simp only [LinearMap.mem_ker, Submodule.mem_comap, Submodule.coe_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
⊢ 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)
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
have 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)
Tactic: ext w