ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>LE β<VAR>t c : Lex (α × β)<VAR>h : t ≤ c<GOAL>(ofLex t).1 ≤ (ofLex c).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>Preorder β<GOAL>Monotone ⇑toLex
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>Preorder β<GOAL>StrictMono ⇑toLex
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.sym2.val = s.val.sym2
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a b : α<GOAL>s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>m : Sym2 α<GOAL>m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<GOAL>(Finset.cons a s ha).sym2 = (Finset.map (Sym2.mkEmbedding a) (Finset.cons a s ha)).disjUnion s.sym2 ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).sym2 = Finset.image (fun b => s(a, b)) (insert a s) ∪ s.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>(Finset.map f s).sym2 = Finset.map f.sym2Map s.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>(Finset.image f s).sym2 = Finset.image (Sym2.map f) s.sym2
<VAR>α : Type u_1<VAR>Fintype α<VAR>inst : Fintype (Sym2 α) := Sym2.instFintype<GOAL>Finset.univ.sym2 = Finset.univ
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>s.sym2 ⊆ t.sym2
<VAR>α : Type u_1<GOAL>Monotone Finset.sym2
<VAR>α : Type u_1<GOAL>Function.Injective Finset.sym2
<VAR>α : Type u_1<GOAL>StrictMono Finset.sym2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.toFinset.sym2 = m.sym2.toFinset
<VAR>α : Type u_1<GOAL>∅.sym2 = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.sym2 = ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.sym2.Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>a : α<GOAL>{a}.sym2 = {Sym2.diag a}
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.sym2.card = (s.card + 1).choose 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.sym2 = Finset.image Sym2.mk (s ×ˢ s)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α × α<VAR>h : a ∈ s.diag<GOAL>(Sym2.mk a).IsDiag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α × α<VAR>h : a ∈ s.offDiag<GOAL>¬(Sym2.mk a).IsDiag
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>(∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>Sym2.diag a ∈ s.sym2 ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.image Sym2.mk s.diag ∪ Finset.image Sym2.mk s.offDiag = s.sym2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.sym 0 = {∅}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>n : ℕ<GOAL>s.sym (n + 1) = s.sup fun a => Finset.image (Sym.cons a) (s.sym n)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>n : ℕ<VAR>m : Sym α n<GOAL>m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>n : ℕ<GOAL>∅.sym (n + 1) = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>Sym.replicate n a ∈ s.sym n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>h : s.Nonempty<VAR>n : ℕ<GOAL>(s.sym n).Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>n : ℕ<GOAL>{a}.sym n = {Sym.replicate n a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>n : ℕ<VAR>h : s.sym n = ∅<GOAL>s = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>n : ℕ<GOAL>s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>n : ℕ<GOAL>(s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>n : ℕ<GOAL>Finset.univ.sym n = Finset.univ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<VAR>n : ℕ<GOAL>s.sym n ⊆ t.sym n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>n : ℕ<GOAL>(s ∩ t).sym n = s.sym n ∩ t.sym n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>n : ℕ<GOAL>s.sym n ∪ t.sym n ⊆ (s ∪ t).sym n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>n : ℕ<VAR>a : α<VAR>i : Fin (n + 1)<VAR>m : Sym α (n - ↑i)<VAR>h : m ∈ s.sym (n - ↑i)<GOAL>Sym.fill a i m ∈ (insert a s).sym n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>n : ℕ<VAR>m : Sym α n<VAR>a : α<VAR>h : m ∈ s.sym n<GOAL>(Sym.filterNe a m).snd ∈ (s.erase a).sym (n - ↑(Sym.filterNe a m).fst)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>m : (i : Fin (n + 1)) × { x // x ∈ s.sym (n - ↑i) }<GOAL>↑((Finset.symInsertEquiv h).symm m) = Sym.fill a m.fst ↑m.snd
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>m : { x // x ∈ (insert a s).sym n }<GOAL>((Finset.symInsertEquiv h) m).fst = (Sym.filterNe a ↑m).fst
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : a ∉ s<VAR>m : { x // x ∈ (insert a s).sym n }<GOAL>↑((Finset.symInsertEquiv h) m).snd = (Sym.filterNe a ↑m).snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>a b : (i : ι) × α i<GOAL>Sigma.Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r₁ r₂ : ι → ι → Prop<VAR>s₁ s₂ : (i : ι) → α i → α i → Prop<VAR>hr : ∀ (a b : ι), r₁ a b → r₂ a b<VAR>hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b<VAR>a b : (i : ι) × α i<VAR>h : Sigma.Lex r₁ s₁ a b<GOAL>Sigma.Lex r₂ s₂ a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r₁ r₂ : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hr : ∀ (a b : ι), r₁ a b → r₂ a b<VAR>a b : (i : ι) × α i<VAR>h : Sigma.Lex r₁ s a b<GOAL>Sigma.Lex r₂ s a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s₁ s₂ : (i : ι) → α i → α i → Prop<VAR>hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b<VAR>a b : (i : ι) × α i<VAR>h : Sigma.Lex r s₁ a b<GOAL>Sigma.Lex r s₂ a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>a b : (i : ι) × α i<GOAL>Sigma.Lex (Function.swap r) s a b ↔ Sigma.Lex r (fun i => Function.swap (s i)) b a
<VAR>ι : Sort u_1<VAR>α : ι → Sort u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>a b : (i : ι) ×' α i<GOAL>PSigma.Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd
<VAR>ι : Sort u_1<VAR>α : ι → Sort u_2<VAR>r₁ r₂ : ι → ι → Prop<VAR>s₁ s₂ : (i : ι) → α i → α i → Prop<VAR>hr : ∀ (a b : ι), r₁ a b → r₂ a b<VAR>hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b<VAR>a b : (i : ι) ×' α i<VAR>h : PSigma.Lex r₁ s₁ a b<GOAL>PSigma.Lex r₂ s₂ a b
<VAR>ι : Sort u_1<VAR>α : ι → Sort u_2<VAR>r₁ r₂ : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hr : ∀ (a b : ι), r₁ a b → r₂ a b<VAR>a b : (i : ι) ×' α i<VAR>h : PSigma.Lex r₁ s a b<GOAL>PSigma.Lex r₂ s a b
<VAR>ι : Sort u_1<VAR>α : ι → Sort u_2<VAR>r : ι → ι → Prop<VAR>s₁ s₂ : (i : ι) → α i → α i → Prop<VAR>hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b<VAR>a b : (i : ι) ×' α i<VAR>h : PSigma.Lex r s₁ a b<GOAL>PSigma.Lex r s₂ a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α × β<GOAL>(p.1, p.2) = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α × β → Prop<GOAL>(∀ (x : α × β), p x) ↔ ∀ (a : α) (b : β), p (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α × β → Prop<GOAL>(∃ x, p x) ↔ ∃ a b, p (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → β → Prop<GOAL>(∀ (x : α × β), p x.1 x.2) ↔ ∀ (a : α) (b : β), p a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → β → Prop<GOAL>(∃ x, p x.1 x.2) ↔ ∃ a b, p a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<GOAL>Prod.snd ∘ Prod.mk x = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<GOAL>Prod.fst ∘ Prod.mk x = Function.const β x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<VAR>a : α<VAR>b : β<GOAL>Prod.map f g (a, b) = (f a, g b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<VAR>p : α × β<GOAL>Prod.map f g p = (f p.1, g p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<GOAL>Prod.fst ∘ Prod.map f g = f ∘ Prod.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<GOAL>Prod.snd ∘ Prod.map f g = g ∘ Prod.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>f : α → β<VAR>f' : γ → δ<VAR>g : β → ε<VAR>g' : δ → ζ<GOAL>Prod.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>f : α → β<VAR>f' : γ → δ<VAR>g : β → ε<VAR>g' : δ → ζ<VAR>x : α × γ<GOAL>Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>(a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>a : α<GOAL>Function.Injective (Prod.mk a)
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>b : β<GOAL>Function.Injective fun a => (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<GOAL>(a, b₁) = (a, b₂) ↔ b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b : β<GOAL>(a₁, b) = (a₂, b) ↔ a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p q : α × β<GOAL>p = q ↔ p.1 = q.1 ∧ p.2 = q.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<GOAL>Prod.map f g = fun p => (f p.1, g p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(fun p => (p.1, p.2)) = id
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Prod.map id id = id
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(Prod.map (fun a => a) fun b => b) = fun x => x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>n : ℕ<GOAL>(Prod.map f g)^[n] = Prod.map f^[n] g^[n]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>h : Nonempty β<GOAL>Function.Surjective Prod.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>h : Nonempty α<GOAL>Function.Surjective Prod.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Subsingleton β<GOAL>Function.Injective Prod.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Subsingleton α<GOAL>Function.Injective Prod.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α × β<GOAL>x.swap.swap = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α × β<GOAL>p.swap.1 = p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α × β<GOAL>p.swap.2 = p.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<GOAL>(a, b).swap = (b, a)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Prod.swap ∘ Prod.swap = id
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.LeftInverse Prod.swap Prod.swap
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.RightInverse Prod.swap Prod.swap
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.Injective Prod.swap
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.Surjective Prod.swap
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.Bijective Prod.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p q : α × β<GOAL>p.swap = q.swap ↔ p = q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ<GOAL>Prod.map f g ∘ Prod.swap = Prod.swap ∘ Prod.map g f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α × β<VAR>x : α<GOAL>p.1 = x ↔ p = (x, p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α × β<VAR>x : β<GOAL>p.2 = x ↔ p = (p.1, x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x y : α × β<GOAL>Prod.Lex r s x y ↔ r x.1 y.1 ∨ x.1 = y.1 ∧ s x.2 y.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsRefl α r<VAR>x : α × β<GOAL>Prod.Lex r s x x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsRefl β s<VAR>x : α × β<GOAL>Prod.Lex r s x x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsTrans α r<VAR>IsTrans β s<VAR>x y z : α × β<GOAL>Prod.Lex r s x y → Prod.Lex r s y z → Prod.Lex r s x z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : Function.Injective f<VAR>hg : Function.Injective g<GOAL>Function.Injective (Prod.map f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : Function.Surjective f<VAR>hg : Function.Surjective g<GOAL>Function.Surjective (Prod.map f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : Function.Bijective f<VAR>hg : Function.Bijective g<GOAL>Function.Bijective (Prod.map f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f₁ : α → β<VAR>g₁ : γ → δ<VAR>f₂ : β → α<VAR>g₂ : δ → γ<VAR>hf : Function.LeftInverse f₁ f₂<VAR>hg : Function.LeftInverse g₁ g₂<GOAL>Function.LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f₁ : α → β<VAR>g₁ : γ → δ<VAR>f₂ : β → α<VAR>g₂ : δ → γ<GOAL>Function.RightInverse f₁ f₂ → Function.RightInverse g₁ g₂ → Function.RightInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<GOAL>Function.Involutive f → Function.Involutive g → Function.Involutive (Prod.map f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>Nonempty α<VAR>Nonempty β<VAR>f : α → γ<VAR>g : β → δ<GOAL>Function.Injective (Prod.map f g) ↔ Function.Injective f ∧ Function.Injective g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>Nonempty γ<VAR>Nonempty δ<VAR>f : α → γ<VAR>g : β → δ<GOAL>Function.Surjective (Prod.map f g) ↔ Function.Surjective f ∧ Function.Surjective g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>Nonempty α<VAR>Nonempty β<VAR>f : α → γ<VAR>g : β → δ<GOAL>Function.Bijective (Prod.map f g) ↔ Function.Bijective f ∧ Function.Bijective g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>Nonempty β<VAR>Nonempty δ<VAR>f₁ : α → β<VAR>g₁ : γ → δ<VAR>f₂ : β → α<VAR>g₂ : δ → γ<GOAL>Function.LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂) ↔ Function.LeftInverse f₁ f₂ ∧ Function.LeftInverse g₁ g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>Nonempty α<VAR>Nonempty γ<VAR>f₁ : α → β<VAR>g₁ : γ → δ<VAR>f₂ : β → α<VAR>g₂ : δ → γ<GOAL>Function.RightInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂) ↔ Function.RightInverse f₁ f₂ ∧ Function.RightInverse g₁ g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>Nonempty β<VAR>f : α → α<VAR>g : β → β<GOAL>Function.Involutive (Prod.map f g) ↔ Function.Involutive f ∧ Function.Involutive g
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<GOAL>(List.TProd.mk (i :: l) f).1 = f i
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<GOAL>(List.TProd.mk (i :: l) f).2 = List.TProd.mk l f
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i : ι<VAR>l : List ι<VAR>DecidableEq ι<VAR>v : List.TProd α (i :: l)<GOAL>v.elim ⋯ = v.1
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i j : ι<VAR>l : List ι<VAR>DecidableEq ι<VAR>hj : j ∈ i :: l<VAR>hji : j ≠ i<VAR>v : List.TProd α (i :: l)<GOAL>v.elim hj = List.TProd.elim v.2 ⋯
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i j : ι<VAR>l : List ι<VAR>DecidableEq ι<VAR>hl : (i :: l).Nodup<VAR>hj : j ∈ l<VAR>v : List.TProd α (i :: l)<GOAL>v.elim ⋯ = List.TProd.elim v.2 hj
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>DecidableEq ι<VAR>l : List ι<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>hi : i ∈ l<GOAL>(List.TProd.mk l f).elim hi = f i
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>DecidableEq ι<VAR>l : List ι<GOAL>l.Nodup → ∀ {v w : List.TProd α l}, (∀ (i : ι) (hi : i ∈ l), v.elim hi = w.elim hi) → v = w
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>l : List ι<VAR>DecidableEq ι<VAR>hnd : l.Nodup<VAR>h : ∀ (i : ι), i ∈ l<VAR>v : List.TProd α l<GOAL>List.TProd.mk l (List.TProd.elim' h v) = v
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>l : List ι<VAR>t : (i : ι) → Set (α i)<GOAL>List.TProd.mk l ⁻¹' Set.tprod l t = {i | i ∈ l}.pi t
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>DecidableEq ι<VAR>l : List ι<VAR>hnd : l.Nodup<VAR>h : ∀ (i : ι), i ∈ l<VAR>t : (i : ι) → Set (α i)<GOAL>List.TProd.elim' h ⁻¹' Set.univ.pi t = Set.tprod l t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>(Finset.map f s).val = Multiset.map (⇑f) s.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<GOAL>Finset.map f ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<VAR>b : β<GOAL>b ∈ Finset.map f s ↔ ∃ a ∈ s, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α ≃ β<VAR>b : β<GOAL>b ∈ Finset.map f.toEmbedding s ↔ f.symm b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>a : α<VAR>s : Finset α<GOAL>f a ∈ Finset.map f s ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>a : α<VAR>s : Finset α<GOAL>a ∈ s → f a ∈ Finset.map f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<VAR>p : (a : β) → a ∈ Finset.map f s → Prop<GOAL>(∀ (y : β) (H : y ∈ Finset.map f s), p y H) ↔ ∀ (x : α) (H : x ∈ s), p (f x) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<VAR>x : { x // x ∈ s }<GOAL>f ↑x ∈ Finset.map f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>↑(Finset.map f s) = ⇑f '' ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>↑(Finset.map f s) ⊆ Set.range ⇑f
<VAR>α : Type u_1<VAR>s : Finset α<VAR>σ : Equiv.Perm α<VAR>hs : {a | σ a ≠ a} ⊆ ↑s<GOAL>Finset.map (Equiv.toEmbedding σ) s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Multiset α<GOAL>Finset.map f s.toFinset = (Multiset.map (⇑f) s).toFinset
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Finset.map (Function.Embedding.refl α) s = s
<VAR>α β : Type u_4<VAR>h : α = β<VAR>s : Finset α<GOAL>HEq (Finset.map (Equiv.cast h).toEmbedding s) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>g : β ↪ γ<VAR>s : Finset α<GOAL>Finset.map g (Finset.map f s) = Finset.map (f.trans g) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>β' : Type u_4<VAR>f : β ↪ γ<VAR>g : α ↪ β<VAR>f' : α ↪ β'<VAR>g' : β' ↪ γ<VAR>h_comm : ∀ (a : α), f (g a) = g' (f' a)<GOAL>Finset.map f (Finset.map g s) = Finset.map g' (Finset.map f' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>ga : α ↪ α<VAR>gb : β ↪ β<VAR>h : Function.Semiconj ⇑f ⇑ga ⇑gb<GOAL>Function.Semiconj (Finset.map f) (Finset.map ga) (Finset.map gb)
<VAR>α : Type u_1<VAR>f g : α ↪ α<VAR>h : Function.Commute ⇑f ⇑g<GOAL>Function.Commute (Finset.map f) (Finset.map g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s₁ s₂ : Finset α<GOAL>Finset.map f s₁ ⊆ Finset.map f s₂ ↔ s₁ ⊆ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α ≃ β<GOAL>s ⊆ Finset.map f.symm.toEmbedding t ↔ Finset.map f.toEmbedding s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α ≃ β<GOAL>Finset.map f.symm.toEmbedding t ⊆ s ↔ t ⊆ Finset.map f.toEmbedding s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s₁ s₂ : Finset α<GOAL>Finset.map f s₁ = Finset.map f s₂ ↔ s₁ = s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<GOAL>Function.Injective (Finset.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s t : Finset α<GOAL>Finset.map f s ⊂ Finset.map f t ↔ s ⊂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>(Finset.mapEmbedding f) s = Finset.map f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<VAR>p : β → Prop<VAR>DecidablePred p<GOAL>Finset.filter p (Finset.map f s) = Finset.map f (Finset.filter (p ∘ ⇑f) s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α ↪ β<VAR>s : Finset α<VAR>DecidablePred fun x => ∃ a, p a ∧ f a = x<GOAL>Finset.map f (Finset.filter p s) = Finset.filter (fun b => ∃ a, p a ∧ f a = b) (Finset.map f s)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>p : { x // x ∈ s } → Prop<VAR>DecidablePred p<GOAL>Finset.filter p s.attach = Finset.map { toFun := Subtype.map id ⋯, inj' := ⋯ } (Finset.filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>Finset.filter (fun a => p ↑a) s.attach = Finset.map ((Function.Embedding.refl α).subtypeMap ⋯) (Finset.filter p s).attach
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α ≃ β<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Finset.map f.toEmbedding (Finset.filter p s) = Finset.filter (p ∘ ⇑f.symm) (Finset.map f.toEmbedding s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>f : α ↪ β<GOAL>Disjoint (Finset.map f s) (Finset.map f t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s₁ s₂ : Finset α<VAR>h : Disjoint s₁ s₂<VAR>h' : Disjoint (Finset.map f s₁) (Finset.map f s₂) := ⋯<GOAL>Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s₁ s₂ : Finset α<VAR>h' : Disjoint (Finset.map f s₁) (Finset.map f s₂)<VAR>h : Disjoint s₁ s₂ := ⋯<GOAL>Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>s₁ s₂ : Finset α<GOAL>Finset.map f (s₁ ∪ s₂) = Finset.map f s₁ ∪ Finset.map f s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>s₁ s₂ : Finset α<GOAL>Finset.map f (s₁ ∩ s₂) = Finset.map f s₁ ∩ Finset.map f s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>a : α<GOAL>Finset.map f {a} = {f a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>a : α<VAR>s : Finset α<GOAL>Finset.map f (insert a s) = insert (f a) (Finset.map f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<GOAL>Finset.map f (Finset.cons a s ha) = Finset.cons (f a) (Finset.map f s) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>Finset.map f s = ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>(Finset.map f s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>(Finset.map f s).Nontrivial ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Finset.map (Function.Embedding.subtype fun x => x ∈ s) s.attach = s
<VAR>a b : ℕ<GOAL>Disjoint (Finset.range a) (Finset.map (addLeftEmbedding a) (Finset.range b))
<VAR>a b : ℕ<GOAL>Disjoint (Finset.range a) (Finset.map (addRightEmbedding a) (Finset.range b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s : Finset α<VAR>t : β → Finset γ<VAR>h : (↑(Finset.map f s)).PairwiseDisjoint t<GOAL>(Finset.map f s).disjiUnion t h = s.disjiUnion (fun a => t (f a)) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>t : α → Finset β<VAR>f : β ↪ γ<VAR>h : (↑s).PairwiseDisjoint t<GOAL>Finset.map f (s.disjiUnion t h) = s.disjiUnion (fun a => Finset.map f (t a)) ⋯
<VAR>n : ℕ<GOAL>Finset.range (n + 1) = insert 0 (Finset.map { toFun := fun i => i + 1, inj' := ⋯ } (Finset.range n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>(Finset.image f s).val = (Multiset.map f s.val).dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<GOAL>Finset.image f ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>b : β<GOAL>b ∈ Finset.image f s ↔ ∃ a ∈ s, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ s<GOAL>f a ∈ Finset.image f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>p : β → Prop<GOAL>(∀ b ∈ Finset.image f s, p b) ↔ ∀ a ∈ s, p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>Finset.map f s = Finset.image (⇑f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>b c : β<GOAL>c ∈ Finset.image (Function.const α b) s ↔ s.Nonempty ∧ b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>b : β<GOAL>b ∈ Finset.image (Function.const α b) s ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>h : Set.EqOn f g ↑s<GOAL>Finset.image f s = Finset.image g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>a : α<VAR>hf : Function.Injective f<GOAL>f a ∈ Finset.image f s ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>h : ∀ x ∈ s, f x ∈ t<GOAL>Finset.filter (fun y => y ∈ Finset.image f s) t = Finset.image f s