case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ length (add (map f as) (map g as)) = length (map (fun x => f x + g x) as)

case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ Equiv (add (map f as) (map g as)) (map (fun x => f x + g x) as)
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ add (map f as) (map g as) = map (fun x => f x + g x) as
apply @eq_of_equiv _ (⟨0⟩ : Inhabited α)
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
⊢ get m (add (map f as) (map g as)) = get m (map (fun x => f x + g x) as)
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ Equiv (add (map f as) (map g as)) (map (fun x => f x + g x) as)
intro m
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
⊢ get m (add (map f as) (map g as)) = get m (map (fun x => f x + g x) as)
rw [get_add]
case pos
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : m < length as
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)

case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : ¬m < length as
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
by_cases h : m < length as
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : ¬m < length as
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
rw [not_lt] at h
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = default
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
repeat' rw [@get_eq_default_of_le _ ⟨0⟩ m] <;> try rw [length_map]; apply h
no goals
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = default
exact zero_add _
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ length (map g as) ≤ length (map f as)
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ length (add (map f as) (map g as)) = length (map (fun x => f x + g x) as)
rw [length_map, length_add, max_eq_left, length_map]
case a.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ length (map g as) = length (map f as)
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ length (map g as) ≤ length (map f as)
apply le_of_eq
no goals
case a.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
⊢ length (map g as) = length (map f as)
rw [length_map, length_map]
no goals
case pos
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : m < length as
⊢ get m (map f as) + get m (map g as) = get m (map (fun x => f x + g x) as)
repeat' rw [@get_map α α ⟨0⟩ ⟨0⟩ _ _ _ h]
no goals
case pos
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : m < length as
⊢ f (get m as) + g (get m as) = get m (map (fun x => f x + g x) as)
rw [@get_map α α ⟨0⟩ ⟨0⟩ _ _ _ h]
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = default
case neg
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ default + default = default
rw [@get_eq_default_of_le _ ⟨0⟩ m] <;> try rw [length_map]; apply h
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length as ≤ m
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length (map (fun x => f x + g x) as) ≤ m
rw [length_map]
no goals
case neg.a
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddMonoid α
f g : α → α
as : List α
m : ℕ
h : length as ≤ m
⊢ length as ≤ m
apply h