-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem wcovBy_span_singleton_sup (x : V) (s : Submodule K V) : WCovBy s ((K ∙ x) ⊔ s)

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
⊢ span K {x} ⊔ s ≤ q

Tactic:
rcases SetLike.exists_of_lt hpq with ⟨y, hyq, hyp⟩

Result:
case intro.intro
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
y : V
hyq : y ∈ q
hyp : y ∉ s
⊢ span K {x} ⊔ s ≤ q

Proof state:
case intro.intro.intro.intro.intro.inr
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ span K {x} ⊔ s ≤ q

Tactic:
have : x ∈ q := by
  rwa [q.add_mem_iff_left (hpq.le hz), q.smul_mem_iff hc] at hyq

Result:
case intro.intro.intro.intro.intro.inr
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
this : x ∈ q
⊢ span K {x} ⊔ s ≤ q

Proof state:
case intro.intro
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
y : V
hyq : y ∈ q
hyp : y ∉ s
⊢ span K {x} ⊔ s ≤ q

Tactic:
obtain ⟨c, z, hz, rfl⟩ : ∃ c : K, ∃ z ∈ s, c • x + z = y := by
  simpa [mem_sup, mem_span_singleton] using hqp.le hyq

Result:
case intro.intro.intro.intro.intro
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
⊢ span K {x} ⊔ s ≤ q

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s : Submodule K V
⊢ s ⩿ span K {x} ⊔ s

Tactic:
refine ⟨le_sup_right, fun q hpq hqp ↦ hqp.not_le ?_⟩

Result:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
⊢ span K {x} ⊔ s ≤ q

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ x ∈ q

Tactic:
rwa [q.add_mem_iff_left (hpq.le hz), q.smul_mem_iff hc] at hyq

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
⊢ span K {x} ⊔ s ≤ q

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Result:
case intro.intro.intro.intro.intro.inl
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
z : V
hz : z ∈ s
hyq : 0 • x + z ∈ q
hyp : 0 • x + z ∉ s
⊢ span K {x} ⊔ s ≤ q

case intro.intro.intro.intro.intro.inr
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
⊢ span K {x} ⊔ s ≤ q

Proof state:
case intro.intro.intro.intro.intro.inl
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
z : V
hz : z ∈ s
hyq : 0 • x + z ∈ q
hyp : 0 • x + z ∉ s
⊢ span K {x} ⊔ s ≤ q

Tactic:
simp [hz] at hyp

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.inr
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
hc : c ≠ 0
this : x ∈ q
⊢ span K {x} ⊔ s ≤ q

Tactic:
simp [hpq.le, this]

Result:
no goals

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < span K {x} ⊔ s
y : V
hyq : y ∈ q
hyp : y ∉ s
⊢ ∃ c, ∃ z ∈ s, c • x + z = y

Tactic:
simpa [mem_sup, mem_span_singleton] using hqp.le hyq

Result:
no goals