ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → β<VAR>q : β → Prop<VAR>h : Computable f<VAR>i : Function.Injective f<GOAL>(fun a => q (f a)) ≤₁ q
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<GOAL>p ≤₁ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<GOAL>p ≤₁ q → q ≤₁ r → p ≤₁ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>p ≤₁ q → p ≤₀ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>e : α ≃ β<VAR>q : β → Prop<VAR>h : Computable ⇑e<GOAL>(q ∘ ⇑e) ≤₁ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>e : α ≃ β<VAR>q : β → Prop<VAR>h : Computable ⇑e.symm<GOAL>q ≤₁ (q ∘ ⇑e)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Reflexive OneOneReducible
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Transitive OneOneReducible
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → Prop<VAR>q : β → Prop<VAR>h₁ : p ≤₀ q<VAR>h₂ : ComputablePred q<GOAL>ComputablePred p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → Prop<VAR>q : β → Prop<VAR>h : p ≤₁ q<GOAL>ComputablePred q → ComputablePred p
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<GOAL>ManyOneEquiv p p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>ManyOneEquiv p q → ManyOneEquiv q p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<GOAL>ManyOneEquiv p q → ManyOneEquiv q r → ManyOneEquiv p r
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Equivalence ManyOneEquiv
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<GOAL>OneOneEquiv p p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>OneOneEquiv p q → OneOneEquiv q p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<GOAL>OneOneEquiv p q → OneOneEquiv q r → OneOneEquiv p r
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Equivalence OneOneEquiv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>OneOneEquiv p q → ManyOneEquiv p q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>e : α ≃ β<GOAL>e.Computable → e.symm.Computable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>e₁ : α ≃ β<VAR>e₂ : β ≃ γ<GOAL>e₁.Computable → e₂.Computable → (e₁.trans e₂).Computable
<VAR>α : Type u_1<VAR>Denumerable α<GOAL>(Denumerable.eqv α).Computable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Denumerable α<VAR>Denumerable β<GOAL>(Denumerable.equiv₂ α β).Computable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>e : α ≃ β<VAR>h : e.Computable<VAR>p : β → Prop<GOAL>OneOneEquiv (p ∘ ⇑e) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>e : α ≃ β<VAR>h : e.Computable<VAR>p : β → Prop<GOAL>ManyOneEquiv (p ∘ ⇑e) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>h : ManyOneEquiv p q<GOAL>p ≤₀ r ↔ q ≤₀ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>h : ManyOneEquiv q r<GOAL>p ≤₀ q ↔ p ≤₀ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>h : OneOneEquiv p q<GOAL>p ≤₁ r ↔ q ≤₁ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>h : OneOneEquiv q r<GOAL>p ≤₁ q ↔ p ≤₁ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>h : ManyOneEquiv p q<GOAL>ManyOneEquiv p r ↔ ManyOneEquiv q r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>h : ManyOneEquiv q r<GOAL>ManyOneEquiv p q ↔ ManyOneEquiv p r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>h : OneOneEquiv p q<GOAL>OneOneEquiv p r ↔ OneOneEquiv q r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>h : OneOneEquiv q r<GOAL>OneOneEquiv p q ↔ OneOneEquiv p r
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>(ULower.equiv α).Computable
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<GOAL>ManyOneEquiv (p ∘ ULower.up) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>p ≤₁ p ⊕' q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>q ≤₁ p ⊕' q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<GOAL>p ≤₀ r → q ≤₀ r → p ⊕' q ≤₀ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<GOAL>p ⊕' q ≤₀ r ↔ p ≤₀ r ∧ q ≤₀ r
<VAR>α : Type u<VAR>Primcodable α<VAR>Inhabited α<VAR>p : Set α<GOAL>toNat p ≤₀ p
<VAR>α : Type u<VAR>Primcodable α<VAR>Inhabited α<VAR>p : Set α<GOAL>p ≤₀ toNat p
<VAR>α : Type u<VAR>Primcodable α<VAR>Inhabited α<VAR>β : Type v<VAR>Primcodable β<VAR>Inhabited β<VAR>p : Set α<VAR>q : Set β<GOAL>toNat p ≤₀ toNat q ↔ p ≤₀ q
<VAR>α : Type u<VAR>Primcodable α<VAR>Inhabited α<VAR>p : Set α<GOAL>ManyOneEquiv (toNat p) p
<VAR>α : Type u<VAR>Primcodable α<VAR>Inhabited α<VAR>β : Type v<VAR>Primcodable β<VAR>Inhabited β<VAR>p : Set α<VAR>q : Set β<GOAL>ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q
<VAR>C : ManyOneDegree → Prop<VAR>d : ManyOneDegree<VAR>h : ∀ (p : Set ℕ), C (ManyOneDegree.of p)<GOAL>C d
<VAR>φ : Sort u_1<VAR>p : Set ℕ<VAR>f : Set ℕ → φ<VAR>h : ∀ (p q : ℕ → Prop), ManyOneEquiv p q → f p = f q<GOAL>(ManyOneDegree.of p).liftOn f h = f p
<VAR>φ : Sort u_1<VAR>p q : Set ℕ<VAR>f : Set ℕ → Set ℕ → φ<VAR>h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂<GOAL>(ManyOneDegree.of p).liftOn₂ (ManyOneDegree.of q) f h = f p q
<VAR>α : Type u<VAR>Primcodable α<VAR>Inhabited α<VAR>β : Type v<VAR>Primcodable β<VAR>Inhabited β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>ManyOneDegree.of p = ManyOneDegree.of q ↔ ManyOneEquiv p q
<VAR>α : Type u<VAR>Primcodable α<VAR>Inhabited α<VAR>β : Type v<VAR>Primcodable β<VAR>Inhabited β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>ManyOneDegree.of p ≤ ManyOneDegree.of q ↔ p ≤₀ q
<VAR>d : ManyOneDegree<GOAL>d ≤ d
<VAR>d₁ d₂ : ManyOneDegree<GOAL>d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂
<VAR>d₁ d₂ d₃ : ManyOneDegree<GOAL>d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃
<VAR>α : Type u<VAR>Primcodable α<VAR>Inhabited α<VAR>β : Type v<VAR>Primcodable β<VAR>Inhabited β<VAR>p : Set α<VAR>q : Set β<GOAL>ManyOneDegree.of (p ⊕' q) = ManyOneDegree.of p + ManyOneDegree.of q
<VAR>d₁ d₂ d₃ : ManyOneDegree<GOAL>d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃
<VAR>d₁ d₂ : ManyOneDegree<GOAL>d₁ ≤ d₁ + d₂
<VAR>d₁ d₂ : ManyOneDegree<GOAL>d₂ ≤ d₁ + d₂
<VAR>α : Sort u_1<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>a : p → α<VAR>b : ¬p → q → α<VAR>c : ¬p → ¬q → α<GOAL>(dite p a fun hp => dite q (b hp) (c hp)) = if hq : q then dite p a fun hp => b hp hq else dite p a fun hp => c hp hq
<VAR>α : Sort u_1<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>a : p → q → α<VAR>b : p → ¬q → α<VAR>c : ¬p → α<GOAL>dite p (fun hp => dite q (a hp) (b hp)) c = if hq : q then dite p (fun hp => a hp hq) c else dite p (fun hp => b hp hq) c
<VAR>α : Sort u_1<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>a : α<VAR>b : q → α<VAR>c : ¬q → α<GOAL>(if p then a else dite q b c) = if hq : q then if p then a else b hq else if p then a else c hq
<VAR>α : Sort u_1<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>a : q → α<VAR>b : ¬q → α<VAR>c : α<GOAL>(if p then dite q a b else c) = if hq : q then if p then a hq else c else if p then b hq else c
<VAR>α : Sort u_1<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>a : p → α<VAR>b c : ¬p → α<GOAL>(dite p a fun hp => if q then b hp else c hp) = if q then dite p a b else dite p a c
<VAR>α : Sort u_1<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>a b : p → α<VAR>c : ¬p → α<GOAL>dite p (fun hp => if q then a hp else b hp) c = if q then dite p a c else dite p b c
<VAR>α : Sort u_1<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>a b c : α<GOAL>(if p then a else if q then b else c) = if q then if p then a else b else if p then a else c
<VAR>α : Sort u_1<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>a b c : α<GOAL>(if p then if q then a else b else c) = if q then if p then a else c else if p then b else c
<VAR>f : Prop → Prop<GOAL>(∀ (p : Prop), f p) ↔ f True ∧ f False
<VAR>f : Prop → Prop<GOAL>(∃ p, f p) ↔ f True ∨ f False
<VAR>α β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>x : α<VAR>y : β<VAR>h₁ : HEq f g<VAR>h₂ : HEq x y<GOAL>f x = g y
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>f : (a : α) → β a<VAR>a₁ a₂ : α<GOAL>a₁ = a₂ → HEq (f a₁) (f a₂)
<VAR>α : Sort u_1<VAR>b c : α<GOAL>(∀ {a : α}, a = b ↔ a = c) ↔ b = c
<VAR>α : Sort u_1<VAR>a b : α<GOAL>(∀ {c : α}, a = c ↔ b = c) ↔ a = b
<VAR>α : Sort u_1<VAR>a b c : α<VAR>h : b ≠ c<GOAL>a ≠ b ∧ a = c ↔ a = c
<VAR>p : Prop<VAR>self : Fact p<GOAL>p
<VAR>p : Prop<VAR>h : Fact p<GOAL>p
<VAR>a b : Prop<GOAL>(a → b) → ¬b → ¬a
<VAR>p : Prop<VAR>Decidable p<GOAL>¬p ∨ p
<VAR>α : Sort u_1<VAR>x y : α<VAR>Decidable (x = y)<GOAL>x = y ∨ x ≠ y
<VAR>α : Sort u_1<VAR>x y : α<VAR>Decidable (x = y)<GOAL>x ≠ y ∨ x = y
<VAR>α : Sort u_1<VAR>x y : α<GOAL>x = y ∨ x ≠ y
<VAR>α : Sort u_1<VAR>x y : α<GOAL>x ≠ y ∨ x = y
<VAR>α : Sort u_1<VAR>a b : α<GOAL>¬a ≠ b ↔ a = b
<VAR>a b : Prop<GOAL>¬(a → b) → a
<VAR>a b : Prop<GOAL>(¬a → b) → ¬b → a
<VAR>a b : Prop<GOAL>¬a → b ↔ ¬b → a
<VAR>a : Prop<GOAL>¬a → a ↔ a
<VAR>a : Sort u_1<VAR>b : Sort u_2<VAR>c : Prop<GOAL>a → b → c ↔ b → a → c
<VAR>a b : Prop<VAR>h : a ↔ ¬b<GOAL>¬a ↔ b
<VAR>a b : Prop<VAR>h : ¬a ↔ b<GOAL>a ↔ ¬b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>a b : α<VAR>c d : β<GOAL>(a = b ↔ c = d) → (a ≠ b ↔ c ≠ d)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>a b : α<VAR>c d : β<GOAL>(a = b ↔ c ≠ d) → (a ≠ b ↔ c = d)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>a b : α<VAR>c d : β<GOAL>(a ≠ b ↔ c = d) → (a = b ↔ c ≠ d)
<VAR>a b : Prop<GOAL>Xor' a b = Xor' b a
<VAR>a b : Prop<GOAL>Xor' (¬a) b ↔ (a ↔ b)
<VAR>a b : Prop<GOAL>Xor' a ¬b ↔ (a ↔ b)
<VAR>a b : Prop<GOAL>Xor' (¬a) ¬b ↔ Xor' a b
<VAR>a b : Prop<VAR>h : Xor' a b<GOAL>a ∨ b
<VAR>α : Sort u_1<VAR>a b : α<VAR>p : Prop<GOAL>p ∧ a = b ↔ p ∧ b = a
<VAR>α : Sort u_1<VAR>a b : α<VAR>p : Prop<GOAL>a = b ∧ p ↔ b = a ∧ p
<VAR>a b c d : Prop<VAR>h : a ∨ b ∨ c<VAR>ha : a → d<VAR>hb : b → d<VAR>hc : c → d<GOAL>d
<VAR>a b d e c f : Prop<VAR>had : a → d<VAR>hbe : b → e<VAR>hcf : c → f<GOAL>a ∨ b ∨ c → d ∨ e ∨ f
<VAR>a b : Prop<GOAL>(a → b) → ¬a ∨ b
<VAR>a b : Prop<VAR>Decidable a<VAR>h : a → b<GOAL>b ∨ ¬a
<VAR>a b : Prop<GOAL>(a → b) → b ∨ ¬a
<VAR>a b : Prop<GOAL>a → b ↔ ¬a ∨ b
<VAR>b a : Prop<GOAL>b → a ↔ a ∨ ¬b
<VAR>a b : Prop<GOAL>¬a → ¬b ↔ b → a
<VAR>a b : Prop<GOAL>(¬a → ¬b) → b → a
<VAR>c a b : Prop<VAR>h : ¬c → (a ↔ b)<GOAL>a ∨ c ↔ b ∨ c
<VAR>a b c : Prop<VAR>h : ¬a → (b ↔ c)<GOAL>a ∨ b ↔ a ∨ c
<VAR>P : Prop<VAR>h : P<GOAL>⋯ = h
<VAR>a b c : Prop<GOAL>a → b ∨ c ↔ (a → b) ∨ (a → c)
<VAR>a : Sort u_1<VAR>b c : Prop<GOAL>a → b ∨ c ↔ (a → b) ∨ (a → c)
<VAR>a b : Prop<GOAL>((a → b) → a) → a
<VAR>a b : Prop<GOAL>(¬a ↔ ¬b) ↔ (a ↔ b)
<VAR>a b : Prop<GOAL>(¬a ↔ b) ↔ (¬b ↔ a)
<VAR>a b : Prop<GOAL>(a ↔ ¬b) ↔ (b ↔ ¬a)
<VAR>a b : Prop<GOAL>(a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b
<VAR>a b : Prop<GOAL>(a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
<VAR>a b : Prop<GOAL>¬(a ∧ ¬b) ↔ a → b
<VAR>a b : Prop<GOAL>a ∨ b ↔ ¬(¬a ∧ ¬b)
<VAR>a b : Prop<GOAL>a ∧ b ↔ ¬(¬a ∨ ¬b)
<VAR>P Q : Prop<GOAL>¬Xor' P Q ↔ (P ↔ Q)
<VAR>P Q : Prop<GOAL>Xor' P Q ↔ ¬(P ↔ Q)
<VAR>α : Sort u_1<VAR>s : α → Prop<VAR>p : α → α → Prop<GOAL>(∀ (a : α), s a → ∀ (b : α), s b → p a b) ↔ ∀ (a b : α), s a → s b → p a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Membership α β<VAR>s : β<VAR>p : α → α → Prop<GOAL>(∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → p a b) ↔ ∀ (a b : α), a ∈ s → b ∈ s → p a b
<VAR>α : Sort u_1<VAR>a b c : α<VAR>h₁ : a = b<VAR>h₂ : b ≠ c<GOAL>a ≠ c
<VAR>α : Sort u_1<VAR>a b c : α<VAR>h₁ : a ≠ b<VAR>h₂ : b = c<GOAL>a ≠ c
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>a b : α<VAR>h : a = b<GOAL>⋯ = ⋯
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f g : α → β<VAR>h : f = g<VAR>a : α<GOAL>⋯ = ⋯
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>a : α<GOAL>⋯ = ⋯
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β → γ<VAR>a a' : α<VAR>p : a = a'<VAR>b : β<GOAL>⋯ = ⋯
<VAR>α : Sort u_1<VAR>P : α → Sort u_2<VAR>x y : α<VAR>h : x = y<VAR>z : P x<GOAL>h ▸ z = cast ⋯ z
<VAR>α : Sort u_1<VAR>a' : α<VAR>motive : (a : α) → a' = a → Sort u_2<VAR>p : motive a' ⋯<VAR>a : α<VAR>t : a' = a<GOAL>HEq (t ▸ p) p
<VAR>α : Sort u_2<VAR>a : α<VAR>β : Sort u_1<VAR>b : α<VAR>C : α → Sort u_1<VAR>x : C a<VAR>y : β<VAR>e : a = b<VAR>h : HEq x y<GOAL>HEq (e ▸ x) y
<VAR>α : Sort u_2<VAR>a : α<VAR>β : Sort u_1<VAR>b : α<VAR>C : α → Sort u_1<VAR>x : C a<VAR>y : β<VAR>e : a = b<GOAL>HEq (e ▸ x) y ↔ HEq x y
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>a b : α<VAR>C : α → Sort u_1<VAR>x : β<VAR>y : C a<VAR>e : a = b<GOAL>HEq x (e ▸ y) ↔ HEq x y
<VAR>α : Sort u_1<VAR>β β' : α → Sort u_2<VAR>h : ∀ (a : α), β a = β' a<GOAL>((a : α) → β a) = ((a : α) → β' a)
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>p q : (a : α) → β a → Prop<VAR>h : ∀ (a : α) (b : β a), p a b → q a b<GOAL>(∀ (a : α) (b : β a), p a b) → ∀ (a : α) (b : β a), q a b
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>p q : (a : α) → (b : β a) → γ a b → Prop<VAR>h : ∀ (a : α) (b : β a) (c : γ a b), p a b c → q a b c<GOAL>(∀ (a : α) (b : β a) (c : γ a b), p a b c) → ∀ (a : α) (b : β a) (c : γ a b), q a b c
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>p q : (a : α) → β a → Prop<VAR>h : ∀ (a : α) (b : β a), p a b → q a b<GOAL>(∃ a b, p a b) → ∃ a b, q a b
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>p q : (a : α) → (b : β a) → γ a b → Prop<VAR>h : ∀ (a : α) (b : β a) (c : γ a b), p a b c → q a b c<GOAL>(∃ a b c, p a b c) → ∃ a b c, q a b c
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → β → Prop<GOAL>(∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x y
<VAR>ι₁ : Sort u_3<VAR>ι₂ : Sort u_4<VAR>κ₁ : ι₁ → Sort u_5<VAR>κ₂ : ι₂ → Sort u_6<VAR>p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop<GOAL>(∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ↔ ∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
<VAR>α : Type u_3<VAR>p : Prop<VAR>q : α → Prop<GOAL>(p → ∀ (x : α), q x) ↔ ∀ (x : α), p → q x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → β → Prop<GOAL>(∃ x y, p x y) ↔ ∃ y x, p x y
<VAR>α : Sort u_3<VAR>p : α → Prop<VAR>b : Prop<VAR>ha : Nonempty α<GOAL>(∀ (x : α), p x) → b ↔ ∃ x, p x → b
<VAR>α : Sort u_1<GOAL>α → True ↔ True
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>h : ∀ (a : α), p a ↔ True<GOAL>(∀ (a : α), p a) ↔ True
<VAR>α : Sort u_1<VAR>β : α → Sort u_3<GOAL>(∀ (a : α), β a → True) ↔ True
<VAR>α : Sort u_1<VAR>β : α → Sort u_3<VAR>γ : (a : α) → β a → Sort u_4<GOAL>(∀ (a : α) (b : β a), γ a b → True) ↔ True
<VAR>α : Sort u_1<VAR>Subsingleton α<VAR>p : α → Prop<GOAL>(∃! x, p x) ↔ ∃ x, p x
<VAR>b : Prop<VAR>α : Sort u_3<VAR>i : Nonempty α<VAR>Subsingleton α<GOAL>(∃! x, b) ↔ b
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a : α<VAR>p : α → Prop<GOAL>(p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a : α<GOAL>(p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
<VAR>α : Sort u_1<VAR>x y : α<VAR>z : α<VAR>h : x ≠ y<GOAL>x ≠ z ∨ y ≠ z
<VAR>α : Sort u_1<VAR>a' : α<GOAL>∃! a, a = a'
<VAR>α : Sort u_1<VAR>a' : α<GOAL>∃! a, a' = a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>a' : α<GOAL>∃ a, f a' = f a
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>f : α → β → γ<VAR>a : α<VAR>b : β<GOAL>∃ x y, f x y = f a b
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>f : α → β → γ<VAR>a : α<VAR>b : β<GOAL>∃ x y, f a b = f x y
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>δ : Sort u_6<VAR>f : α → β → γ → δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>∃ x y z, f x y z = f a b c
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>δ : Sort u_6<VAR>f : α → β → γ → δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>∃ x y z, f a b c = f x y z
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>a : α<VAR>b : β<GOAL>∃ f, f a = b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>p : α → Prop<VAR>q : β → Prop<GOAL>(∃ b, (∃ a, p a ∧ f a = b) ∧ q b) ↔ ∃ a, p a ∧ q (f a)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>p : β → Prop<GOAL>(∃ b, (∃ a, f a = b) ∧ p b) ↔ ∃ a, p (f a)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<GOAL>(∃ c, (∃ a, p a ∧ ∃ b, q b ∧ f a b = c) ∧ r c) ↔ ∃ a, p a ∧ ∃ b, q b ∧ r (f a b)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>p : γ → Prop<GOAL>(∃ c, (∃ a b, f a b = c) ∧ p c) ↔ ∃ a b, p (f a b)
<VAR>α : Sort u_1<VAR>y : α<VAR>p : α → Prop<GOAL>∃ x, x = y ∨ p x
<VAR>α : Sort u_1<VAR>y : α<VAR>p : α → Prop<GOAL>∃ x, p x ∨ x = y
<VAR>α : Sort u_1<VAR>y : α<VAR>p : α → Prop<GOAL>∃ x, y = x ∨ p x
<VAR>α : Sort u_1<VAR>y : α<VAR>p : α → Prop<GOAL>∃ x, p x ∨ y = x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>p : β → Prop<GOAL>(∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>p : β → Prop<GOAL>(∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a' : α<GOAL>(∃ a, p a ∧ a' = a) ↔ p a'
<VAR>ι₁ : Sort u_3<VAR>ι₂ : Sort u_4<VAR>κ₁ : ι₁ → Sort u_5<VAR>κ₂ : ι₂ → Sort u_6<VAR>p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop<GOAL>(∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂
<VAR>p q : Prop<VAR>f : p ∧ q → Prop<GOAL>(∃ h, f h) ↔ ∃ hp hq, f ⋯
<VAR>α : Sort u_3<VAR>p : α → Prop<VAR>b : Prop<VAR>h : b ∨ ∀ (x : α), p x<VAR>x : α<GOAL>b ∨ p x
<VAR>α : Sort u_1<VAR>q : Prop<VAR>p : α → Prop<VAR>Decidable q<GOAL>(∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x
<VAR>α : Sort u_1<VAR>q : Prop<VAR>p : α → Prop<GOAL>(∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x
<VAR>α : Sort u_1<VAR>q : Prop<VAR>p : α → Prop<VAR>Decidable q<GOAL>(∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
<VAR>α : Sort u_1<VAR>q : Prop<VAR>p : α → Prop<GOAL>(∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
<VAR>p q : Prop<GOAL>(∃! x, q) ↔ p ∧ q
<VAR>α : Sort u_1<GOAL>¬∃! x, False
<VAR>b : Prop<VAR>p : b → Prop<GOAL>Exists p → b
<VAR>b : Prop<VAR>p : b → Prop<VAR>h : Exists p<GOAL>p ⋯
<VAR>p : Prop → Prop<GOAL>(∃ h, p h) ↔ p False ∨ p True
<VAR>p : Prop → Prop<GOAL>(∀ (h : Prop), p h) ↔ p False ∧ p True
<VAR>p : Prop<VAR>q : p → Prop<VAR>h : p<GOAL>(∃ h', q h') ↔ q h
<VAR>p : Prop<VAR>q : p → Prop<VAR>h : ∀ (h : p), q h<GOAL>(∃ h, q h) ↔ p
<VAR>p : Prop<VAR>q : p → Prop<VAR>h : p<GOAL>(∃! h', q h') ↔ q h
<VAR>p : Prop<VAR>q : p → Prop<GOAL>¬p → ¬∃ h', q h'
<VAR>p p' : Prop<VAR>q q' : p → Prop<VAR>hq : ∀ (h : p), q h ↔ q' h<VAR>hp : p ↔ p'<GOAL>Exists q ↔ ∃ h, q' ⋯
<VAR>p : True → Prop<GOAL>(∃ x, p x) ↔ p True.intro
<VAR>p p' : Prop<VAR>q q' : p → Prop<VAR>hq : ∀ (h : p), q h ↔ q' h<VAR>hp : p ↔ p'<GOAL>(∀ (h : p), q h) ↔ ∀ (h : p'), q' ⋯
<VAR>p p' : Prop<VAR>q q' : p → Prop<VAR>hq : ∀ (h : p), q h ↔ q' h<VAR>hp : p ↔ p'<GOAL>(∀ (h : p), q h) = ∀ (h : p'), q' ⋯
<VAR>a b c d : Prop<VAR>h₁ : a = c<VAR>h₂ : b = d<GOAL>(a → b) = (c → d)
<VAR>a b c d : Prop<VAR>h₁ : a = c<VAR>h₂ : c → b = d<GOAL>(a → b) = (c → d)
<VAR>a : Prop<VAR>h : a<GOAL>a = True
<VAR>a : Prop<VAR>h : ¬a<GOAL>a = False
<VAR>a b : Prop<GOAL>(a ↔ b) = (a = b)
<VAR>p : True → Prop<GOAL>(∀ (x : True), p x) ↔ p True.intro
<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>b : Prop<VAR>h₂ : ∃! x, ∃! h, q x h<VAR>h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b<GOAL>b
<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>w : α<VAR>hp : p w<VAR>hq : q w hp<VAR>H : ∀ (y : α) (hy : p y), q y hy → y = w<GOAL>∃! x, ∃! hx, q x hx
<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>q : (x : α) → p x → Prop<VAR>h : ∃! x, ∃! hx, q x hx<GOAL>∃ x hx, q x hx
<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>h : ∃! x, ∃! hx, q x hx<VAR>y₁ y₂ : α<VAR>hpy₁ : p y₁<VAR>hqy₁ : q y₁ hpy₁<VAR>hpy₂ : p y₂<VAR>hqy₂ : q y₂ hpy₂<GOAL>y₁ = y₂
<VAR>α : Sort u_2<VAR>p : α → Prop<VAR>h : ∃ a, p a<VAR>q : α → Prop<VAR>hpq : ∀ (a : α), p a → q a<GOAL>q (Classical.choose h)
<VAR>α : Sort u_1<VAR>a : α<GOAL>⋯.choose = a
<VAR>α : Sort u_1<VAR>p q : α → Prop<GOAL>(∃ x x_1, q x) ↔ ∃ x, p x ∧ q x
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P : (x : α) → p x → Prop<VAR>b : Prop<GOAL>(∃ x h, P x h) → (∀ (a : α) (h : p a), P a h → b) → b
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P : (x : α) → p x → Prop<VAR>a : α<VAR>h₁ : p a<VAR>h₂ : P a h₁<GOAL>∃ x h, P x h
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>a : α<GOAL>(∃ x x_1, p x) ↔ p a
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P Q : (x : α) → p x → Prop<VAR>H : ∀ (x : α) (h : p x), P x h → Q x h<VAR>h₁ : ∀ (x : α) (h : p x), P x h<VAR>x : α<VAR>h : p x<GOAL>Q x h
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P Q : (x : α) → p x → Prop<VAR>H : ∀ (x : α) (h : p x), P x h → Q x h<GOAL>(∃ x h, P x h) → ∃ x h, Q x h
<VAR>α : Sort u_1<VAR>r p q : α → Prop<VAR>H : ∀ (x : α), p x → q x<VAR>h₁ : ∀ (x : α), q x → r x<VAR>x : α<VAR>h : p x<GOAL>r x
<VAR>α : Sort u_1<VAR>r p q : α → Prop<VAR>H : ∀ (x : α), p x → q x<GOAL>(∃ x x_1, r x) → ∃ x x_1, r x
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>h : ∀ (x : α), p x<VAR>x : α<GOAL>p x
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>H : ∀ (x : α), p x<VAR>h : ∀ (x : α), p x → q x<VAR>x : α<GOAL>q x
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>H : ∀ (x : α), p x<GOAL>(∃ x, q x) → ∃ x x_1, q x
<VAR>α : Sort u_1<VAR>p q : α → Prop<GOAL>(∃ x x_1, q x) → ∃ x, q x
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P : (x : α) → p x → Prop<VAR>b : Prop<GOAL>(∃ x h, P x h) → b ↔ ∀ (x : α) (h : p x), P x h → b
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P : (x : α) → p x → Prop<GOAL>(¬∃ x h, P x h) ↔ ∀ (x : α) (h : p x), ¬P x h
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P : (x : α) → p x → Prop<GOAL>(∃ x h, ¬P x h) → ¬∀ (x : α) (h : p x), P x h
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P : (x : α) → p x → Prop<VAR>Decidable (∃ x h, ¬P x h)<VAR>(x : α) → (h : p x) → Decidable (P x h)<GOAL>(¬∀ (x : α) (h : p x), P x h) ↔ ∃ x h, ¬P x h
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P : (x : α) → p x → Prop<GOAL>(¬∀ (x : α) (h : p x), P x h) ↔ ∃ x h, ¬P x h
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P Q : (x : α) → p x → Prop<GOAL>(∀ (x : α) (h : p x), P x h ∧ Q x h) ↔ (∀ (x : α) (h : p x), P x h) ∧ ∀ (x : α) (h : p x), Q x h
<VAR>α : Sort u_1<VAR>Nonempty α<VAR>q : Prop<VAR>p : α → Prop<GOAL>(∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x
<VAR>α : Sort u_1<VAR>Nonempty α<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>P Q : (x : α) → p x → Prop<GOAL>(∃ x h, P x h ∨ Q x h) ↔ (∃ x h, P x h) ∨ ∃ x h, Q x h
<VAR>α : Sort u_1<VAR>r p q : α → Prop<GOAL>(∀ (x : α), p x ∨ q x → r x) ↔ (∀ (x : α), p x → r x) ∧ ∀ (x : α), q x → r x
<VAR>α : Sort u_1<VAR>r p q : α → Prop<GOAL>(∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>c : α<VAR>A : P → α<VAR>B : ¬P → α<GOAL>dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
<VAR>α : Sort u_1<VAR>P : Prop<VAR>Decidable P<VAR>a b c : α<GOAL>(if P then a else b) = c ↔ P ∧ a = c ∨ ¬P ∧ b = c