α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ length ((a :: as) {0 ↦ a✝}) = length (a :: as)

α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ 0 + 1 ≤ length (a :: as)
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ length ((a :: as) {0 ↦ a✝}) = max (length (a :: as)) (0 + 1)
rw [max_eq_left]
no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ length ((a :: as) {0 ↦ a✝}) = length (a :: as)
rfl
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ 1 ≤ Nat.succ (length as)
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ 0 + 1 ≤ length (a :: as)
simp [Nat.le_add_right]
no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a : α
as : List α
⊢ 1 ≤ Nat.succ (length as)
exact Nat.succ_le_succ (Nat.zero_le _)
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
m : ℕ
this : length ([] {m ↦ a}) = max (length []) (m + 1)
⊢ length ([] {m + 1 ↦ a}) = max (length []) (m + 1 + 1)
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
m : ℕ
⊢ length ([] {m + 1 ↦ a}) = max (length []) (m + 1 + 1)
have := @length_set m []
no goals
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
m : ℕ
this : length ([] {m ↦ a}) = max (length []) (m + 1)
⊢ length ([] {m + 1 ↦ a}) = max (length []) (m + 1 + 1)
simp [set, length, @length_set m, Nat.zero_max]
no goals
α : Type u
β : Type v
γ : Type w
a : α
as✝ as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
m : ℕ
head✝ : α
as : List α
⊢ length ((head✝ :: as) {m + 1 ↦ a}) = max (length (head✝ :: as)) (m + 1 + 1)
simp [set, length, @length_set m, Nat.max_succ_succ]