ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>DivisionMonoid α<VAR>s t : Set α<GOAL>s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
<VAR>α : Type u_2<VAR>SubtractionMonoid α<VAR>s t : Set α<GOAL>s + t = 0 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a + b = 0
<VAR>α : Type u_2<VAR>SubtractionMonoid α<VAR>s : Set α<GOAL>IsAddUnit s ↔ ∃ a, s = {a} ∧ IsAddUnit a
<VAR>α : Type u_2<VAR>DivisionMonoid α<VAR>s : Set α<GOAL>IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a
<VAR>α : Type u_2<VAR>DivisionMonoid α<GOAL>Set.univ / Set.univ = Set.univ
<VAR>α : Type u_2<VAR>SubtractionMonoid α<GOAL>Set.univ - Set.univ = Set.univ
<VAR>α : Type u_2<VAR>Distrib α<VAR>s t u : Set α<GOAL>s * (t + u) ⊆ s * t + s * u
<VAR>α : Type u_2<VAR>Distrib α<VAR>s t u : Set α<GOAL>(s + t) * u ⊆ s * u + t * u
<VAR>α : Type u_2<VAR>MulZeroClass α<VAR>s : Set α<GOAL>s * 0 ⊆ 0
<VAR>α : Type u_2<VAR>MulZeroClass α<VAR>s : Set α<GOAL>0 * s ⊆ 0
<VAR>α : Type u_2<VAR>MulZeroClass α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>s * 0 = 0
<VAR>α : Type u_2<VAR>MulZeroClass α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>0 * s = 0
<VAR>α : Type u_2<VAR>Group α<VAR>s t : Set α<GOAL>1 ∈ s / t ↔ ¬Disjoint s t
<VAR>α : Type u_2<VAR>AddGroup α<VAR>s t : Set α<GOAL>0 ∈ s - t ↔ ¬Disjoint s t
<VAR>α : Type u_2<VAR>Group α<VAR>s t : Set α<GOAL>1 ∉ s / t ↔ Disjoint s t
<VAR>α : Type u_2<VAR>AddGroup α<VAR>s t : Set α<GOAL>0 ∉ s - t ↔ Disjoint s t
<VAR>α : Type u_2<VAR>Group α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>1 ∈ s / s
<VAR>α : Type u_2<VAR>AddGroup α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>0 ∈ s - s
<VAR>α : Type u_2<VAR>Group α<VAR>a : α<GOAL>IsUnit {a}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a : α<GOAL>IsAddUnit {a}
<VAR>α : Type u_2<VAR>Group α<VAR>s : Set α<GOAL>IsUnit s ↔ ∃ a, s = {a}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>s : Set α<GOAL>IsAddUnit s ↔ ∃ a, s = {a}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>t : Set α<VAR>a : α<GOAL>(fun x => a + x) '' t = (fun x => -a + x) ⁻¹' t
<VAR>α : Type u_2<VAR>Group α<VAR>t : Set α<VAR>a : α<GOAL>(fun x => a * x) '' t = (fun x => a⁻¹ * x) ⁻¹' t
<VAR>α : Type u_2<VAR>AddGroup α<VAR>t : Set α<VAR>b : α<GOAL>(fun x => x + b) '' t = (fun x => x + -b) ⁻¹' t
<VAR>α : Type u_2<VAR>Group α<VAR>t : Set α<VAR>b : α<GOAL>(fun x => x * b) '' t = (fun x => x * b⁻¹) ⁻¹' t
<VAR>α : Type u_2<VAR>Group α<VAR>t : Set α<VAR>a : α<GOAL>(fun x => a⁻¹ * x) '' t = (fun x => a * x) ⁻¹' t
<VAR>α : Type u_2<VAR>AddGroup α<VAR>t : Set α<VAR>a : α<GOAL>(fun x => -a + x) '' t = (fun x => a + x) ⁻¹' t
<VAR>α : Type u_2<VAR>AddGroup α<VAR>t : Set α<VAR>b : α<GOAL>(fun x => x + -b) '' t = (fun x => x + b) ⁻¹' t
<VAR>α : Type u_2<VAR>Group α<VAR>t : Set α<VAR>b : α<GOAL>(fun x => x * b⁻¹) '' t = (fun x => x * b) ⁻¹' t
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a b : α<GOAL>(fun x => a + x) ⁻¹' {b} = {-a + b}
<VAR>α : Type u_2<VAR>Group α<VAR>a b : α<GOAL>(fun x => a * x) ⁻¹' {b} = {a⁻¹ * b}
<VAR>α : Type u_2<VAR>Group α<VAR>a b : α<GOAL>(fun x => x * a) ⁻¹' {b} = {b * a⁻¹}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a b : α<GOAL>(fun x => x + a) ⁻¹' {b} = {b + -a}
<VAR>α : Type u_2<VAR>Group α<VAR>a : α<GOAL>(fun x => a * x) ⁻¹' 1 = {a⁻¹}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a : α<GOAL>(fun x => a + x) ⁻¹' 0 = {-a}
<VAR>α : Type u_2<VAR>Group α<VAR>b : α<GOAL>(fun x => x * b) ⁻¹' 1 = {b⁻¹}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>b : α<GOAL>(fun x => x + b) ⁻¹' 0 = {-b}
<VAR>α : Type u_2<VAR>Group α<VAR>a : α<GOAL>(fun x => a⁻¹ * x) ⁻¹' 1 = {a}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a : α<GOAL>(fun x => -a + x) ⁻¹' 0 = {a}
<VAR>α : Type u_2<VAR>Group α<VAR>b : α<GOAL>(fun x => x * b⁻¹) ⁻¹' 1 = {b}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>b : α<GOAL>(fun x => x + -b) ⁻¹' 0 = {b}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>s + Set.univ = Set.univ
<VAR>α : Type u_2<VAR>Group α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>s * Set.univ = Set.univ
<VAR>α : Type u_2<VAR>Group α<VAR>t : Set α<VAR>ht : t.Nonempty<GOAL>Set.univ * t = Set.univ
<VAR>α : Type u_2<VAR>AddGroup α<VAR>t : Set α<VAR>ht : t.Nonempty<GOAL>Set.univ + t = Set.univ
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>s : Set α<GOAL>s / 0 ⊆ 0
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>s : Set α<GOAL>0 / s ⊆ 0
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>s / 0 = 0
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>0 / s = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Mul β<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>m : F<VAR>s t : Set α<GOAL>⇑m '' (s * t) = ⇑m '' s * ⇑m '' t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>m : F<VAR>s t : Set α<GOAL>⇑m '' (s + t) = ⇑m '' s + ⇑m '' t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Mul β<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>m : F<VAR>s t : Set β<VAR>hs : s ⊆ Set.range ⇑m<VAR>ht : t ⊆ Set.range ⇑m<GOAL>s * t ⊆ Set.range ⇑m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>m : F<VAR>s t : Set β<VAR>hs : s ⊆ Set.range ⇑m<VAR>ht : t ⊆ Set.range ⇑m<GOAL>s + t ⊆ Set.range ⇑m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Mul β<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>m : F<VAR>s t : Set β<GOAL>⇑m ⁻¹' s * ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s * t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>m : F<VAR>s t : Set β<GOAL>⇑m ⁻¹' s + ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s + t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>Mul β<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>m : F<VAR>hm : Function.Injective ⇑m<VAR>s t : Set β<VAR>hs : s ⊆ Set.range ⇑m<VAR>ht : t ⊆ Set.range ⇑m<GOAL>⇑m ⁻¹' (s * t) = ⇑m ⁻¹' s * ⇑m ⁻¹' t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>Add β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>m : F<VAR>hm : Function.Injective ⇑m<VAR>s t : Set β<VAR>hs : s ⊆ Set.range ⇑m<VAR>ht : t ⊆ Set.range ⇑m<GOAL>⇑m ⁻¹' (s + t) = ⇑m ⁻¹' s + ⇑m ⁻¹' t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>m : F<VAR>s t : Set α<GOAL>⇑m '' (s - t) = ⇑m '' s - ⇑m '' t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>m : F<VAR>s t : Set α<GOAL>⇑m '' (s / t) = ⇑m '' s / ⇑m '' t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>m : F<VAR>s t : Set β<VAR>hs : s ⊆ Set.range ⇑m<VAR>ht : t ⊆ Set.range ⇑m<GOAL>s - t ⊆ Set.range ⇑m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>m : F<VAR>s t : Set β<VAR>hs : s ⊆ Set.range ⇑m<VAR>ht : t ⊆ Set.range ⇑m<GOAL>s / t ⊆ Set.range ⇑m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>m : F<VAR>s t : Set β<GOAL>⇑m ⁻¹' s / ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s / t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>m : F<VAR>s t : Set β<GOAL>⇑m ⁻¹' s - ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s - t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>DivisionMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>m : F<VAR>hm : Function.Injective ⇑m<VAR>s t : Set β<VAR>hs : s ⊆ Set.range ⇑m<VAR>ht : t ⊆ Set.range ⇑m<GOAL>⇑m ⁻¹' (s / t) = ⇑m ⁻¹' s / ⇑m ⁻¹' t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>SubtractionMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>m : F<VAR>hm : Function.Injective ⇑m<VAR>s t : Set β<VAR>hs : s ⊆ Set.range ⇑m<VAR>ht : t ⊆ Set.range ⇑m<GOAL>⇑m ⁻¹' (s - t) = ⇑m ⁻¹' s - ⇑m ⁻¹' t
<VAR>f : ℕ → ℕ<VAR>h1 : Monotone f<VAR>B : ℕ<VAR>h2 : ∀ (n : ℕ), f n ≤ B<VAR>h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)<VAR>k : ℕ<GOAL>B ≤ k → f k = f B
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x d : α<GOAL>[].nextOr x d = d
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y d : α<GOAL>[y].nextOr x d = d
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>x y d : α<GOAL>(x :: y :: xs).nextOr x d = y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>y x d : α<VAR>h : x ≠ y<GOAL>(y :: xs).nextOr x d = xs.nextOr x d
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>x d d' : α<VAR>x_mem : x ∈ xs<VAR>x_ne : x ≠ xs.getLast ⋯<GOAL>xs.nextOr x d = xs.nextOr x d'
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>x d : α<VAR>h : xs.nextOr x d ≠ d<GOAL>x ∈ xs
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>x : α<VAR>d : α<VAR>h : x ∉ xs<GOAL>(xs ++ [x]).nextOr x d = d
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs : List α<VAR>x d : α<VAR>hd : d ∈ xs<GOAL>xs.nextOr x d ∈ xs
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<VAR>h : x ∈ [y]<GOAL>[y].next x h = y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<VAR>h : x ∈ [y]<GOAL>[y].prev x h = y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x y z : α<VAR>h : x ∈ y :: z :: l<VAR>hx : x = y<GOAL>(y :: z :: l).next x h = z
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x z : α<VAR>h : x ∈ x :: z :: l<GOAL>(x :: z :: l).next x h = z
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : x ∈ l<VAR>y : α<GOAL>∀ (h : x ∈ y :: l) (hy : x ≠ y), x ≠ (y :: l).getLast ⋯ → (y :: l).next x h = l.next x ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>hy : x ≠ y<VAR>hx : x ∉ l<VAR>h : x ∈ y :: l ++ [x] := ⋯<GOAL>(y :: l ++ [x]).next x h = y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : x ∈ l<VAR>y : α<GOAL>∀ (h : x ∈ y :: l), x ≠ y → x = (y :: l).getLast ⋯ → l.Nodup → (y :: l).next x h = y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>hxy : x ∈ y :: l<VAR>hx : x = y<GOAL>(y :: l).prev x hxy = (y :: l).getLast ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : x ∈ x :: l<GOAL>(x :: l).prev x h = (x :: l).getLast ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x y z : α<VAR>h : x ∈ y :: z :: l<VAR>hx : x = y<GOAL>(y :: z :: l).prev x h = (z :: l).getLast ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x z : α<VAR>h : x ∈ x :: z :: l<GOAL>(x :: z :: l).prev x h = (z :: l).getLast ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x y z : α<VAR>h : x ∈ y :: z :: l<VAR>hy : x ≠ y<VAR>hz : x = z<GOAL>(y :: z :: l).prev x h = y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>h : x ∈ y :: x :: l<VAR>hy : x ≠ y<GOAL>(y :: x :: l).prev x h = y
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x y z : α<VAR>h : x ∈ y :: z :: l<VAR>hy : x ≠ y<VAR>hz : x ≠ z<GOAL>(y :: z :: l).prev x h = (z :: l).prev x ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : x ∈ l<GOAL>l.next x h ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : x ∈ l<GOAL>l.prev x h ∈ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>_h : l.Nodup<VAR>i : Fin l.length<GOAL>l.next (l.get i) ⋯ = l.get ⟨(↑i + 1) % l.length, ⋯⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>n : ℕ<VAR>hn : n < l.length<GOAL>l.next (l.nthLe n hn) ⋯ = l.nthLe ((n + 1) % l.length) ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>n : ℕ<VAR>hn : n < l.length<GOAL>l.prev (l.nthLe n hn) ⋯ = l.nthLe ((n + (l.length - 1)) % l.length) ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<GOAL>List.pmap l.next l ⋯ = l.rotate 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<GOAL>List.pmap l.prev l ⋯ = l.rotate (l.length - 1)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.prev (l.next x hx) ⋯ = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.next (l.prev x hx) ⋯ = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.reverse.prev x ⋯ = l.next x hx
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.reverse.next x ⋯ = l.prev x hx
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<VAR>h : l ~r l'<VAR>hn : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.next x hx = l'.next x ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l l' : List α<VAR>h : l ~r l'<VAR>hn : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.prev x hx = l'.prev x ⋯
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>↑l₁ = ↑l₂ ↔ l₁ ~r l₂
<VAR>α : Type u_1<VAR>l : List α<GOAL>Quot.mk Setoid.r l = ↑l
<VAR>α : Type u_1<VAR>l : List α<GOAL>Quotient.mk'' l = ↑l
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>↑(a :: l) = ↑(l ++ [a])
<VAR>α : Type u_1<GOAL>↑[] = Cycle.nil
<VAR>α : Type u_1<VAR>l : List α<GOAL>↑l = Cycle.nil ↔ l = []
<VAR>α : Type u_1<GOAL>∅ = Cycle.nil
<VAR>α : Type u_1<VAR>C : Cycle α → Prop<VAR>s : Cycle α<VAR>H0 : C Cycle.nil<VAR>HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)<GOAL>C s
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ ↑l ↔ a ∈ l
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∉ Cycle.nil
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).reverse = ↑l.reverse
<VAR>α : Type u_1<VAR>a : α<VAR>s : Cycle α<GOAL>a ∈ s.reverse ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Cycle α<GOAL>s.reverse.reverse = s
<VAR>α : Type u_1<GOAL>Cycle.nil.reverse = Cycle.nil
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).length = l.length
<VAR>α : Type u_1<GOAL>Cycle.nil.length = 0
<VAR>α : Type u_1<VAR>s : Cycle α<GOAL>s.reverse.length = s.length
<VAR>α : Type u_1<GOAL>Cycle.nil.Subsingleton
<VAR>α : Type u_1<VAR>s : Cycle α<GOAL>s.Subsingleton ↔ s.length ≤ 1
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>h : s.Subsingleton<VAR>x : α<VAR>_hx : x ∈ s<VAR>y : α<VAR>_hy : y ∈ s<GOAL>x = y
<VAR>α : Type u_1<VAR>l : List α<VAR>hl : l.Nodup<GOAL>(↑l).Nontrivial ↔ 2 ≤ l.length
<VAR>α : Type u_1<VAR>s : Cycle α<GOAL>s.reverse.Nontrivial ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>h : s.Nontrivial<GOAL>2 ≤ s.length
<VAR>α : Type u_1<GOAL>Cycle.nil.Nodup
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).Nodup ↔ l.Nodup
<VAR>α : Type u_1<VAR>s : Cycle α<GOAL>s.reverse.Nodup ↔ s.Nodup
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).toMultiset = ↑l
<VAR>α : Type u_1<GOAL>Cycle.nil.toMultiset = 0
<VAR>α : Type u_1<VAR>s : Cycle α<GOAL>Multiset.card s.toMultiset = s.length
<VAR>α : Type u_1<VAR>s : Cycle α<GOAL>s.toMultiset = 0 ↔ s = Cycle.nil
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Cycle.map f Cycle.nil = Cycle.nil
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>Cycle.map f ↑l = ↑(List.map f l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Cycle α<GOAL>Cycle.map f s = Cycle.nil ↔ s = Cycle.nil
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>s : Cycle α<GOAL>b ∈ Cycle.map f s ↔ ∃ a ∈ s, f a = b
<VAR>α : Type u_1<VAR>l : List α<GOAL>(↑l).lists = ↑l.cyclicPermutations
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>l : List α<GOAL>l ∈ s.lists ↔ ↑l = s
<VAR>α : Type u_1<GOAL>Cycle.nil.lists = ↑[[]]
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<GOAL>s.toMultiset.toFinset = s.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>(↑l).toFinset = l.toFinset
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Cycle.nil.toFinset = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<GOAL>s.toFinset = ∅ ↔ s = Cycle.nil
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.reverse.prev ⋯ x ⋯ = s.next hs x hx
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>hs : s.reverse.Nodup<VAR>x : α<VAR>hx : x ∈ s.reverse<GOAL>s.reverse.prev hs x hx = s.next ⋯ x ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.reverse.next ⋯ x ⋯ = s.prev hs x hx
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>hs : s.reverse.Nodup<VAR>x : α<VAR>hx : x ∈ s.reverse<GOAL>s.reverse.next hs x hx = s.prev ⋯ x ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.next hs x hx ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.prev hs x hx ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.prev hs (s.next hs x hx) ⋯ = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.next hs (s.prev hs x hx) ⋯ = x
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Cycle.Chain r Cycle.nil
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<VAR>l : List α<GOAL>Cycle.Chain r ↑(a :: l) ↔ List.Chain r a (l ++ [a])
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>Cycle.Chain r ↑[a] ↔ r a a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>l : List α<VAR>hl : l ≠ []<GOAL>Cycle.Chain r ↑l ↔ List.Chain r (l.getLast hl) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>f : β → α<VAR>s : Cycle β<GOAL>Cycle.Chain r (Cycle.map f s) ↔ Cycle.Chain (fun a b => r (f a) (f b)) s
<VAR>r : ℕ → ℕ → Prop<VAR>n : ℕ<GOAL>Cycle.Chain r ↑(List.range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>r₁ r₂ : α → α → Prop<VAR>H : ∀ (a b : α), r₁ a b → r₂ a b<VAR>p : Cycle.Chain r₁ s<GOAL>Cycle.Chain r₂ s
<VAR>α : Type u_1<GOAL>Monotone Cycle.Chain
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<GOAL>(∀ a ∈ s, ∀ b ∈ s, r a b) → Cycle.Chain r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>IsTrans α r<GOAL>Cycle.Chain r s ↔ ∀ a ∈ s, ∀ b ∈ s, r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>IsTrans α r<VAR>IsIrrefl α r<VAR>h : Cycle.Chain r s<GOAL>s = Cycle.nil
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>IsWellFounded α r<VAR>h : Cycle.Chain r s<GOAL>s = Cycle.nil
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>hs : Cycle.Chain r s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>a = b
<VAR>α : Type u_1<VAR>s : Set α<GOAL>SetSemiring.down (Set.up s) = s
<VAR>α : Type u_1<VAR>s : SetSemiring α<GOAL>Set.up (SetSemiring.down s) = s
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>Set.up s ≤ Set.up t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>Set.up s < Set.up t ↔ s ⊂ t
<VAR>α : Type u_1<VAR>s t : SetSemiring α<GOAL>SetSemiring.down s ⊆ SetSemiring.down t ↔ s ≤ t
<VAR>α : Type u_1<VAR>s t : SetSemiring α<GOAL>SetSemiring.down s ⊂ SetSemiring.down t ↔ s < t
<VAR>α : Type u_1<GOAL>0 = Set.up ∅
<VAR>α : Type u_1<GOAL>SetSemiring.down 0 = ∅
<VAR>α : Type u_1<GOAL>Set.up ∅ = 0
<VAR>α : Type u_1<VAR>s t : SetSemiring α<GOAL>s + t = Set.up (SetSemiring.down s ∪ SetSemiring.down t)
<VAR>α : Type u_1<VAR>s t : SetSemiring α<GOAL>SetSemiring.down (s + t) = SetSemiring.down s ∪ SetSemiring.down t
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>Set.up (s ∪ t) = Set.up s + Set.up t
<VAR>α : Type u_1<VAR>Mul α<VAR>s t : SetSemiring α<GOAL>s * t = Set.up (SetSemiring.down s * SetSemiring.down t)
<VAR>α : Type u_1<VAR>Mul α<VAR>s t : SetSemiring α<GOAL>SetSemiring.down (s * t) = SetSemiring.down s * SetSemiring.down t
<VAR>α : Type u_1<VAR>Mul α<VAR>s t : Set α<GOAL>Set.up (s * t) = Set.up s * Set.up t
<VAR>α : Type u_1<VAR>One α<GOAL>1 = Set.up 1
<VAR>α : Type u_1<VAR>One α<GOAL>SetSemiring.down 1 = 1
<VAR>α : Type u_1<VAR>One α<GOAL>Set.up 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →* β<VAR>s : SetSemiring α<GOAL>(SetSemiring.imageHom f) s = Set.up (⇑f '' SetSemiring.down s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →* β<VAR>s : SetSemiring α<GOAL>SetSemiring.down ((SetSemiring.imageHom f) s) = ⇑f '' SetSemiring.down s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α →* β<VAR>s : Set α<GOAL>Set.up (⇑f '' s) = (SetSemiring.imageHom f) (Set.up s)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>W.polynomial = { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly, d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>Nontrivial R<GOAL>W.polynomial ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>Nontrivial R<GOAL>W.polynomial.degree = 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>Nontrivial R<GOAL>W.polynomial.natDegree = 2
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>W.polynomial.Monic
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>IsDomain R<GOAL>Irreducible W.polynomial
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>Polynomial.evalEval x y W.polynomial = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>Polynomial.evalEval 0 0 W.polynomial = -W.a₆
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>W.Equation 0 0 ↔ W.a₆ = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>W.Equation x y ↔ (WeierstrassCurve.variableChange W { u := 1, r := x, s := 0, t := y }).toAffine.Equation 0 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>Polynomial.evalEval x y W.polynomialX = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>Polynomial.evalEval 0 0 W.polynomialX = -W.a₄
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>Polynomial.evalEval x y W.polynomialY = 2 * y + W.a₁ * x + W.a₃
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>Polynomial.evalEval 0 0 W.polynomialY = W.a₃
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y ≠ -y - W.a₁ * x - W.a₃)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>W.Nonsingular x y ↔ (WeierstrassCurve.variableChange W { u := 1, r := x, s := 0, t := y }).toAffine.Nonsingular 0 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>h : W.Equation 0 0<VAR>hΔ : WeierstrassCurve.Δ W ≠ 0<GOAL>W.Nonsingular 0 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<VAR>h : W.Equation x y<VAR>hΔ : WeierstrassCurve.Δ W ≠ 0<GOAL>W.Nonsingular x y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>Y - W.polynomialY = W.negPolynomial
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>Y - W.negPolynomial = W.polynomialY
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>W.negY x (W.negY x y) = y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>Polynomial.evalEval x y W.negPolynomial = W.negY x y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y L : R<GOAL>Polynomial.C (W.addPolynomial x y L) = (Y - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y L)) * (W.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y L)) + W.polynomial
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y L : R<GOAL>W.addPolynomial x y L = -{ a := 1, b := -L ^ 2 - W.a₁ * L + W.a₂, c := 2 * x * L ^ 2 + (W.a₁ * x - 2 * y - W.a₃) * L + (-W.a₁ * y + W.a₄), d := -x ^ 2 * L ^ 2 + (2 * x * y + W.a₃ * x) * L - (y ^ 2 + W.a₃ * y - W.a₆) }.toPoly
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>W.Equation x (W.negY x y) ↔ W.Equation x y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<GOAL>W.Nonsingular x (W.negY x y) ↔ W.Nonsingular x y