ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>h : b ≤ a<VAR>c : Ordinal.{u_4}<VAR>e : a - b = succ c<GOAL>b + (a - b) ≤ 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>h : b ≤ a<VAR>l : (a - b).IsLimit<GOAL>b + (a - b) ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>fst✝ snd✝ : α<GOAL>Sym2.mk (fst✝, snd✝).swap = s(fst✝, snd✝)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<GOAL>p = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<GOAL>C (p.coeff p.natDegree) * X ^ p.natDegree + ∑ x ∈ range p.natDegree, C (p.coeff x) * X ^ x = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<GOAL>C (p.coeff p.natDegree) = 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : AddGroup N<VAR>f f₁ f₂ g g₁ g₂ : α →₀ N<GOAL>f.neLocus (f + g) = g.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ : Finset α<VAR>a✝ b : α<VAR>s : Finset α<VAR>a : α<GOAL>s ⊂ {a} ↔ s = ∅
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℕ<GOAL>p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>ha : a ≠ 0<GOAL>p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>h1 : (f ^ n).IsCycle<VAR>h2 : f.support ⊆ (f ^ n).support<GOAL>f.IsCycle
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>h1 : (f ^ n).IsCycle<VAR>h2 : f.support ⊆ (f ^ n).support<VAR>key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x<GOAL>f.IsCycle
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x✝ y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>h2 : f.support ⊆ (f ^ n).support<VAR>key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x<VAR>x : α<VAR>hx1 : (f ^ n) x ≠ x<VAR>hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y<GOAL>f.IsCycle
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x✝ y✝ : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>h2 : f.support ⊆ (f ^ n).support<VAR>key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x<VAR>x : α<VAR>hx1 : (f ^ n) x ≠ x<VAR>hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y<VAR>y : α<VAR>hy : f y ≠ y<GOAL>f.SameCycle x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x✝ y✝ : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>h2 : f.support ⊆ (f ^ n).support<VAR>key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x<VAR>x : α<VAR>hx1 : (f ^ n) x ≠ x<VAR>hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y<VAR>y : α<VAR>hy : f y ≠ y<VAR>i : ℤ<VAR>h✝ : ((f ^ n) ^ i) x = y<GOAL>f.SameCycle x y
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : MulPosStrictMono α<VAR>hb : 0 < b<VAR>h : a < 1<GOAL>a * b < b
<VAR>R : Type u_1<VAR>inst✝ : Monoid R<VAR>b : R<VAR>a : Rˣ<GOAL>IsRegular ↑a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f g : ℝ → E<VAR>x : ℝ<VAR>f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<VAR>y : ℝ<GOAL>HasDerivAt f (g y) y
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f g : ℝ → E<VAR>y : ℝ<VAR>f_diff : ∀ (y_1 : ℝ), y_1 ≠ y → HasDerivAt f (g y_1) y_1<VAR>hf : ContinuousAt f y<VAR>hg : ContinuousAt g y<GOAL>HasDerivAt f (g y) y
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f g : ℝ → E<VAR>x : ℝ<VAR>f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<VAR>y : ℝ<VAR>hne : y ≠ x<GOAL>HasDerivAt f (g y) y
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>IH : s.dedup.gcd = s.gcd<VAR>h : a ∈ s<GOAL>fold GCDMonoid.gcd 0 s = GCDMonoid.gcd a (fold GCDMonoid.gcd 0 s)
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>IH : s.dedup.gcd = s.gcd<VAR>h : a ∈ s<GOAL>GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (s.erase a)) = GCDMonoid.gcd (normalize a) (fold GCDMonoid.gcd 0 (s.erase a))
<VAR>l mr lm r : List Char<VAR>e : lm ++ r = { str := { data := l ++ mr }, startPos := { byteIdx := utf8ByteSize.go l }, stopPos := { byteIdx := utf8ByteSize.go lm } }.str.data<VAR>h : { str := { data := l ++ mr }, startPos := { byteIdx := utf8ByteSize.go l }, stopPos := { byteIdx := utf8ByteSize.go lm } }.startPos ≤ { str := { data := l ++ mr }, startPos := { byteIdx := utf8ByteSize.go l }, stopPos := { byteIdx := utf8ByteSize.go lm } }.stopPos<GOAL>∃ l_1 m r, ValidFor l_1 m r { str := { data := l ++ mr }, startPos := { byteIdx := utf8ByteSize.go l }, stopPos := { byteIdx := utf8ByteSize.go lm } }
<VAR>l mr lm r : List Char<VAR>e : lm ++ r = l ++ mr<VAR>h : utf8Len l ≤ utf8Len lm<GOAL>∃ l_1 m r, ValidFor l_1 m r { str := { data := l ++ mr }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len lm } }
<VAR>l mr lm r : List Char<VAR>e : lm ++ r = l ++ mr<VAR>h : utf8Len l ≤ utf8Len lm<VAR>this : ∃ c', lm = l ++ c' ∧ mr = c' ++ r<GOAL>∃ l_1 m r, ValidFor l_1 m r { str := { data := l ++ mr }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len lm } }
<VAR>l mr lm r : List Char<VAR>e : lm ++ r = l ++ mr<VAR>h✝ : utf8Len l ≤ utf8Len lm<VAR>h : ∃ a', l = lm ++ a' ∧ r = a' ++ mr<GOAL>∃ c', lm = l ++ c' ∧ mr = c' ++ r
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>h : z ∈ 𝒟ᵒ<GOAL>|2 * z.re| < 1
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>h : z ∈ 𝒟ᵒ<GOAL>|z.re| < 1 / 2
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>η : 𝟙 a ≅ f ≫ g<VAR>ε : g ≫ f ≅ 𝟙 b<VAR>h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv<GOAL>rightZigzag η.hom ε.hom = (ρ_ g).hom ≫ (λ_ g).inv
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>η : 𝟙 a ≅ f ≫ g<VAR>ε : g ≫ f ≅ 𝟙 b<VAR>h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv<GOAL>(rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom = (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>filter (fun x => i ≠ x) f = erase i f
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>filter (fun x => i ≠ x) f = filter (fun x => x ≠ i) f
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>f : Π₀ (i : ι), β i<VAR>i j : ι<GOAL>i ≠ j ↔ j ≠ i
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : I.IsMaximal<GOAL>∃ x, setOfIdeal I = {x}ᶜ
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : I.IsMaximal<VAR>h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal<GOAL>∃ x, setOfIdeal I = {x}ᶜ
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : I.IsMaximal<VAR>h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal<VAR>x : X<VAR>hx : opensOfIdeal I = (Closeds.singleton x).compl<GOAL>∃ x, setOfIdeal I = {x}ᶜ
<VAR>m n : ℕ+<GOAL>(m.lcm n).factorMultiset = m.factorMultiset ⊔ n.factorMultiset
<VAR>m n : ℕ+<GOAL>(m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset
<VAR>m n : ℕ+<GOAL>m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>ContinuousOn (↑(f.extend I)) (f.extend I).source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>ContinuousOn (↑(f.symm.restr I.source).symm) (f.extend I).source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>ContinuousOn (↑(f.symm.restr I.source).symm) f.source
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a b : ℝ<GOAL>volume (Ioo a b) = ofReal (b - a)
<VAR>m n : ℕ<VAR>f : Vector ℕ m → Vector ℕ n<VAR>h : Vec f<GOAL>Computable f
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>C : CoprodI M → Prop<VAR>m : CoprodI M<VAR>h_one : C 1<VAR>h_of : ∀ (i : ι) (m : M i), C (of m)<VAR>h_mul : ∀ (x y : CoprodI M), C x → C y → C (x * y)<GOAL>C m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<VAR>h : (x :: xs).Nodup<GOAL>(map (fun p => x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<VAR>h : (x :: xs).Nodup<GOAL>Function.Injective fun p => x ::ₛ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<VAR>h : (x :: xs).Nodup<GOAL>(map (fun p => x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<GOAL>x ∈ support (deriv f) → x ∈ tsupport f
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<GOAL>x ∉ tsupport f → x ∉ support (deriv f)
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>h2x : x ∉ tsupport f<GOAL>x ∉ support (deriv f)
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>h2x : f =ᶠ[nhds x] 0<GOAL>x ∉ support (deriv f)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>K : Type u_6<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>N₁ : Type u_12<VAR>N₂ : Type u_13<VAR>N₃ : Type u_14<VAR>N₄ : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>e : M ≃ₗ[R] M₂<VAR>x✝ : M₂<GOAL>(e.conj LinearMap.id) x✝ = LinearMap.id x✝
<VAR>n : ℕ<VAR>h : IsUnit ↑n<GOAL>n = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>ι : Sort u_3<VAR>inst✝ : Finite ι<VAR>N : ι → Submodule R M<VAR>h : ∀ (i : ι), (N i).FG<GOAL>(iSup N).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>ι : Sort u_3<VAR>inst✝ : Finite ι<VAR>N : ι → Submodule R M<VAR>h : ∀ (i : ι), (N i).FG<VAR>val✝ : Fintype (PLift ι)<GOAL>(iSup N).FG
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<GOAL>-a = -a + 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<GOAL>-a + 0 = -a + -a + a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<GOAL>-a + -a + a = a
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G H I : C ⥤ D<VAR>α β : 𝟭 C ⟶ 𝟭 C<VAR>X : C<GOAL>(α ≫ β).app X = (β ≫ α).app X
<VAR>α : Type u_1<VAR>m : Set (OuterMeasure α)<VAR>h : m.Nonempty<VAR>t : Set α<GOAL>⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t
<VAR>α : Type u_1<VAR>m : Set (OuterMeasure α)<VAR>h : m.Nonempty<GOAL>⨆ (_ : ∅.Nonempty), sInfGen m ∅ = ⨅ μ ∈ m, μ ∅
<VAR>α : Type u_1<VAR>m : Set (OuterMeasure α)<VAR>h : m.Nonempty<VAR>t : Set α<VAR>ht : t.Nonempty<GOAL>⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t
<VAR>G : Type u_1<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : CompleteSpace G<VAR>H : Type u_2<VAR>inst✝¹ : NormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>j : NormedAddGroupHom K H<VAR>hj : ∀ (x : K), ‖j x‖ = ‖x‖<VAR>C ε : ℝ<VAR>hC : 0 < C<VAR>hε : 0 < ε<VAR>hyp : ∀ (k : K), ∃ g, f g = j k ∧ ‖g‖ ≤ C * ‖k‖<GOAL>f.SurjectiveOnWith j.range.topologicalClosure (C + ε)
<VAR>G : Type u_1<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : CompleteSpace G<VAR>H : Type u_2<VAR>inst✝¹ : NormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>j : NormedAddGroupHom K H<VAR>hj : ∀ (x : K), ‖j x‖ = ‖x‖<VAR>C ε : ℝ<VAR>hC : 0 < C<VAR>hε : 0 < ε<VAR>hyp : ∀ h ∈ j.range, ∃ g, f g = h ∧ ‖g‖ ≤ C * ‖h‖<GOAL>f.SurjectiveOnWith j.range.topologicalClosure (C + ε)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N✝ : ℕ<VAR>τ✝ : ℝ<VAR>a✝ : SatelliteConfig E N✝ τ✝<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<GOAL>a.centerAndRescale.r (last N) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* α ≃o α<VAR>h : α → α<VAR>H : ∀ (x : α), IsLUB (range fun g' => (f₁ g')⁻¹ ((f₂ g') x)) (h x)<VAR>g : G<GOAL>Semiconj h ⇑(f₂ g) ⇑(f₁ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* α ≃o α<VAR>h : α → α<VAR>H : ∀ (x : α), IsLUB (range fun g' => (f₁ g')⁻¹ ((f₂ g') x)) (h x)<VAR>g : G<VAR>y : α<GOAL>IsLUB (range fun g' => (f₁ g')⁻¹ ((f₂ g') ((f₂ g) y))) ((f₁ g) (h y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* α ≃o α<VAR>h : α → α<VAR>H : ∀ (x : α), IsLUB (range fun g' => (f₁ g')⁻¹ ((f₂ g') x)) (h x)<VAR>g : G<VAR>y : α<VAR>this : IsLUB (⇑(f₁ g) '' range fun g' => (f₁ g')⁻¹ ((f₂ g') y)) ((f₁ g) (h y))<GOAL>IsLUB (range fun g' => (f₁ g')⁻¹ ((f₂ g') ((f₂ g) y))) ((f₁ g) (h y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Group G<VAR>f₁ f₂ : G →* α ≃o α<VAR>h : α → α<VAR>H : ∀ (x : α), IsLUB (range fun g' => (f₁ g')⁻¹ ((f₂ g') x)) (h x)<VAR>g : G<VAR>y : α<VAR>this : IsLUB (range ((⇑(f₁ g) ∘ fun g' => (f₁ g')⁻¹ ((f₂ g') y)) ∘ ⇑(Equiv.mulRight g))) ((f₁ g) (h y))<GOAL>IsLUB (range fun g' => (f₁ g')⁻¹ ((f₂ g') ((f₂ g) y))) ((f₁ g) (h y))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.123089, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain F K m<VAR>β : Cochain G K n<VAR>h : m + 1 = n<VAR>p₁ p₂ : ℤ<VAR>h₁₂ : p₁ + n = p₂<GOAL>(inr φ).f p₁ ≫ (descCochain φ α β h).v p₁ p₂ h₁₂ = β.v p₁ p₂ h₁₂
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C✝ : Type u<VAR>inst✝⁴ : Category.{v, u} C✝<VAR>D : Type u''<VAR>inst✝³ : Category.{v'', u''} D<VAR>X Y : C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasPullbacksOfInclusions C<VAR>T : C<VAR>HT : IsTerminal T<VAR>c₀ : BinaryCofan T T<VAR>hc₀ : IsColimit c₀<GOAL>FinitaryExtensive C ↔ IsVanKampenColimit c₀
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C✝ : Type u<VAR>inst✝⁴ : Category.{v, u} C✝<VAR>D : Type u''<VAR>inst✝³ : Category.{v'', u''} D<VAR>X Y : C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasPullbacksOfInclusions C<VAR>T : C<VAR>HT : IsTerminal T<VAR>c₀ : BinaryCofan T T<VAR>hc₀ : IsColimit c₀<VAR>H : IsVanKampenColimit c₀<GOAL>FinitaryExtensive C
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C✝ : Type u<VAR>inst✝⁴ : Category.{v, u} C✝<VAR>D : Type u''<VAR>inst✝³ : Category.{v'', u''} D<VAR>X Y : C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasPullbacksOfInclusions C<VAR>T : C<VAR>HT : IsTerminal T<VAR>c₀ : BinaryCofan T T<VAR>hc₀ : IsColimit c₀<VAR>H : IsVanKampenColimit c₀<GOAL>∀ {X Y : C} (c : BinaryCofan X Y), IsColimit c → IsVanKampenColimit c
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C✝ : Type u<VAR>inst✝⁴ : Category.{v, u} C✝<VAR>D : Type u''<VAR>inst✝³ : Category.{v'', u''} D<VAR>X Y : C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasPullbacksOfInclusions C<VAR>T : C<VAR>HT : IsTerminal T<VAR>c₀ : BinaryCofan T T<VAR>hc₀ : IsColimit c₀<VAR>H : ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt), αX ≫ c₀.inl = c'.inl ≫ f → αY ≫ c₀.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)<GOAL>∀ {X Y : C} (c : BinaryCofan X Y), IsColimit c → ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt), αX ≫ c.inl = c'.inl ≫ f → αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C✝ : Type u<VAR>inst✝⁴ : Category.{v, u} C✝<VAR>D : Type u''<VAR>inst✝³ : Category.{v'', u''} D<VAR>X✝ Y✝ : C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasPullbacksOfInclusions C<VAR>T : C<VAR>HT : IsTerminal T<VAR>c₀ : BinaryCofan T T<VAR>hc₀ : IsColimit c₀<VAR>H : ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt), αX ≫ c₀.inl = c'.inl ≫ f → αY ≫ c₀.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<VAR>X' Y' : C<VAR>c' : BinaryCofan X' Y'<VAR>αX : X' ⟶ X<VAR>αY : Y' ⟶ Y<VAR>f : c'.pt ⟶ c.pt<VAR>hX : αX ≫ c.inl = c'.inl ≫ f<VAR>hY : αY ≫ c.inr = c'.inr ≫ f<VAR>d : c.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c₀.pt).obj { as := WalkingPair.left }<VAR>hd : c.inl ≫ d = HT.from X ≫ c₀.inl<VAR>hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr<GOAL>Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C✝ : Type u<VAR>inst✝⁴ : Category.{v, u} C✝<VAR>D : Type u''<VAR>inst✝³ : Category.{v'', u''} D<VAR>X✝ Y✝ : C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasPullbacksOfInclusions C<VAR>T : C<VAR>HT : IsTerminal T<VAR>c₀ : BinaryCofan T T<VAR>hc₀ : IsColimit c₀<VAR>H : ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt), αX ≫ c₀.inl = c'.inl ≫ f → αY ≫ c₀.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<VAR>X' Y' : C<VAR>c' : BinaryCofan X' Y'<VAR>αX : X' ⟶ X<VAR>αY : Y' ⟶ Y<VAR>f : c'.pt ⟶ c.pt<VAR>hX : αX ≫ c.inl = c'.inl ≫ f<VAR>hY : αY ≫ c.inr = c'.inr ≫ f<VAR>d : c.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c₀.pt).obj { as := WalkingPair.left }<VAR>hd : c.inl ≫ d = HT.from X ≫ c₀.inl<VAR>hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr<GOAL>IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C✝ : Type u<VAR>inst✝⁴ : Category.{v, u} C✝<VAR>D : Type u''<VAR>inst✝³ : Category.{v'', u''} D<VAR>X✝ Y✝ : C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasPullbacksOfInclusions C<VAR>T : C<VAR>HT : IsTerminal T<VAR>c₀ : BinaryCofan T T<VAR>hc₀ : IsColimit c₀<VAR>H : ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt), αX ≫ c₀.inl = c'.inl ≫ f → αY ≫ c₀.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<VAR>X' Y' : C<VAR>c' : BinaryCofan X' Y'<VAR>αX : X' ⟶ X<VAR>αY : Y' ⟶ Y<VAR>f : c'.pt ⟶ c.pt<VAR>hX : αX ≫ c.inl = c'.inl ≫ f<VAR>hY : αY ≫ c.inr = c'.inr ≫ f<VAR>d : c.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c₀.pt).obj { as := WalkingPair.left }<VAR>hd : c.inl ≫ d = HT.from X ≫ c₀.inl<VAR>hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr<VAR>hl : IsPullback c.inl (HT.from X) d c₀.inl<VAR>hr : IsPullback c.inr (HT.from Y) d c₀.inr<GOAL>IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
<VAR>n✝ m n : ℕ<VAR>a b : Fin n<VAR>h : a ≤ b<GOAL>∃ k ≤ b, b = a + k
<VAR>n✝ m n : ℕ<VAR>a b : Fin n<VAR>h : a ≤ b<VAR>k : ℕ<VAR>hk : ↑b = ↑a + k<GOAL>∃ k ≤ b, b = a + k
<VAR>n✝ m n : ℕ<VAR>a b : Fin n<VAR>h : a ≤ b<VAR>k : ℕ<VAR>hk : ↑b = ↑a + k<VAR>hkb : k ≤ ↑b<GOAL>∃ k ≤ b, b = a + k
<VAR>n✝ m n : ℕ<VAR>a b : Fin n<VAR>h : a ≤ b<VAR>k : ℕ<VAR>hk : ↑b = ↑a + k<VAR>hkb : k ≤ ↑b<GOAL>b = a + ⟨k, ⋯⟩
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set (OnePoint X)<VAR>t s : Set X<GOAL>IsOpen (some '' s) ↔ IsOpen s
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condexpKernel μ m) ω) μ