awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
h : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M)
rw : Eq.{u_5 + 1} (α := M) (-(((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) y : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) x : M) (0 : M)
have rw₁ : Eq.{u_5 + 1} (α := M) (-0) 0
Tactic: rw [← neg H, h, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
h : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M)
rw : Eq.{u_5 + 1} (α := M) (-(((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M)
rw₁ : Eq.{u_5 + 1} (α := M) (-0) 0
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) y : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) x : M) (0 : M)
have rw₂ : Eq.{u_5 + 1} (α := M) 0 0
Tactic: rw [← neg H, h, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.IsAlt ↔ B = -B.flip
have mp : B.IsAlt → B = -B.flip
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
mp : B.IsAlt → B = -B.flip
⊢ B.IsAlt ↔ B = -B.flip
have mpr : B = -B.flip → B.IsAlt
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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.IsAlt
⊢ B = -B.flip
have mp : ∀ (x x_1 : M₁),
  Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
    ((((-B.flip : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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.IsAlt
x x_1 : M₁
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
    ((((-B.flip : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
have mp : Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x_1 : R)
  (-(((B : (a : M₁) → M₁ →ₛₗ[I] R) x_1 : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R)
Tactic: simp_rw [neg_apply, flip_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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) :=
  ⋯
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M₁) → M₁ →ₛₗ[I] R) x : M₁ →ₛₗ[I] R) : (a : M₁) → R) x : R) (0 : R)
have 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
Tactic: simp only [neg_apply, flip_apply, ← add_eq_zero_iff_eq_neg] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.IsOrtho n (a + b)
have rw : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) n : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) (a + b) : M) (0 : M)
Tactic: rw [LinearMap.IsOrtho, map_add, show B n _ = 0 from hx n hn, show B n _ = 0 from hy n hn,
      zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ B.IsOrtho n (a + b)
have 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
Tactic: rw [LinearMap.IsOrtho, map_add, show B n _ = 0 from hx n hn, show B n _ = 0 from hy n hn,
      zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.IsOrtho n (a + b)
have rw₂ : HAdd.hAdd (α := M) (β := M) (0 : M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) n : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) b : M) = 0
Tactic: rw [LinearMap.IsOrtho, map_add, show B n _ = 0 from hx n hn, show B n _ = 0 from hy n hn,
      zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.IsOrtho n (a + b)
have rw₃ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [LinearMap.IsOrtho, map_add, show B n _ = 0 from hx n hn, show B n _ = 0 from hy n hn,
      zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.IsOrtho n (a + b)
have rw₄ : Eq.{u_5 + 1} (α := M) 0 0
Tactic: rw [LinearMap.IsOrtho, map_add, show B n _ = 0 from hx n hn, show B n _ = 0 from hy n hn,
      zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.IsOrtho n (c • x)
have rw : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₂ →ₛₗ[I₂] M) n : M₂ →ₛₗ[I₂] M) : (a : M₂) → M) (c • x) : M) (0 : M)
Tactic: rw [LinearMap.IsOrtho, map_smulₛₗ, show B n x = 0 from hx n hn, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ B.IsOrtho n (c • x)
have 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
Tactic: rw [LinearMap.IsOrtho, map_smulₛₗ, show B n x = 0 from hx n hn, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.IsOrtho n (c • x)
have rw₂ : HSMul.hSMul.{u_1, u_5, u_5} (α := R) (β := M) ((I₂ : (a : R₂) → R) c : R) 0 = 0
Tactic: rw [LinearMap.IsOrtho, map_smulₛₗ, show B n x = 0 from hx n hn, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ B.IsOrtho n (c • x)
have rw₃ : Eq.{u_5 + 1} (α := M) 0 0
Tactic: rw [LinearMap.IsOrtho, map_smulₛₗ, show B n x = 0 from hx n hn, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ K₁ ∙ x ⊓ Submodule.orthogonalBilin B (K₁ ∙ x) = ⊥
have rw : Submodule.span K₁ (↑{x} : Set V₁) ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ (↑{x} : Set V₁)) = ⊥
Tactic: rw [← Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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₁)) = ⊥
have 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
Tactic: refine eq_bot_iff.2 fun y h ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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₁))
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ y
have 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)
Tactic: obtain ⟨μ, -, rfl⟩ := Submodule.mem_span_finset.1 h.1
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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₁) ⊥ (∑ a ∈ {x}, μ a • a)
have h₁ : 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₁))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ (∑ a ∈ {x}, μ a • a)
have rw : ∀ (h : B.IsOrtho x (μ x • x)), Membership.mem (γ := Submodule K₁ V₁) ⊥ (μ x • x)
Tactic: rw [Finset.sum_singleton] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ (μ x • x)
have rw : Membership.mem (γ := Submodule K₁ V₁) ⊥ (HSMul.hSMul.{u_14, u_17, u_17} (α := K₁) 0 x)
Tactic: rw [hμzero, zero_smul, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ (μ x • x)
have rw₁ : Membership.mem (γ := Submodule K₁ V₁) ⊥ 0
Tactic: rw [hμzero, zero_smul, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ (μ x • x)
have rw₂ : Eq.{u_17 + 1} (α := V₁) 0 0
Tactic: rw [hμzero, zero_smul, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ Membership.mem (γ := Submodule K₁ V₁) ⊥ (μ x • x)
have suffices : μ x = 0
Tactic: suffices hμzero : μ x = 0 by rw [hμzero, zero_smul, Submodule.mem_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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)
⊢ μ x = 0
have 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
Tactic: rw [isOrtho_def, map_smulₛₗ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ 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)
have 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
Tactic: ext y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ 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
have 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₂)
Tactic: simp_rw [Submodule.mem_orthogonalBilin_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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₂)
have 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₂)
Tactic: constructor