case nil
ι : Type ?u.235575
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List (α → α)
f✝ : α → α
hl✝ : ∀ (f : α → α), f ∈ l → Injective f
hf✝ : Injective f✝
f : α → α
hl : ∀ (f : α → α), f ∈ [] → Injective f
hf : Injective f
⊢ Injective (foldl comp f [])

case cons
ι : Type ?u.235575
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List (α → α)
f✝ : α → α
hl✝ : ∀ (f : α → α), f ∈ l → Injective f
hf✝ : Injective f✝
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (foldl comp f (lh :: lt))
ι : Type ?u.235575
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List (α → α)
f : α → α
hl : ∀ (f : α → α), f ∈ l → Injective f
hf : Injective f
⊢ Injective (foldl comp f l)
induction' l with lh lt l_ih generalizing f
no goals
case nil
ι : Type ?u.235575
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List (α → α)
f✝ : α → α
hl✝ : ∀ (f : α → α), f ∈ l → Injective f
hf✝ : Injective f✝
f : α → α
hl : ∀ (f : α → α), f ∈ [] → Injective f
hf : Injective f
⊢ Injective (foldl comp f [])
exact hf
case cons
ι : Type ?u.235575
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List (α → α)
f✝ : α → α
hl✝ : ∀ (f : α → α), f ∈ l → Injective f
hf✝ : Injective f✝
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (f ∘ lh)
case cons
ι : Type ?u.235575
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List (α → α)
f✝ : α → α
hl✝ : ∀ (f : α → α), f ∈ l → Injective f
hf✝ : Injective f✝
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (foldl comp f (lh :: lt))
apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)
case cons
ι : Type ?u.235575
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List (α → α)
f✝ : α → α
hl✝ : ∀ (f : α → α), f ∈ l → Injective f
hf✝ : Injective f✝
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective lh
case cons
ι : Type ?u.235575
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List (α → α)
f✝ : α → α
hl✝ : ∀ (f : α → α), f ∈ l → Injective f
hf✝ : Injective f✝
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (f ∘ lh)
apply Function.Injective.comp hf
no goals
case cons
ι : Type ?u.235575
α✝ : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
l : List (α → α)
f✝ : α → α
hl✝ : ∀ (f : α → α), f ∈ l → Injective f
hf✝ : Injective f✝
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective lh
apply hl _ (List.mem_cons_self _ _)