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
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.SeparatingRight ↔ B.flip.ker = ⊥
have rw : B.flip.SeparatingLeft ↔ B.flip.ker = ⊥
Tactic: rw [← flip_separatingLeft, separatingLeft_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
inst_6 : CommSemiring R₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
rw : B.flip.SeparatingLeft ↔ B.flip.ker = ⊥
⊢ B.SeparatingRight ↔ B.flip.ker = ⊥
have rw₁ : B.flip.ker = ⊥ ↔ B.flip.ker = ⊥
Tactic: rw [← flip_separatingLeft, separatingLeft_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
⊢ B.Nondegenerate ↔ B.SeparatingLeft
have refine : ∀ (hB' : B.SeparatingLeft), B.SeparatingRight
Tactic: refine ⟨fun h ↦ h.1, fun hB' ↦ ⟨hB', ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingLeft
⊢ B.SeparatingRight
have rw : B.ker = ⊥
Tactic: rw [separatingRight_iff_flip_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
⊢ B.Nondegenerate ↔ B.SeparatingRight
have refine : ∀ (hB' : B.SeparatingRight), B.SeparatingLeft
Tactic: refine ⟨fun h ↦ h.2, fun hB' ↦ ⟨?_, hB'⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ B.SeparatingLeft
have rw : B.flip.ker = ⊥
Tactic: rw [separatingLeft_iff_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mpr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
⊢ Disjoint W B.ker
have refine : ∀ (x : M) (hx : x ∈ W) (hx' : x ∈ B.ker), x = 0
Tactic: refine Submodule.disjoint_def.mpr fun x hx hx' ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
⊢ x = 0
have suffices : x' = 0
Tactic: suffices x' = 0 by simpa [x']
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
⊢ x' = 0
have apply : ∀ (y : ↥W),
  Eq.{u_6 + 1} (α := M₁)
    ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) x' : LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
          (a : ↥W) → M₁)
        y :
      M₁)
    (0 : M₁)
Tactic: apply hW.1 x'
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
⊢ ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) x' : LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)
have simp_rw : ∀ (a : M) (b : a ∈ W),
  Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) (↑x' : M) : M →ₗ[R] M₁) : (a : M) → M₁) a : M₁) (0 : M₁)
Tactic: simp_rw [Subtype.forall, domRestrict₁₂_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx
y : M
hy : y ∈ W
⊢ Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) (↑x' : M) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
have rw : ∀ (hx' : Eq (α := M →ₗ[R] M₁) ((B : (a : M) → M →ₗ[R] M₁) x : M →ₗ[R] M₁) (0 : M →ₗ[R] M₁)),
  let x' := Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx;
  ∀ (y : M) (hy : y ∈ W),
    Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) (↑x' : M) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
Tactic: rw [mem_ker] at hx'
Cleared hypotheses: hx', x', y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
⊢ (B.domRestrict₁₂ W W).Nondegenerate
have hB' : (B.domRestrict₁₂ W W).IsRefl
Tactic: have hB' : (B.domRestrict₁₂ W W).IsRefl := fun x y ↦ hB.isRefl (W.subtype x) (W.subtype y)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
⊢ (B.domRestrict₁₂ W W).Nondegenerate
have rw : (B.domRestrict₁₂ W W).SeparatingLeft
Tactic: rw [LinearMap.IsRefl.nondegenerate_iff_separatingLeft hB']
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' :
  ∀ (y : ↥W),
    Eq.{u_1 + 1} (α := R)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_1} (RingHom.id R) (↥W) R) :
            (a : ↥W) → R)
          y :
        R)
      (0 : R)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx = 0
have simp : x = 0
Tactic: simp only [Submodule.mk_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' :
  ∀ (y : ↥W),
    Eq.{u_1 + 1} (α := R)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_1} (RingHom.id R) (↥W) R) :
            (a : ↥W) → R)
          y :
        R)
      (0 : R)
⊢ x = 0
have hx'₁ : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
Tactic: replace hx' : ∀ y ∈ W, B x y = 0 := by simpa [Subtype.forall] using hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ x ∈ W ⊓ B.ker
have refine : x ∈ (↑B.ker : Set M)
Tactic: refine ⟨hx, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ x ∈ (↑B.ker : Set M)
have h : ∀ (y : M),
  Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) ((0 : (a : M) → R) y : R)
Tactic: ext y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
y : M
⊢ ∃ u ∈ W, ∃ v ∈ B.ker, u + v = y
have rw : Membership.mem (γ := Submodule R M) ⊤ y
Tactic: rw [← Submodule.mem_sup, hW.sup_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
y : M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) ((0 : (a : M) → R) y : R)
have h : ∀ (u : M) (hu : u ∈ W) (v : M) (hv : v ∈ B.ker),
  Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (u + v) : R)
    ((0 : (a : M) → R) (u + v) : R)
Tactic: obtain ⟨u, hu, v, hv, rfl⟩ : ∃ u ∈ W, ∃ v ∈ ker B, u + v = y := by
      rw [← Submodule.mem_sup, hW.sup_eq_top]; exact Submodule.mem_top
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
u : M
hu : u ∈ W
v : M
hv : v ∈ B.ker
this : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) u : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (u + v) : R)
    ((0 : (a : M) → R) (u + v) : R)
