ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ+<VAR>p : ℕ+ → Sort u_1<VAR>p1 : p 1<VAR>hp : (n : ℕ+) → p n → p (n + 1)<GOAL>(n + 1).recOn p1 hp = hp n (n.recOn p1 hp)
<VAR>m n : ℕ<VAR>NeZero m<VAR>NeZero n<GOAL>OfNat.ofNat m ≤ OfNat.ofNat n ↔ OfNat.ofNat m ≤ OfNat.ofNat n
<VAR>m n : ℕ<VAR>NeZero m<VAR>NeZero n<GOAL>OfNat.ofNat m < OfNat.ofNat n ↔ OfNat.ofNat m < OfNat.ofNat n
<VAR>m n : ℕ<VAR>NeZero m<VAR>NeZero n<GOAL>OfNat.ofNat m = OfNat.ofNat n ↔ OfNat.ofNat m = OfNat.ofNat n
<VAR>m n : ℕ+<GOAL>↑(m * n) = ↑m * ↑n
<GOAL>⇑PNat.coeMonoidHom = Coe.coe
<VAR>n : ℕ+<GOAL>n ≤ 1 ↔ n = 1
<VAR>n m : ℕ+<GOAL>n < m + n
<VAR>n m : ℕ+<GOAL>n < n + m
<VAR>m : ℕ+<VAR>n : ℕ<GOAL>↑(m ^ n) = ↑m ^ n
<VAR>a b : ℕ+<VAR>hab : a < b<GOAL>1 < b
<VAR>a : ℕ+<GOAL>a + 1 = (↑a).succPNat
<VAR>a : ℕ+<GOAL>a < (↑a).succPNat
<VAR>a b : ℕ+<GOAL>↑(a - b) = if b < a then ↑a - ↑b else 1
<VAR>a b : ℕ+<GOAL>a < b → a + (b - a) = b
<VAR>n : ℕ+<GOAL>n ≠ 1 → ∃ k, n = k + 1
<VAR>k : ℕ+<VAR>r q : ℕ<GOAL>¬(r = 0 ∧ q = 0) → ↑(k.modDivAux r q).1 + ↑k * (k.modDivAux r q).2 = r + ↑k * q
<VAR>m k : ℕ+<GOAL>m.mod k ≤ m ∧ m.mod k ≤ k
<VAR>k m : ℕ+<GOAL>k ∣ m ↔ ↑k ∣ ↑m
<VAR>m n : ℕ+<GOAL>m ∣ n → n ∣ m → m = n
<VAR>n : ℕ+<GOAL>n ∣ 1 ↔ n = 1
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x : (i : Fin (n + 1)) → α i<VAR>s : (i : Fin (n + 1)) → Finset (α i)<GOAL>x ∈ Fintype.piFinset s ↔ x 0 ∈ s 0 ∧ Fin.tail x ∈ Fintype.piFinset (Fin.tail s)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x : (i : Fin (n + 1)) → α i<VAR>s : (i : Fin (n + 1)) → Finset (α i)<GOAL>x ∈ Fintype.piFinset s ↔ Fin.init x ∈ Fintype.piFinset (Fin.init s) ∧ x (Fin.last n) ∈ s (Fin.last n)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x₀ : α 0<VAR>x : (i : Fin n) → α i.succ<VAR>s₀ : Finset (α 0)<VAR>s : (i : Fin n) → Finset (α i.succ)<GOAL>Fin.cons x₀ x ∈ Fintype.piFinset (Fin.cons s₀ s) ↔ x₀ ∈ s₀ ∧ x ∈ Fintype.piFinset s
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x : (i : Fin n) → α i.castSucc<VAR>xₙ : α (Fin.last n)<VAR>s : (i : Fin n) → Finset (α i.castSucc)<VAR>sₙ : Finset (α (Fin.last n))<GOAL>Fin.snoc x xₙ ∈ Fintype.piFinset (Fin.snoc s sₙ) ↔ x ∈ Fintype.piFinset s ∧ xₙ ∈ sₙ
<VAR>m n : ℕ<VAR>self : Fin2.IsLT m n<GOAL>m < n
<VAR>n : ℕ<GOAL>Fin2.last.rev = Fin2.fz
<VAR>n : ℕ<VAR>i : Fin2 n<GOAL>i.castSucc.rev = i.rev.fs
<VAR>n : ℕ<VAR>i : Fin2 n<GOAL>i.rev.rev = i
<VAR>n : ℕ<GOAL>Function.Involutive Fin2.rev
<VAR>α β γ : Type u<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<GOAL>Option.map₂ f a b = Seq.seq (f <$> a) fun x => b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : α<VAR>b : β<GOAL>Option.map₂ f (some a) (some b) = some (f a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>b : Option β<GOAL>Option.map₂ f none b = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : Option α<GOAL>Option.map₂ f a none = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : α<VAR>b : Option β<GOAL>Option.map₂ f (some a) b = Option.map (fun b => f a b) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : β<GOAL>Option.map₂ f a (some b) = Option.map (fun a => f a b) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<VAR>c : γ<GOAL>c ∈ Option.map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<GOAL>Option.map₂ f a b = none ↔ a = none ∨ b = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<GOAL>Option.map₂ f a b = Option.map₂ (fun a b => f b a) b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>f : α → β → γ<VAR>g : γ → δ<GOAL>Option.map g (Option.map₂ f a b) = Option.map₂ (fun a b => g (f a b)) a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>f : γ → β → δ<VAR>g : α → γ<GOAL>Option.map₂ f (Option.map g a) b = Option.map₂ (fun a b => f (g a) b) a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>f : α → γ → δ<VAR>g : β → γ<GOAL>Option.map₂ f a (Option.map g b) = Option.map₂ (fun a b => f a (g b)) a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α × β → γ<VAR>a : Option α<VAR>b : Option β<GOAL>Option.map₂ (Function.curry f) a b = Option.map f (Option.map₂ Prod.mk a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>x : Option (α × β)<GOAL>Option.map (Function.uncurry f) x = Option.map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>c : Option γ<VAR>ε : Type u_8<VAR>ε' : Type u_9<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>Option.map₂ f (Option.map₂ g a b) c = Option.map₂ f' a (Option.map₂ g' b c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<VAR>g : β → α → γ<VAR>h_comm : ∀ (a : α) (b : β), f a b = g b a<GOAL>Option.map₂ f a b = Option.map₂ g b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>c : Option γ<VAR>δ' : Type u_7<VAR>ε : Type u_8<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>Option.map₂ f a (Option.map₂ g b c) = Option.map₂ g' b (Option.map₂ f' a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>c : Option γ<VAR>δ' : Type u_7<VAR>ε : Type u_8<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>Option.map₂ f (Option.map₂ g a b) c = Option.map₂ g' (Option.map₂ f' a c) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>g : γ → δ<VAR>f' : α' → β' → δ<VAR>g₁ : α → α'<VAR>g₂ : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)<GOAL>Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g₁ a) (Option.map g₂ b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<VAR>α' : Type u_5<VAR>g : γ → δ<VAR>f' : α' → β → δ<VAR>g' : α → α'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b<GOAL>Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g' a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<VAR>β' : Type u_6<VAR>g : γ → δ<VAR>f' : α → β' → δ<VAR>g' : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)<GOAL>Option.map g (Option.map₂ f a b) = Option.map₂ f' a (Option.map g' b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>α' : Type u_5<VAR>f : α' → β → γ<VAR>g : α → α'<VAR>f' : α → β → δ<VAR>g' : δ → γ<VAR>h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)<GOAL>Option.map₂ f (Option.map g a) b = Option.map g' (Option.map₂ f' a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>β' : Type u_6<VAR>f : α → β' → γ<VAR>g : β → β'<VAR>f' : α → β → δ<VAR>g' : δ → γ<VAR>h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)<GOAL>Option.map₂ f a (Option.map g b) = Option.map g' (Option.map₂ f' a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<VAR>α' : Type u_5<VAR>β' : Type u_6<VAR>g : γ → δ<VAR>f' : β' → α' → δ<VAR>g₁ : β → β'<VAR>g₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)<GOAL>Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g₁ b) (Option.map g₂ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<VAR>β' : Type u_6<VAR>g : γ → δ<VAR>f' : β' → α → δ<VAR>g' : β → β'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a<GOAL>Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g' b) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<VAR>α' : Type u_5<VAR>g : γ → δ<VAR>f' : β → α' → δ<VAR>g' : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)<GOAL>Option.map g (Option.map₂ f a b) = Option.map₂ f' b (Option.map g' a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>α' : Type u_5<VAR>f : α' → β → γ<VAR>g : α → α'<VAR>f' : β → α → δ<VAR>g' : δ → γ<VAR>h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)<GOAL>Option.map₂ f (Option.map g a) b = Option.map g' (Option.map₂ f' b a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a : Option α<VAR>b : Option β<VAR>β' : Type u_6<VAR>f : α → β' → γ<VAR>g : β → β'<VAR>f' : β → α → δ<VAR>g' : δ → γ<VAR>h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)<GOAL>Option.map₂ f a (Option.map g b) = Option.map g' (Option.map₂ f' b a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>a : α<VAR>h : ∀ (b : β), f a b = b<VAR>o : Option β<GOAL>Option.map₂ f (some a) o = o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → α<VAR>b : β<VAR>h : ∀ (a : α), f a b = a<VAR>o : Option α<GOAL>Option.map₂ f o (some b) = o
<VAR>p : Nat.Primes<GOAL>Multiset.card (PrimeMultiset.ofPrime p) = 1
<GOAL>⇑PrimeMultiset.coeNatMonoidHom = Coe.coe
<VAR>p : Nat.Primes<GOAL>(PrimeMultiset.ofPrime p).toNatMultiset = {↑p}
<GOAL>⇑PrimeMultiset.coePNatMonoidHom = Coe.coe
<VAR>p : Nat.Primes<GOAL>(PrimeMultiset.ofPrime p).toPNatMultiset = {↑p}
<VAR>v : PrimeMultiset<GOAL>Multiset.map PNat.val v.toPNatMultiset = v.toNatMultiset
<VAR>p : Nat.Primes<GOAL>(PrimeMultiset.ofPrime p).prod = ↑p
<VAR>v : Multiset ℕ<VAR>h : ∀ p ∈ v, Nat.Prime p<GOAL>(PrimeMultiset.ofNatMultiset v h).toNatMultiset = v
<VAR>v : Multiset ℕ<VAR>h : ∀ p ∈ v, Nat.Prime p<GOAL>↑(PrimeMultiset.ofNatMultiset v h).prod = v.prod
<VAR>v : Multiset ℕ+<VAR>h : ∀ p ∈ v, p.Prime<GOAL>(PrimeMultiset.ofPNatMultiset v h).toPNatMultiset = v
<VAR>v : Multiset ℕ+<VAR>h : ∀ p ∈ v, p.Prime<GOAL>(PrimeMultiset.ofPNatMultiset v h).prod = v.prod
<VAR>l : List ℕ<VAR>h : ∀ p ∈ l, Nat.Prime p<GOAL>↑(PrimeMultiset.ofNatList l h).prod = l.prod
<VAR>l : List ℕ+<VAR>h : ∀ p ∈ l, p.Prime<GOAL>(PrimeMultiset.ofPNatList l h).prod = l.prod
<VAR>u v : PrimeMultiset<GOAL>(u + v).prod = u.prod * v.prod
<VAR>n : ℕ+<GOAL>n.factorMultiset.prod = n
<VAR>n : ℕ+<GOAL>n.factorMultiset.toNatMultiset = ↑(↑n).primeFactorsList
<VAR>n m : ℕ+<GOAL>(n * m).factorMultiset = n.factorMultiset + m.factorMultiset
<VAR>n : ℕ+<VAR>m : ℕ<GOAL>(n ^ m).factorMultiset = m • n.factorMultiset
<VAR>m n : ℕ+<GOAL>m.factorMultiset ≤ n.factorMultiset ↔ m ∣ n
<VAR>u v : PrimeMultiset<GOAL>(u ⊓ v).prod = u.prod.gcd v.prod
<VAR>u v : PrimeMultiset<GOAL>(u ⊔ v).prod = u.prod.lcm v.prod
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<VAR>P : (Fin n → α) → Prop<VAR>hf : P f<VAR>h : ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n), i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))<GOAL>P (f ∘ ⇑(Tuple.sort f))
<VAR>n : ℕ<VAR>α : Type u_1<VAR>LinearOrder α<VAR>f : Fin n → α<VAR>P : (Fin n → α) → Prop<VAR>hf : P f<VAR>h : ∀ (g : Fin n → α) (i j : Fin n), i < j → g j < g i → P g → P (g ∘ ⇑(Equiv.swap i j))<GOAL>P (f ∘ ⇑(Tuple.sort f))
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>s : Finset α<VAR>H : ∀ (x : α), x ∈ s ↔ p x<GOAL>Fintype.card { x // p x } = s.card
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>s : Finset α<VAR>H : ∀ (x : α), x ∈ s ↔ p x<VAR>Fintype { x // p x }<GOAL>Fintype.card { x // p x } = s.card
<VAR>α : Type u_1<VAR>p : Set α<VAR>s : Finset α<VAR>H : ∀ (x : α), x ∈ s ↔ x ∈ p<GOAL>Fintype.card ↑p = s.card
<VAR>α : Type u_1<VAR>p : Set α<VAR>s : Finset α<VAR>H : ∀ (x : α), x ∈ s ↔ x ∈ p<VAR>Fintype ↑p<GOAL>Fintype.card ↑p = s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>f : α ≃ β<GOAL>Fintype.card β = Fintype.card α
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Fintype α<VAR>Fintype β<VAR>f : α ≃ β<GOAL>Fintype.card α = Fintype.card β
<VAR>α β : Type u_4<VAR>Fintype α<VAR>Fintype β<VAR>h : α = β<GOAL>Fintype.card α = Fintype.card β
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>_F : Fintype α<VAR>_G : Fintype β<GOAL>Fintype.card α = Fintype.card β ↔ Nonempty (α ≃ β)
<VAR>α : Type u_1<VAR>a : α<VAR>Subsingleton α<GOAL>Fintype.card α = 1
<VAR>α : Type u_1<VAR>Unique α<VAR>h : Fintype α<GOAL>Fintype.card α = 1
<VAR>α : Type u_1<VAR>IsEmpty α<GOAL>Fintype.card α = 0
<VAR>α : Type u_4<VAR>s : Set α<VAR>Fintype ↑s<GOAL>s.toFinset.card = Fintype.card ↑s
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Finset.univ.card = Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>hs : s.card = Fintype.card α<GOAL>s = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>s.card = Fintype.card α ↔ s = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>s.card ≤ Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>x : α<VAR>hx : x ∉ s<GOAL>s.card < Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>s.card < Fintype.card α ↔ s ≠ Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>sᶜ.card < Fintype.card α ↔ s.Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<GOAL>(Finset.univ \ s).card = Fintype.card α - s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<GOAL>sᶜ.card = Fintype.card α - s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<GOAL>s.card + sᶜ.card = Fintype.card α
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Finset α<GOAL>sᶜ.card + s.card = Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Set α<VAR>Fintype ↑s<VAR>Fintype ↑sᶜ<GOAL>Fintype.card ↑sᶜ = Fintype.card α - Fintype.card ↑s
<VAR>n : ℕ<GOAL>Fintype.card (Fin n) = n
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>Fintype.card { i // ↑i < m } = m
<VAR>n : ℕ<GOAL>Finset.univ.card = n
<VAR>n m : ℕ<VAR>h : Fin n = Fin m<GOAL>cast h = Fin.cast ⋯
<VAR>n : ℕ<VAR>s : Finset (Fin n)<GOAL>s.card ≤ n
<VAR>α : Type u_1<VAR>y : α<VAR>Fintype { x // x = y }<GOAL>Fintype.card { x // x = y } = 1
<VAR>α : Type u_1<VAR>y : α<VAR>Fintype { x // y = x }<GOAL>Fintype.card { x // y = x } = 1
<GOAL>Fintype.card PEmpty.{u_4 + 1} = 0
<GOAL>Fintype.card PUnit.{u_4 + 1} = 1
<VAR>α : Type u_4<VAR>Fintype α<GOAL>Fintype.card (ULift.{u_5, u_4} α) = Fintype.card α
<VAR>α : Type u_4<VAR>Fintype α<GOAL>Fintype.card (PLift α) = Fintype.card α
<VAR>α : Type u_4<VAR>Fintype α<GOAL>Fintype.card αᵒᵈ = Fintype.card α
<VAR>α : Type u_4<VAR>Fintype α<GOAL>Fintype.card (Lex α) = Fintype.card α
<VAR>α : Type u_4<VAR>Fintype α<GOAL>Fintype.card (Multiplicative α) = Fintype.card α
<VAR>α : Type u_4<VAR>Fintype α<GOAL>Fintype.card (Additive α) = Fintype.card α
<VAR>α : Type u_4<VAR>_inst : Fintype α<GOAL>Finite α
<VAR>α : Type u_4<GOAL>Finite α ↔ Nonempty (Fintype α)
<VAR>α : Type u_4<VAR>Finite α<GOAL>Nonempty (Fintype α)
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>Finite β<VAR>f : α → β<VAR>H : Function.Injective f<GOAL>Finite α
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>Finite α<VAR>f : α → β<VAR>H : Function.Surjective f<GOAL>Finite β
<VAR>α : Type u_4<VAR>Finite α<GOAL>∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l
<VAR>α : Type u_4<VAR>Fintype α<VAR>l : List α<VAR>h : l.Nodup<GOAL>l.length ≤ Fintype.card α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Fintype.card α ≤ Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α ↪ β<GOAL>Fintype.card α ≤ Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>h : Function.Injective f<VAR>b : β<VAR>w : b ∉ Set.range f<GOAL>Fintype.card α < Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>h : Function.Injective f<VAR>h' : ¬Function.Surjective f<GOAL>Fintype.card α < Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>h : Function.Surjective f<GOAL>Fintype.card β ≤ Fintype.card α
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : α → β<VAR>Fintype α<VAR>Fintype ↑(Set.range f)<GOAL>Fintype.card ↑(Set.range f) ≤ Fintype.card α
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>F : Type u_6<VAR>FunLike F α β<VAR>EmbeddingLike F α β<VAR>f : F<VAR>Fintype α<VAR>Fintype ↑(Set.range ⇑f)<GOAL>Fintype.card ↑(Set.range ⇑f) = Fintype.card α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>h : Fintype.card β < Fintype.card α<GOAL>∃ x y, x ≠ y ∧ f x = f y
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Fintype.card α = 1 ↔ ∃ x, ∀ (y : α), y = x
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Fintype.card α = 0 ↔ IsEmpty α
<VAR>α : Type u_1<VAR>Fintype α<VAR>IsEmpty α<GOAL>Fintype.card α = 0
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Fintype.card α = 1 ↔ Nonempty (Unique α)
<VAR>α : Type u_1<VAR>Fintype α<GOAL>0 < Fintype.card α ↔ Nonempty α
<VAR>α : Type u_1<VAR>Fintype α<VAR>h : Nonempty α<GOAL>0 < Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<GOAL>Fintype.card α ≠ 0
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Fintype.card α ≤ 1 ↔ ∀ (a b : α), a = b
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Fintype.card α ≤ 1 ↔ Subsingleton α
<VAR>α : Type u_1<VAR>Fintype α<GOAL>1 < Fintype.card α ↔ Nontrivial α
<VAR>α : Type u_1<VAR>Fintype α<VAR>h : 1 < Fintype.card α<VAR>a : α<GOAL>∃ b, b ≠ a
<VAR>α : Type u_1<VAR>Fintype α<VAR>h : 1 < Fintype.card α<GOAL>∃ a b, a ≠ b
<VAR>α : Type u_1<VAR>Fintype α<VAR>i : α<VAR>h : ∀ (j : α), j = i<GOAL>Fintype.card α = 1
<VAR>α : Type u_4<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>(∃! a, p a) ↔ (Finset.filter p Finset.univ).card = 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>h : Nontrivial α<GOAL>1 < Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<GOAL>1 < Fintype.card α ↔ ∃ a b, a ≠ b
<VAR>α : Type u_1<VAR>Fintype α<GOAL>2 < Fintype.card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>hf : Function.Bijective f<GOAL>Fintype.card α = Fintype.card β
<VAR>α : Type u_1<VAR>Finite α<VAR>f : α → α<VAR>hinj : Function.Injective f<GOAL>Function.Surjective f
<VAR>α : Type u_1<VAR>Finite α<VAR>f : α → α<GOAL>Function.Injective f ↔ Function.Surjective f
<VAR>α : Type u_1<VAR>Finite α<VAR>f : α → α<GOAL>Function.Injective f ↔ Function.Bijective f
<VAR>α : Type u_1<VAR>Finite α<VAR>f : α → α<GOAL>Function.Surjective f ↔ Function.Bijective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite α<VAR>f : α → β<VAR>e : α ≃ β<GOAL>Function.Injective f ↔ Function.Surjective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<GOAL>Function.Bijective f ↔ Function.Injective f ∧ Fintype.card α = Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<GOAL>Function.Bijective f ↔ Function.Surjective f ∧ Fintype.card α = Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>g : β → α<VAR>hfg : Function.LeftInverse f g<VAR>hcard : Fintype.card α ≤ Fintype.card β<GOAL>Function.RightInverse f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>g : β → α<VAR>hfg : Function.RightInverse f g<VAR>hcard : Fintype.card β ≤ Fintype.card α<GOAL>Function.LeftInverse f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>hβα : Fintype.card β ≤ Fintype.card α<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse g f<GOAL>∀ (a : β), (Equiv.ofLeftInverseOfCardLE hβα f g h).symm a = g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>hβα : Fintype.card β ≤ Fintype.card α<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse g f<GOAL>∀ (a : α), (Equiv.ofLeftInverseOfCardLE hβα f g h) a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>hαβ : Fintype.card α ≤ Fintype.card β<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.RightInverse g f<GOAL>∀ (a : α), (Equiv.ofRightInverseOfCardLE hαβ f g h) a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>hαβ : Fintype.card α ≤ Fintype.card β<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.RightInverse g f<GOAL>∀ (a : β), (Equiv.ofRightInverseOfCardLE hαβ f g h).symm a = g a
<VAR>α : Type u_1<VAR>s : Finset α<VAR>Fintype { x // x ∈ s }<GOAL>Fintype.card { x // x ∈ s } = s.card
<VAR>α : Type u_1<VAR>s : Finset α<VAR>n : ℕ<VAR>i : { x // x ∈ s } ≃ Fin n<GOAL>s.card = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>Fintype β<VAR>i : { x // x ∈ s } ≃ β<GOAL>s.card = Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>i : { x // x ∈ s } ≃ { x // x ∈ t }<GOAL>s.card = t.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>n : ℕ<VAR>s : Finset α<VAR>hsn : s.card ≤ n<VAR>hnα : n ≤ Fintype.card α<GOAL>∃ t, s ⊆ t ∧ t.card = n
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Set α<VAR>Fintype ↑s<GOAL>Fintype.card ↑s ≤ Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Set α<VAR>Fintype ↑s<GOAL>Fintype.card ↑s = Fintype.card α ↔ s = Set.univ
<VAR>α : Type u_1<VAR>Finite α<VAR>e : α ↪ α<GOAL>e.equivOfFintypeSelfEmbedding.toEmbedding = e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>h : Fintype.card β < Fintype.card α<GOAL>IsEmpty (α ↪ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>h : Fintype.card α ≤ Fintype.card β<GOAL>Nonempty (α ↪ β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<GOAL>Nonempty (α ↪ β) ↔ Fintype.card α ≤ Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>s : Finset β<VAR>h : Fintype.card α ≤ s.card<GOAL>∃ f, Set.range ⇑f ⊆ ↑s
<VAR>α : Type u_4<VAR>Fintype α<VAR>e : α ↪ α<GOAL>Finset.map e Finset.univ = Finset.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : α → β<VAR>h : Function.Surjective f<VAR>h' : ¬Function.Injective f<GOAL>Fintype.card β < Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Fintype.card { x // p x } ≤ Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>x : α<VAR>hx : ¬p x<GOAL>Fintype.card { x // p x } < Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Fintype.card { x // p x } = (Finset.filter p Finset.univ).card
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>Fintype { x // p x }<VAR>Fintype { x // ¬p x }<GOAL>Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x }
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>h : p ≤ q<VAR>Fintype { x // p x }<VAR>Fintype { x // q x }<GOAL>Fintype.card { x // p x } ≤ Fintype.card { x // q x }
<VAR>α : Type u_1<VAR>Finite α<VAR>p q : α → Prop<VAR>Fintype { x // p x }<VAR>Fintype { x // ¬p x }<VAR>Fintype { x // q x }<VAR>Fintype { x // ¬q x }<VAR>h : Fintype.card { x // p x } = Fintype.card { x // q x }<GOAL>Fintype.card { x // ¬p x } = Fintype.card { x // ¬q x }
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Setoid α<VAR>DecidableRel fun x x_1 => x ≈ x_1<GOAL>Fintype.card (Quotient s) ≤ Fintype.card α
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Setoid α<VAR>DecidableRel fun x x_1 => x ≈ x_1<VAR>x y : α<VAR>h1 : x ≠ y<VAR>h2 : x ≈ y<GOAL>Fintype.card (Quotient s) < Fintype.card α
<VAR>α : Type u_4<VAR>Fintype α<VAR>x : α<VAR>h : Fintype.card α = 1<GOAL>Finset.univ = {x}
<VAR>α : Type u_1<VAR>Finite α<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>IsIrrefl α r<GOAL>WellFounded r
<VAR>α : Type u_1<VAR>Infinite α<VAR>_h : Fintype α<GOAL>False
<VAR>α : Type u_4<GOAL>IsEmpty (Fintype α) ↔ Infinite α
<VAR>α : Type u_4<VAR>Preorder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>∃ m ∈ s, ∀ x ∈ s, ¬x < m
<VAR>α : Type u_4<VAR>Preorder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>∃ m ∈ s, ∀ x ∈ s, ¬m < x
<VAR>α : Type u_1<VAR>h : Fintype α → False<GOAL>Infinite α
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s ≠ Set.univ<VAR>f : α → ↑s<VAR>hf : Function.Injective f<GOAL>Infinite α
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s ≠ Set.univ<VAR>f : ↑s → α<VAR>hf : Function.Surjective f<GOAL>Infinite α