ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))<VAR>hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))<VAR>hg2 : IntervalIntegrable (fun x => f' x • (g ∘ f) x) volume a b<VAR>hG : CompleteSpace G<VAR>h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]<VAR>h_der : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)<GOAL>cylinder s S₁ ∪ cylinder s S₂ = cylinder s (S₁ ∪ S₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → γ<VAR>g : β → δ<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>y : β<VAR>hf : Tendsto f (𝓝[s] x) (𝓝 (f x))<VAR>hg : Tendsto g (𝓝[t] y) (𝓝 (g y))<GOAL>Tendsto (Prod.map f g) (𝓝[s ×ˢ t] (x, y)) (𝓝 (Prod.map f g (x, y)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → γ<VAR>g : β → δ<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>y : β<VAR>hf : Tendsto f (𝓝[s] x) (𝓝 (f x))<VAR>hg : Tendsto g (𝓝[t] y) (𝓝 (g y))<GOAL>Tendsto (Prod.map f g) (𝓝[s] x ×ˢ 𝓝[t] y) (𝓝 (f x) ×ˢ 𝓝 (g y))
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<GOAL>⇑f =O[cocompact E] fun x => ‖x‖ ^ (-↑k)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<VAR>d : ℝ<VAR>left✝ : 0 < d<VAR>hd' : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ d<GOAL>⇑f =O[cocompact E] fun x => ‖x‖ ^ (-↑k)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<VAR>d : ℝ<VAR>left✝ : 0 < d<VAR>hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d<GOAL>⇑f =O[cocompact E] fun x => ‖x‖ ^ (-↑k)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<VAR>d : ℝ<VAR>left✝ : 0 < d<VAR>hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d<GOAL>∃ c, ∀ᶠ (x : E) in cocompact E, ‖f x‖ ≤ c * ‖‖x‖ ^ (-↑k)‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<VAR>d : ℝ<VAR>left✝ : 0 < d<VAR>hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d<GOAL>∀ᶠ (x : E) in cofinite, ‖f x‖ ≤ d * ‖‖x‖ ^ (-↑k)‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<VAR>d : ℝ<VAR>left✝ : 0 < d<VAR>hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d<VAR>x : E<VAR>hx : x ≠ 0<GOAL>‖f x‖ ≤ d * ‖‖x‖ ^ (-↑k)‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<VAR>d : ℝ<VAR>left✝ : 0 < d<VAR>hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d<VAR>x : E<VAR>hx : x ≠ 0<GOAL>‖x‖ ^ ↑k * ‖f x‖ ≤ d
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<VAR>d : ℝ<VAR>left✝ : 0 < d<VAR>hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d<VAR>x : E<VAR>hx : x ≠ 0<GOAL>0 < ‖x‖ ^ ↑k
<VAR>B : Type u<VAR>inst✝ : Quiver B<VAR>a b c : B<VAR>f : Hom a b<VAR>g : Hom b c<GOAL>normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : Fintype β<VAR>f : α ↪ β<GOAL>(map f s).dens ≤ s.dens
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : Fintype β<VAR>f : α ↪ β<VAR>h✝ : IsEmpty α<GOAL>(map f s).dens ≤ s.dens
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : Fintype β<VAR>f : α ↪ β<VAR>h✝ : Nonempty α<GOAL>(map f s).dens ≤ s.dens
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : Fintype β<VAR>f : α ↪ β<VAR>h✝ : Nonempty α<GOAL>↑s.card / ↑(Fintype.card β) ≤ ↑s.card / ↑(Fintype.card α)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>0 ≤ trailingDegree 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>0 ≤ (C 1).trailingDegree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>hμν : μ ≪ ν<GOAL>essInf f ν ≤ essInf f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>hμν : μ ≪ ν<GOAL>IsBoundedUnder (fun x x_1 => x ≥ x_1) (ae ν) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>f : α → β<VAR>hμν : μ ≪ ν<GOAL>IsCoboundedUnder (fun x x_1 => x ≥ x_1) (ae μ) f
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>h : ¬i = j<GOAL>auxGroup i = auxGroup j
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>h : ¬i = j<GOAL>∀ (a b c d : HomotopyGroup N X x), Mul.mul (Mul.mul a b) (Mul.mul c d) = Mul.mul (Mul.mul a c) (Mul.mul b d)
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>h : ¬i = j<VAR>a✝ : HomotopyGroup N X x<VAR>a : ↑(Ω^ N X x)<VAR>b✝ : HomotopyGroup N X x<VAR>b : ↑(Ω^ N X x)<VAR>c✝ : HomotopyGroup N X x<VAR>c : ↑(Ω^ N X x)<VAR>d✝ : HomotopyGroup N X x<VAR>d : ↑(Ω^ N X x)<GOAL>(loopHomeo i).symm (Path.trans ((loopHomeo i).toEquiv ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv d) ((loopHomeo j).toEquiv c)))) ((loopHomeo i).toEquiv ((loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv b) ((loopHomeo j).toEquiv a))))) = (loopHomeo j).symm (Path.trans ((loopHomeo j).toEquiv ((loopHomeo i).symm (Path.trans ((loopHomeo i).toEquiv d) ((loopHomeo i).toEquiv b)))) ((loopHomeo j).toEquiv ((loopHomeo i).symm (Path.trans ((loopHomeo i).toEquiv c) ((loopHomeo i).toEquiv a)))))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>b0 : b ≠ 0<VAR>c : Ordinal.{u_4}<GOAL>(b * a + c) / b = a + c / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>b0 : b ≠ 0<VAR>c : Ordinal.{u_4}<GOAL>(b * a + c) / b ≤ a + c / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>b0 : b ≠ 0<VAR>c : Ordinal.{u_4}<GOAL>a + c / b ≤ (b * a + c) / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>(∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LE α<VAR>inst✝¹ : MulOneClass α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : MulLECancellable a<GOAL>a * b ≤ a ↔ a * b ≤ a * 1
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>inst✝ : Mono f<VAR>a b : X₁ ⊕ X₂<GOAL>Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Rel' f g a b
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>inst✝ : Mono f<VAR>a b : X₁ ⊕ X₂<GOAL>Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G M : Type<VAR>inst✝² : Group G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulDistribMulAction G M<VAR>f : ↥(twoCoboundaries (Rep.ofMulDistribMulAction G M))<GOAL>IsMulTwoCoboundary (⇑Additive.toMul ∘ ↑↑f)
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G M : Type<VAR>inst✝² : Group G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulDistribMulAction G M<VAR>f : ↥(twoCoboundaries (Rep.ofMulDistribMulAction G M))<VAR>x : G → CoeSort.coe (Rep.ofMulDistribMulAction G M)<VAR>hx : (dOne (Rep.ofMulDistribMulAction G M)) x = (twoCocycles (Rep.ofMulDistribMulAction G M)).subtype ↑f<GOAL>IsMulTwoCoboundary (⇑Additive.toMul ∘ ↑↑f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPullback f.op g.op<GOAL>(pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd f.op g.op = (pushout.inr f g).op
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPullback f.op g.op<GOAL>((pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd f.op g.op).unop = (pushout.inr f g).op.unop
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : X ⟶ Y<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPullback f.op g.op<GOAL>(pullback.snd f.op g.op).unop ≫ (pushoutIsoUnopPullback f g).inv = pushout.inr f g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<GOAL>(mk₀ 0).hom = hom 0
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>head₁ : G i<VAR>tail₁ : Word G<VAR>fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i<VAR>normalized✝¹ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1<VAR>head₂ : G i<VAR>tail₂ : Word G<VAR>fstIdx_ne✝ : tail₂.fstIdx ≠ some i<VAR>normalized✝ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1<GOAL>rcons i { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹, normalized := normalized✝¹ } = rcons i { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝, normalized := normalized✝ } → { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹, normalized := normalized✝¹ } = { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝, normalized := normalized✝ }
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>head₁ : G i<VAR>tail₁ : Word G<VAR>fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i<VAR>normalized✝¹ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1<VAR>head₂ : G i<VAR>tail₂ : Word G<VAR>fstIdx_ne✝ : tail₂.fstIdx ≠ some i<VAR>normalized✝ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1<GOAL>↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2 → tail₁ = tail₂ → (⋯.equiv head₁).1 = (⋯.equiv head₂).1 → head₁ = head₂ ∧ tail₁ = tail₂
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>head₁ : G i<VAR>tail₁ : Word G<VAR>fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i<VAR>normalized✝¹ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1<VAR>head₂ : G i<VAR>h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2<VAR>h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1<VAR>fstIdx_ne✝ : tail₁.fstIdx ≠ some i<VAR>normalized✝ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₁, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1<GOAL>head₁ = head₂ ∧ tail₁ = tail₁
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>head₁ : G i<VAR>tail₁ : Word G<VAR>fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i<VAR>normalized✝¹ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1<VAR>head₂ : G i<VAR>h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2<VAR>h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1<VAR>fstIdx_ne✝ : tail₁.fstIdx ≠ some i<VAR>normalized✝ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₁, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1<GOAL>↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 = ↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 ∧ tail₁ = tail₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>s t : Set α<VAR>a b✝ : α<VAR>hs : IsAntichain r s<VAR>f : α → β<VAR>h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b<VAR>b : α<VAR>hb : b ∈ s<VAR>c : α<VAR>hc : c ∈ s<VAR>hbc : f b ≠ f c<VAR>hr : r' (f b) (f c)<GOAL>False
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>δ : ℝ<GOAL>closedBall x δ ⊆ cthickening δ {x}
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>δ : ℝ<VAR>hδ : δ < 0<GOAL>closedBall x δ ⊆ cthickening δ {x}
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>δ : ℝ<VAR>hδ : 0 ≤ δ<GOAL>closedBall x δ ⊆ cthickening δ {x}
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c✝ a b c d : α<GOAL>|max a b - max c d| ≤ max |a - c| |b - d|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c✝ a b c d : α<GOAL>max a b - max c d ≤ max |a - c| |b - d|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c✝ a b c d : α<GOAL>max c d - max a b ≤ max |a - c| |b - d|
<GOAL>-π < 0 ∧ 0 ≤ π
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>m : (s : α) → P s → ℝ≥0∞<VAR>s : α<VAR>h : P s<GOAL>m s h ≤ extend m s
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>m : (s : α) → P s → ℝ≥0∞<VAR>s : α<VAR>h : P s<GOAL>∀ (i : P s), m s h ≤ m s i
<VAR>x : ℂ<VAR>hx : 0 ≤ x.im<GOAL>(x ^ 2⁻¹).im = √((abs x - x.re) / 2)
<VAR>x : ℂ<VAR>hx : 0 ≤ x.im<GOAL>0 ≤ x.arg
<VAR>x : ℂ<VAR>hx : 0 ≤ x.im<GOAL>x.arg ≤ 2 * π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>h : (μ + ν) t ≠ ⊤<VAR>h' : s ⊆ t<VAR>h'' : (μ + ν) s = (μ + ν) t<GOAL>μ s = μ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>h : (μ + ν) t ≠ ⊤<VAR>h' : s ⊆ t<VAR>h'' : (μ + ν) s = (μ + ν) t<GOAL>μ t ≤ μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>h : (μ + ν) t ≠ ⊤<VAR>h' : s ⊆ t<VAR>h'' : (μ + ν) s = (μ + ν) t<VAR>this : μ t + ν t ≤ μ s + ν t<GOAL>μ t ≤ μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>h : (μ + ν) t ≠ ⊤<VAR>h' : s ⊆ t<VAR>h'' : (μ + ν) s = (μ + ν) t<VAR>this : μ t + ν t ≤ μ s + ν t<GOAL>ν t ≠ ⊤
<VAR>p : ℕ+<VAR>pp : p.Prime<GOAL>¬p ∣ 1
<VAR>p : ℕ+<VAR>pp : p.Prime<GOAL>¬↑p ∣ ↑1
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.24510, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>h : Octahedron comm h₁₂ h₂₃ h₁₃<GOAL>u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₃
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.24510, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>h : Octahedron comm h₁₂ h₂₃ h₁₃<GOAL>w₁₂ ≫ (shiftFunctor C 1).map (𝟙 X₁) = h.m₁ ≫ w₁₃
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → α<VAR>n : ℕ<GOAL>(∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ span ((fun i => f i ^ (n + 1)) '' ↑s)
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>n : ℕ<GOAL>p.fslope.coeff n = p.coeff (n + 1)
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>n : ℕ<GOAL>(p (n + 1)) (cons 1 1) = (p (n + 1)) 1
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>n : ℕ<GOAL>cons 1 1 = 1
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x z : M<VAR>f g : M → E'<VAR>f' g' : TangentSpace I z →L[𝕜] E'<VAR>hf : MDifferentiableAt I 𝓘(𝕜, E') (-f) z<GOAL>MDifferentiableAt I 𝓘(𝕜, E') f z
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x z : M<VAR>f g : M → E'<VAR>f' g' : TangentSpace I z →L[𝕜] E'<VAR>hf : MDifferentiableAt I 𝓘(𝕜, E') (-f) z<GOAL>f = - -f
<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>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<GOAL>∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
<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>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<VAR>val✝ : Fintype η<GOAL>∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
<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>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<VAR>val✝ : Fintype η<VAR>ι : Type<VAR>w✝ : Fintype ι<VAR>hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l<GOAL>∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l