-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self [NoZeroSMulDivisors R M₁]
    {B : M →ₗ[R] M →ₗ[R] M₁} (v : Basis n R M) (hO : B.IsOrthoᵢ v)
    (h : ∀ i, ¬B.IsOrtho (v i) (v i)) : B.SeparatingLeft

Proof state:
case intro.h.h₀
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ 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

Tactic:
rw [hij, RingHom.id_apply, smul_zero]

Result:
no goals

Proof state:
case intro.h
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
⊢ vi i = 0

Tactic:
rw [Finset.sum_eq_single i] at hB

Result:
case intro.h
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (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
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
⊢ ∀ b ∈ vi.support, b ≠ i → (RingHom.id R) (vi b) • (B (v b)) (v i) = 0

case intro.h.h₁
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ 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

Proof state:
case intro.h
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (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, map_sum₂,
         map_smulₛₗ₂] at hB

Result:
case intro.h
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
⊢ vi i = 0

Proof state:
case intro
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0
⊢ v.repr.symm vi = 0

Tactic:
rw [LinearEquiv.map_eq_zero_iff]

Result:
case intro
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0
⊢ vi = 0

Proof state:
case intro.h.h₀
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ 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

Tactic:
replace hij : B (v j) (v i) = 0 := hO hij

Result:
case intro.h.h₀
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ 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

Proof state:
case intro.h
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0
i : n
⊢ vi i = 0 i

Tactic:
rw [Finsupp.zero_apply]

Result:
case intro.h
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0
i : n
⊢ vi i = 0

Proof state:
case intro.h.h₀
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
⊢ ∀ b ∈ vi.support, b ≠ i → (RingHom.id R) (vi b) • (B (v b)) (v i) = 0

Tactic:
intro j _hj hij

Result:
case intro.h.h₀
R : Type u_1
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M₁
inst✝ : NoZeroSMulDivisors R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
vi : n →₀ R
i : n
hB : ∑ x ∈ 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