awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f g : End K M
inst_3 : FiniteDimensional K M
inst_4 : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this_1 : Module.Finite K R
this_2 : Module.Finite R S
this_3 : Module.Finite K S
this_4 : IsArtinianRing R
this_5 : IsReduced R
this_6 : IsReduced S
φ : AlgHom.{u_3, u_3, u_2} K S (End K M) :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : Membership.mem (α := End K M) (γ := Subalgebra K (End K M)) K[f, g] ((φ : (a : S) → End K M) p : End K M)
refine_4 : Eq.{u_2 + 1} (α := End K M) ((φ.comp (aeval p) : (a : K[X]) → End K M) (minpoly K p) : End K M) (0 : End K M)
refine_4₁ :
  Eq.{u_2 + 1} (α := End K M) ((φ : (a : S) → End K M) ((aeval p : (a : K[X]) → S) (minpoly K p)) : End K M)
    (0 : End K M)
refine_4₂ : Eq.{u_2 + 1} (α := End K M) ((φ : (a : S) → End K M) 0) 0
⊢ Eq.{u_2 + 1} (α := End K M)
    (((aeval ((φ : (a : S) → End K M) p) : AlgHom.{u_3, u_3, u_2} K K[X] (End K M)) : (a : K[X]) → End K M)
        (minpoly K p) :
      End K M)
    (0 : End K M)
have refine_4₃ : Eq.{u_2 + 1} (α := End K M) 0 0
Tactic: rw [aeval_algHom, φ.comp_apply, minpoly.aeval, map_zero]
-- 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 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : CommSemiring R₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid M
inst_8 : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₂
⊢ Eq.{u_5 + 1} (α := M) (((B : (a : M₁) → M₂ →ₛₗ[I₂] M) 0 : (a : M₂) → M) x : M) (0 : M)
have rw : Eq.{u_5 + 1} (α := M) ((0 : (a : M₂) → M) x : M) (0 : M)
Tactic: rw [map_zero B, zero_apply]
-- 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 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : CommSemiring R₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₂ M₂
inst_7 : AddCommMonoid M
inst_8 : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₂
rw : Eq.{u_5 + 1} (α := M) ((0 : (a : M₂) → M) x : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) (((B : (a : M₁) → M₂ →ₛₗ[I₂] M) 0 : (a : M₂) → M) x : M) (0 : M)
have rw₁ : Eq.{u_5 + 1} (α := M) 0 0
Tactic: rw [map_zero B, zero_apply]
-- 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 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
x y : M₁
⊢ B.IsOrtho x y ↔ B.flip.IsOrtho y x
have simp_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.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) y : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) x : M) (0 : M)
Tactic: simp_rw [isOrtho_def, flip_apply]
-- 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
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v
have simp_rw : (∀ (i j : n),
    i ≠ j →
      Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
        (0 : M)) ↔
  ∀ (i j : n),
    i ≠ j →
      Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
        (0 : M)
Tactic: simp_rw [isOrthoᵢ_def]
-- 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
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) ↔
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)
have mp : (∀ (i j : n),
    i ≠ j →
      Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
        (0 : M)) →
  ∀ (i j : n),
    i ≠ j →
      Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
        (0 : M)
Tactic: constructor
-- 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
n : Type u_19
inst : CommSemiring R
inst_1 : CommSemiring R₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : AddCommMonoid M
inst_5 : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
mp :
  (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) →
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)
⊢ (∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M)
          (0 : M)) ↔
    ∀ (i j : n),
      i ≠ j →
        Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
          (0 : M)
have mpr : (∀ (i j : n),
    i ≠ j →
      Eq.{u_5 + 1} (α := M) ((((B.flip : (a : M₁) → M₁ →ₛₗ[I₁] M) (v i) : M₁ →ₛₗ[I₁] M) : (a : M₁) → M) (v j) : M)
        (0 : M)) →
  ∀ (i j : n),
    i ≠ j →
      Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₁'] M) (v i) : M₁ →ₛₗ[I₁'] M) : (a : M₁) → M) (v j) : M) (0 : M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V) ↔
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
have mp : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V) →
  Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
mp :
  Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V) →
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V) ↔
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
have mpr : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V) →
  Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
have mp : HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) a : K)
    ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) =
  0
Tactic: rw [map_smulₛₗ₂, H, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
mp :
  HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) a : K)
      ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) =
    0
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
have mp₁ : HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) a : K) 0 = 0
Tactic: rw [map_smulₛₗ₂, H, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
mp :
  HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) a : K)
      ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) =
    0
mp₁ : HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) a : K) 0 = 0
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
have mp₂ : Eq.{u_16 + 1} (α := V) 0 0
Tactic: rw [map_smulₛₗ₂, H, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) (a • x) : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
have H₁ : Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K) ∨
  Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
Tactic: rw [map_smulₛₗ₂, smul_eq_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H :
  Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K) ∨
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
have mpr : ∀ (H : Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K)),
  Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H :
  Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K) ∨
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
mpr :
  ∀ (H : Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K)),
    Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
have mpr₁ : ∀ (H : Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)),
  Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
inst_6 : Field K₂
inst_7 : AddCommGroup V₂
inst_8 : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) a : K) (0 : K)
⊢ Eq.{u_16 + 1} (α := V) ((((B : (a : V₁) → V₂ →ₛₗ[I₂] V) x : V₂ →ₛₗ[I₂] V) : (a : V₂) → V) y : V) (0 : V)
have H₁ : a = 0
Tactic: rw [map_eq_zero I₁] 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_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
⊢ LinearIndependent K₁ v
have rw : ∀ (s : Finset n) (g : n → K₁), Eq.{u_17 + 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.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
⊢ Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
have rw : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) 0 : (a : V₁) → V) (v i) : V) (0 : V)
Tactic: rw [hs, map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
rw : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) 0 : (a : V₁) → V) (v i) : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
have rw₁ : Eq.{u_16 + 1} (α := V) ((0 : (a : V₁) → V) (v i) : V) (0 : V)
Tactic: rw [hs, map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
rw : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) 0 : (a : V₁) → V) (v i) : V) (0 : V)
rw₁ : Eq.{u_16 + 1} (α := V) ((0 : (a : V₁) → V) (v i) : V) (0 : V)
⊢ Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
have rw₂ : Eq.{u_16 + 1} (α := V) 0 0
Tactic: rw [hs, map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
⊢ w i = 0
have this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
Tactic: have : B (s.sum fun i : n ↦ w i • v i) (v i) = 0 := by rw [hs, map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
⊢ ∑ j ∈ s,
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)
have apply : ∀ b ∈ s,
  b ≠ i →
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w b) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v b) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
      0
Tactic: apply Finset.sum_eq_single_of_mem i hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
j : n
_hj : j ∈ s
hij : j ≠ i
⊢ HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    0
have rw : HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K) 0 = 0
Tactic: rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
j : n
_hj : j ∈ s
hij : j ≠ i
rw : HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K) 0 = 0
⊢ HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    0
have rw₁ : Eq.{u_16 + 1} (α := V) 0 0
Tactic: rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
⊢ w i = 0
have hsum : ∑ j ∈ s,
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
  HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
    ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)
Tactic: have hsum : (s.sum fun j : n ↦ I₁ (w j) • B (v j) (v i)) = I₁ (w i) • B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _hj hij
      rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]