awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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 h₁ : 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₁)
Tactic: suffices B (v i) (v j) = 0 by 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
⊢ 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₁)
have h₁ : 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) i : M) : M₁)
  (0 : M₁)
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j
-- 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
h₁ :
  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) i : M) :
      M₁)
    (0 : M₁)
⊢ 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₁)
have h₂ : ∀ (hij : i ≠ j),
  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₁)
Tactic: obtain rfl | hij := eq_or_ne i j
-- 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.SeparatingRight
i : n
⊢ ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
have rw : ∀ (h : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)) (hB : B.SeparatingRight) (i : n),
  ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
Tactic: rw [isOrthoᵢ_flip] at h
Cleared hypotheses: h, hB, i
-- 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.flip (⇑v : (a : n) → M)
hB : B.SeparatingRight
i : n
⊢ ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
have rw : ¬B.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
Tactic: rw [isOrtho_flip]
-- 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
m : M
hB : ∀ (y : M), Eq.{u_22 + 1} (α := M₁) ((((B : (a : M) → M →ₗ[R] M₁) m : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
⊢ m = 0
have obtain : ∀ (vi : n →₀ R)
  (hB :
    ∀ (y : M),
      Eq.{u_22 + 1} (α := M₁)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁)
        (0 : M₁)),
  Eq.{u_21 + 1} (α := M) ((v.repr.symm : (a : n →₀ R) → M) vi : M) (0 : M)
Tactic: obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
Cleared hypotheses: m, hB
-- 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
hB :
  ∀ (y : M),
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
⊢ Eq.{u_21 + 1} (α := M) ((v.repr.symm : (a : n →₀ R) → M) vi : M) (0 : M)
have rw : vi = 0
Tactic: rw [LinearEquiv.map_eq_zero_iff]
-- 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
hB :
  ∀ (y : M),
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
⊢ vi = 0
have h₁ : ∀ (i : n), Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) ((0 : (a : n) → R) i : R)
Tactic: ext i
-- 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
hB :
  ∀ (y : M),
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
i : n
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) ((0 : (a : n) → R) i : R)
have h₁ : Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
Tactic: rw [Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
hB :
  ∀ (y : M),
    Eq.{u_22 + 1} (α := M₁)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁) y : M₁) (0 : M₁)
i : n
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
have hB₁ : Eq.{u_22 + 1} (α := M₁)
  ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁)
      ((v : (a : n) → M) i : M) :
    M₁)
  (0 : M₁)
Tactic: specialize hB (v i)
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₗ[R] M₁) ((v.repr.symm : (a : n →₀ R) → M) vi) : M →ₗ[R] M₁) : (a : M) → M₁)
        ((v : (a : n) → M) i : M) :
      M₁)
    (0 : M₁)
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
have hB₁ : Eq.{u_22 + 1} (α := M₁)
  (∑ x ∈ vi.support,
    HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) : M₁))
  0
Tactic: simp_rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂,
           map_smulₛₗ₂] at hB
Cleared hypotheses: hB
-- 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
have h₁ : ∀
  (hB :
    HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁) =
      0),
  Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
Tactic: rw [Finset.sum_eq_single i] at hB
Cleared hypotheses: hB
-- 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
h₁ :
  ∀
    (hB :
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
          ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
            M₁) =
        0),
    Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
have h₂ : ∀ b ∈ vi.support,
  b ≠ i →
    HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) b : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) b) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁) =
      0
Tactic: rw [Finset.sum_eq_single i] at hB
-- 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
h₁ :
  ∀
    (hB :
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
          ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
            M₁) =
        0),
    Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
h₂ :
  ∀ b ∈ vi.support,
    b ≠ i →
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) b : R) : R)
          ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) b) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
            M₁) =
        0
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
have h₃ : i ∉ vi.support →
  HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
Tactic: rw [Finset.sum_eq_single i] at hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
j : n
_hj : j ∈ vi.support
hij : j ≠ i
⊢ HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
have hij₁ : Eq.{u_22 + 1} (α := M₁)
  ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) : M₁)
  (0 : M₁)
Tactic: replace hij : B (v j) (v i) = 0 := hO hij
Cleared hypotheses: hij
-- 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
j : n
_hj : j ∈ vi.support
hij :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) : M₁)
    (0 : M₁)
⊢ HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
have h₁ : HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) j : R) : R) 0 = 0
Tactic: rw [hij, RingHom.id_apply, 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
j : n
_hj : j ∈ vi.support
hij :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) : M₁)
    (0 : M₁)
h₁ : HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) j : R) : R) 0 = 0
⊢ HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
have h₂ : HSMul.hSMul.{u_20, u_22, u_22} (α := R) (β := M₁) ((vi : (a : n) → R) j : R) 0 = 0
Tactic: rw [hij, RingHom.id_apply, 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
j : n
_hj : j ∈ vi.support
hij :
  Eq.{u_22 + 1} (α := M₁)
    ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) : M₁)
    (0 : M₁)
h₁ : HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) j : R) : R) 0 = 0
h₂ : HSMul.hSMul.{u_20, u_22, u_22} (α := R) (β := M₁) ((vi : (a : n) → R) j : R) 0 = 0
⊢ HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) j : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) j) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
have h₃ : Eq.{u_22 + 1} (α := M₁) 0 0
Tactic: rw [hij, RingHom.id_apply, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
hi : i ∉ vi.support
⊢ HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
have hi₁ : Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
Tactic: replace hi : vi i = 0 := Finsupp.notMem_support_iff.mp hi
Cleared hypotheses: hi
-- 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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
hi : Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
⊢ HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
have h₁ : HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) 0 : R)
    ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) : M₁) =
  0
Tactic: rw [hi, RingHom.id_apply, zero_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₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
hi : Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
h₁ :
  HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) 0 : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
⊢ HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
have h₂ : HSMul.hSMul.{u_20, u_22, u_22} (α := R) (β := M₁) 0
    ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) : M₁) =
  0
Tactic: rw [hi, RingHom.id_apply, zero_smul]