R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
m : M
hB : ∀ (y : M), ↑(↑B m) y = 0
⊢ m = 0
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingLeft B
intro m hB
case intro
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
⊢ ↑(LinearEquiv.symm v.repr) vi = 0
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
m : M
hB : ∀ (y : M), ↑(↑B m) y = 0
⊢ m = 0
obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
case intro
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
⊢ vi = 0
case intro
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
⊢ ↑(LinearEquiv.symm v.repr) vi = 0
rw [LinearEquiv.map_eq_zero_iff]
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
i : n
⊢ ↑vi i = ↑0 i
case intro
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
⊢ vi = 0
ext i
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
i : n
⊢ ↑vi i = 0
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
i : n
⊢ ↑vi i = ↑0 i
rw [Finsupp.zero_apply]
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) (↑v i) = 0
⊢ ↑vi i = 0
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
hB : ∀ (y : M), ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) y = 0
i : n
⊢ ↑vi i = 0
specialize hB (v i)
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
⊢ ↑vi i = 0
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ↑(↑B (↑(LinearEquiv.symm v.repr) vi)) (↑v i) = 0
⊢ ↑vi i = 0
simp_rw [Basis.repr_symm_apply, Finsupp.total_apply, Finsupp.sum, map_sum₂, map_smulₛₗ₂,
  smul_eq_mul] at hB
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
⊢ ↑vi i = 0

case intro.h.h₀
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
⊢ ∀ (b : n), b ∈ vi.support → b ≠ i → ↑(RingHom.id R) (↑vi b) * ↑(↑B (↑v b)) (↑v i) = 0

case intro.h.h₁
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
⊢ ¬i ∈ vi.support → ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
⊢ ↑vi i = 0
rw [Finset.sum_eq_single i] at hB
no goals
case intro.h
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
⊢ ↑vi i = 0
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (h i) hB
case intro.h.h₀
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
j : n
_hj : j ∈ vi.support
hij : j ≠ i
⊢ ↑(RingHom.id R) (↑vi j) * ↑(↑B (↑v j)) (↑v i) = 0
case intro.h.h₀
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
⊢ ∀ (b : n), b ∈ vi.support → b ≠ i → ↑(RingHom.id R) (↑vi b) * ↑(↑B (↑v b)) (↑v i) = 0
intro j _hj hij
case intro.h.h₀
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
j : n
_hj : j ∈ vi.support
hij : ↑(↑B (↑v j)) (↑v i) = 0
⊢ ↑(RingHom.id R) (↑vi j) * ↑(↑B (↑v j)) (↑v i) = 0
case intro.h.h₀
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
j : n
_hj : j ∈ vi.support
hij : j ≠ i
⊢ ↑(RingHom.id R) (↑vi j) * ↑(↑B (↑v j)) (↑v i) = 0
replace hij : B (v j) (v i) = 0 := hO hij
no goals
case intro.h.h₀
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
j : n
_hj : j ∈ vi.support
hij : ↑(↑B (↑v j)) (↑v i) = 0
⊢ ↑(RingHom.id R) (↑vi j) * ↑(↑B (↑v j)) (↑v i) = 0
rw [hij, RingHom.id_apply, mul_zero]
case intro.h.h₁
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
hi : ¬i ∈ vi.support
⊢ ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
case intro.h.h₁
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
⊢ ¬i ∈ vi.support → ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
intro hi
case intro.h.h₁
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
hi : ↑vi i = 0
⊢ ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
case intro.h.h₁
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
hi : ¬i ∈ vi.support
⊢ ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
replace hi : vi i = 0 := Finsupp.not_mem_support_iff.mp hi
no goals
case intro.h.h₁
R : Type u_1
R₁ : Type ?u.601671
R₂ : Type ?u.601674
R₃ : Type ?u.601677
M : Type u_2
M₁ : Type ?u.601683
M₂ : Type ?u.601686
Mₗ₁ : Type ?u.601689
Mₗ₁' : Type ?u.601692
Mₗ₂ : Type ?u.601695
Mₗ₂' : Type ?u.601698
K : Type ?u.601701
K₁ : Type ?u.601704
K₂ : Type ?u.601707
V : Type ?u.601710
V₁ : Type ?u.601713
V₂ : Type ?u.601716
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
i : n
hB : ∑ x in vi.support, ↑(RingHom.id R) (↑vi x) * ↑(↑B (↑v x)) (↑v i) = 0
hi : ↑vi i = 0
⊢ ↑(RingHom.id R) (↑vi i) * ↑(↑B (↑v i)) (↑v i) = 0
rw [hi, RingHom.id_apply, zero_mul]