ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>h : ¬G.IsAcyclic<VAR>w✝¹ : α<VAR>w✝ : G.Walk w✝¹ w✝¹<VAR>h✝ : w✝.IsCycle ∧ G.egirth = ↑w✝.length<GOAL>∃ a w, w.IsCycle ∧ w✝.length = w.length
<VAR>this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|<VAR>a b : ℤ<VAR>n : ℕ<GOAL>|a / -↑n| ≤ |a|
<VAR>this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|<VAR>a b : ℤ<VAR>n : ℕ<GOAL>|a / ↑n| ≤ |a|
<VAR>a : ℤ<VAR>n : ℕ<GOAL>|a / ↑n| ≤ |a|
<VAR>a : ℤ<VAR>n : ℕ<GOAL>↑(a / ↑n).natAbs ≤ ↑a.natAbs
<VAR>a x z✝ z : ℂ<GOAL>z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
<VAR>a x z✝ z : ℂ<VAR>hre : 0 ≤ z.re<GOAL>z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<GOAL>z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<GOAL>z.arg ≤ π / 2 ↔ z.im < 0
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<VAR>him : 0 ≤ z.im<GOAL>z.arg ≤ π / 2 ↔ z.im < 0
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im < 0<GOAL>z.arg ≤ π / 2 ↔ z.im < 0
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(W.baseChange B).preΨ₄ = Polynomial.map (↑f) (W.baseChange A).preΨ₄
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ<GOAL>Submartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<GOAL>StarConvex 𝕜 (-x) (-s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t : Set E<VAR>hs : StarConvex 𝕜 x s<GOAL>StarConvex 𝕜 (-x) (Neg.neg '' s)
<VAR>α : Type u_1<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSingletonClass α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : PMF α<VAR>f : α → E<VAR>hf : Integrable f p.toMeasure<GOAL>∫ (a : α), f a ∂p.toMeasure = ∫ (a : α) in p.support, f a ∂p.toMeasure
<VAR>α : Type u_1<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSingletonClass α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : PMF α<VAR>f : α → E<VAR>hf : Integrable f p.toMeasure<GOAL>∫ (a : α) in p.support, f a ∂p.toMeasure = ∑' (a : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a
<VAR>α : Type u_1<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSingletonClass α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : PMF α<VAR>f : α → E<VAR>hf : Integrable f p.toMeasure<GOAL>Integrable f (p.toMeasure.restrict p.support)
<VAR>α : Type u_1<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSingletonClass α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : PMF α<VAR>f : α → E<VAR>hf : Integrable f p.toMeasure<VAR>x : ↑p.support<GOAL>p.toMeasure {↑x} = p ↑x
<VAR>α : Type u_1<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSingletonClass α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : PMF α<VAR>f : α → E<VAR>hf : Integrable f p.toMeasure<GOAL>Function.support ?m.4776 ⊆ ?m.4777
<VAR>n : ℕ<GOAL>cos (↑n * (2 * ↑π) - ↑π) = -1
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝² : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝¹ : yoneda.HasPointwiseLeftKanExtension A<VAR>L✝ : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ<VAR>α : A ⟶ yoneda ⋙ L✝<VAR>L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ<VAR>e : A ≅ yoneda ⋙ L<VAR>inst✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L<GOAL>L.IsLeftKanExtension e.hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝² : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝¹ : yoneda.HasPointwiseLeftKanExtension A<VAR>L✝ : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ<VAR>α : A ⟶ yoneda ⋙ L✝<VAR>L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ<VAR>e : A ≅ yoneda ⋙ L<VAR>inst✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L<GOAL>IsIso e.hom ∧ Nonempty (PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>L : IntermediateField F E<GOAL>separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>L : IntermediateField F E<VAR>h : separableClosure F E ≤ L<GOAL>IsPurelyInseparable (↥L) E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>L : IntermediateField F E<VAR>h : separableClosure F E ≤ L<VAR>this : IsPurelyInseparable (↥(separableClosure F E)) E<GOAL>IsPurelyInseparable (↥L) E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>L : IntermediateField F E<VAR>h : separableClosure F E ≤ L<VAR>this✝¹ : IsPurelyInseparable (↥(separableClosure F E)) E<VAR>this✝ : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra<VAR>this : SMul ↥(separableClosure F E) ↥L := Algebra.toSMul<GOAL>IsPurelyInseparable (↥L) E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>L : IntermediateField F E<VAR>h : separableClosure F E ≤ L<VAR>this✝² : IsPurelyInseparable (↥(separableClosure F E)) E<VAR>this✝¹ : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra<VAR>this✝ : SMul ↥(separableClosure F E) ↥L := Algebra.toSMul<VAR>this : IsScalarTower (↥(separableClosure F E)) (↥L) E<GOAL>IsPurelyInseparable (↥L) E
<VAR>p a b : ℕ<VAR>hpa : p ∈ a.primeFactorsList<VAR>hb : b ≠ 0<GOAL>p ∈ (a * b).primeFactorsList
<VAR>p b : ℕ<VAR>hb : b ≠ 0<VAR>hpa : p ∈ primeFactorsList 0<GOAL>p ∈ (0 * b).primeFactorsList
<VAR>p a b : ℕ<VAR>hpa : p ∈ a.primeFactorsList<VAR>hb : b ≠ 0<VAR>ha : a ≠ 0<GOAL>p ∈ (a * b).primeFactorsList
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>countP p l = (filter p l).length
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>a✝ : Nontrivial E<GOAL>MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ) (μ.toSphere.prod (volumeIoiPow (dim E - 1)))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>a✝ : Nontrivial E<GOAL>μ.toSphere.prod (volumeIoiPow (dim E - 1)) = map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>a✝ : Nontrivial E<VAR>s : Set ↑(sphere 0 1)<VAR>hs : s ∈ {s | MeasurableSet s}<VAR>r : ↑(Ioi 0)<GOAL>(map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) = μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>a✝ : Nontrivial E<VAR>s : Set ↑(sphere 0 1)<VAR>hs : s ∈ {s | MeasurableSet s}<VAR>r : ↑(Ioi 0)<VAR>this : Ioo 0 ↑r = ↑r • Ioo 0 1<GOAL>(map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) = μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>a✝ : Nontrivial E<VAR>s : Set ↑(sphere 0 1)<VAR>hs : s ∈ {s | MeasurableSet s}<VAR>r : ↑(Ioi 0)<VAR>this : Ioo 0 ↑r = ↑r • Ioo 0 1<VAR>hpos : 0 < dim E<GOAL>(map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) = μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>a✝ : Nontrivial E<VAR>s : Set ↑(sphere 0 1)<VAR>hs : s ∈ {s | MeasurableSet s}<VAR>r : ↑(Ioi 0)<VAR>this : Ioo 0 ↑r = ↑r • Ioo 0 1<VAR>hpos : 0 < dim E<GOAL>↑(dim E) ≠ 0
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>a✝ : Nontrivial E<VAR>s : Set ↑(sphere 0 1)<VAR>hs : s ∈ {s | MeasurableSet s}<VAR>r : ↑(Ioi 0)<VAR>this : Ioo 0 ↑r = ↑r • Ioo 0 1<VAR>hpos : 0 < dim E<GOAL>0 ≤ ↑(dim E)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus : u ⊆ insert x s<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this : (insert x s ∪ v) \ u ∈ 𝒜<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this : v \ u = v<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝ : v \ u = v<VAR>this : x ∉ u<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝ : v \ u = v<VAR>this : x ∉ u<VAR>hus : u ⊆ s<GOAL>u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝ : v \ u = v<VAR>this : x ∉ u<VAR>hus : u ⊆ s<GOAL>u ⊆ s ∧ Disjoint v s ∧ (∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜) ∧ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝ : v \ u = v<VAR>this : x ∉ u<VAR>hus : u ⊆ s<GOAL>x ∉ (s ∪ v) \ u
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝ : v \ u = v<VAR>this : x ∉ u<VAR>hus : u ⊆ s<GOAL>insert x ((s ∪ v) \ u) ∈ 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝ : v \ u = v<VAR>this : x ∉ u<VAR>hus : u ⊆ s<GOAL>¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝ : v \ u = v<VAR>this : x ∉ u<VAR>hus : u ⊆ s<VAR>w : α<VAR>hwB : w ∉ (s ∪ v) \ u<VAR>hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝² : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝¹ : v \ u = v<VAR>this✝ : x ∉ u<VAR>hus : u ⊆ s<VAR>w : α<VAR>hwB : w ∉ (s ∪ v) \ u<VAR>hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'<VAR>this : v ⊆ insert w ((s ∪ v) \ u)<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝² : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝¹ : v \ u = v<VAR>this✝ : x ∉ u<VAR>hus : u ⊆ s<VAR>w : α<VAR>hwB : w ∉ (s ∪ v) \ u<VAR>hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'<VAR>this : v ⊆ insert w ((s ∪ v) \ u)<VAR>hwu : w ∉ u<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝² : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝¹ : v \ u = v<VAR>this✝ : x ∉ u<VAR>hus : u ⊆ s<VAR>w : α<VAR>hwB : w ∈ s ∪ v → w ∈ u<VAR>hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'<VAR>this : v ⊆ insert w ((s ∪ v) \ u)<VAR>hwu : w ∉ u<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝² : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝¹ : v \ u = v<VAR>this✝ : x ∉ u<VAR>hus : u ⊆ s<VAR>w : α<VAR>hwB : w ∈ s ∪ v → w ∈ u<VAR>hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'<VAR>this : v ⊆ insert w ((s ∪ v) \ u)<VAR>hwu : w ∉ u<GOAL>insert w s ∈ 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u✝ v✝ a : Finset α<VAR>r : ℕ<VAR>u v : Finset α<VAR>huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜<VAR>𝒜' : Finset (Finset α) := 𝓒 u v 𝒜<VAR>s : Finset α<VAR>hs𝒜' : s ∈ ∂ 𝒜'<VAR>hs𝒜 : s ∉ ∂ 𝒜<VAR>m : ∀ y ∉ s, insert y s ∉ 𝒜<VAR>x : α<VAR>left✝ : x ∉ s<VAR>right✝ : insert x s ∈ 𝒜'<VAR>hus✝ : u ⊆ insert x s<VAR>hvs : Disjoint v (insert x s)<VAR>this✝³ : (insert x s ∪ v) \ u ∈ 𝒜<VAR>hsv : Disjoint s v<VAR>hvu : Disjoint v u<VAR>hxv : x ∉ v<VAR>this✝² : v \ u = v<VAR>this✝¹ : x ∉ u<VAR>hus : u ⊆ s<VAR>w : α<VAR>hwB : w ∈ s ∪ v → w ∈ u<VAR>hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'<VAR>this✝ : v ⊆ insert w ((s ∪ v) \ u)<VAR>hwu : w ∉ u<VAR>this : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜<GOAL>insert w s ∈ 𝒜