α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldl f a l) ⊆ Set.range fun l => foldl g a l
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldl f a) ⊆ Set.range (foldl g a)
change (Set.range fun l => _) ⊆ Set.range fun l => _
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldr (fun z w => f w z) a (reverse l)) ⊆
    Set.range fun l => foldr (fun z w => g w z) a (reverse l)
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldl f a l) ⊆ Set.range fun l => foldl g a l
simp_rw [← foldr_reverse _ (fun z w => g w z), ← foldr_reverse _ (fun z w => f w z)]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a ∘ reverse) ⊆ Set.range (foldr (fun z w => g w z) a ∘ reverse)
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ (Set.range fun l => foldr (fun z w => f w z) a (reverse l)) ⊆
    Set.range fun l => foldr (fun z w => g w z) a (reverse l)
change (Set.range (foldr (fun z w => f w z) a ∘ reverse)) ⊆
  Set.range (foldr (fun z w => g w z) a ∘ reverse)
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a) ⊆ Set.range (foldr (fun z w => g w z) a)
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a ∘ reverse) ⊆ Set.range (foldr (fun z w => g w z) a ∘ reverse)
simp_rw [Set.range_comp _ reverse, reverse_involutive.bijective.surjective.range_eq,
  Set.image_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b
a : α
⊢ Set.range (foldr (fun z w => f w z) a) ⊆ Set.range (foldr (fun z w => g w z) a)
exact foldr_range_subset_of_range_subset hfg a