R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
⊢ False
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
⊢ ¬IsOrtho B (↑v i) (↑v i)
intro ho
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
m : M
⊢ bilin B (↑v i) m = 0
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
⊢ False
refine' v.ne_zero i (hB (v i) fun m => _)
case intro
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ bilin B (↑v i) (↑(LinearEquiv.symm v.repr) vi) = 0
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
m : M
⊢ bilin B (↑v i) m = 0
obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
case intro
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∑ i_1 in vi.support, bilin B (↑v i) (↑vi i_1 • ↑v i_1) = 0
case intro
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ bilin B (↑v i) (↑(LinearEquiv.symm v.repr) vi) = 0
rw [Basis.repr_symm_apply, Finsupp.total_apply, Finsupp.sum, sum_right]
case intro.h
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∀ (x : n), x ∈ vi.support → bilin B (↑v i) (↑vi x • ↑v x) = 0
case intro
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∑ i_1 in vi.support, bilin B (↑v i) (↑vi i_1 • ↑v i_1) = 0
apply Finset.sum_eq_zero
case intro.h
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ bilin B (↑v i) (↑vi j • ↑v j) = 0
case intro.h
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∀ (x : n), x ∈ vi.support → bilin B (↑v i) (↑vi x • ↑v x) = 0
rintro j -
case intro.h
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑vi j * bilin B (↑v i) (↑v j) = 0
case intro.h
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ bilin B (↑v i) (↑vi j • ↑v j) = 0
rw [smul_right]
case h.e'_2.h.e'_6
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ bilin B (↑v i) (↑v j) = 0
case intro.h
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑vi j * bilin B (↑v i) (↑v j) = 0
convert MulZeroClass.mul_zero (vi j) using 2
case h.e'_2.h.e'_6.inl
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ bilin B (↑v i) (↑v i) = 0

case h.e'_2.h.e'_6.inr
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
hij : i ≠ j
⊢ bilin B (↑v i) (↑v j) = 0
case h.e'_2.h.e'_6
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ bilin B (↑v i) (↑v j) = 0
obtain rfl | hij := eq_or_ne i j
no goals
case h.e'_2.h.e'_6.inl
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ bilin B (↑v i) (↑v i) = 0
exact ho
no goals
case h.e'_2.h.e'_6.inr
R : Type u_1
M : Type u_2
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1495046
M₁ : Type ?u.1495049
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1495658
M₂ : Type ?u.1495661
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1495848
M₃ : Type ?u.1495851
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type ?u.1496439
K : Type ?u.1496442
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1497656
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
n : Type w
inst✝ : Nontrivial R
B : BilinForm R M
v : Basis n R M
h : iIsOrtho B ↑v
hB : Nondegenerate B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
hij : i ≠ j
⊢ bilin B (↑v i) (↑v j) = 0
exact h hij