-- 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
hi : i ∉ vi.support
⊢ (RingHom.id R) (vi i) • (B (v i)) (v i) = 0

Tactic:
replace hi : vi i = 0 := Finsupp.not_mem_support_iff.mp hi

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
hi : vi i = 0
⊢ (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
hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0
i : n
⊢ vi i = 0

Tactic:
specialize hB (v i)

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 : (B (v.repr.symm vi)) (v i) = 0
⊢ vi i = 0

Proof state:
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)
⊢ B.SeparatingLeft

Tactic:
intro m hB

Result:
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)
m : M
hB : ∀ (y : M), (B m) y = 0
⊢ m = 0

Proof state:
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)
m : M
hB : ∀ (y : M), (B m) y = 0
⊢ m = 0

Tactic:
obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m

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
⊢ v.repr.symm 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
⊢ i ∉ vi.support → (RingHom.id R) (vi i) • (B (v i)) (v i) = 0

Tactic:
intro hi

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
hi : i ∉ vi.support
⊢ (RingHom.id R) (vi i) • (B (v i)) (v 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
hi : vi i = 0
⊢ (RingHom.id R) (vi i) • (B (v i)) (v i) = 0

Tactic:
rw [hi, RingHom.id_apply, zero_smul]

Result:
no goals

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
⊢ vi = 0

Tactic:
ext i

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 i

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 : (RingHom.id R) (vi i) • (B (v i)) (v i) = 0
⊢ vi i = 0

Tactic:
exact (smul_eq_zero.mp hB).elim _root_.id (h i).elim

Result:
no goals