ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ⊕ β → γ<VAR>b : β<GOAL>((Equiv.sumArrowEquivProdArrow α β γ) f).2 b = f (Sum.inr b)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>a : α<GOAL>(Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inl a) = f a
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>b : β<GOAL>(Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inr b) = g b
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>a : α<VAR>c : γ<GOAL>(Equiv.sumProdDistrib α β γ) (Sum.inl a, c) = Sum.inl (a, c)
<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>α : Type u_3<VAR>b : β<VAR>c : γ<GOAL>(Equiv.sumProdDistrib α β γ) (Sum.inr b, c) = Sum.inr (b, c)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>a : α × γ<GOAL>(Equiv.sumProdDistrib α β γ).symm (Sum.inl a) = (Sum.inl a.1, a.2)
<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>α : Type u_3<VAR>b : β × γ<GOAL>(Equiv.sumProdDistrib α β γ).symm (Sum.inr b) = (Sum.inr b.1, b.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>b : β<GOAL>(Equiv.prodSumDistrib α β γ) (a, Sum.inl b) = Sum.inl (a, b)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>a : α<VAR>c : γ<GOAL>(Equiv.prodSumDistrib α β γ) (a, Sum.inr c) = Sum.inr (a, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α × β<GOAL>(Equiv.prodSumDistrib α β γ).symm (Sum.inl a) = (a.1, Sum.inl a.2)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>β : Type u_3<VAR>a : α × γ<GOAL>(Equiv.prodSumDistrib α β γ).symm (Sum.inr a) = (a.1, Sum.inr a.2)
<VAR>ι : Type u_3<VAR>α : ι → Type u_1<VAR>β : ι → Type u_2<VAR>p : (i : ι) × (α i ⊕ β i)<GOAL>(Equiv.sigmaSumDistrib α β) p = Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd
<VAR>ι : Type u_3<VAR>α : ι → Type u_1<VAR>β : ι → Type u_2<GOAL>∀ (a : (i : ι) × α i ⊕ (i : ι) × β i), (Equiv.sigmaSumDistrib α β).symm a = Sum.elim (Sigma.map id fun x => Sum.inl) (Sigma.map id fun x => Sum.inr) a
<VAR>α : Type u_1<GOAL>∀ (a : α ⊕ α), (Equiv.boolProdEquivSum α).symm a = Sum.elim (Prod.mk false) (Prod.mk true) a
<VAR>α : Type u_1<VAR>p : Bool × α<GOAL>(Equiv.boolProdEquivSum α) p = Bool.casesOn p.1 (Sum.inl p.2) (Sum.inr p.2)
<VAR>α : Type u_1<VAR>f : Bool → α<GOAL>(Equiv.boolArrowEquivProd α) f = (f false, f true)
<VAR>α : Type u_1<VAR>p : α × α<VAR>b : Bool<GOAL>(Equiv.boolArrowEquivProd α).symm p b = Bool.casesOn b p.1 p.2
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>e : α ≃ β<GOAL>IsEmpty α ↔ IsEmpty β
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>e : α ≃ β<VAR>IsEmpty β<GOAL>IsEmpty α
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>p : X → Prop<VAR>q : Y → Prop<VAR>e : X ≃ Y<VAR>h : ∀ (x : X), p x ↔ q (e x)<GOAL>⇑(e.subtypeEquiv h) = Subtype.map ⇑e ⋯
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>h : ∀ (a : α), p a ↔ p ((Equiv.refl α) a) := ⋯<GOAL>(Equiv.refl α).subtypeEquiv h = Equiv.refl { a // p a }
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (a : α), p a ↔ q (e a)<GOAL>(e.subtypeEquiv h).symm = e.symm.subtypeEquiv ⋯
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>p : α → Prop<VAR>q : β → Prop<VAR>r : γ → Prop<VAR>e : α ≃ β<VAR>f : β ≃ γ<VAR>h : ∀ (a : α), p a ↔ q (e a)<VAR>h' : ∀ (b : β), q b ↔ r (f b)<GOAL>(e.subtypeEquiv h).trans (f.subtypeEquiv h') = (e.trans f).subtypeEquiv ⋯
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (a : α), p a ↔ q (e a)<VAR>x : { x // p x }<GOAL>(e.subtypeEquiv h) x = ⟨e ↑x, ⋯⟩
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>e : ∀ (x : α), p x ↔ q x<VAR>b : { b // q b }<GOAL>↑((Equiv.subtypeEquivRight e).symm b) = ↑b
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>e : ∀ (x : α), p x ↔ q x<VAR>a : { a // p a }<GOAL>↑((Equiv.subtypeEquivRight e) a) = ↑a
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>e : ∀ (x : α), p x ↔ q x<VAR>z : { x // p x }<GOAL>(Equiv.subtypeEquivRight e) z = ⟨↑z, ⋯⟩
<VAR>α : Sort u_1<VAR>p q : α → Prop<VAR>e : ∀ (x : α), p x ↔ q x<VAR>z : { x // q x }<GOAL>(Equiv.subtypeEquivRight e).symm z = ⟨↑z, ⋯⟩
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>q : Subtype p → Prop<VAR>a : Subtype q<GOAL>↑((Equiv.subtypeSubtypeEquivSubtypeExists p q) a) = ↑↑a
<VAR>α : Sort u_1<VAR>p : α → Prop<VAR>q : Subtype p → Prop<VAR>a : { a // ∃ h, q ⟨a, h⟩ }<GOAL>↑↑((Equiv.subtypeSubtypeEquivSubtypeExists p q).symm a) = ↑a
<VAR>α : Type u<VAR>p q : α → Prop<GOAL>∀ (a : { x // q ↑x }), ↑((Equiv.subtypeSubtypeEquivSubtypeInter p q) a) = ↑↑a
<VAR>α : Type u<VAR>p q : α → Prop<GOAL>∀ (a : { x // p x ∧ q x }), ↑↑((Equiv.subtypeSubtypeEquivSubtypeInter p q).symm a) = ↑a
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>h : ∀ {x : α}, q x → p x<GOAL>∀ (a : Subtype q), ↑↑((Equiv.subtypeSubtypeEquivSubtype h).symm a) = ↑a
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>h : ∀ {x : α}, q x → p x<GOAL>∀ (a : { x // q ↑x }), ↑((Equiv.subtypeSubtypeEquivSubtype h) a) = ↑↑a
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>h : ∀ (x : α), p x<VAR>x : Subtype p<GOAL>(Equiv.subtypeUnivEquiv h) x = ↑x
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>h : ∀ (x : α), p x<VAR>x : α<GOAL>(Equiv.subtypeUnivEquiv h).symm x = ⟨x, ⋯⟩
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>β : α → Type u_2<VAR>DecidablePred p<VAR>f : (i : α) → β i<GOAL>(Equiv.piEquivPiSubtypeProd p β) f = (fun x => f ↑x, fun x => f ↑x)
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>β : α → Type u_2<VAR>DecidablePred p<VAR>f : ((i : { x // p x }) → β ↑i) × ((i : { x // ¬p x }) → β ↑i)<VAR>x : α<GOAL>(Equiv.piEquivPiSubtypeProd p β).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>i : α<VAR>β : α → Type u_2<VAR>f : β i × ((j : { j // j ≠ i }) → β ↑j)<VAR>j : α<GOAL>(Equiv.piSplitAt i β).symm f j = if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>i : α<VAR>β : α → Type u_2<VAR>f : (j : α) → β j<GOAL>(Equiv.piSplitAt i β) f = (f i, fun j => f ↑j)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>i : α<VAR>β : Type u_2<VAR>f : (j : α) → (fun a => β) j<GOAL>(Equiv.funSplitAt i β) f = (f i, fun j => f ↑j)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>i : α<VAR>β : Type u_2<VAR>f : (fun a => β) i × ((j : { j // j ≠ i }) → (fun a => β) ↑j)<VAR>j : α<GOAL>(Equiv.funSplitAt i β).symm f j = if h : j = i then f.1 else f.2 ⟨j, ⋯⟩
<VAR>X : Sort u_2<VAR>DecidableEq X<VAR>x : X<VAR>Y : Sort u_1<VAR>f : { x' // x' ≠ x } → Y<GOAL>⇑(Equiv.subtypeEquivCodomain f) = fun g => ↑g x
<VAR>X : Sort u_2<VAR>DecidableEq X<VAR>x : X<VAR>Y : Sort u_1<VAR>f : { x' // x' ≠ x } → Y<VAR>g : { g // g ∘ Subtype.val = f }<GOAL>(Equiv.subtypeEquivCodomain f) g = ↑g x
<VAR>X : Sort u_2<VAR>DecidableEq X<VAR>x : X<VAR>Y : Sort u_1<VAR>f : { x' // x' ≠ x } → Y<GOAL>⇑(Equiv.subtypeEquivCodomain f).symm = fun y => ⟨fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y, ⋯⟩
<VAR>X : Sort u_2<VAR>DecidableEq X<VAR>x : X<VAR>Y : Sort u_1<VAR>f : { x' // x' ≠ x } → Y<VAR>y : Y<VAR>x' : X<GOAL>↑((Equiv.subtypeEquivCodomain f).symm y) x' = if h : x' ≠ x then f ⟨x', h⟩ else y
<VAR>X : Sort u_2<VAR>DecidableEq X<VAR>x : X<VAR>Y : Sort u_1<VAR>f : { x' // x' ≠ x } → Y<VAR>y : Y<GOAL>↑((Equiv.subtypeEquivCodomain f).symm y) x = y
<VAR>X : Sort u_2<VAR>DecidableEq X<VAR>x : X<VAR>Y : Sort u_1<VAR>f : { x' // x' ≠ x } → Y<VAR>y : Y<VAR>x' : X<VAR>h : x' ≠ x<GOAL>↑((Equiv.subtypeEquivCodomain f).symm y) x' = f ⟨x', h⟩
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : Equiv.Perm α'<VAR>p : β' → Prop<VAR>DecidablePred p<VAR>f : α' ≃ Subtype p<VAR>a : α'<GOAL>(e.extendDomain f) ↑(f a) = ↑(f (e a))
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : Equiv.Perm α'<VAR>p : β' → Prop<VAR>DecidablePred p<VAR>f : α' ≃ Subtype p<VAR>b : β'<VAR>h : p b<GOAL>(e.extendDomain f) b = ↑(f (e (f.symm ⟨b, h⟩)))
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : Equiv.Perm α'<VAR>p : β' → Prop<VAR>DecidablePred p<VAR>f : α' ≃ Subtype p<VAR>b : β'<VAR>h : ¬p b<GOAL>(e.extendDomain f) b = b
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>p : β' → Prop<VAR>DecidablePred p<VAR>f : α' ≃ Subtype p<GOAL>Equiv.Perm.extendDomain (Equiv.refl α') f = Equiv.refl β'
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : Equiv.Perm α'<VAR>p : β' → Prop<VAR>DecidablePred p<VAR>f : α' ≃ Subtype p<GOAL>Equiv.symm (e.extendDomain f) = Equiv.Perm.extendDomain (Equiv.symm e) f
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>p : β' → Prop<VAR>DecidablePred p<VAR>f : α' ≃ Subtype p<VAR>e e' : Equiv.Perm α'<GOAL>Equiv.trans (e.extendDomain f) (e'.extendDomain f) = Equiv.Perm.extendDomain (Equiv.trans e e') f
<VAR>α : Sort u_1<VAR>p₁ : α → Prop<VAR>s₁ : Setoid α<VAR>s₂ : Setoid (Subtype p₁)<VAR>p₂ : Quotient s₁ → Prop<VAR>hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧<VAR>h : ∀ (x y : Subtype p₁), Setoid.r x y ↔ ↑x ≈ ↑y<VAR>x : α<VAR>hx : p₂ ⟦x⟧<GOAL>(Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h) ⟨⟦x⟧, hx⟩ = ⟦⟨x, ⋯⟩⟧
<VAR>α : Sort u_1<VAR>p₁ : α → Prop<VAR>s₁ : Setoid α<VAR>s₂ : Setoid (Subtype p₁)<VAR>p₂ : Quotient s₁ → Prop<VAR>hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧<VAR>h : ∀ (x y : Subtype p₁), Setoid.r x y ↔ ↑x ≈ ↑y<VAR>x : Subtype p₁<GOAL>(Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h).symm ⟦x⟧ = ⟨⟦↑x⟧, ⋯⟩
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>r a : α<GOAL>Equiv.swapCore a a r = r
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>r a b : α<GOAL>Equiv.swapCore a b (Equiv.swapCore a b r) = r
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>r a b : α<GOAL>Equiv.swapCore a b r = Equiv.swapCore b a r
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a : α<GOAL>Equiv.swap a a = Equiv.refl α
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>Equiv.swap a b = Equiv.swap b a
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b x : α<GOAL>(Equiv.swap a b) x = if x = a then b else if x = b then a else x
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>(Equiv.swap a b) a = b
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>(Equiv.swap a b) b = a
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b x : α<GOAL>x ≠ a → x ≠ b → (Equiv.swap a b) x = x
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b x : α<VAR>h : (Equiv.swap a b) x ≠ x<GOAL>x = a ∨ x = b
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>Equiv.trans (Equiv.swap a b) (Equiv.swap a b) = Equiv.refl α
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>Equiv.symm (Equiv.swap a b) = Equiv.swap a b
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>x y : α<GOAL>Equiv.swap x y = Equiv.refl α ↔ x = y
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b x : α<VAR>π : Equiv.Perm α<GOAL>(Equiv.trans π (Equiv.swap a b)) x = if π x = a then b else if π x = b then a else π x
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>i j : α<GOAL>⇑(Equiv.swap i j) = Function.update (Function.update id j i) i j
<VAR>α : Sort u_2<VAR>DecidableEq α<VAR>β : Sort u_1<VAR>i j : α<VAR>f : α → β<GOAL>f ∘ ⇑(Equiv.swap i j) = Function.update (Function.update f j (f i)) i (f j)
<VAR>α : Sort u_2<VAR>DecidableEq α<VAR>β : Sort u_1<VAR>DecidableEq β<VAR>a b : α<VAR>e : α ≃ β<GOAL>(e.symm.trans (Equiv.swap a b)).trans e = Equiv.swap (e a) (e b)
<VAR>α : Sort u_2<VAR>DecidableEq α<VAR>β : Sort u_1<VAR>DecidableEq β<VAR>a b : β<VAR>e : α ≃ β<GOAL>(e.trans (Equiv.swap a b)).trans e.symm = Equiv.swap (e.symm a) (e.symm b)
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>i j a : α<GOAL>(Equiv.swap i j) ((Equiv.swap i j) a) = a
<VAR>α : Sort u_2<VAR>DecidableEq α<VAR>β : Sort u_1<VAR>v : α → β<VAR>i j : α<VAR>hv : v i = v j<VAR>k : α<GOAL>v ((Equiv.swap i j) k) = v k
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>x y z w : α<GOAL>(Equiv.swap x y) z = w ↔ z = (Equiv.swap x y) w
<VAR>α : Sort u_1<VAR>DecidableEq α<VAR>a b x : α<GOAL>(Equiv.swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>i j : α<GOAL>(Equiv.swap i j).sumCongr (Equiv.refl β) = Equiv.swap (Sum.inl i) (Sum.inl j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>i j : β<GOAL>Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j)
<VAR>α : Sort u_2<VAR>DecidableEq α<VAR>β : Sort u_1<VAR>f : α ≃ β<VAR>a : α<VAR>b : β<GOAL>(f.setValue a b) a = b
<VAR>α : Sort u_1<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>⇑(Function.Involutive.toPerm f h) = f
<VAR>α : Sort u_1<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>Equiv.symm (Function.Involutive.toPerm f h) = Function.Involutive.toPerm f h
<VAR>α : Sort u_1<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>Function.Involutive ⇑(Function.Involutive.toPerm f h)
<VAR>α : Sort u_1<VAR>x : PLift α<VAR>y : α<GOAL>x = { down := y } ↔ x.down = y
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x y z : α<GOAL>f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>f : (b : β) → P (e.symm b)<VAR>x : α<GOAL>(Equiv.piCongrLeft' P e).symm f x = ⋯ ▸ f (e x)
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>f : (a : α) → P a<VAR>x : β<GOAL>(Equiv.piCongrLeft' P e) f x = f (e.symm x)
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>P : Sort u_1<VAR>e : α ≃ β<GOAL>(Equiv.piCongrLeft' (fun x => P) e).symm = Equiv.piCongrLeft' (fun a => P) e.symm
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>g : (b : β) → P (e.symm b)<VAR>b : β<GOAL>(Equiv.piCongrLeft' P e).symm g (e.symm b) = g b
<VAR>β : Sort u_1<VAR>α : Sort u_2<VAR>P : β → Sort w<VAR>e : α ≃ β<VAR>f : (a : α) → P (e a)<VAR>b : β<GOAL>(Equiv.piCongrLeft P e) f b = ⋯ ▸ f (e.symm b)
<VAR>β : Sort u_1<VAR>α : Sort u_2<VAR>P : β → Sort w<VAR>e : α ≃ β<VAR>g : (b : β) → P b<VAR>a : α<GOAL>(Equiv.piCongrLeft P e).symm g a = g (e a)
<VAR>β : Sort u_1<VAR>α : Sort u_2<VAR>P : β → Sort w<VAR>e : α ≃ β<VAR>f : (a : α) → P (e a)<VAR>a : α<GOAL>(Equiv.piCongrLeft P e) f (e a) = f a
<VAR>β : Sort u_2<VAR>α : Sort u_1<VAR>P : β → Sort v<VAR>e : α ≃ β<VAR>f : (a : α) → P (e a)<VAR>b : β<GOAL>(Equiv.piCongrLeft P e) f b = cast ⋯ (f (e.symm b))
<VAR>ι'' : Sort u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>π : ι'' → Type u_1<VAR>e : ι ⊕ ι' ≃ ι''<VAR>f : (i : ι) → π (e (Sum.inl i))<VAR>g : (i : ι') → π (e (Sum.inr i))<VAR>i : ι<GOAL>(Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun x => π (e x)).symm (f, g)) (e (Sum.inl i)) = f i
<VAR>ι'' : Sort u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>π : ι'' → Type u_1<VAR>e : ι ⊕ ι' ≃ ι''<VAR>f : (i : ι) → π (e (Sum.inl i))<VAR>g : (i : ι') → π (e (Sum.inr i))<VAR>j : ι'<GOAL>(Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun x => π (e x)).symm (f, g)) (e (Sum.inr j)) = g j
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>W : α → Sort w<VAR>Z : β → Sort z<VAR>h₁ : α ≃ β<VAR>h₂ : (a : α) → W a ≃ Z (h₁ a)<GOAL>⇑(h₁.piCongr h₂).symm = fun f a => (h₂ a).symm (f (h₁ a))
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>W : α → Sort w<VAR>Z : β → Sort z<VAR>h₁ : α ≃ β<VAR>h₂ : (a : α) → W a ≃ Z (h₁ a)<VAR>f : (b : β) → Z b<GOAL>(h₁.piCongr h₂).symm f = fun a => (h₂ a).symm (f (h₁ a))
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>W : α → Sort w<VAR>Z : β → Sort z<VAR>h₁ : α ≃ β<VAR>h₂ : (b : β) → W (h₁.symm b) ≃ Z b<GOAL>⇑(h₁.piCongr' h₂) = fun f b => (h₂ b) (f (h₁.symm b))
<VAR>α : Sort u_2<VAR>β : Sort u_1<VAR>W : α → Sort w<VAR>Z : β → Sort z<VAR>h₁ : α ≃ β<VAR>h₂ : (b : β) → W (h₁.symm b) ≃ Z b<VAR>f : (a : α) → W a<GOAL>(h₁.piCongr' h₂) f = fun b => (h₂ b) (f (h₁.symm b))
<VAR>α₁ : Type u_1<VAR>β₁ : Type u_2<VAR>e : α₁ ≃ β₁<VAR>f : α₁ → α₁<GOAL>Function.Semiconj (⇑e) f (e.conj f)
<VAR>α₁ : Type u_1<VAR>β₁ : Type u_2<VAR>e : α₁ ≃ β₁<VAR>f : α₁ → α₁ → α₁<GOAL>Function.Semiconj₂ (⇑e) f ((e.arrowCongr e.conj) f)
<VAR>α : Type v<VAR>x : α<GOAL>(Equiv.ulift.symm x).down = x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x y z : α<GOAL>(Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x y : α<GOAL>⇑(Equiv.swap (f x) (f y)) ∘ f = f ∘ ⇑(Equiv.swap x y)
<VAR>α' : Sort u_1<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>DecidableEq α'<VAR>DecidableEq α<VAR>f : α → β<VAR>g : α' ≃ α<VAR>a : α<VAR>v : β<GOAL>Function.update f a v ∘ ⇑g = Function.update (f ∘ ⇑g) (g.symm a) v
<VAR>α' : Sort u_1<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>DecidableEq α'<VAR>DecidableEq α<VAR>f : α → β<VAR>g : α' ≃ α<VAR>a : α<VAR>v : β<VAR>a' : α'<GOAL>Function.update f a v (g a') = Function.update (f ∘ ⇑g) (g.symm a) v a'
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>f : (a : α) → P a<VAR>b : β<VAR>x : P (e.symm b)<GOAL>(Equiv.piCongrLeft' P e) (Function.update f (e.symm b) x) = Function.update ((Equiv.piCongrLeft' P e) f) b x
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>f : (b : β) → P (e.symm b)<VAR>b : β<VAR>x : P (e.symm b)<GOAL>(Equiv.piCongrLeft' P e).symm (Function.update f b x) = Function.update ((Equiv.piCongrLeft' P e).symm f) (e.symm b) x
<VAR>α : Sort u_3<VAR>p : Nonempty α → Prop<GOAL>(∀ (h : Nonempty α), p h) ↔ ∀ (a : α), p ⋯
<VAR>α : Sort u_3<VAR>p : Nonempty α → Prop<GOAL>(∃ h, p h) ↔ ∃ a, p ⋯
<VAR>α : Sort u_3<GOAL>(∃ x, True) ↔ Nonempty α
<VAR>p : Prop<GOAL>Nonempty p ↔ p
<VAR>α : Sort u_3<VAR>p : Prop<GOAL>Nonempty α → p ↔ α → p
<VAR>α : Sort u_3<GOAL>¬Nonempty α ↔ α → False
<VAR>α : Sort u_4<VAR>β : α → Sort u_3<GOAL>Nonempty (PSigma β) ↔ ∃ a, Nonempty (β a)
<VAR>α : Sort u_3<VAR>p : α → Prop<GOAL>Nonempty (Subtype p) ↔ ∃ a, p a
<VAR>α : Sort u_3<VAR>β : Sort u_4<GOAL>Nonempty (PProd α β) ↔ Nonempty α ∧ Nonempty β
<VAR>α : Sort u_3<VAR>β : Sort u_4<GOAL>Nonempty (α ⊕' β) ↔ Nonempty α ∨ Nonempty β
<VAR>α : Sort u_3<GOAL>Nonempty (PLift α) ↔ Nonempty α
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>f : α → β<GOAL>Nonempty α → Nonempty β
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>f : α → β → γ<GOAL>Nonempty α → Nonempty β → Nonempty γ
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>f : α → β<VAR>g : β → α<GOAL>Nonempty α ↔ Nonempty β
<VAR>α : Sort u_3<VAR>h : Nonempty α<VAR>p : Prop<VAR>f : Inhabited α → p<GOAL>p
<VAR>ι : Sort u_4<VAR>α : ι → Sort u_3<GOAL>Nonempty ((i : ι) → α i) ↔ ∀ (i : ι), Nonempty (α i)
<VAR>α : Sort u_3<VAR>h : ¬Nonempty α<GOAL>Subsingleton α
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>h : Nonempty β<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Nonempty α
<VAR>α : Type u_1<VAR>γ : α → Type u_3<GOAL>Nonempty ((a : α) × γ a) ↔ ∃ a, Nonempty (γ a)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Nonempty (α ⊕ β) ↔ Nonempty α ∨ Nonempty β
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Nonempty (α × β) ↔ Nonempty α ∧ Nonempty β
<VAR>α : Type u_1<GOAL>Nonempty (ULift.{u_4, u_1} α) ↔ Nonempty α
<VAR>α : Type u_3<VAR>self : Nontrivial α<GOAL>∃ x y, x ≠ y
<VAR>α : Type u_1<GOAL>Nontrivial α ↔ ∃ x y, x ≠ y
<VAR>α : Type u_3<VAR>Nontrivial α<GOAL>∃ x y, x ≠ y
<VAR>α : Type u_1<VAR>Nontrivial α<VAR>DecidableEq α<VAR>x : α<GOAL>∃ y, y ≠ x
<VAR>α : Type u_1<VAR>Nontrivial α<VAR>x : α<GOAL>∃ y, y ≠ x
<VAR>α : Type u_1<VAR>x y : α<VAR>h : x ≠ y<GOAL>Nontrivial α
<VAR>α : Type u_1<VAR>x : α<GOAL>Nontrivial α ↔ ∃ y, y ≠ x
<VAR>α : Type u_1<GOAL>Subsingleton α ↔ ∀ (x y : α), x = y
<VAR>α : Type u_1<GOAL>¬Nontrivial α ↔ Subsingleton α
<VAR>α : Type u_3<VAR>Subsingleton α<GOAL>¬Nontrivial α
<VAR>α : Type u_3<VAR>Nontrivial α<GOAL>¬Subsingleton α
<VAR>α : Type u_1<GOAL>¬Subsingleton α ↔ Nontrivial α
<VAR>α : Type u_3<GOAL>Subsingleton α ∨ Nontrivial α
<VAR>α : Type u_3<VAR>Nontrivial α<VAR>Subsingleton α<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nontrivial β<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Nontrivial α
<VAR>α : Type u_1<VAR>Preorder α<VAR>x y : α<VAR>h : x < y<GOAL>Nontrivial α
<VAR>α : Type u_3<VAR>Nontrivial α<VAR>LinearOrder α<GOAL>∃ x y, x < y
<VAR>α : Type u_1<VAR>LinearOrder α<GOAL>Nontrivial α ↔ ∃ x y, x < y
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>x : Subtype p<GOAL>Nontrivial (Subtype p) ↔ ∃ y x_1, y ≠ ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nontrivial α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Nontrivial β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nontrivial α<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>y : β<GOAL>∃ x, f x ≠ y
<VAR>I : Type u_3<VAR>f : I → Type u_4<VAR>i' : I<VAR>inst : ∀ (i : I), Nonempty (f i)<VAR>Nontrivial (f i')<GOAL>Nontrivial ((i : I) → f i)
<VAR>α : Type u_1<VAR>Preorder α<VAR>Subsingleton α<VAR>x y : α<GOAL>x ≤ y
<VAR>α : Type u_1<VAR>Zero α<VAR>Subsingleton α<VAR>a : α<GOAL>a = 0
<VAR>α : Type u_1<VAR>One α<VAR>Subsingleton α<VAR>a : α<GOAL>a = 1
<VAR>α : Type u_1<VAR>r p : α → α → Prop<VAR>hr : Pairwise r<VAR>h : ∀ ⦃i j : α⦄, r i j → p i j<GOAL>Pairwise p
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Pairwise r<GOAL>¬r a b → a = b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>Subsingleton α<GOAL>Pairwise r
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → α<GOAL>Function.Injective f ↔ Pairwise ((fun x x_1 => x ≠ x_1) on f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>hr : Pairwise r<VAR>f : β → α<VAR>hf : Function.Injective f<GOAL>Pairwise (r on f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>f : β → α<VAR>hr : Pairwise (r on f)<VAR>hf : Function.Surjective f<GOAL>Pairwise r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>f : β → α<VAR>hf : Function.Bijective f<GOAL>Pairwise (r on f) ↔ Pairwise r
<VAR>α : Type u_1<VAR>s : Set α<VAR>r : α → α → Prop<VAR>h : ∀ (a b : α), r a b<GOAL>s.Pairwise r
<VAR>α : Type u_1<VAR>r p : α → α → Prop<VAR>s : Set α<VAR>h : s.Pairwise r<VAR>hrp : s.Pairwise fun ⦃a b⦄ => r a b → p a b<GOAL>s.Pairwise p
<VAR>α : Type u_1<VAR>r p : α → α → Prop<VAR>s : Set α<VAR>h : s.Pairwise r<VAR>hpq : ∀ ⦃a b : α⦄, r a b → p a b<GOAL>s.Pairwise p
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a b : α<VAR>hs : s.Pairwise r<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>h : ¬r a b<GOAL>a = b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>hr : Reflexive r<GOAL>s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>r : α → α → Prop<VAR>f : ι → α<VAR>s : Set α<VAR>hs : s.Pairwise r<VAR>hf : Function.Injective f<VAR>hfs : ∀ (x : ι), f x ∈ s<GOAL>Pairwise (r on f)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : Pairwise r<VAR>s : Set α<GOAL>s.Pairwise r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable β<VAR>CompleteLattice α<VAR>f : β → α<GOAL>⨆ i, ⨆ b ∈ Encodable.decode₂ β i, f b = ⨆ b, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable β<VAR>f : β → Set α<GOAL>⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b = ⋃ b, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable β<VAR>f : β → Set α<VAR>C : Set α → Prop<VAR>H0 : C ∅<VAR>H1 : ∀ (b : β), C (f b)<VAR>n : ℕ<GOAL>C (⋃ b ∈ Encodable.decode₂ β n, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<GOAL>Pairwise (Disjoint on fun i => ⋃ b ∈ Encodable.decode₂ β i, f b)
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>R : α → β → Prop<VAR>h : Relator.RightTotal R<GOAL>((R ⇒ fun x x_1 => x → x_1) ⇒ fun x x_1 => x → x_1) (fun p => (i : α) → p i) fun q => ∀ (i : β), q i
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>R : α → β → Prop<VAR>h : Relator.LeftTotal R<GOAL>((R ⇒ fun x x_1 => x → x_1) ⇒ fun x x_1 => x → x_1) (fun p => ∃ i, p i) fun q => ∃ i, q i
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>R : α → β → Prop<VAR>h : Relator.BiTotal R<GOAL>((R ⇒ Iff) ⇒ Iff) (fun p => ∀ (i : α), p i) fun q => ∀ (i : β), q i
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>R : α → β → Prop<VAR>h : Relator.BiTotal R<GOAL>((R ⇒ Iff) ⇒ Iff) (fun p => ∃ i, p i) fun q => ∃ i, q i
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>R : α → β → Prop<VAR>eq' : β → β → Prop<VAR>he : (R ⇒ R ⇒ Iff) Eq eq'<GOAL>Relator.LeftUnique R
<GOAL>(Iff ⇒ Iff ⇒ Iff) (fun x x_1 => x → x_1) fun x x_1 => x → x_1
<VAR>α : Type u₁<GOAL>Relator.BiTotal Eq
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>h : Relator.LeftUnique r<GOAL>Relator.RightUnique (flip r)
<GOAL>((fun x x_1 => x ↔ x_1) ⇒ (fun x x_1 => x ↔ x_1) ⇒ fun x x_1 => x ↔ x_1) (fun x x_1 => x ∧ x_1) fun x x_1 => x ∧ x_1
<GOAL>((fun x x_1 => x ↔ x_1) ⇒ (fun x x_1 => x ↔ x_1) ⇒ fun x x_1 => x ↔ x_1) (fun x x_1 => x ∨ x_1) fun x x_1 => x ∨ x_1
<GOAL>((fun x x_1 => x ↔ x_1) ⇒ (fun x x_1 => x ↔ x_1) ⇒ fun x x_1 => x ↔ x_1) (fun x x_1 => x ↔ x_1) fun x x_1 => x ↔ x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>hr : Relator.BiUnique r<GOAL>(r ⇒ r ⇒ fun x x_1 => x ↔ x_1) (fun x x_1 => x = x_1) fun x x_1 => x = x_1
<VAR>α : Type u_5<VAR>r₁₁ : α → α → Prop<VAR>hr : ∀ (a : α), r₁₁ a a<GOAL>Relator.LeftTotal r₁₁