have hv₁ : Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) v : M →ₗ[R] R) (0 : M →ₗ[R] R)
Tactic: rw [mem_ker] at hv
Cleared hypotheses: hv, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
u : M
hu : u ∈ W
v : M
hv : v ∈ B.ker
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (u + v) : R)
    ((0 : (a : M) → R) (u + v) : R)
have h : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) u : R) (0 : R)
Tactic: suffices B x u = 0 by rw [mem_ker] at hv; simpa [← hB.eq v, hv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ x = 0
have hx'₁ : x ∈ W ⊓ B.ker
Tactic: replace hx' : x ∈ W ⊓ ker B := by
    refine ⟨hx, ?_⟩
    ext y
    obtain ⟨u, hu, v, hv, rfl⟩ : ∃ u ∈ W, ∃ v ∈ ker B, u + v = y := by
      rw [← Submodule.mem_sup, hW.sup_eq_top]; exact Submodule.mem_top
    suffices B x u = 0 by rw [mem_ker] at hv; simpa [← hB.eq v, hv]
    exact hx' u hu
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
⊢ (B.domRestrict₁₂ W W).Nondegenerate
have rw : (B.domRestrict₁₂ W W).SeparatingLeft
Tactic: rw [(hB.domRestrict W).nondegenerate_iff_separatingLeft]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
b₁ :
  ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx = 0
have rw : Membership.mem (γ := Submodule R M) ⊥ x
Tactic: rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
b₁ :
  ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have refine : ∀ (y : M) (hy : y ∈ W), B.IsOrtho y x
Tactic: refine hW.le_bot ⟨hx, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
b₁ :
  ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := M₁)
      ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
              LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
            (a : ↥W) → M₁)
          y :
        M₁)
      (0 : M₁)
y : M
hy : y ∈ W
⊢ B.IsOrtho y x
have b₂ : Eq.{u_6 + 1} (α := M₁)
  ((((B.domRestrict₁₂ W W : (a : ↥W) → ↥W →ₗ[R] M₁) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) x hx) :
          LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (↥W) M₁) :
        (a : ↥W) → M₁)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ W) y hy) :
    M₁)
  (0 : M₁)
Tactic: specialize b₁ ⟨y, hy⟩
Cleared hypotheses: b₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : Eq.{u_6 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) x : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
⊢ B.IsOrtho y x
have rw : B.IsOrtho x y
Tactic: rw [hB.ortho_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
⊢ False
have refine : ∀ (m : M),
  Eq.{u_22 + 1} (α := M₁) ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) m : M₁)
    (0 : M₁)
Tactic: refine v.ne_zero i (hB (v i) fun m ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
m : M
⊢ Eq.{u_22 + 1} (α := M₁) ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) m : M₁)
    (0 : M₁)
have obtain : ∀ (vi : n →₀ R),
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
        ((v.repr.symm : (a : n →₀ R) → M) vi : M) :
      M₁)
    (0 : M₁)
Tactic: obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
        ((v.repr.symm : (a : n →₀ R) → M) vi : M) :
      M₁)
    (0 : M₁)
have rw : Eq.{u_22 + 1} (α := M₁)
  (∑ x ∈ vi.support,
    (((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
      (HSMul.hSMul.{u_20, u_21, u_21} (α := R) (β := M) ((vi : (a : n) → R) x : R) ((v : (a : n) → M) x : M)))
  0
Tactic: rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, map_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
⊢ Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      (((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
        (HSMul.hSMul.{u_20, u_21, u_21} (α := R) (β := M) ((vi : (a : n) → R) x : R) ((v : (a : n) → M) x : M)))
    0
have h₁ : ∀ x ∈ vi.support,
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
        (HSMul.hSMul.{u_20, u_21, u_21} (α := R) (β := M) ((vi : (a : n) → R) x : R) ((v : (a : n) → M) x : M)) :
      M₁)
    (0 : M₁)
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
j : n
⊢ Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁)
        (HSMul.hSMul.{u_20, u_21, u_21} (α := R) (β := M) ((vi : (a : n) → R) j : R) ((v : (a : n) → M) j : M)) :
      M₁)
    (0 : M₁)
have h₁ : HSMul.hSMul (α := R) (β := M₁) ((I' : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
      M₁) =
  0
Tactic: rw [map_smulₛₗ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
j : n
this :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
      M₁)
    (0 : M₁)
⊢ HSMul.hSMul (α := R) (β := M₁) ((I' : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
        M₁) =
    0
have rw : HSMul.hSMul (α := R) (β := M₁) ((I' : (a : R) → R) ((vi : (a : n) → R) j : R) : R) 0 = 0
Tactic: rw [this, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst_5 : Nontrivial R
v : Basis n R M
h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
hB : B.SeparatingLeft
i : n
ho : B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
j : n
this :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
      M₁)
    (0 : M₁)
rw : HSMul.hSMul (α := R) (β := M₁) ((I' : (a : R) → R) ((vi : (a : n) → R) j : R) : R) 0 = 0
⊢ HSMul.hSMul (α := R) (β := M₁) ((I' : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₛₗ[I'] M₁) ((v : (a : n) → M) i) : M →ₛₗ[I'] M₁) : (a : M) → M₁) ((v : (a : n) → M) j : M) :
        M₁) =
    0
have rw₁ : Eq.{u_22 + 1} (α := M₁) 0 0
Tactic: rw [this, smul_zero]