ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → γ → δ<VAR>g : β → γ<GOAL>Finset.image₂ f s (Finset.image g t) = Finset.image₂ (fun a b => f a (g b)) s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image₂ Prod.mk s t = s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α × β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image₂ (Function.curry f) s t = Finset.image f (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image (Function.uncurry f) (s ×ˢ t) = Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image₂ f s t = Finset.image₂ (fun a b => f b a) t s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>s : Finset α<VAR>t : Finset β<VAR>DecidableEq α<VAR>h : t.Nonempty<GOAL>Finset.image₂ (fun x x_1 => x) s t = s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>s : Finset α<VAR>t : Finset β<VAR>DecidableEq β<VAR>h : s.Nonempty<GOAL>Finset.image₂ (fun x y => y) s t = t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>DecidableEq δ<VAR>DecidableEq ε<VAR>DecidableEq ε'<VAR>s : Finset α<VAR>t : Finset β<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f' : α → ε' → ε<VAR>g' : β → γ → ε'<VAR>h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)<GOAL>Finset.image₂ f (Finset.image₂ g s t) u = Finset.image₂ f' s (Finset.image₂ g' t u)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>g : β → α → γ<VAR>h_comm : ∀ (a : α) (b : β), f a b = g b a<GOAL>Finset.image₂ f s t = Finset.image₂ g t s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>DecidableEq δ<VAR>DecidableEq δ'<VAR>DecidableEq ε<VAR>s : Finset α<VAR>t : Finset β<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>f' : α → γ → δ'<VAR>g' : β → δ' → ε<VAR>h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)<GOAL>Finset.image₂ f s (Finset.image₂ g t u) = Finset.image₂ g' t (Finset.image₂ f' s u)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>DecidableEq δ<VAR>DecidableEq δ'<VAR>DecidableEq ε<VAR>s : Finset α<VAR>t : Finset β<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f' : α → γ → δ'<VAR>g' : δ' → β → ε<VAR>h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b<GOAL>Finset.image₂ f (Finset.image₂ g s t) u = Finset.image₂ g' (Finset.image₂ f' s u) t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>DecidableEq ε<VAR>DecidableEq ε'<VAR>s : Finset α<VAR>t : Finset β<VAR>γ : Type u_14<VAR>δ : Type u_15<VAR>u : Finset γ<VAR>v : Finset δ<VAR>DecidableEq ζ<VAR>DecidableEq ζ'<VAR>DecidableEq ν<VAR>f : ε → ζ → ν<VAR>g : α → β → ε<VAR>h : γ → δ → ζ<VAR>f' : ε' → ζ' → ν<VAR>g' : α → γ → ε'<VAR>h' : β → δ → ζ'<VAR>h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)<GOAL>Finset.image₂ f (Finset.image₂ g s t) (Finset.image₂ h u v) = Finset.image₂ f' (Finset.image₂ g' s u) (Finset.image₂ h' t v)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq α'<VAR>DecidableEq β'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>g : γ → δ<VAR>f' : α' → β' → δ<VAR>g₁ : α → α'<VAR>g₂ : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)<GOAL>Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g₁ s) (Finset.image g₂ t)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq α'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>g : γ → δ<VAR>f' : α' → β → δ<VAR>g' : α → α'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b<GOAL>Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g' s) t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq β'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>g : γ → δ<VAR>f' : α → β' → δ<VAR>g' : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)<GOAL>Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' s (Finset.image g' t)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq α'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α' → β → γ<VAR>g : α → α'<VAR>f' : α → β → δ<VAR>g' : δ → γ<VAR>h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)<GOAL>Finset.image₂ f (Finset.image g s) t = Finset.image g' (Finset.image₂ f' s t)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq β'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β' → γ<VAR>g : β → β'<VAR>f' : α → β → δ<VAR>g' : δ → γ<VAR>h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)<GOAL>Finset.image₂ f s (Finset.image g t) = Finset.image g' (Finset.image₂ f' s t)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>DecidableEq β'<VAR>DecidableEq γ'<VAR>DecidableEq δ<VAR>DecidableEq ε<VAR>s : Finset α<VAR>t : Finset β<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>f₁ : α → β → β'<VAR>f₂ : α → γ → γ'<VAR>g' : β' → γ' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)<GOAL>Finset.image₂ f s (Finset.image₂ g t u) ⊆ Finset.image₂ g' (Finset.image₂ f₁ s t) (Finset.image₂ f₂ s u)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>DecidableEq α'<VAR>DecidableEq β'<VAR>DecidableEq δ<VAR>DecidableEq ε<VAR>s : Finset α<VAR>t : Finset β<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f₁ : α → γ → α'<VAR>f₂ : β → γ → β'<VAR>g' : α' → β' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)<GOAL>Finset.image₂ f (Finset.image₂ g s t) u ⊆ Finset.image₂ g' (Finset.image₂ f₁ s u) (Finset.image₂ f₂ t u)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq α'<VAR>DecidableEq β'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>g : γ → δ<VAR>f' : β' → α' → δ<VAR>g₁ : β → β'<VAR>g₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)<GOAL>Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g₁ t) (Finset.image g₂ s)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq β'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>g : γ → δ<VAR>f' : β' → α → δ<VAR>g' : β → β'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a<GOAL>Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g' t) s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq α'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>g : γ → δ<VAR>f' : β → α' → δ<VAR>g' : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)<GOAL>Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' t (Finset.image g' s)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq α'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α' → β → γ<VAR>g : α → α'<VAR>f' : β → α → δ<VAR>g' : δ → γ<VAR>h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)<GOAL>Finset.image₂ f (Finset.image g s) t = Finset.image g' (Finset.image₂ f' t s)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq β'<VAR>DecidableEq γ<VAR>DecidableEq δ<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β' → γ<VAR>g : β → β'<VAR>f' : β → α → δ<VAR>g' : δ → γ<VAR>h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)<GOAL>Finset.image₂ f s (Finset.image g t) = Finset.image g' (Finset.image₂ f' t s)
<VAR>α : Type u_1<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → γ → γ<VAR>a : α<VAR>h : ∀ (b : γ), f a b = b<VAR>t : Finset γ<GOAL>Finset.image₂ f {a} t = t
<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : γ → β → γ<VAR>b : β<VAR>h : ∀ (a : γ), f a b = a<VAR>s : Finset γ<GOAL>Finset.image₂ f s {b} = s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>hf : ∀ a ∈ s, Function.Injective (f a)<VAR>hs : ((fun a => Finset.image (f a) t) '' ↑s).PairwiseDisjoint id<GOAL>t.card ∣ (Finset.image₂ f s t).card
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>hf : ∀ b ∈ t, Function.Injective fun a => f a b<VAR>ht : ((fun b => Finset.image (fun a => f a b) s) '' ↑t).PairwiseDisjoint id<GOAL>s.card ∣ (Finset.image₂ f s t).card
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>u : Finset γ<VAR>s : Set α<VAR>t : Set β<VAR>hu : ↑u ⊆ Set.image2 f s t<GOAL>∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ Finset.image₂ f s' t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>DecidableEq α<VAR>DecidableEq β<GOAL>Finset.image₂ f (s ∩ s') (t ∪ t') ⊆ Finset.image₂ f s t ∪ Finset.image₂ f s' t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>DecidableEq α<VAR>DecidableEq β<GOAL>Finset.image₂ f (s ∪ s') (t ∩ t') ⊆ Finset.image₂ f s t ∪ Finset.image₂ f s' t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → α → β<VAR>s t : Finset α<VAR>hf : ∀ (a b : α), f a b = f b a<GOAL>Finset.image₂ f (s ∩ t) (s ∪ t) ⊆ Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → α → β<VAR>s t : Finset α<VAR>hf : ∀ (a b : α), f a b = f b a<GOAL>Finset.image₂ f (s ∪ t) (s ∩ t) ⊆ Finset.image₂ f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeSup δ<VAR>g : γ → δ<VAR>a : δ<VAR>h : (Finset.image₂ f s t).Nonempty<GOAL>(Finset.image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeSup δ<VAR>g : γ → δ<VAR>h : (Finset.image₂ f s t).Nonempty<GOAL>(Finset.image₂ f s t).sup' h g = s.sup' ⋯ fun x => t.sup' ⋯ fun x_1 => g (f x x_1)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeSup δ<VAR>g : γ → δ<VAR>h : (Finset.image₂ f s t).Nonempty<GOAL>(Finset.image₂ f s t).sup' h g = t.sup' ⋯ fun y => s.sup' ⋯ fun x => g (f x y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeSup δ<VAR>OrderBot δ<VAR>g : γ → δ<VAR>a : δ<GOAL>(Finset.image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeSup δ<VAR>OrderBot δ<VAR>g : γ → δ<GOAL>(Finset.image₂ f s t).sup g = s.sup fun x => t.sup fun x_1 => g (f x x_1)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeSup δ<VAR>OrderBot δ<VAR>g : γ → δ<GOAL>(Finset.image₂ f s t).sup g = t.sup fun y => s.sup fun x => g (f x y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeInf δ<VAR>g : γ → δ<VAR>a : δ<VAR>h : (Finset.image₂ f s t).Nonempty<GOAL>a ≤ (Finset.image₂ f s t).inf' h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeInf δ<VAR>g : γ → δ<VAR>h : (Finset.image₂ f s t).Nonempty<GOAL>(Finset.image₂ f s t).inf' h g = s.inf' ⋯ fun x => t.inf' ⋯ fun x_1 => g (f x x_1)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeInf δ<VAR>g : γ → δ<VAR>h : (Finset.image₂ f s t).Nonempty<GOAL>(Finset.image₂ f s t).inf' h g = t.inf' ⋯ fun y => s.inf' ⋯ fun x => g (f x y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeInf δ<VAR>OrderTop δ<VAR>g : γ → δ<VAR>a : δ<GOAL>a ≤ (Finset.image₂ f s t).inf g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeInf δ<VAR>OrderTop δ<VAR>g : γ → δ<GOAL>(Finset.image₂ f s t).inf g = s.inf fun x => t.inf (g ∘ f x)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>SemilatticeInf δ<VAR>OrderTop δ<VAR>g : γ → δ<GOAL>(Finset.image₂ f s t).inf g = t.inf fun y => s.inf fun x => g (f x y)
<VAR>ι : Type u_14<VAR>α : ι → Type u_15<VAR>β : ι → Type u_16<VAR>γ : ι → Type u_17<VAR>DecidableEq ι<VAR>Fintype ι<VAR>(i : ι) → DecidableEq (γ i)<VAR>f : (i : ι) → α i → β i → γ i<VAR>s : (i : ι) → Finset (α i)<VAR>t : (i : ι) → Finset (β i)<GOAL>(Fintype.piFinset fun i => Finset.image₂ (f i) (s i) (t i)) = Finset.image₂ (fun a b i => f i (a i) (b i)) (Fintype.piFinset s) (Fintype.piFinset t)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(Set.image2 f s t)<GOAL>(Set.image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>DecidableEq γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β → γ<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hf : (Set.image2 f s t).Finite := ⋯<GOAL>Set.Finite.toFinset hf = Finset.image₂ f hs.toFinset ht.toFinset
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>f g : α.Arrow β<GOAL>(∀ (i : Fin2 n), f i = g i) → f = g
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>f : α.Arrow β<GOAL>TypeVec.comp TypeVec.id f = f
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>f : α.Arrow β<GOAL>TypeVec.comp f TypeVec.id = f
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>γ : TypeVec.{u_3} n<VAR>δ : TypeVec.{u_4} n<VAR>h : γ.Arrow δ<VAR>g : β.Arrow γ<VAR>f : α.Arrow β<GOAL>TypeVec.comp (TypeVec.comp h g) f = TypeVec.comp h (TypeVec.comp g f)
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : Type u_1<VAR>i : Fin2 n<GOAL>(α ::: β).drop i = α i
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : Type u_1<GOAL>(α ::: β).drop = α
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : Type u_1<GOAL>(α ::: β).last = β
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<GOAL>α.drop ::: α.last = α
<VAR>n : ℕ<VAR>C : TypeVec.{u_1} (n + 1) → Sort u<VAR>H : (α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β)<VAR>α : TypeVec.{u_1} n<VAR>β : Type u_1<GOAL>TypeVec.append1Cases H (α ::: β) = H α β
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>β : TypeVec.{u_2} (n + 1)<VAR>f g : α.Arrow β<VAR>h₀ : TypeVec.dropFun f = TypeVec.dropFun g<VAR>h₁ : TypeVec.lastFun f = TypeVec.lastFun g<GOAL>f = g
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>α' : TypeVec.{u_2} (n + 1)<VAR>f : α.drop.Arrow α'.drop<VAR>g : α.last → α'.last<GOAL>TypeVec.dropFun (TypeVec.splitFun f g) = f
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>α' : TypeVec.{u_2} (n + 1)<VAR>f : α.drop.Arrow α'.drop<VAR>g : α.last → α'.last<GOAL>TypeVec.lastFun (TypeVec.splitFun f g) = g
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>α' : TypeVec.{u_2} n<VAR>β : Type u_1<VAR>β' : Type u_2<VAR>f : α.Arrow α'<VAR>g : β → β'<GOAL>TypeVec.dropFun (f ::: g) = f
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>α' : TypeVec.{u_2} n<VAR>β : Type u_1<VAR>β' : Type u_2<VAR>f : α.Arrow α'<VAR>g : β → β'<GOAL>TypeVec.lastFun (f ::: g) = g
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>α' : TypeVec.{u_2} (n + 1)<VAR>f : α.Arrow α'<GOAL>TypeVec.splitFun (TypeVec.dropFun f) (TypeVec.lastFun f) = f
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>α' : TypeVec.{u_2} (n + 1)<VAR>f f' : α.drop.Arrow α'.drop<VAR>g g' : α.last → α'.last<VAR>H : TypeVec.splitFun f g = TypeVec.splitFun f' g'<GOAL>f = f' ∧ g = g'
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>α' : TypeVec.{u_2} n<VAR>β : Type u_1<VAR>β' : Type u_2<VAR>f f' : α.Arrow α'<VAR>g g' : β → β'<GOAL>(f ::: g) = (f' ::: g') → f = f' ∧ g = g'
<VAR>n : ℕ<VAR>α₀ : TypeVec.{u_1} (n + 1)<VAR>α₁ : TypeVec.{u_2} (n + 1)<VAR>α₂ : TypeVec.{u_3} (n + 1)<VAR>f₀ : α₀.drop.Arrow α₁.drop<VAR>f₁ : α₁.drop.Arrow α₂.drop<VAR>g₀ : α₀.last → α₁.last<VAR>g₁ : α₁.last → α₂.last<GOAL>TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ ∘ g₀) = TypeVec.comp (TypeVec.splitFun f₁ g₁) (TypeVec.splitFun f₀ g₀)
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>γ : TypeVec.{u_2} n<VAR>β : Type u_1<VAR>δ : Type u_2<VAR>ε : TypeVec.{u_3} (n + 1)<VAR>f₀ : ε.drop.Arrow α<VAR>f₁ : α.Arrow γ<VAR>g₀ : ε.last → β<VAR>g₁ : β → δ<GOAL>TypeVec.comp (f₁ ::: g₁) (TypeVec.splitFun f₀ g₀) = TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ ∘ g₀)
<VAR>n : ℕ<VAR>α₀ : TypeVec.{u_1} n<VAR>α₁ : TypeVec.{u_2} n<VAR>α₂ : TypeVec.{u_3} n<VAR>β₀ : Type u_1<VAR>β₁ : Type u_2<VAR>β₂ : Type u_3<VAR>f₀ : α₀.Arrow α₁<VAR>f₁ : α₁.Arrow α₂<VAR>g₀ : β₀ → β₁<VAR>g₁ : β₁ → β₂<GOAL>(TypeVec.comp f₁ f₀ ::: g₁ ∘ g₀) = TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀)
<VAR>n : ℕ<VAR>α₀ : TypeVec.{u_1} n<VAR>α₁ : TypeVec.{u_2} n<VAR>α₂ : TypeVec.{u_3} n<VAR>β₀ : Type u_1<VAR>β₁ : Type u_2<VAR>β₂ : Type u_3<VAR>f₀ : α₀.Arrow α₁<VAR>f₁ : α₁.Arrow α₂<VAR>g₀ : β₀ → β₁<VAR>g₁ : β₁ → β₂<GOAL>TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀) = (TypeVec.comp f₁ f₀ ::: g₁ ∘ g₀)
<VAR>α₀ : TypeVec.{u_1} 0<VAR>f₀ : α₀.Arrow Fin2.elim0<GOAL>TypeVec.comp TypeVec.nilFun f₀ = f₀
<VAR>n : ℕ<VAR>α : TypeVec.{u} n<VAR>β₀ β₁ β₂ : Type u<VAR>g₀ : β₀ → β₁<VAR>g₁ : β₁ → β₂<GOAL>(TypeVec.id ::: g₁ ∘ g₀) = TypeVec.comp (TypeVec.id ::: g₁) (TypeVec.id ::: g₀)
<VAR>n : ℕ<VAR>α₀ : TypeVec.{u_1} (n + 1)<VAR>α₁ : TypeVec.{u_2} (n + 1)<VAR>α₂ : TypeVec.{u_3} (n + 1)<VAR>f₀ : α₀.Arrow α₁<VAR>f₁ : α₁.Arrow α₂<GOAL>TypeVec.dropFun (TypeVec.comp f₁ f₀) = TypeVec.comp (TypeVec.dropFun f₁) (TypeVec.dropFun f₀)
<VAR>n : ℕ<VAR>α₀ : TypeVec.{u_1} (n + 1)<VAR>α₁ : TypeVec.{u_2} (n + 1)<VAR>α₂ : TypeVec.{u_3} (n + 1)<VAR>f₀ : α₀.Arrow α₁<VAR>f₁ : α₁.Arrow α₂<GOAL>TypeVec.lastFun (TypeVec.comp f₁ f₀) = TypeVec.lastFun f₁ ∘ TypeVec.lastFun f₀
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>α' : TypeVec.{u_2} n<VAR>β : Type u_1<VAR>β' : Type u_2<VAR>f : (α ::: β).Arrow (α' ::: β')<GOAL>(TypeVec.dropFun f ::: TypeVec.lastFun f) = f
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : Type u_1<GOAL>(TypeVec.id ::: id) = TypeVec.id
<VAR>β : TypeVec.{u_2} 0 → Sort u_1<VAR>f : β Fin2.elim0<GOAL>TypeVec.casesNil f Fin2.elim0 = f
<VAR>n : ℕ<VAR>β : TypeVec.{u_2} (n + 1) → Sort u_1<VAR>f : (t : Type u_2) → (v : TypeVec.{u_2} n) → β (v ::: t)<VAR>v : TypeVec.{u_2} n<VAR>α : Type u_2<GOAL>TypeVec.casesCons n f (v ::: α) = f α v
<VAR>β : TypeVec.Arrow Fin2.elim0 Fin2.elim0 → Sort u_1<VAR>f : β TypeVec.nilFun<GOAL>TypeVec.typevecCasesNil₂ f TypeVec.nilFun = f
<VAR>n : ℕ<VAR>t : Type u_1<VAR>t' : Type u_2<VAR>v : TypeVec.{u_1} n<VAR>v' : TypeVec.{u_2} n<VAR>β : (v ::: t).Arrow (v' ::: t') → Sort u_3<VAR>F : (f : t → t') → (fs : v.Arrow v') → β (fs ::: f)<VAR>f : t → t'<VAR>fs : v.Arrow v'<GOAL>TypeVec.typevecCasesCons₂ n t t' v v' F (fs ::: f) = F f fs
<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>x : γ<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<GOAL>TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun x_1 => x)
<VAR>α : TypeVec.{u_1} 0<VAR>β : TypeVec.{u_2} 0<VAR>f : α.Arrow β<GOAL>f = TypeVec.nilFun
<VAR>α : TypeVec.{u_1} 0<GOAL>TypeVec.id = TypeVec.nilFun
<VAR>β : Type u_1<VAR>x : β<VAR>α : TypeVec.{u_2} 0<GOAL>TypeVec.const x α = TypeVec.nilFun
<VAR>β : Type u_1<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<GOAL>(α ::: β).repeatEq = TypeVec.splitFun α.repeatEq (Function.uncurry Eq)
<VAR>α : TypeVec.{u_1} 0<GOAL>α.repeatEq = TypeVec.nilFun
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>i : Fin2 n<VAR>x : α i<VAR>p : Prop<GOAL>TypeVec.ofRepeat (TypeVec.const p α i x) ↔ p
<VAR>n : ℕ<VAR>α β : TypeVec.{u_1} n<VAR>i : Fin2 n<VAR>a : α i<VAR>b : β i<GOAL>TypeVec.prod.fst i (TypeVec.prod.mk i a b) = a
<VAR>n : ℕ<VAR>α β : TypeVec.{u_1} n<VAR>i : Fin2 n<VAR>a : α i<VAR>b : β i<GOAL>TypeVec.prod.snd i (TypeVec.prod.mk i a b) = b
<VAR>n : ℕ<VAR>α α' β β' : TypeVec.{u_1} n<VAR>f : α.Arrow β<VAR>g : α'.Arrow β'<GOAL>TypeVec.comp TypeVec.prod.fst (TypeVec.prod.map f g) = TypeVec.comp f TypeVec.prod.fst
<VAR>n : ℕ<VAR>α α' β β' : TypeVec.{u_1} n<VAR>f : α.Arrow β<VAR>g : α'.Arrow β'<GOAL>TypeVec.comp TypeVec.prod.snd (TypeVec.prod.map f g) = TypeVec.comp g TypeVec.prod.snd
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<GOAL>TypeVec.comp TypeVec.prod.fst TypeVec.prod.diag = TypeVec.id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<GOAL>TypeVec.comp TypeVec.prod.snd TypeVec.prod.diag = TypeVec.id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>i : Fin2 n<VAR>x y : α i<GOAL>TypeVec.ofRepeat (α.repeatEq i (TypeVec.prod.mk i x y)) ↔ x = y
<VAR>α : TypeVec.{u} 0<VAR>ps : α.Arrow (TypeVec.repeat 0 Prop)<GOAL>TypeVec.subtypeVal ps = TypeVec.nilFun
<VAR>n : ℕ<VAR>α : TypeVec.{u} n<GOAL>TypeVec.comp (TypeVec.subtypeVal α.repeatEq) TypeVec.diagSub = TypeVec.prod.diag
<VAR>n : ℕ<VAR>α β : TypeVec.{u} n<GOAL>TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id
<VAR>n : ℕ<VAR>α α' β β' : TypeVec.{u} n<VAR>φ φ' ψ ψ' : Type u<VAR>f₀ : α.Arrow α'<VAR>g₀ : β.Arrow β'<VAR>f₁ : φ → φ'<VAR>g₁ : ψ → ψ'<GOAL>(TypeVec.prod.map f₀ g₀ ::: Prod.map f₁ g₁) = TypeVec.prod.map (f₀ ::: f₁) (g₀ ::: g₁)
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<GOAL>TypeVec.dropFun TypeVec.prod.diag = TypeVec.prod.diag
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>p : α.Arrow (TypeVec.repeat (n + 1) Prop)<GOAL>TypeVec.dropFun (TypeVec.subtypeVal p) = TypeVec.subtypeVal (TypeVec.dropFun p)
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>p : α.Arrow (TypeVec.repeat (n + 1) Prop)<GOAL>TypeVec.lastFun (TypeVec.subtypeVal p) = Subtype.val
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>p : α.Arrow (TypeVec.repeat (n + 1) Prop)<GOAL>TypeVec.dropFun (TypeVec.toSubtype p) = TypeVec.toSubtype fun i => p i.fs
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>p : α.Arrow (TypeVec.repeat (n + 1) Prop)<GOAL>TypeVec.lastFun (TypeVec.toSubtype p) = id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>p : α.Arrow (TypeVec.repeat (n + 1) Prop)<GOAL>TypeVec.dropFun (TypeVec.ofSubtype p) = TypeVec.ofSubtype (TypeVec.dropFun p)
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>p : α.Arrow (TypeVec.repeat (n + 1) Prop)<GOAL>TypeVec.lastFun (TypeVec.ofSubtype p) = id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : Type u_1<VAR>R : β → β → Prop<GOAL>TypeVec.dropFun (α.RelLast' R) = α.repeatEq
<VAR>n : ℕ<VAR>α α' β β' : TypeVec.{u_1} (n + 1)<VAR>f : α.Arrow β<VAR>f' : α'.Arrow β'<GOAL>TypeVec.dropFun (TypeVec.prod.map f f') = TypeVec.prod.map (TypeVec.dropFun f) (TypeVec.dropFun f')
<VAR>n : ℕ<VAR>α α' β β' : TypeVec.{u_1} (n + 1)<VAR>f : α.Arrow β<VAR>f' : α'.Arrow β'<GOAL>TypeVec.lastFun (TypeVec.prod.map f f') = Prod.map (TypeVec.lastFun f) (TypeVec.lastFun f')
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<GOAL>TypeVec.dropFun TypeVec.fromAppend1DropLast = TypeVec.id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<GOAL>TypeVec.lastFun TypeVec.fromAppend1DropLast = id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<GOAL>TypeVec.dropFun TypeVec.id = TypeVec.id