K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
this : ¬LinearIndependent K fun x => ↑x
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
have := mt finset_card_le_finrank_of_linearIndependent (by simpa using h)
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
this : ∃ s g, ∑ i in s, g i • ↑i = 0 ∧ ∃ i, i ∈ s ∧ g i ≠ 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
this : ¬LinearIndependent K fun x => ↑x
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
rw [not_linearIndependent_iff] at this
case intro.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
this : ∃ s g, ∑ i in s, g i • ↑i = 0 ∧ ∃ i, i ∈ s ∧ g i ≠ 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
obtain ⟨s, g, sum, z, zm, nonzero⟩ := this
case intro.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
case intro.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
let f : V → K := fun x => if h : x ∈ t then if (⟨x, h⟩ : t) ∈ s then g ⟨x, h⟩ else 0 else 0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∑ e in t, f e • e = 0

case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∃ x, x ∈ t ∧ f x ≠ 0
case intro.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∃ f, ∑ e in t, f e • e = 0 ∧ ∃ x, x ∈ t ∧ f x ≠ 0
refine' ⟨f, _, _⟩
no goals
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
⊢ ¬card ?m.324349 ≤ finrank ?m.324343 ?m.324344
simpa using h
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∑ e in t,
      (if h : e ∈ t then if { val := e, property := h } ∈ s then g { val := e, property := h } else 0 else 0) • e =
    0
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∑ e in t, f e • e = 0
dsimp
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∑ e in t,
      (if h : e ∈ t then if { val := e, property := h } ∈ s then g { val := e, property := h } else 0 else 0) • e =
    ∑ i in s, g i • ↑i
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∑ e in t,
      (if h : e ∈ t then if { val := e, property := h } ∈ s then g { val := e, property := h } else 0 else 0) • e =
    0
