-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {n : Type w} [Nontrivial R]
    [NoZeroDivisors R] (B : BilinForm R M) (v : Basis n R M) (hO : B.iIsOrtho v) :
    B.Nondegenerate ↔ ∀ i, ¬B.IsOrtho (v i) (v i)

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0
⊢ v.repr.symm vi = 0

Tactic:
rw [LinearEquiv.map_eq_zero_iff]

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0
⊢ vi = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
⊢ B.Nondegenerate ↔ ∀ (i : n), ¬B.IsOrtho (v i) (v i)

Tactic:
refine ⟨hO.not_isOrtho_basis_self_of_nondegenerate, fun ho m hB => ?_⟩

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
m : M
hB : ∀ (n : M), (B m) n = 0
⊢ m = 0

Proof state:
case intro.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : vi i * (B (v i)) (v i) = 0
⊢ vi i = 0

Tactic:
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (ho i) hB

Result:
no goals

Proof state:
case intro.h.h₁
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0
⊢ i ∉ vi.support → vi i * (B (v i)) (v i) = 0

Tactic:
intro hi

Result:
case intro.h.h₁
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0
hi : i ∉ vi.support
⊢ vi i * (B (v i)) (v i) = 0

Proof state:
case h.e'_2.h.e'_6
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0
j : n
a✝ : j ∈ vi.support
hij : j ≠ i
⊢ (B (v j)) (v i) = 0

Tactic:
exact hO hij

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0
⊢ vi = 0

Tactic:
ext i

Result:
case intro.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0
i : n
⊢ vi i = 0 i

Proof state:
case h.e'_2.h.e'_5
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0
hi : i ∉ vi.support
⊢ vi i = 0

Tactic:
exact Finsupp.not_mem_support_iff.mp hi

Result:
no goals

Proof state:
case intro.h.h₀
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0
⊢ ∀ b ∈ vi.support, b ≠ i → vi b * (B (v b)) (v i) = 0

Tactic:
intro j _ hij

Result:
case intro.h.h₀
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0
j : n
a✝ : j ∈ vi.support
hij : j ≠ i
⊢ vi j * (B (v j)) (v i) = 0

Proof state:
case intro.h.h₀
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0
j : n
a✝ : j ∈ vi.support
hij : j ≠ i
⊢ vi j * (B (v j)) (v i) = 0

Tactic:
convert mul_zero (vi j) using 2

Result:
case h.e'_2.h.e'_6
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0
j : n
a✝ : j ∈ vi.support
hij : j ≠ i
⊢ (B (v j)) (v i) = 0

Proof state:
case intro.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : (B (v.repr.symm vi)) (v i) = 0
⊢ vi i = 0

Tactic:
simp_rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, sum_left,
         smul_left] at hB

Result:
case intro.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0
⊢ vi i = 0

Proof state:
case intro.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0
i : n
⊢ vi i = 0 i

Tactic:
rw [Finsupp.zero_apply]

Result:
case intro.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
n : Type w
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
B : BilinForm R M
v : Basis n R M
hO : B.iIsOrtho ⇑v
ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0
i : n
⊢ vi i = 0