case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
l : List β
⊢ foldr f a l ∈ Set.range (foldr g a)
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ Set.range (foldr f a) ⊆ Set.range (foldr g a)
rintro _ ⟨l, rfl⟩
case intro.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ foldr f a [] ∈ Set.range (foldr g a)

case intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
l : List β
⊢ foldr f a l ∈ Set.range (foldr g a)
induction' l with b l H
no goals
case intro.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ foldr f a [] ∈ Set.range (foldr g a)
exact ⟨[], rfl⟩
case intro.cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
c : γ
hgf : g c = f b
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
case intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
cases' hfg (Set.mem_range_self b) with c hgf
case intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
case intro.cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
c : γ
hgf : g c = f b
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
cases' H with m hgf'
case intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)
case intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
rw [foldr_cons, ← hgf, ← hgf']
no goals
case intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)
exact ⟨c :: m, rfl⟩