case nil
ι : Type ?u.8615
α : Type ?u.8618
M : Type ?u.8621
N : Type ?u.8624
P : Type ?u.8627
M₀ : Type ?u.8630
G : Type ?u.8633
R : Type ?u.8636
L : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L → 1 ≤ i
h : ∀ (i : ℕ), i ∈ [] → 1 ≤ i
⊢ length [] ≤ sum []

case cons
ι : Type ?u.8615
α : Type ?u.8618
M : Type ?u.8621
N : Type ?u.8624
P : Type ?u.8627
M₀ : Type ?u.8630
G : Type ?u.8633
R : Type ?u.8636
L✝ : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L✝ → 1 ≤ i
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → length L ≤ sum L
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ length (j :: L) ≤ sum (j :: L)
ι : Type ?u.8615
α : Type ?u.8618
M : Type ?u.8621
N : Type ?u.8624
P : Type ?u.8627
M₀ : Type ?u.8630
G : Type ?u.8633
R : Type ?u.8636
L : List ℕ
h : ∀ (i : ℕ), i ∈ L → 1 ≤ i
⊢ length L ≤ sum L
induction' L with j L IH h
case cons
ι : Type ?u.8615
α : Type ?u.8618
M : Type ?u.8621
N : Type ?u.8624
P : Type ?u.8627
M₀ : Type ?u.8630
G : Type ?u.8633
R : Type ?u.8636
L✝ : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L✝ → 1 ≤ i
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → length L ≤ sum L
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + length L ≤ j + sum L
case cons
ι : Type ?u.8615
α : Type ?u.8618
M : Type ?u.8621
N : Type ?u.8624
P : Type ?u.8627
M₀ : Type ?u.8630
G : Type ?u.8633
R : Type ?u.8636
L✝ : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L✝ → 1 ≤ i
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → length L ≤ sum L
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ length (j :: L) ≤ sum (j :: L)
rw [sum_cons, length, add_comm]
no goals
case cons
ι : Type ?u.8615
α : Type ?u.8618
M : Type ?u.8621
N : Type ?u.8624
P : Type ?u.8627
M₀ : Type ?u.8630
G : Type ?u.8633
R : Type ?u.8636
L✝ : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L✝ → 1 ≤ i
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → length L ≤ sum L
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + length L ≤ j + sum L
exact add_le_add (h _ (mem_cons_self _ _)) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))
no goals
case nil
ι : Type ?u.8615
α : Type ?u.8618
M : Type ?u.8621
N : Type ?u.8624
P : Type ?u.8627
M₀ : Type ?u.8630
G : Type ?u.8633
R : Type ?u.8636
L : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L → 1 ≤ i
h : ∀ (i : ℕ), i ∈ [] → 1 ≤ i
⊢ length [] ≤ sum []
simp