ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>e +ᵥ (Finset.addDysonETransform e x).2 ⊆ (Finset.addDysonETransform e x).1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addETransformLeft e x).1 = x.1 ∩ (AddOpposite.op e +ᵥ x.1)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulETransformLeft e x).1 = x.1 ∩ MulOpposite.op e • x.1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addETransformLeft e x).2 = x.2 ∪ (-e +ᵥ x.2)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulETransformLeft e x).2 = x.2 ∪ e⁻¹ • x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulETransformRight e x).1 = x.1 ∪ MulOpposite.op e • x.1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulETransformRight e x).2 = x.2 ∩ e⁻¹ • x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addETransformRight e x).2 = x.2 ∩ (-e +ᵥ x.2)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addETransformRight e x).1 = x.1 ∪ (AddOpposite.op e +ᵥ x.1)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>x : Finset α × Finset α<GOAL>Finset.mulETransformLeft 1 x = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>x : Finset α × Finset α<GOAL>Finset.addETransformLeft 0 x = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>x : Finset α × Finset α<GOAL>Finset.mulETransformRight 1 x = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>x : Finset α × Finset α<GOAL>Finset.addETransformRight 0 x = x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulETransformLeft e x).1 * (Finset.mulETransformLeft e x).2 ⊆ x.1 * x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addETransformLeft e x).1 + (Finset.addETransformLeft e x).2 ⊆ x.1 + x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulETransformRight e x).1 * (Finset.mulETransformRight e x).2 ⊆ x.1 * x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addETransformRight e x).1 + (Finset.addETransformRight e x).2 ⊆ x.1 + x.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addETransformLeft e x).1.card + (Finset.addETransformRight e x).1.card = 2 * x.1.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulETransformLeft e x).1.card + (Finset.mulETransformRight e x).1.card = 2 * x.1.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulETransformLeft e x).2.card + (Finset.mulETransformRight e x).2.card = 2 * x.2.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addETransformLeft e x).2.card + (Finset.addETransformRight e x).2.card = 2 * x.2.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.addETransformLeft e x).1.card + (Finset.addETransformLeft e x).2.card + ((Finset.addETransformRight e x).1.card + (Finset.addETransformRight e x).2.card) = x.1.card + x.2.card + (x.1.card + x.2.card)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(Finset.mulETransformLeft e x).1.card + (Finset.mulETransformLeft e x).2.card + ((Finset.mulETransformRight e x).1.card + (Finset.mulETransformRight e x).2.card) = x.1.card + x.2.card + (x.1.card + x.2.card)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>Finset.addETransformLeft (-e) x = (Finset.addETransformRight e x.swap).swap
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>Finset.mulETransformLeft e⁻¹ x = (Finset.mulETransformRight e x.swap).swap
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>Finset.mulETransformRight e⁻¹ x = (Finset.mulETransformLeft e x.swap).swap
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>AddCommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>Finset.addETransformRight (-e) x = (Finset.addETransformLeft e x.swap).swap
<VAR>ι : Type u<VAR>α : Type v<VAR>DecidableEq α<VAR>t : ι → Finset α<VAR>h : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ι' : Finset ι<GOAL>Nonempty ↑(hallMatchingsOn t ι')
<VAR>ι : Type u<VAR>α : Type v<VAR>DecidableEq α<VAR>t : ι → Finset α<GOAL>(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq β<VAR>r : α → β → Prop<VAR>(a : α) → Fintype ↑(Rel.image r {a})<GOAL>(∀ (A : Finset α), A.card ≤ Fintype.card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>Fintype β<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<GOAL>(∀ (A : Finset α), A.card ≤ (Finset.filter (fun b => ∃ a ∈ A, r a b) Finset.univ).card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>A : Set (G × G)<VAR>x₁ y₁ x₂ y₂ : G<VAR>self : IsCorner A x₁ y₁ x₂ y₂<GOAL>x₁ + y₂ = x₂ + y₁
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>A : Set (G × G)<VAR>x₁ y₁ x₂ y₂ : G<GOAL>IsCorner A x₁ y₁ x₂ y₂ ↔ (x₁, y₁) ∈ A ∧ (x₁, y₂) ∈ A ∧ (x₂, y₁) ∈ A ∧ x₁ + y₂ = x₂ + y₁
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>A : Set (G × G)<VAR>x₁ y₁ x₂ y₂ : G<VAR>self : IsCorner A x₁ y₁ x₂ y₂<GOAL>(x₂, y₁) ∈ A
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>A : Set (G × G)<VAR>x₁ y₁ x₂ y₂ : G<VAR>self : IsCorner A x₁ y₁ x₂ y₂<GOAL>(x₁, y₂) ∈ A
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>A : Set (G × G)<VAR>x₁ y₁ x₂ y₂ : G<VAR>self : IsCorner A x₁ y₁ x₂ y₂<GOAL>(x₁, y₁) ∈ A
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>A : Set (G × G)<VAR>s : Set G<VAR>hAs : A ⊆ s ×ˢ s<GOAL>IsCornerFree A ↔ ∀ ⦃x₁ : G⦄, x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>A B : Set (G × G)<VAR>x₁ y₁ x₂ y₂ : G<VAR>hAB : A ⊆ B<VAR>hA : IsCorner A x₁ y₁ x₂ y₂<GOAL>IsCorner B x₁ y₁ x₂ y₂
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>A B : Set (G × G)<VAR>hAB : A ⊆ B<VAR>hB : IsCornerFree B<GOAL>IsCornerFree A
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>x₁ y₁ x₂ y₂ : G<GOAL>¬IsCorner ∅ x₁ y₁ x₂ y₂
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>A : Set (G × G)<VAR>hA : A.Subsingleton<GOAL>IsCornerFree A
<VAR>G : Type u_1<VAR>AddCommMonoid G<GOAL>IsCornerFree ∅
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>x : G × G<GOAL>IsCornerFree {x}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddCommMonoid G<VAR>AddCommMonoid H<VAR>A : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>x₁ y₁ x₂ y₂ : G<VAR>hf : IsAddFreimanHom 2 s t f<VAR>hAs : A ⊆ s ×ˢ s<VAR>hA : IsCorner A x₁ y₁ x₂ y₂<GOAL>IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddCommMonoid G<VAR>AddCommMonoid H<VAR>A : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>hf : IsAddFreimanHom 2 s t f<VAR>hf' : Set.InjOn f s<VAR>hAs : A ⊆ s ×ˢ s<VAR>hA : IsCornerFree (Prod.map f f '' A)<GOAL>IsCornerFree A
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddCommMonoid G<VAR>AddCommMonoid H<VAR>A : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>x₁ y₁ x₂ y₂ : G<VAR>hf : IsAddFreimanIso 2 s t f<VAR>hAs : A ⊆ s ×ˢ s<VAR>hx₁ : x₁ ∈ s<VAR>hy₁ : y₁ ∈ s<VAR>hx₂ : x₂ ∈ s<VAR>hy₂ : y₂ ∈ s<GOAL>IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddCommMonoid G<VAR>AddCommMonoid H<VAR>A : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>hf : IsAddFreimanIso 2 s t f<VAR>hAs : A ⊆ s ×ˢ s<GOAL>IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A
<VAR>x y : ONote<GOAL>x < y ↔ x.repr < y.repr
<VAR>x y : ONote<GOAL>x ≤ y ↔ x.repr ≤ y.repr
<VAR>n : ℕ<GOAL>↑n.succ = ONote.oadd 0 n.succPNat 0
<VAR>n : ℕ<GOAL>(↑n).repr = ↑n
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<GOAL>0 < e.oadd n a
<VAR>o₁ o₂ : ONote<GOAL>o₁.cmp o₂ = Ordering.eq → o₁ = o₂
<VAR>o : ONote<VAR>self : o.NF<GOAL>Exists o.NFBelow
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>b : Ordinal.{0}<GOAL>e.NF → a.NFBelow e.repr → e.repr < b → (e.oadd n a).NFBelow b
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>b : Ordinal.{0}<VAR>h : (e.oadd n a).NFBelow b<GOAL>e.NF
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<GOAL>(e.oadd n a).NF → e.NF
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>b : Ordinal.{0}<VAR>h : (e.oadd n a).NFBelow b<GOAL>a.NFBelow e.repr
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<GOAL>(e.oadd n a).NF → a.NFBelow e.repr
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>h : (e.oadd n a).NF<GOAL>a.NF
<VAR>e a : ONote<VAR>h₁ : e.NF<VAR>n : ℕ+<VAR>h₂ : a.NFBelow e.repr<GOAL>(e.oadd n a).NF
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>b : Ordinal.{0}<VAR>h : (e.oadd n a).NFBelow b<GOAL>e.repr < b
<VAR>o : ONote<GOAL>o.NFBelow 0 ↔ o = 0
<VAR>o : ONote<VAR>b : Ordinal.{0}<VAR>h : o.NFBelow b<GOAL>o.repr < ω ^ b
<VAR>o : ONote<VAR>b₁ b₂ : Ordinal.{0}<VAR>bb : b₁ ≤ b₂<VAR>h : o.NFBelow b₁<GOAL>o.NFBelow b₂
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>b : Ordinal.{0}<VAR>H : e.repr < b<GOAL>(e.oadd n a).NF → (e.oadd n a).NFBelow b
<VAR>o : ONote<VAR>b : Ordinal.{0}<GOAL>o.repr < ω ^ b → o.NF → o.NFBelow b
<VAR>n : ℕ<GOAL>(↑n).NFBelow 1
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>o₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>o₂ : ONote<VAR>h₁ : (e₁.oadd n₁ o₁).NF<VAR>h : e₁ < e₂<GOAL>e₁.oadd n₁ o₁ < e₂.oadd n₂ o₂
<VAR>a b : ONote<VAR>a.NF<VAR>b.NF<GOAL>(a.cmp b).Compares a b
<VAR>a b : ONote<VAR>a.NF<VAR>b.NF<GOAL>a.repr = b.repr ↔ a = b
<VAR>b : ONote<VAR>b.NF<VAR>o : ONote<GOAL>o.NFBelow b.repr ↔ o.NF ∧ b.TopBelow o
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<GOAL>e.oadd n a + o = e.addAux n (a + o)
<VAR>b : Ordinal.{0}<VAR>o₁ o₂ : ONote<GOAL>o₁.NFBelow b → o₂.NFBelow b → (o₁ + o₂).NFBelow b
<VAR>o₁ o₂ : ONote<VAR>o₁.NF<VAR>o₂.NF<GOAL>(o₁ + o₂).repr = o₁.repr + o₂.repr
<VAR>o₁ o₂ : ONote<VAR>b : Ordinal.{0}<GOAL>o₁.NFBelow b → o₂.NF → (o₁ - o₂).NFBelow b
<VAR>o₁ o₂ : ONote<VAR>o₁.NF<VAR>o₂.NF<GOAL>(o₁ - o₂).repr = o₁.repr - o₂.repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<GOAL>e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂ = if e₂ = 0 then e₁.oadd (n₁ * n₂) a₁ else (e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>b₁ : Ordinal.{0}<VAR>h₁ : (e₁.oadd n₁ a₁).NFBelow b₁<VAR>o₂ : ONote<VAR>b₂ : Ordinal.{0}<GOAL>o₂.NFBelow b₂ → (e₁.oadd n₁ a₁ * o₂).NFBelow (e₁.repr + b₂)
<VAR>o₁ o₂ : ONote<VAR>o₁.NF<VAR>o₂.NF<GOAL>(o₁ * o₂).repr = o₁.repr * o₂.repr
<VAR>o₁ o₂ : ONote<GOAL>o₁ ^ o₂ = o₂.opowAux2 o₁.split
<VAR>o o' : ONote<VAR>m : ℕ<VAR>o.NF<GOAL>o.split' = (o', m) → o.split = (ONote.scale 1 o', m)
<VAR>o o' : ONote<VAR>m : ℕ<VAR>o.NF<GOAL>o.split' = (o', m) → o'.NF ∧ o.repr = ω * o'.repr + ↑m
<VAR>x : ONote<VAR>x.NF<VAR>o : ONote<VAR>o.NF<GOAL>x.scale o = x.oadd 1 0 * o
<VAR>x : ONote<VAR>x.NF<VAR>o : ONote<VAR>o.NF<GOAL>(x.scale o).repr = ω ^ x.repr * o.repr
<VAR>o o' : ONote<VAR>m : ℕ<VAR>o.NF<VAR>h : o.split = (o', m)<GOAL>o'.NF ∧ o.repr = o'.repr + ↑m
<VAR>o o' : ONote<VAR>m : ℕ<VAR>o.NF<VAR>h : o.split = (o', m)<GOAL>ω ∣ o'.repr
<VAR>o e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>m : ℕ<VAR>o.NF<VAR>h : o.split = (e.oadd n a, m)<GOAL>a.repr + ↑m < ω ^ e.repr
<VAR>n : ℕ<VAR>o : ONote<GOAL>o.mulNat n = o * ↑n
<VAR>e a0 a : ONote<VAR>e.NF<VAR>a0.NF<VAR>a.NF<VAR>k m : ℕ<GOAL>(e.opowAux a0 a k m).repr = ω ^ e.repr * (ONote.opowAux 0 a0 a k m).repr
<VAR>e a : ONote<VAR>Ne : e.NF<VAR>Na : a.NF<VAR>a' : Ordinal.{0}<VAR>e0 : e.repr ≠ 0<VAR>h : a' < ω ^ e.repr<VAR>aa : a.repr = a'<VAR>n : ℕ+<GOAL>(ω ^ e.repr * ↑↑n + a') ^ ω = (ω ^ e.repr) ^ ω
<VAR>a0 a' : ONote<VAR>N0 : a0.NF<VAR>Na' : a'.NF<VAR>m : ℕ<VAR>d : ω ∣ a'.repr<VAR>e0 : a0.repr ≠ 0<VAR>h : a'.repr + ↑m < ω ^ a0.repr<VAR>n : ℕ+<VAR>k : ℕ<GOAL>let R := (ONote.opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr;
(k ≠ 0 → R < (ω ^ a0.repr) ^ Order.succ ↑k) ∧ (ω ^ a0.repr) ^ ↑k * (ω ^ a0.repr * ↑↑n + a'.repr) + R = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ Order.succ ↑k
<VAR>o₁ o₂ : ONote<VAR>o₁.NF<VAR>o₂.NF<GOAL>(o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
<VAR>α : Sort u_1<VAR>hα : Nonempty α<VAR>o : Ordinal.{u_2}<VAR>f : α → Ordinal.{u_2}<VAR>H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i<VAR>b : Ordinal.{u_2}<VAR>a : Ordinal.{u_2}<VAR>h : a < b + o<GOAL>∃ i, a < b + f i
<VAR>o : Ordinal.{u_1}<VAR>a : Ordinal.{u_1}<VAR>h : a < o * ω<GOAL>∃ i, a < o * ↑i + o
<VAR>o : ONote<GOAL>o.FundamentalSequenceProp (Sum.inl none) ↔ o = 0
<VAR>o a : ONote<GOAL>o.FundamentalSequenceProp (Sum.inl (some a)) ↔ o.repr = Order.succ a.repr ∧ (o.NF → a.NF)
<VAR>o : ONote<VAR>f : ℕ → ONote<GOAL>o.FundamentalSequenceProp (Sum.inr f) ↔ o.repr.IsLimit ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < o ∧ (o.NF → (f i).NF)) ∧ ∀ a < o.repr, ∃ i, a < (f i).repr
<VAR>o : ONote<GOAL>o.FundamentalSequenceProp o.fundamentalSequence
<VAR>o : ONote<VAR>x : Option ONote ⊕ (ℕ → ONote)<VAR>e : o.fundamentalSequence = x<GOAL>o.fastGrowing = match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) x, ⋯ with | Sum.inl none, x => Nat.succ | Sum.inl (some a), x => fun i => a.fastGrowing^[i] i | Sum.inr f, x => fun i => (f i).fastGrowing i
<VAR>o : ONote<VAR>a : ONote<VAR>h : o.fundamentalSequence = Sum.inl (some a)<GOAL>o.fastGrowing = fun i => a.fastGrowing^[i] i
<GOAL>ONote.fastGrowing 1 = fun n => 2 * n
<GOAL>ONote.fastGrowing 2 = fun n => 2 ^ n * n
<GOAL>ONote.fastGrowingε₀ 0 = 1
<GOAL>ONote.fastGrowingε₀ 1 = 2
<GOAL>ONote.fastGrowingε₀ 2 = 2048
<VAR>a b : NONote<GOAL>(a.cmp b).Compares a b
<VAR>a b : NONote<GOAL>(a + b).repr = a.repr + b.repr
<VAR>a b : NONote<GOAL>(a - b).repr = a.repr - b.repr
<VAR>a b : NONote<GOAL>(a * b).repr = a.repr * b.repr
<VAR>a b : NONote<GOAL>(a.opow b).repr = a.repr ^ b.repr
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>self : G.Subgraph<VAR>v w : V<GOAL>self.Adj v w → v ∈ self.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>self : G.Subgraph<GOAL>Symmetric self.Adj
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>self : G.Subgraph<VAR>v w : V<GOAL>self.Adj v w → G.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>(G.singletonSubgraph v).verts = {v}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>∀ (a a_1 : V), (G.singletonSubgraph v).Adj a a_1 = ⊥ a a_1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj hvw).verts = {v, w}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>hvw : G.Adj v w<VAR>a b : V<GOAL>(G.subgraphOfAdj hvw).Adj a b = (s(v, w) = s(a, b))
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>Irreflexive G'.Adj
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v w : V<GOAL>G'.Adj v w ↔ G'.Adj w v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>u v : V<VAR>h : G'.Adj u v<GOAL>G'.Adj v u
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>u v : V<VAR>h : H.Adj u v<GOAL>G.Adj u v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>u v : V<VAR>h : H.Adj u v<GOAL>u ∈ H.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>u v : V<VAR>h : H.Adj u v<GOAL>v ∈ H.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>u v : V<VAR>h : H.Adj u v<GOAL>u ≠ v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v w : ↑G'.verts<GOAL>G'.coe.Adj v w = G'.Adj ↑v ↑w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>u v : ↑G'.verts<VAR>h : G'.coe.Adj u v<GOAL>G.Adj ↑u ↑v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>u v : V<VAR>h : H.Adj u v<GOAL>H.coe.Adj ⟨u, ⋯⟩ ⟨v, ⋯⟩
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>G'.IsSpanning ↔ G'.verts = Set.univ
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>∀ (a a_1 : V), G'.spanningCoe.Adj a a_1 = G'.Adj a a_1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>u v : ↑G'.verts<VAR>h : G'.spanningCoe.Adj ↑u ↑v<GOAL>G.Adj ↑u ↑v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<GOAL>G₁.spanningCoe = G₂.spanningCoe ↔ G₁.Adj = G₂.Adj
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>h : G'.IsSpanning<VAR>v : V<GOAL>↑((G'.spanningCoeEquivCoeOfSpanning h) v) = v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>h : G'.IsSpanning<VAR>v : ↑G'.verts<GOAL>(RelIso.symm (G'.spanningCoeEquivCoeOfSpanning h)) v = ↑v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<VAR>v : V<GOAL>v ∈ H.support ↔ ∃ w, H.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : G.Subgraph<GOAL>H.support ⊆ H.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v : V<GOAL>G'.neighborSet v ⊆ G.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v : V<GOAL>G'.neighborSet v ⊆ G'.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v w : V<GOAL>w ∈ G'.neighborSet v ↔ G'.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<GOAL>G'.edgeSet ⊆ G.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v w : V<GOAL>s(v, w) ∈ G'.edgeSet ↔ G'.Adj v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>e : Sym2 V<VAR>v : V<VAR>he : e ∈ G'.edgeSet<VAR>hv : v ∈ e<GOAL>v ∈ G'.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v : V<GOAL>G'.incidenceSet v ⊆ G.incidenceSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>v : V<GOAL>G'.incidenceSet v ⊆ G'.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>V'' : Set V<VAR>hV : V'' = G'.verts<VAR>adj' : V → V → Prop<VAR>hadj : adj' = G'.Adj<GOAL>G'.copy V'' hV adj' hadj = G'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<GOAL>(G₁ ⊔ G₂).Adj a b ↔ G₁.Adj a b ∨ G₂.Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<GOAL>(G₁ ⊓ G₂).Adj a b ↔ G₁.Adj a b ∧ G₂.Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<GOAL>⊤.Adj a b ↔ G.Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<GOAL>¬⊥.Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<GOAL>(G₁ ⊔ G₂).verts = G₁.verts ∪ G₂.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<GOAL>(G₁ ⊓ G₂).verts = G₁.verts ∩ G₂.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>⊤.verts = Set.univ
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>⊥.verts = ∅
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>s : Set G.Subgraph<GOAL>(sSup s).Adj a b ↔ ∃ G_1 ∈ s, G_1.Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>s : Set G.Subgraph<GOAL>(sInf s).Adj a b ↔ (∀ G' ∈ s, G'.Adj a b) ∧ G.Adj a b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>f : ι → G.Subgraph<GOAL>(⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>f : ι → G.Subgraph<GOAL>(⨅ i, f i).Adj a b ↔ (∀ (i : ι), (f i).Adj a b) ∧ G.Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>s : Set G.Subgraph<VAR>hs : s.Nonempty<GOAL>(sInf s).Adj a b ↔ ∀ G' ∈ s, G'.Adj a b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b : V<VAR>Nonempty ι<VAR>f : ι → G.Subgraph<GOAL>(⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set G.Subgraph<GOAL>(sSup s).verts = ⋃ G' ∈ s, G'.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set G.Subgraph<GOAL>(sInf s).verts = ⋂ G' ∈ s, G'.verts
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>f : ι → G.Subgraph<GOAL>(⨆ i, f i).verts = ⋃ i, (f i).verts
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>f : ι → G.Subgraph<GOAL>(⨅ i, f i).verts = ⋂ i, (f i).verts
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>Function.Injective fun G' => (G'.verts, G'.spanningCoe)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H H' : G.Subgraph<VAR>h : H ≤ H'<GOAL>H.verts ⊆ H'.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>Monotone SimpleGraph.Subgraph.verts
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>default = ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H H' : G.Subgraph<VAR>v : V<GOAL>(H ⊔ H').neighborSet v = H.neighborSet v ∪ H'.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H H' : G.Subgraph<VAR>v : V<GOAL>(H ⊓ H').neighborSet v = H.neighborSet v ∩ H'.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>⊤.neighborSet v = G.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>⊥.neighborSet v = ∅
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set G.Subgraph<VAR>v : V<GOAL>(sSup s).neighborSet v = ⋃ G' ∈ s, G'.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set G.Subgraph<VAR>v : V<GOAL>(sInf s).neighborSet v = (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>f : ι → G.Subgraph<VAR>v : V<GOAL>(⨆ i, f i).neighborSet v = ⋃ i, (f i).neighborSet v
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>f : ι → G.Subgraph<VAR>v : V<GOAL>(⨅ i, f i).neighborSet v = (⋂ i, (f i).neighborSet v) ∩ G.neighborSet v
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>⊤.edgeSet = G.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>⊥.edgeSet = ∅
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H₁ H₂ : G.Subgraph<GOAL>(H₁ ⊓ H₂).edgeSet = H₁.edgeSet ∩ H₂.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H₁ H₂ : G.Subgraph<GOAL>(H₁ ⊔ H₂).edgeSet = H₁.edgeSet ∪ H₂.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set G.Subgraph<GOAL>(sSup s).edgeSet = ⋃ G' ∈ s, G'.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>s : Set G.Subgraph<GOAL>(sInf s).edgeSet = (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>f : ι → G.Subgraph<GOAL>(⨆ i, f i).edgeSet = ⋃ i, (f i).edgeSet
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>f : ι → G.Subgraph<GOAL>(⨅ i, f i).edgeSet = (⋂ i, (f i).edgeSet) ∩ G.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>⊤.spanningCoe = G
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>⊥.spanningCoe = ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : SimpleGraph V<VAR>h : H ≤ G<GOAL>(SimpleGraph.toSubgraph H h).verts = Set.univ
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : SimpleGraph V<VAR>h : H ≤ G<GOAL>∀ (a a_1 : V), (SimpleGraph.toSubgraph H h).Adj a a_1 = H.Adj a a_1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H H' : G.Subgraph<VAR>h : H ≤ H'<GOAL>H.support ⊆ H'.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H : SimpleGraph V<VAR>h : H ≤ G<GOAL>(SimpleGraph.toSubgraph H h).IsSpanning
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H H' : G.Subgraph<VAR>h : H ≤ H'<GOAL>H.spanningCoe ≤ H'.spanningCoe
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H₁ H₂ : G.Subgraph<VAR>h : H₁ ≤ H₂<GOAL>H₁.edgeSet ≤ H₂.edgeSet
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>H₁ H₂ : G.Subgraph<VAR>h : Disjoint H₁ H₂<GOAL>Disjoint H₁.edgeSet H₂.edgeSet
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>H : G.Subgraph<GOAL>∀ (a a_1 : W), (SimpleGraph.Subgraph.map f H).Adj a a_1 = Relation.Map H.Adj (⇑f) (⇑f) a a_1
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>H : G.Subgraph<GOAL>(SimpleGraph.Subgraph.map f H).verts = ⇑f '' H.verts
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<GOAL>Monotone (SimpleGraph.Subgraph.map f)
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>H H' : G.Subgraph<GOAL>SimpleGraph.Subgraph.map f (H ⊔ H') = SimpleGraph.Subgraph.map f H ⊔ SimpleGraph.Subgraph.map f H'
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>H : G'.Subgraph<VAR>u v : V<GOAL>(SimpleGraph.Subgraph.comap f H).Adj u v = (G.Adj u v ∧ H.Adj (f u) (f v))
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>H : G'.Subgraph<GOAL>(SimpleGraph.Subgraph.comap f H).verts = ⇑f ⁻¹' H.verts
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<GOAL>Monotone (SimpleGraph.Subgraph.comap f)