case intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → { x // x ∈ S }) → κ), ∃ l, Line.IsMono C l
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
obtain ⟨ι, _inst, hι⟩ := Line.exists_mono_in_high_dimension S κ
case intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → { x // x ∈ S }) → κ), ∃ l, Line.IsMono C l
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
case intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → { x // x ∈ S }) → κ), ∃ l, Line.IsMono C l
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
skip
case intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∃ l, Line.IsMono (fun v => C (∑ i : ι, ↑(v i))) l
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
case intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∀ (C : (ι → { x // x ∈ S }) → κ), ∃ l, Line.IsMono C l
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
specialize hι fun v => C <| ∑ i, v i
case intro.intro.intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
case intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
hι : ∃ l, Line.IsMono (fun v => C (∑ i : ι, ↑(v i))) l
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
obtain ⟨l, c, hl⟩ := hι
case intro.intro.intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
case intro.intro.intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
set s : Finset ι :=  Finset.univ.filter (fun i => l.idxFun i = none ) with hs
case intro.intro.intro.intro.refine'_1
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ Exists.choose (_ : ∃ i, Line.idxFun l i = none) ∈ s

case intro.intro.intro.intro.refine'_2
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
i : ι
⊢ { x // x ∈ S } → M

case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ ∀ (s_1 : M),
    s_1 ∈ S → C (Finset.card s • s_1 + ∑ i in sᶜ, Option.getD (Option.map (?m.28895 i) (Line.idxFun l i)) 0) = c
case intro.intro.intro.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ ∃ a, a > 0 ∧ ∃ b c, ∀ (s : M), s ∈ S → C (a • s + b) = c
refine'
  ⟨s.card, Finset.card_pos.mpr ⟨l.proper.choose, _⟩, ∑ i in sᶜ, ((l.idxFun i).map _).getD 0,
    c, _⟩
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ C (Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) = c
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ ∀ (s_1 : M),
    s_1 ∈ S → C (Finset.card s • s_1 + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) = c
intro x xs
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ C (Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) =
    (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs })
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ C (Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) = c
rw [← hl ⟨x, xs⟩]
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ C (Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) =
    (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs })
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ C (Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) =
    (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs })
clear hl
case intro.intro.intro.intro.refine'_3.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ∑ i : ι, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
case intro.intro.intro.intro.refine'_3
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ C (Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0) =
    (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs })
congr
case intro.intro.intro.intro.refine'_3.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ∑ i in s, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i) +
      ∑ i in sᶜ, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
case intro.intro.intro.intro.refine'_3.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ∑ i : ι, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
rw [← Finset.sum_add_sum_compl s]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ Finset.card s • x = ∑ i in s, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)

case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ∑ i in sᶜ, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
case intro.intro.intro.intro.refine'_3.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ Finset.card s • x + ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ∑ i in s, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i) +
      ∑ i in sᶜ, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
congr 1
case intro.intro.intro.intro.refine'_1
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ Exists.choose (_ : ∃ i, Line.idxFun l i = none) ∈ Finset.univ ∧
    Line.idxFun l (Exists.choose (_ : ∃ i, Line.idxFun l i = none)) = none
case intro.intro.intro.intro.refine'_1
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ Exists.choose (_ : ∃ i, Line.idxFun l i = none) ∈ s
rw [hs, Finset.mem_filter]
no goals
case intro.intro.intro.intro.refine'_1
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
⊢ Exists.choose (_ : ∃ i, Line.idxFun l i = none) ∈ Finset.univ ∧
    Line.idxFun l (Exists.choose (_ : ∃ i, Line.idxFun l i = none)) = none
exact ⟨Finset.mem_univ _, l.proper.choose_spec⟩
no goals
case intro.intro.intro.intro.refine'_2
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
hl : ∀ (x : { x // x ∈ S }), (fun v => C (∑ i : ι, ↑(v i))) ((fun x i => Option.getD (Line.idxFun l i) x) x) = c
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
i : ι
⊢ { x // x ∈ S } → M
exact fun m => m
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∑ _x in s, x = ∑ i in s, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ Finset.card s • x = ∑ i in s, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
rw [← Finset.sum_const]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∀ (x_1 : ι), x_1 ∈ s → x = ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } x_1)
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∑ _x in s, x = ∑ i in s, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
apply Finset.sum_congr rfl
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ s
⊢ x = ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∀ (x_1 : ι), x_1 ∈ s → x = ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } x_1)
intro i hi
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ Line.idxFun l i = none
⊢ x = ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ s
⊢ x = ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
rw [hs, Finset.mem_filter] at hi
no goals
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ Line.idxFun l i = none
⊢ x = ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
rw [l.apply_none _ _ hi.right, Subtype.coe_mk]
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∀ (x_1 : ι),
    x_1 ∈ sᶜ →
      Option.getD (Option.map (fun m => ↑m) (Line.idxFun l x_1)) 0 =
        ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } x_1)
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∑ i in sᶜ, Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ∑ i in sᶜ, ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
apply Finset.sum_congr rfl
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ sᶜ
⊢ Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
⊢ ∀ (x_1 : ι),
    x_1 ∈ sᶜ →
      Option.getD (Option.map (fun m => ↑m) (Line.idxFun l x_1)) 0 =
        ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } x_1)
intro i hi
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ ¬Line.idxFun l i = none
⊢ Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ sᶜ
⊢ Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
rw [hs, Finset.compl_filter, Finset.mem_filter] at hi
case intro.intro.intro.intro.refine'_3.e_a.e_a.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ ¬Line.idxFun l i = none
y : { x // x ∈ S }
hy : some y = Line.idxFun l i
⊢ Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
case intro.intro.intro.intro.refine'_3.e_a.e_a
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ ¬Line.idxFun l i = none
⊢ Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
obtain ⟨y, hy⟩ := Option.ne_none_iff_exists.mp hi.right
no goals
case intro.intro.intro.intro.refine'_3.e_a.e_a.intro
M : Type u_1
κ : Type u_2
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line { x // x ∈ S } ι
c : κ
s : Finset ι := Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
hs : s = Finset.filter (fun i => Line.idxFun l i = none) Finset.univ
x : M
xs : x ∈ S
i : ι
hi : i ∈ Finset.univ ∧ ¬Line.idxFun l i = none
y : { x // x ∈ S }
hy : some y = Line.idxFun l i
⊢ Option.getD (Option.map (fun m => ↑m) (Line.idxFun l i)) 0 =
    ↑((fun x i => Option.getD (Line.idxFun l i) x) { val := x, property := xs } i)
simp_rw [← hy, Option.map_some', Option.getD]