rw [← (sum)]
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∀ (a : V) (h₁ : a ∈ t),
    (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a ≠ 0 →
      { val := a, property := h₁ } ∈ s

case intro.intro.intro.intro.intro.refine'_1.i_inj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∀ (a₁ a₂ : V) (h₁₁ : a₁ ∈ t),
    (if h : a₁ ∈ t then if { val := a₁, property := h } ∈ s then g { val := a₁, property := h } else 0 else 0) • a₁ ≠
        0 →
      ∀ (h₂₁ : a₂ ∈ t),
        (if h : a₂ ∈ t then if { val := a₂, property := h } ∈ s then g { val := a₂, property := h } else 0 else 0) •
              a₂ ≠
            0 →
          { val := a₁, property := h₁₁ } = { val := a₂, property := h₂₁ } → a₁ = a₂

case intro.intro.intro.intro.intro.refine'_1.i_surj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∀ (b : { v // v ∈ t }), b ∈ s → g b • ↑b ≠ 0 → ∃ a h₁ h₂, b = { val := a, property := h₁ }

case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∀ (a : V) (h₁ : a ∈ t),
    (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a ≠ 0 →
      (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a =
        g { val := a, property := h₁ } • ↑{ val := a, property := h₁ }
case intro.intro.intro.intro.intro.refine'_1
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∑ e in t,
      (if h : e ∈ t then if { val := e, property := h } ∈ s then g { val := e, property := h } else 0 else 0) • e =
    ∑ i in s, g i • ↑i
fapply sum_bij_ne_zero fun v hvt _ => (⟨v, hvt⟩ : { v // v ∈ t })
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
v : V
hvt : v ∈ t
H : (if h : v ∈ t then if { val := v, property := h } ∈ s then g { val := v, property := h } else 0 else 0) • v ≠ 0
⊢ { val := v, property := hvt } ∈ s
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∀ (a : V) (h₁ : a ∈ t),
    (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a ≠ 0 →
      { val := a, property := h₁ } ∈ s
intro v hvt H
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
v : V
hvt : v ∈ t
H : (if h : v ∈ t then if { val := v, property := h } ∈ s then g { val := v, property := h } else 0 else 0) • v ≠ 0
⊢ { val := v, property := hvt } ∈ s
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
v : V
hvt : v ∈ t
H : (if h : v ∈ t then if { val := v, property := h } ∈ s then g { val := v, property := h } else 0 else 0) • v ≠ 0
⊢ { val := v, property := hvt } ∈ s
dsimp
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
v : V
hvt : v ∈ t
H : (if { val := v, property := hvt } ∈ s then g { val := v, property := hvt } else 0) • v ≠ 0
⊢ { val := v, property := hvt } ∈ s
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
v : V
hvt : v ∈ t
H : (if h : v ∈ t then if { val := v, property := h } ∈ s then g { val := v, property := h } else 0 else 0) • v ≠ 0
⊢ { val := v, property := hvt } ∈ s
rw [dif_pos hvt] at H
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
v : V
hvt : v ∈ t
H : ¬{ val := v, property := hvt } ∈ s
⊢ (if { val := v, property := hvt } ∈ s then g { val := v, property := hvt } else 0) • v = 0
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
v : V
hvt : v ∈ t
H : (if { val := v, property := hvt } ∈ s then g { val := v, property := hvt } else 0) • v ≠ 0
⊢ { val := v, property := hvt } ∈ s
contrapose! H
no goals
case intro.intro.intro.intro.intro.refine'_1.hi
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
v : V
hvt : v ∈ t
H : ¬{ val := v, property := hvt } ∈ s
⊢ (if { val := v, property := hvt } ∈ s then g { val := v, property := hvt } else 0) • v = 0
rw [if_neg H, zero_smul]
case intro.intro.intro.intro.intro.refine'_1.i_inj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a₁✝ a₂✝ : V
h₁₁✝ : a₁✝ ∈ t
h₁₂✝ :
  (if h : a₁✝ ∈ t then if { val := a₁✝, property := h } ∈ s then g { val := a₁✝, property := h } else 0 else 0) • a₁✝ ≠
    0
h₂₁✝ : a₂✝ ∈ t
h₂₂✝ :
  (if h : a₂✝ ∈ t then if { val := a₂✝, property := h } ∈ s then g { val := a₂✝, property := h } else 0 else 0) • a₂✝ ≠
    0
⊢ { val := a₁✝, property := h₁₁✝ } = { val := a₂✝, property := h₂₁✝ } → a₁✝ = a₂✝
case intro.intro.intro.intro.intro.refine'_1.i_inj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∀ (a₁ a₂ : V) (h₁₁ : a₁ ∈ t),
    (if h : a₁ ∈ t then if { val := a₁, property := h } ∈ s then g { val := a₁, property := h } else 0 else 0) • a₁ ≠
        0 →
      ∀ (h₂₁ : a₂ ∈ t),
        (if h : a₂ ∈ t then if { val := a₂, property := h } ∈ s then g { val := a₂, property := h } else 0 else 0) •
              a₂ ≠
            0 →
          { val := a₁, property := h₁₁ } = { val := a₂, property := h₂₁ } → a₁ = a₂
intro _ _ _ _ _ _
no goals
case intro.intro.intro.intro.intro.refine'_1.i_inj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a₁✝ a₂✝ : V
h₁₁✝ : a₁✝ ∈ t
h₁₂✝ :
  (if h : a₁✝ ∈ t then if { val := a₁✝, property := h } ∈ s then g { val := a₁✝, property := h } else 0 else 0) • a₁✝ ≠
    0
h₂₁✝ : a₂✝ ∈ t
h₂₂✝ :
  (if h : a₂✝ ∈ t then if { val := a₂✝, property := h } ∈ s then g { val := a₂✝, property := h } else 0 else 0) • a₂✝ ≠
    0
⊢ { val := a₁✝, property := h₁₁✝ } = { val := a₂✝, property := h₂₁✝ } → a₁✝ = a₂✝
exact Subtype.mk.inj
case intro.intro.intro.intro.intro.refine'_1.i_surj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
b : { v // v ∈ t }
hbs : b ∈ s
hb : g b • ↑b ≠ 0
⊢ ∃ a h₁ h₂, b = { val := a, property := h₁ }
case intro.intro.intro.intro.intro.refine'_1.i_surj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∀ (b : { v // v ∈ t }), b ∈ s → g b • ↑b ≠ 0 → ∃ a h₁ h₂, b = { val := a, property := h₁ }
intro b hbs hb
case intro.intro.intro.intro.intro.refine'_1.i_surj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
b : { v // v ∈ t }
hbs : b ∈ s
hb : g b • ↑b ≠ 0
⊢ ∃ h₁ h₂, b = { val := ↑b, property := h₁ }
case intro.intro.intro.intro.intro.refine'_1.i_surj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
b : { v // v ∈ t }
hbs : b ∈ s
hb : g b • ↑b ≠ 0
⊢ ∃ a h₁ h₂, b = { val := a, property := h₁ }
use b
no goals
case intro.intro.intro.intro.intro.refine'_1.i_surj
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
b : { v // v ∈ t }
hbs : b ∈ s
hb : g b • ↑b ≠ 0
⊢ ∃ h₁ h₂, b = { val := ↑b, property := h₁ }
simpa only [hbs, exists_prop, dif_pos, Finset.mk_coe, and_true_iff, if_true, Finset.coe_mem,
  eq_self_iff_true, exists_prop_of_true, Ne.def] using hb
case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
⊢ (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a ≠ 0 →
    (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a =
      g { val := a, property := h₁ } • ↑{ val := a, property := h₁ }
case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∀ (a : V) (h₁ : a ∈ t),
    (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a ≠ 0 →
      (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a =
        g { val := a, property := h₁ } • ↑{ val := a, property := h₁ }
intro a h₁
case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
⊢ ¬(if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a = 0 →
    (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a =
      g { val := a, property := h₁ } • a
case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
⊢ (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a ≠ 0 →
    (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a =
      g { val := a, property := h₁ } • ↑{ val := a, property := h₁ }
dsimp
case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
⊢ ¬(if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a = 0 →
    (if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a =
      g { val := a, property := h₁ } • a
case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
⊢ ¬(if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a = 0 →
    (if h : a ∈ t then if { val := a, property := h } ∈ s then g { val := a, property := h } else 0 else 0) • a =
      g { val := a, property := h₁ } • a
rw [dif_pos h₁]
case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
h₂ : ¬(if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a = 0
⊢ (if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a =
    g { val := a, property := h₁ } • a
case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
⊢ ¬(if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a = 0 →
    (if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a =
      g { val := a, property := h₁ } • a
intro h₂
case intro.intro.intro.intro.intro.refine'_1.h.hc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
h₂ : ¬(if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a = 0
⊢ { val := a, property := h₁ } ∈ s
case intro.intro.intro.intro.intro.refine'_1.h
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
h₂ : ¬(if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a = 0
⊢ (if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a =
    g { val := a, property := h₁ } • a
rw [if_pos]
case intro.intro.intro.intro.intro.refine'_1.h.hc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
h₂ : ¬{ val := a, property := h₁ } ∈ s
⊢ (if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a = 0
case intro.intro.intro.intro.intro.refine'_1.h.hc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
h₂ : ¬(if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a = 0
⊢ { val := a, property := h₁ } ∈ s
contrapose! h₂
no goals
case intro.intro.intro.intro.intro.refine'_1.h.hc
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
a : V
h₁ : a ∈ t
h₂ : ¬{ val := a, property := h₁ } ∈ s
⊢ (if { val := a, property := h₁ } ∈ s then g { val := a, property := h₁ } else 0) • a = 0
rw [if_neg h₂, zero_smul]
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ f ↑z ≠ 0
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ ∃ x, x ∈ t ∧ f x ≠ 0
refine' ⟨z, z.2, _⟩
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ (if h : ↑z ∈ t then if { val := ↑z, property := h } ∈ s then g { val := ↑z, property := h } else 0 else 0) ≠ 0
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ f ↑z ≠ 0
dsimp only
no goals
case intro.intro.intro.intro.intro.refine'_2
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
t : Finset V
h : finrank K V < card t
s : Finset { x // x ∈ t }
g : { x // x ∈ t } → K
sum : ∑ i in s, g i • ↑i = 0
z : { x // x ∈ t }
zm : z ∈ s
nonzero : g z ≠ 0
f : V → K :=
  fun x => if h : x ∈ t then if { val := x, property := h } ∈ s then g { val := x, property := h } else 0 else 0
⊢ (if h : ↑z ∈ t then if { val := ↑z, property := h } ∈ s then g { val := ↑z, property := h } else 0 else 0) ≠ 0
erw [dif_pos z.2, if_pos] <;> rwa [Subtype.coe_eta]