ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<VAR>h : b ∈ f.fix a<GOAL>(f a).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β ⊕ α<VAR>a : α<VAR>b : β<GOAL>b ∈ f.fix a ↔ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a : α<VAR>hb : Sum.inl b ∈ f a<GOAL>b ∈ f.fix a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β ⊕ α<VAR>a a' : α<VAR>ha' : Sum.inr a' ∈ f a<GOAL>f.fix a = f.fix a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a a' : α<VAR>hb : b ∈ f.fix a<VAR>ha' : Sum.inr a' ∈ f a<GOAL>b ∈ f.fix a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : α → Sort u_7<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a : α<VAR>h : b ∈ f.fix a<VAR>H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'<GOAL>PFun.fixInduction h H = H a h fun a' h' => PFun.fixInduction ⋯ H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : α → Sort u_7<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a : α<VAR>h : b ∈ f.fix a<VAR>fa : Sum.inl b ∈ f a<VAR>hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final<VAR>hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀<GOAL>PFun.fixInduction' h hbase hind = hbase a fa
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : α → Sort u_7<VAR>f : α →. β ⊕ α<VAR>b : β<VAR>a a' : α<VAR>h : b ∈ f.fix a<VAR>h' : b ∈ f.fix a'<VAR>fa : Sum.inr a' ∈ f a<VAR>hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final<VAR>hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀<GOAL>PFun.fixInduction' h hbase hind = hind a a' h' fa (PFun.fixInduction' h' hbase hind)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set α<GOAL>f.image s = {y | ∃ x ∈ s, y ∈ f x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>y : β<VAR>s : Set α<GOAL>y ∈ f.image s ↔ ∃ x ∈ s, y ∈ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>f.image s ⊆ f.image t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s t : Set α<GOAL>f.image (s ∩ t) ⊆ f.image s ∩ f.image t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s t : Set α<GOAL>f.image (s ∪ t) = f.image s ∪ f.image t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set β<GOAL>f.preimage s = {x | ∃ y ∈ s, y ∈ f x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set β<VAR>x : α<GOAL>x ∈ f.preimage s ↔ ∃ y ∈ s, y ∈ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set β<GOAL>f.preimage s ⊆ f.Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s t : Set β<VAR>h : s ⊆ t<GOAL>f.preimage s ⊆ f.preimage t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s t : Set β<GOAL>f.preimage (s ∩ t) ⊆ f.preimage s ∩ f.preimage t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s t : Set β<GOAL>f.preimage (s ∪ t) = f.preimage s ∪ f.preimage t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<GOAL>f.preimage Set.univ = f.Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>(↑f).preimage s = f ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set β<GOAL>f.core s = {x | ∀ y ∈ f x, y ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>x : α<VAR>s : Set β<GOAL>x ∈ f.core s ↔ ∀ y ∈ f x, y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set β<GOAL>f.Domᶜ ⊆ f.core s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s t : Set β<VAR>h : s ⊆ t<GOAL>f.core s ⊆ f.core t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s t : Set β<GOAL>f.core (s ∩ t) = f.core s ∩ f.core t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>x : α<GOAL>x ∈ (PFun.res f s).core t ↔ x ∈ s → f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>(PFun.res f s).core t = sᶜ ∪ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>(↑f).core s = f ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set β<GOAL>f.preimage s ⊆ f.core s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set β<GOAL>f.preimage s = f.core s ∩ f.Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set β<GOAL>f.core s = f.preimage s ∪ f.Domᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set β<GOAL>f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : α → β<GOAL>(PFun.toSubtype p f).Dom = {a | p (f a)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : α → β<VAR>a : α<GOAL>PFun.toSubtype p f a = { Dom := p (f a), get := Subtype.mk (f a) }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : α → β<VAR>a : α<GOAL>(PFun.toSubtype p f a).Dom ↔ p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : α → β<VAR>a : α<VAR>b : Subtype p<GOAL>b ∈ PFun.toSubtype p f a ↔ ↑b = f a
<VAR>α : Type u_7<GOAL>↑id = PFun.id α
<VAR>α : Type u_1<VAR>a : α<GOAL>PFun.id α a = Part.some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β →. γ<VAR>g : α →. β<VAR>a : α<GOAL>f.comp g a = (g a).bind f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<GOAL>(PFun.id β).comp f = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<GOAL>f.comp (PFun.id α) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β →. γ<VAR>g : α →. β<GOAL>(f.comp g).Dom = g.preimage f.Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β →. γ<VAR>g : α →. β<VAR>s : Set γ<GOAL>(f.comp g).preimage s = g.preimage (f.preimage s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β →. γ<VAR>g : α →. β<VAR>a : Part α<GOAL>a.bind (f.comp g) = (a.bind g).bind f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : γ →. δ<VAR>g : β →. γ<VAR>h : α →. β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<GOAL>↑(g ∘ f) = (↑g).comp ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α →. β<VAR>g : α →. γ<GOAL>(f.prodLift g).Dom = {x | (f x).Dom ∧ (g x).Dom}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α →. β<VAR>g : α →. γ<VAR>x : α<VAR>h : (f.prodLift g x).Dom<GOAL>(f.prodLift g x).get h = ((f x).get ⋯, (g x).get ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α →. β<VAR>g : α →. γ<VAR>x : α<GOAL>f.prodLift g x = { Dom := (f x).Dom ∧ (g x).Dom, get := fun h => ((f x).get ⋯, (g x).get ⋯) }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α →. β<VAR>g : α →. γ<VAR>x : α<VAR>y : β × γ<GOAL>y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α →. γ<VAR>g : β →. δ<GOAL>(f.prodMap g).Dom = {x | (f x.1).Dom ∧ (g x.2).Dom}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α →. γ<VAR>g : β →. δ<VAR>x : α × β<VAR>h : (f.prodMap g x).Dom<GOAL>(f.prodMap g x).get h = ((f x.1).get ⋯, (g x.2).get ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α →. γ<VAR>g : β →. δ<VAR>x : α × β<GOAL>f.prodMap g x = { Dom := (f x.1).Dom ∧ (g x.2).Dom, get := fun h => ((f x.1).get ⋯, (g x.2).get ⋯) }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α →. γ<VAR>g : β →. δ<VAR>x : α × β<VAR>y : γ × δ<GOAL>y ∈ f.prodMap g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α →. γ<VAR>g : β →. δ<GOAL>(f.comp ↑Prod.fst).prodLift (g.comp ↑Prod.snd) = f.prodMap g
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(PFun.id α).prodMap (PFun.id β) = PFun.id (α × β)
<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>(f₂.comp f₁).prodMap (g₂.comp g₁) = (f₂.prodMap g₂).comp (f₁.prodMap g₁)
<VAR>α : Type u_1<VAR>x y : α × α<GOAL>Sym2.Rel α x y → Sym2.Rel α y x
<VAR>α : Type u_1<VAR>x y z : α × α<VAR>a : Sym2.Rel α x y<VAR>b : Sym2.Rel α y z<GOAL>Sym2.Rel α x z
<VAR>α : Type u_1<GOAL>Equivalence (Sym2.Rel α)
<VAR>α : Type u_1<VAR>p q : α × α<GOAL>Sym2.Rel α p q ↔ p = q ∨ p = q.swap
<VAR>α : Type u_1<VAR>x y z w : α<GOAL>Sym2.Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
<VAR>α : Type u_1<VAR>p p' : α × α<VAR>h : Sym2.Rel α p p'<GOAL>Sym2.mk p = Sym2.mk p'
<VAR>α : Type u_1<VAR>p p' : α × α<VAR>h : Sym2.mk p = Sym2.mk p'<GOAL>Sym2.Rel α p p'
<VAR>α : Type u_1<VAR>p p' : α × α<GOAL>Sym2.mk p = Sym2.mk p' ↔ Sym2.Rel α p p'
<VAR>α : Type u_1<VAR>f : Sym2 α → Prop<VAR>h : ∀ (x y : α), f s(x, y)<VAR>i : Sym2 α<GOAL>f i
<VAR>α : Type u_1<VAR>f : Sym2 α → Prop<VAR>i : Sym2 α<VAR>hf : ∀ (x y : α), f s(x, y)<GOAL>f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Sym2 α → Sym2 β → Prop<VAR>i : Sym2 α<VAR>j : Sym2 β<VAR>hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)<GOAL>f i j
<VAR>α : Type u_4<VAR>f : Sym2 α → Prop<GOAL>(∃ x, f x) ↔ ∃ x y, f s(x, y)
<VAR>α : Type u_4<VAR>f : Sym2 α → Prop<GOAL>(∀ (x : Sym2 α), f x) ↔ ∀ (x y : α), f s(x, y)
<VAR>α : Type u_1<VAR>a b : α<GOAL>s(a, b) = s(b, a)
<VAR>α : Type u_1<VAR>p : α × α<GOAL>Sym2.mk p.swap = Sym2.mk p
<VAR>α : Type u_1<VAR>a b c : α<GOAL>s(a, b) = s(a, c) ↔ b = c
<VAR>α : Type u_1<VAR>a b c : α<GOAL>s(b, a) = s(c, a) ↔ b = c
<VAR>α : Type u_1<VAR>x y z w : α<GOAL>s(x, y) = s(z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
<VAR>α : Type u_1<VAR>p q : α × α<GOAL>Sym2.mk p = Sym2.mk q ↔ p = q ∨ p = q.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }<VAR>a₁ a₂ : α<GOAL>Sym2.lift f s(a₁, a₂) = ↑f a₁ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Sym2 α → β<VAR>a₁ a₂ : α<GOAL>↑(Sym2.lift.symm F) a₁ a₂ = F s(a₁, a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>Sym2.lift₂ f s(a₁, a₂) s(b₁, b₂) = ↑f a₁ a₂ b₁ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Sym2 α → Sym2 β → γ<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>↑(Sym2.lift₂.symm F) a₁ a₂ b₁ b₂ = F s(a₁, a₂) s(b₁, b₂)
<VAR>α : Type u_1<GOAL>Sym2.map id = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<GOAL>Sym2.map (g ∘ f) = Sym2.map g ∘ Sym2.map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<VAR>x : Sym2 α<GOAL>Sym2.map g (Sym2.map f x) = Sym2.map (g ∘ f) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x y : α<GOAL>Sym2.map f s(x, y) = s(f x, f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hinj : Function.Injective f<GOAL>Function.Injective (Sym2.map f)
<VAR>α : Type u_1<VAR>a b : α<GOAL>(Sym2.mkEmbedding a) b = s(a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<GOAL>∀ (a : Sym2 α), f.sym2Map a = Sym2.map (⇑f) a
<VAR>α : Type u_1<VAR>a b c : α<GOAL>Sym2.Mem a s(b, c) ↔ a = b ∨ a = c
<VAR>α : Type u_1<VAR>x : α<VAR>z : Sym2 α<GOAL>Sym2.Mem x z ↔ x ∈ z
<VAR>α : Type u_1<VAR>x : α<VAR>z : Sym2 α<GOAL>x ∈ z ↔ ∃ y, z = s(x, y)
<VAR>α : Type u_1<VAR>p q : Sym2 α<VAR>h : ∀ (x : α), x ∈ p ↔ x ∈ q<GOAL>p = q
<VAR>α : Type u_1<VAR>x y : α<GOAL>x ∈ s(x, y)
<VAR>α : Type u_1<VAR>x y : α<GOAL>y ∈ s(x, y)
<VAR>α : Type u_1<VAR>a b c : α<GOAL>a ∈ s(b, c) ↔ a = b ∨ a = c
<VAR>α : Type u_1<VAR>e : Sym2 α<GOAL>(Quot.out e).1 ∈ e
<VAR>α : Type u_1<VAR>e : Sym2 α<GOAL>(Quot.out e).2 ∈ e
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>a b : α<GOAL>(∀ c ∈ s(a, b), p c) ↔ p a ∧ p b
<VAR>α : Type u_1<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>s(a, Sym2.Mem.other h) = z
<VAR>α : Type u_1<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>Sym2.Mem.other h ∈ z
<VAR>α : Type u_1<VAR>x y : α<VAR>z : Sym2 α<VAR>hne : x ≠ y<GOAL>x ∈ z ∧ y ∈ z ↔ z = s(x, y)
<VAR>α : Type u_1<VAR>x y : α<VAR>z z' : Sym2 α<VAR>h : x ≠ y<VAR>h1 : x ∈ z<VAR>h2 : y ∈ z<VAR>h3 : x ∈ z'<VAR>h4 : y ∈ z'<GOAL>z = z'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>z : Sym2 α<GOAL>b ∈ Sym2.map f z ↔ ∃ a ∈ z, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>s : Sym2 α<VAR>h : ∀ x ∈ s, f x = g x<GOAL>Sym2.map f s = Sym2.map g s
<VAR>α : Type u_1<GOAL>(Sym2.map fun x => x) = id
<VAR>α : Type u_1<GOAL>Function.Injective Sym2.diag
<VAR>α : Type u_1<VAR>x y : α<GOAL>s(x, y).IsDiag ↔ x = y
<VAR>α : Type u_1<VAR>z : α × α<GOAL>(Sym2.mk z).IsDiag ↔ z.1 = z.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Sym2 α<VAR>f : α → β<GOAL>e.IsDiag → (Sym2.map f e).IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Sym2 α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>(Sym2.map f e).IsDiag ↔ e.IsDiag
<VAR>α : Type u_1<VAR>a : α<GOAL>(Sym2.diag a).IsDiag
<VAR>α : Type u_1<VAR>z : Sym2 α<GOAL>z.IsDiag → z ∈ Set.range Sym2.diag
<VAR>α : Type u_1<VAR>z : Sym2 α<GOAL>z.IsDiag ↔ z ∈ Set.range Sym2.diag
<VAR>α : Type u_1<VAR>a : α<VAR>z : Sym2 α<VAR>hd : ¬z.IsDiag<VAR>h : a ∈ z<GOAL>Sym2.Mem.other h ≠ a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>sym : Symmetric r<VAR>z : α × α<GOAL>Sym2.mk z ∈ Sym2.fromRel sym ↔ r z.1 z.2
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>sym : Symmetric r<VAR>a b : α<GOAL>s(a, b) ∈ Sym2.fromRel sym ↔ r a b
<VAR>α : Type u_1<GOAL>Sym2.fromRel ⋯ = ∅
<VAR>α : Type u_1<GOAL>Sym2.fromRel ⋯ = Set.univ
<VAR>α : Type u_1<GOAL>Sym2.fromRel ⋯ = {z | ¬z.IsDiag}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>sym : Symmetric r<GOAL>Irreflexive r ↔ ∀ {z : Sym2 α}, z ∈ Sym2.fromRel sym → ¬z.IsDiag
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>sym : Symmetric r<VAR>irrefl : Irreflexive r<VAR>a : α<VAR>z : Sym2 α<VAR>hz : z ∈ Sym2.fromRel sym<VAR>h : a ∈ z<GOAL>Sym2.Mem.other h ≠ a
<VAR>α : Type u_1<VAR>s : Set (Sym2 α)<VAR>x y : α<GOAL>Sym2.ToRel s x y ↔ s(x, y) ∈ s
<VAR>α : Type u_1<VAR>s : Set (Sym2 α)<GOAL>Symmetric (Sym2.ToRel s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>sym : Symmetric r<GOAL>Sym2.ToRel (Sym2.fromRel sym) = r
<VAR>α : Type u_1<VAR>s : Set (Sym2 α)<GOAL>Sym2.fromRel ⋯ = s
<VAR>α : Type u_1<VAR>a₁ b₁ a₂ b₂ : α<GOAL>[a₁, b₁].Perm [a₂, b₂] ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>s(a, Sym2.Mem.other' h) = z
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>Sym2.Mem.other h = Sym2.Mem.other' h
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>Sym2.Mem.other' h ∈ z
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>z : Sym2 α<VAR>ha : a ∈ z<VAR>hb : Sym2.Mem.other' ha ∈ z<GOAL>Sym2.Mem.other' hb = a
<VAR>α : Type u_1<VAR>a : α<VAR>z : Sym2 α<VAR>ha : a ∈ z<VAR>hb : Sym2.Mem.other ha ∈ z<GOAL>Sym2.Mem.other hb = a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.filter Sym2.IsDiag (Finset.image Sym2.mk (s ×ˢ s)) = Finset.image Sym2.mk s.diag
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.filter (fun a => ¬a.IsDiag) (Finset.image Sym2.mk (s ×ˢ s)) = Finset.image Sym2.mk s.offDiag
<VAR>P : PFunctor.{u}<VAR>α β : Type v<VAR>f : α → β<VAR>x : ↑P α<GOAL>f <$> x = P.map f x
<VAR>P : PFunctor.{u}<VAR>α : Type v₁<VAR>β : Type v₂<VAR>f : α → β<VAR>a : P.A<VAR>g : P.B a → α<GOAL>P.map f ⟨a, g⟩ = ⟨a, f ∘ g⟩
<VAR>P : PFunctor.{u}<VAR>α : Type v₁<VAR>x : ↑P α<GOAL>P.map id x = x
<VAR>P : PFunctor.{u}<VAR>α : Type v₁<VAR>β : Type v₂<VAR>γ : Type v₃<VAR>f : α → β<VAR>g : β → γ<VAR>x : ↑P α<GOAL>P.map g (P.map f x) = P.map (g ∘ f) x
<VAR>P : PFunctor.{u}<VAR>p : ↑P P.W<GOAL>(PFunctor.W.mk p).dest = p
<VAR>P : PFunctor.{u}<VAR>p : P.W<GOAL>PFunctor.W.mk p.dest = p
<VAR>P : PFunctor.{u}<VAR>α : Type v₁<VAR>β : Type v₂<VAR>x : ↑P α<VAR>f : α → β<GOAL>(P.map f x).fst = x.fst
<VAR>P : PFunctor.{u}<VAR>α : Type v₁<VAR>β : Type v₂<VAR>DecidableEq P.A<VAR>Inhabited α<VAR>Inhabited β<VAR>x : ↑P α<VAR>f : α → β<VAR>i : P.Idx<VAR>h : i.fst = x.fst<GOAL>(P.map f x).iget i = f (x.iget i)
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>p : α → Prop<VAR>x : ↑P α<GOAL>Functor.Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>p : α → Prop<VAR>a : P.A<VAR>f : P.B a → α<GOAL>Functor.Liftp p ⟨a, f⟩ ↔ ∀ (i : P.B a), p (f i)
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x y : ↑P α<GOAL>Functor.Liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>a : P.A<VAR>f : P.B a → α<GOAL>Functor.supp ⟨a, f⟩ = f '' Set.univ
<VAR>R : Type u<VAR>P : Fin 3 → R<GOAL>P = ![P 0, P 1, P 2]
<VAR>R : Type u<VAR>CommRing R<VAR>P : Fin 3 → R<VAR>u : Rˣ<GOAL>u • P = ![↑u * P 0, ↑u * P 1, ↑u * P 2]
<VAR>R : Type u<VAR>CommRing R<VAR>P : Fin 3 → R<VAR>u : Rˣ<GOAL>(u • P) 0 = ↑u * P 0 ∧ (u • P) 1 = ↑u * P 1 ∧ (u • P) 2 = ↑u * P 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<GOAL>(MvPolynomial.eval P) W.polynomial = P 1 ^ 2 * P 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 2 - (P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 + W.a₄ * P 0 * P 2 ^ 2 + W.a₆ * P 2 ^ 3)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<GOAL>W.Equation P ↔ P 1 ^ 2 * P 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 2 = P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 + W.a₄ * P 0 * P 2 ^ 2 + W.a₆ * P 2 ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>Y : R<GOAL>W.Equation ![0, Y, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>X Y : R<GOAL>W.Equation ![X, Y, 1] ↔ W.toAffine.Equation X Y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<VAR>u : Rˣ<GOAL>W.Equation (u • P) ↔ W.Equation P
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<GOAL>W.polynomialX = MvPolynomial.C W.a₁ * MvPolynomial.X 1 * MvPolynomial.X 2 - (MvPolynomial.C 3 * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W.a₂) * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C W.a₄ * MvPolynomial.X 2 ^ 2)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<GOAL>(MvPolynomial.eval P) W.polynomialX = W.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<GOAL>W.polynomialY = MvPolynomial.C 2 * MvPolynomial.X 1 * MvPolynomial.X 2 + MvPolynomial.C W.a₁ * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C W.a₃ * MvPolynomial.X 2 ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<GOAL>(MvPolynomial.eval P) W.polynomialY = 2 * P 1 * P 2 + W.a₁ * P 0 * P 2 + W.a₃ * P 2 ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<GOAL>W.polynomialZ = MvPolynomial.X 1 ^ 2 + MvPolynomial.C W.a₁ * MvPolynomial.X 0 * MvPolynomial.X 1 + MvPolynomial.C (2 * W.a₃) * MvPolynomial.X 1 * MvPolynomial.X 2 - (MvPolynomial.C W.a₂ * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W.a₄) * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C (3 * W.a₆) * MvPolynomial.X 2 ^ 2)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<GOAL>(MvPolynomial.eval P) W.polynomialZ = P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 - (W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<GOAL>3 * (MvPolynomial.eval P) W.polynomial = P 0 * (MvPolynomial.eval P) W.polynomialX + P 1 * (MvPolynomial.eval P) W.polynomialY + P 2 * (MvPolynomial.eval P) W.polynomialZ
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<GOAL>W.Nonsingular P ↔ W.Equation P ∧ (W.a₁ * P 1 * P 2 ≠ 3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2 ∨ P 1 * P 2 ≠ -P 1 * P 2 - W.a₁ * P 0 * P 2 - W.a₃ * P 2 ^ 2 ∨ P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 ≠ W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>Nontrivial R<GOAL>W.Nonsingular ![0, 1, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>NoZeroDivisors R<VAR>Y : R<VAR>hy : Y ≠ 0<GOAL>W.Nonsingular ![0, Y, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>X Y : R<GOAL>W.Nonsingular ![X, Y, 1] ↔ W.toAffine.Nonsingular X Y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<VAR>u : Rˣ<GOAL>W.Nonsingular (u • P) ↔ W.Nonsingular P
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<GOAL>W.Nonsingular P ↔ W.Nonsingular Q
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>P : Fin 3 → R<GOAL>W.NonsingularLift ⟦P⟧ ↔ W.Nonsingular P
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>Nontrivial R<GOAL>W.NonsingularLift ⟦![0, 1, 0]⟧
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>NoZeroDivisors R<VAR>Y : R<VAR>hy : Y ≠ 0<GOAL>W.NonsingularLift ⟦![0, Y, 0]⟧
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Projective R<VAR>X Y : R<GOAL>W.NonsingularLift ⟦![X, Y, 1]⟧ ↔ W.toAffine.Nonsingular X Y
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Projective F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P 2 = 0<VAR>hQz : Q 2 = 0<GOAL>P ≈ Q
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Projective F<VAR>P : Fin 3 → F<VAR>h : W.Nonsingular P<VAR>hPz : P 2 = 0<GOAL>P ≈ ![0, 1, 0]
<VAR>F : Type u<VAR>Field F<VAR>P : Fin 3 → F<VAR>hPz : P 2 ≠ 0<GOAL>P ≈ ![P 0 / P 2, P 1 / P 2, 1]
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Projective F<VAR>P : Fin 3 → F<VAR>hPz : P 2 ≠ 0<GOAL>W.Nonsingular P ↔ W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Projective F<VAR>P : Fin 3 → F<VAR>h : W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)<VAR>hPz : P 2 ≠ 0<GOAL>W.Nonsingular P
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Projective F<VAR>P : Fin 3 → F<VAR>h : W.Nonsingular P<VAR>hPz : P 2 ≠ 0<GOAL>W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u_1} n<VAR>a : P.A<VAR>f : P.last.B a → P.last.W<VAR>g' : (P.drop.B a).Arrow α<VAR>g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α<GOAL>P.wPathDestLeft (P.wPathCasesOn g' g) = g'
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u_1} n<VAR>a : P.A<VAR>f : P.last.B a → P.last.W<VAR>g' : (P.drop.B a).Arrow α<VAR>g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α<GOAL>P.wPathDestRight (P.wPathCasesOn g' g) = g
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u_1} n<VAR>a : P.A<VAR>f : P.last.B a → P.last.W<VAR>h : TypeVec.Arrow (P.WPath (WType.mk a f)) α<GOAL>P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>h : α.Arrow β<VAR>a : P.A<VAR>f : P.last.B a → P.last.W<VAR>g' : (P.drop.B a).Arrow α<VAR>g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α<GOAL>TypeVec.comp h (P.wPathCasesOn g' g) = P.wPathCasesOn (TypeVec.comp h g') fun i => TypeVec.comp h (g i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u_2} n<VAR>C : Type u_1<VAR>g : (a : P.A) → (f : P.last.B a → P.last.W) → TypeVec.Arrow (P.WPath (WType.mk a f)) α → (P.last.B a → C) → C<VAR>a : P.A<VAR>f : P.last.B a → P.last.W<VAR>f' : TypeVec.Arrow (P.WPath (WType.mk a f)) α<GOAL>P.wpRec g (WType.mk a f) f' = g a f f' fun i => P.wpRec g (f i) (P.wPathDestRight f' i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u_1} n<VAR>C : (x : P.last.W) → TypeVec.Arrow (P.WPath x) α → Prop<VAR>ih : ∀ (a : P.A) (f : P.last.B a → P.last.W) (f' : TypeVec.Arrow (P.WPath (WType.mk a f)) α), (∀ (i : P.last.B a), C (f i) (P.wPathDestRight f' i)) → C (WType.mk a f) f'<VAR>x : P.last.W<VAR>f' : TypeVec.Arrow (P.WPath x) α<GOAL>C x f'
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : Type u_1<VAR>g : (a : P.A) → (P.drop.B a).Arrow α → (P.last.B a → P.W α) → (P.last.B a → C) → C<VAR>a : P.A<VAR>f' : (P.drop.B a).Arrow α<VAR>f : P.last.B a → P.W α<GOAL>P.wRec g (P.wMk a f' f) = g a f' f fun i => P.wRec g (f i)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : P.W α → Prop<VAR>ih : ∀ (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)<VAR>x : P.W α<GOAL>C x
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : P.W α → Prop<VAR>ih : ∀ (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B a → P.W α), C (P.wMk a f' f)<VAR>x : P.W α<GOAL>C x