ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hp : ∀ n' ≥ n, ¬p n'<VAR>this : setOf p ⊆ ↑(range n)<GOAL>nth p n = 0
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hp : ∀ n' ≥ n, ¬p n'<VAR>this : setOf p ⊆ ↑(range n)<GOAL>⋯.toFinset.card ≤ n
<VAR>n : ℕ<GOAL>fib (n + 2) = fib n + fib (n + 1)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Set E<VAR>hs : Absorbent 𝕜 s<VAR>h : ∀ x ∈ s, BddAbove (range fun x_1 => (p x_1) x)<GOAL>BddAbove (range p)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Set E<VAR>hs : Absorbent 𝕜 s<VAR>h : ∀ x ∈ s, BddAbove (range fun x_1 => (p x_1) x)<GOAL>∀ (x : E), BddAbove (range fun i => (p i) x)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Set E<VAR>hs : Absorbent 𝕜 s<VAR>h : ∀ x ∈ s, BddAbove (range fun x_1 => (p x_1) x)<VAR>x : E<GOAL>BddAbove (range fun i => (p i) x)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Set E<VAR>hs : Absorbent 𝕜 s<VAR>h : ∀ x ∈ s, BddAbove (range fun x_1 => (p x_1) x)<VAR>x : E<VAR>c : 𝕜<VAR>hc₀ : c ≠ 0<VAR>hc : c • x ∈ s<GOAL>BddAbove (range fun i => (p i) x)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Set E<VAR>hs : Absorbent 𝕜 s<VAR>h : ∀ x ∈ s, BddAbove (range fun x_1 => (p x_1) x)<VAR>x : E<VAR>c : 𝕜<VAR>hc₀ : c ≠ 0<VAR>hc : c • x ∈ s<VAR>M : ℝ<VAR>hM : M ∈ upperBounds (range fun x_1 => (p x_1) (c • x))<GOAL>BddAbove (range fun i => (p i) x)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι✝ : Type u_12<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>ι : Sort u_13<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Set E<VAR>hs : Absorbent 𝕜 s<VAR>h : ∀ x ∈ s, BddAbove (range fun x_1 => (p x_1) x)<VAR>x : E<VAR>c : 𝕜<VAR>hc₀ : c ≠ 0<VAR>hc : c • x ∈ s<VAR>M : ℝ<VAR>hM : M ∈ upperBounds (range fun x_1 => (p x_1) (c • x))<VAR>i : ι<GOAL>‖c‖ * (p i) x ≤ M
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c✝ u : αˣ<VAR>a c : α<VAR>h : a * ↑b⁻¹ = c<GOAL>a = c * ↑b
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c✝ u : αˣ<VAR>a c : α<VAR>h : a = c * ↑b<GOAL>a * ↑b⁻¹ = c
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝³ : CommRing R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>inst✝ : Fintype ι<GOAL>∑ i : ι, e.toMatrix v i j • e i = v j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Nontrivial α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>P : α → Prop<GOAL>(∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (succ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Nontrivial α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>P : α → Prop<VAR>h : ∀ (i : α), P (succ i)<VAR>i : α<VAR>hi : i ≠ ⊥<GOAL>P i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Nontrivial α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>P : α → Prop<VAR>h : ∀ (i : α), P (succ i)<VAR>j : ℕ<VAR>hi : Order.succ^[j] ⊥ ≠ ⊥<GOAL>P (Order.succ^[j] ⊥)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Nontrivial α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>P : α → Prop<VAR>h : ∀ (i : α), P (succ i)<VAR>j : ℕ<VAR>hi : Order.succ^[j] ⊥ ≠ ⊥<VAR>hj : 0 < j<GOAL>P (Order.succ^[j] ⊥)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Nontrivial α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>P : α → Prop<VAR>h : ∀ (i : α), P (succ i)<VAR>j : ℕ<VAR>hi : Order.succ^[j] ⊥ ≠ ⊥<VAR>hj : 0 < j<GOAL>P (Order.succ^[j.pred.succ] ⊥)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Nontrivial α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>P : α → Prop<VAR>h : ∀ (i : α), P (succ i)<VAR>j : ℕ<VAR>hi : Order.succ^[j] ⊥ ≠ ⊥<VAR>hj : 0 < j<GOAL>P (Order.succ (Order.succ^[j.pred] ⊥))
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>s' : Finset α<VAR>hs' : s' ⊆ s<VAR>t' : Finset α<VAR>ht' : t' ⊆ t<VAR>hs : ↑s.card * 1 ≤ ↑s'.card<VAR>ht : ↑t.card * 1 ≤ ↑t'.card<GOAL>|↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>s' : Finset α<VAR>hs' : s' ⊆ s<VAR>t' : Finset α<VAR>ht' : t' ⊆ t<VAR>hs : ↑s.card ≤ ↑s'.card<VAR>ht : ↑t.card ≤ ↑t'.card<GOAL>|↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>s' : Finset α<VAR>hs' : s' ⊆ s<VAR>t' : Finset α<VAR>ht' : t' ⊆ t<VAR>hs : ↑s.card ≤ ↑s'.card<VAR>ht : ↑t.card ≤ ↑t'.card<GOAL>0 < 1
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝³ : NonUnitalNonAssocSemiring R✝<VAR>M : Subsemigroup R✝<VAR>inst✝² : NonUnitalNonAssocSemiring S<VAR>inst✝¹ : NonUnitalNonAssocSemiring T<VAR>R : Type u_1<VAR>inst✝ : NonUnitalSemiring R<VAR>z : R<GOAL>z ∈ center R ↔ ∀ (g : R), g * z = z * g
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝³ : NonUnitalNonAssocSemiring R✝<VAR>M : Subsemigroup R✝<VAR>inst✝² : NonUnitalNonAssocSemiring S<VAR>inst✝¹ : NonUnitalNonAssocSemiring T<VAR>R : Type u_1<VAR>inst✝ : NonUnitalSemiring R<VAR>z : R<GOAL>z ∈ center R ↔ z ∈ Set.center R
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.dblZ P = 0
<VAR>a✝ b✝ : Cardinal.{u}<VAR>n m : ℕ<VAR>a x : Cardinal.{u_1}<VAR>b0 : x ≠ 0<VAR>b : Cardinal.{u_1}<VAR>hab : x = a * b<GOAL>a ≤ x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f✝ : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝ : Algebra R S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : RingHom.ker f ≤ I<VAR>hf₂ : f.IsIntegral<GOAL>map f I = ⊤ → I = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f✝ : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝ : Algebra R S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : RingHom.ker f ≤ I<VAR>hf₂ : f.IsIntegral<GOAL>¬I = ⊤ → ¬map f I = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f✝ : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝ : Algebra R S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : RingHom.ker f ≤ I<VAR>hf₂ : f.IsIntegral<VAR>h : ¬I = ⊤<GOAL>¬map f I = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f✝ : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝ : Algebra R S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : RingHom.ker f ≤ I<VAR>hf₂ : f.IsIntegral<VAR>h : ¬I = ⊤<VAR>m : Ideal R<VAR>left✝ : m.IsMaximal<VAR>hm : I ≤ m<GOAL>¬map f I = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f✝ : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝ : Algebra R S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : RingHom.ker f ≤ I<VAR>hf₂ : f.IsIntegral<VAR>h : ¬I = ⊤<VAR>m : Ideal R<VAR>left✝ : m.IsMaximal<VAR>hm : I ≤ m<VAR>x✝ : Algebra R S := f.toAlgebra<VAR>this : Algebra.IsIntegral R S<GOAL>¬map f I = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f✝ : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝ : Algebra R S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : RingHom.ker f ≤ I<VAR>hf₂ : f.IsIntegral<VAR>h : ¬I = ⊤<VAR>x✝ : Algebra R S := f.toAlgebra<VAR>this : Algebra.IsIntegral R S<VAR>m' : Ideal S<VAR>left✝¹ : m'.IsMaximal<VAR>left✝ : (comap (algebraMap R S) m').IsMaximal<VAR>hm : I ≤ comap (algebraMap R S) m'<GOAL>¬map f I = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>f✝ : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝ : Algebra R S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : RingHom.ker f ≤ I<VAR>hf₂ : f.IsIntegral<VAR>h : ¬I = ⊤<VAR>x✝ : Algebra R S := f.toAlgebra<VAR>this : Algebra.IsIntegral R S<VAR>m' : Ideal S<VAR>left✝¹ : m'.IsMaximal<VAR>left✝ : (comap (algebraMap R S) m').IsMaximal<VAR>hm : map (algebraMap R S) I ≤ m'<GOAL>¬map f I = ⊤
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>z : 𝕝<VAR>m : z ∈ {z | z ≠ 0}<GOAL>AnalyticAt 𝕜 (fun z => z⁻¹) z
<VAR>q a b c : ℚ<VAR>n d : ℤ<GOAL>↑n / ↑d = n /. d
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : (cocompact α).IsMeasurablyGenerated<VAR>hf : LocallyIntegrable f μ<VAR>ho : f =O[cocompact α] g<VAR>hg : IntegrableAtFilter g (cocompact α) μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : (cocompact α).IsMeasurablyGenerated<VAR>hf : LocallyIntegrable f μ<VAR>ho : f =O[cocompact α] g<VAR>hg : IntegrableAtFilter g (cocompact α) μ<GOAL>StronglyMeasurableAtFilter f (cocompact α) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g : α → E<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>hf : ∀ i ∈ s, Memℒp (f i) p μ<GOAL>Memℒp (∑ i ∈ s, f i) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g : α → E<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>hf : ∀ i ∈ s, Memℒp (f i) p μ<GOAL>∑ i ∈ s, f i = fun a => ∑ i ∈ s, f i a
<VAR>I : Type w₀<VAR>J✝ : Type w₁<VAR>C : I → Type u₁<VAR>inst✝ : (i : I) → Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>K : Type w₂<VAR>f : K → J<VAR>g : J → I<VAR>X Y : (i : I) → C i<VAR>f' : X ⟶ Y<GOAL>(({ obj := fun f i => f (g i), map := fun {X Y} α i => α (g i), map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i), map_id := ⋯, map_comp := ⋯ }).map f' ≫ fun b => 𝟙 (Y (g (f b)))) = (fun b => 𝟙 (X (g (f b)))) ≫ fun i => f' (g (f i))
<VAR>I : Type w₀<VAR>J✝ : Type w₁<VAR>C : I → Type u₁<VAR>inst✝ : (i : I) → Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>K : Type w₂<VAR>f : K → J<VAR>g : J → I<VAR>X Y : (i : I) → C i<VAR>f' : X ⟶ Y<VAR>x✝ : K<GOAL>(({ obj := fun f i => f (g i), map := fun {X Y} α i => α (g i), map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i), map_id := ⋯, map_comp := ⋯ }).map f' ≫ fun b => 𝟙 (Y (g (f b)))) x✝ = ((fun b => 𝟙 (X (g (f b)))) ≫ fun i => f' (g (f i))) x✝
<VAR>I : Type w₀<VAR>J✝ : Type w₁<VAR>C : I → Type u₁<VAR>inst✝ : (i : I) → Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>K : Type w₂<VAR>f : K → J<VAR>g : J → I<VAR>X Y : (i : I) → C i<VAR>f' : X ⟶ Y<GOAL>((fun i => f' (g (f i))) ≫ fun b => 𝟙 (Y (g (f b)))) = (fun b => 𝟙 (X (g (f b)))) ≫ ({ obj := fun f i => f (g i), map := fun {X Y} α i => α (g i), map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i), map_id := ⋯, map_comp := ⋯ }).map f'
<VAR>I : Type w₀<VAR>J✝ : Type w₁<VAR>C : I → Type u₁<VAR>inst✝ : (i : I) → Category.{v₁, u₁} (C i)<VAR>J : Type w₁<VAR>K : Type w₂<VAR>f : K → J<VAR>g : J → I<VAR>X Y : (i : I) → C i<VAR>f' : X ⟶ Y<VAR>x✝ : K<GOAL>((fun i => f' (g (f i))) ≫ fun b => 𝟙 (Y (g (f b)))) x✝ = ((fun b => 𝟙 (X (g (f b)))) ≫ ({ obj := fun f i => f (g i), map := fun {X Y} α i => α (g i), map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i), map_id := ⋯, map_comp := ⋯ }).map f') x✝
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.176514 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.181965 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>(pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ = pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>n : ℕ<VAR>ih : mk K p (n, 0) = 0<VAR>this : R K p (n, 0) (n + 1, (frobenius K p) 0)<GOAL>R K p (n, 0) (n + 1, 0)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : l₁ <+~ l₂<VAR>x : α<VAR>hx : count x l₁ < count x l₂<GOAL>x :: l₁ <+~ l₂
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂<VAR>x : α<VAR>hx : count x l₁ < count x l₂<GOAL>∀ (x_1 : α), x_1 ∈ x :: l₁ → count x_1 (x :: l₁) ≤ count x_1 l₂
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂<VAR>x : α<VAR>hx : count x l₁ < count x l₂<VAR>y : α<VAR>hy : y ∈ x :: l₁<GOAL>count y (x :: l₁) ≤ count y l₂
<VAR>ι✝ : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>x : ι → A<GOAL>∏ i ∈ s, span R {x i} = span R {∏ i ∈ s, x i}
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>x : E<GOAL>x ∈ closure {1} ↔ ‖x‖ = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹² : MeasurableSpace α<VAR>inst✝¹¹ : MeasurableSpace α'<VAR>inst✝¹⁰ : MeasurableSpace β<VAR>inst✝⁹ : MeasurableSpace β'<VAR>inst✝⁸ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : SFinite ν<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : SFinite μ<VAR>E' : Type u_7<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace ℝ E'<VAR>𝕜 : Type u_8<VAR>inst✝¹ : _root_.RCLike 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : β → E<VAR>hE : CompleteSpace E<VAR>h : ¬Integrable (fun z => f z.1 • g z.2) (μ.prod ν)<GOAL>∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹² : MeasurableSpace α<VAR>inst✝¹¹ : MeasurableSpace α'<VAR>inst✝¹⁰ : MeasurableSpace β<VAR>inst✝⁹ : MeasurableSpace β'<VAR>inst✝⁸ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : SFinite ν<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : SFinite μ<VAR>E' : Type u_7<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace ℝ E'<VAR>𝕜 : Type u_8<VAR>inst✝¹ : _root_.RCLike 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : β → E<VAR>hE : CompleteSpace E<VAR>h : ¬Integrable (fun z => f z.1 • g z.2) (μ.prod ν)<VAR>H : ¬Integrable f μ ∨ ¬Integrable g ν<GOAL>∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν
<VAR>a b c d : Ordinal.{u}<GOAL>a ⨳ b ≤ c ↔ ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'
<VAR>a b c d : Ordinal.{u}<GOAL>¬a ⨳ b ≤ c ↔ ¬∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>o.nfpBFamily f a ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>∀ (i : Ordinal.{u}) (j : i < o), o.nfpBFamily f a ∈ fixedPoints (f i j)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<GOAL>xInTermsOfW p R n * C (↑p ^ n) = X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : PolishSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : SecondCountableTopology Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>hsurj : Surjective f<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<GOAL>MeasurableSpace.map f (borel X) = borel Y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>a : α<GOAL>⇑e '' Iic a = Iic (e a)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : G ≤ G'<VAR>hF : Presieve.IsSheaf J F<VAR>hG' : Presieve.IsSheaf J G'.toPresheaf<VAR>U : Cᵒᵖ<VAR>x : F.obj U<VAR>hx : x ∈ (sheafify J G).obj U<GOAL>x ∈ G'.obj U
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : G ≤ G'<VAR>hF : Presieve.IsSheaf J F<VAR>hG' : Presieve.IsSheaf J G'.toPresheaf<VAR>U : Cᵒᵖ<VAR>x : F.obj U<VAR>hx : x ∈ (sheafify J G).obj U<GOAL>x = ↑((G.sheafifyLift (homOfLe h) hG').app U ⟨x, hx⟩)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : G ≤ G'<VAR>hF : Presieve.IsSheaf J F<VAR>hG' : Presieve.IsSheaf J G'.toPresheaf<VAR>U : Cᵒᵖ<VAR>x : F.obj U<VAR>hx : x ∈ (sheafify J G).obj U<GOAL>∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄, (G.sieveOfSection x).arrows f → F.map f.op x = F.map f.op ↑((G.sheafifyLift (homOfLe h) hG').app U ⟨x, hx⟩)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : G ≤ G'<VAR>hF : Presieve.IsSheaf J F<VAR>hG' : Presieve.IsSheaf J G'.toPresheaf<VAR>U : Cᵒᵖ<VAR>x : F.obj U<VAR>hx : x ∈ (sheafify J G).obj U<VAR>V : C<VAR>i : V ⟶ unop U<VAR>hi : (G.sieveOfSection x).arrows i<GOAL>F.map i.op x = F.map i.op ↑((G.sheafifyLift (homOfLe h) hG').app U ⟨x, hx⟩)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : G ≤ G'<VAR>hF : Presieve.IsSheaf J F<VAR>hG' : Presieve.IsSheaf J G'.toPresheaf<VAR>U : Cᵒᵖ<VAR>x : F.obj U<VAR>hx : x ∈ (sheafify J G).obj U<VAR>V : C<VAR>i : V ⟶ unop U<VAR>hi : (G.sieveOfSection x).arrows i<VAR>this : (fun f => ↑(f.app (op V) ⟨F.map i.op x, hi⟩)) (homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG') = (fun f => ↑(f.app (op V) ⟨F.map i.op x, hi⟩)) (homOfLe h)<GOAL>F.map i.op x = F.map i.op ↑((G.sheafifyLift (homOfLe h) hG').app U ⟨x, hx⟩)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : G ≤ G'<VAR>hF : Presieve.IsSheaf J F<VAR>hG' : Presieve.IsSheaf J G'.toPresheaf<VAR>U : Cᵒᵖ<VAR>x : F.obj U<VAR>hx : x ∈ (sheafify J G).obj U<VAR>V : C<VAR>i : V ⟶ unop U<VAR>hi : (G.sieveOfSection x).arrows i<VAR>this : (fun f => ↑(f.app (op V) ⟨F.map i.op x, hi⟩)) (homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG') = (fun f => ↑(f.app (op V) ⟨F.map i.op x, hi⟩)) (homOfLe h)<GOAL>F.map i.op ↑((G.sheafifyLift (homOfLe h) hG').app U ⟨x, hx⟩) = (fun f => ↑(f.app (op V) ⟨F.map i.op x, hi⟩)) (homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG')
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>h : G ≤ G'<VAR>hF : Presieve.IsSheaf J F<VAR>hG' : Presieve.IsSheaf J G'.toPresheaf<VAR>U : Cᵒᵖ<VAR>x : F.obj U<VAR>hx : x ∈ (sheafify J G).obj U<VAR>V : C<VAR>i : V ⟶ unop U<VAR>hi : (G.sieveOfSection x).arrows i<VAR>this : (fun f => ↑(f.app (op V) ⟨F.map i.op x, hi⟩)) (homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG') = (fun f => ↑(f.app (op V) ⟨F.map i.op x, hi⟩)) (homOfLe h)<GOAL>↑((G.sheafifyLift (homOfLe h) hG').app (op V) ((sheafify J G).toPresheaf.map i.op ⟨x, hx⟩)) = (fun f => ↑(f.app (op V) ⟨F.map i.op x, hi⟩)) (homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG')
<VAR>a✝ b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hdn : d ∣ n<VAR>a : ℕ<GOAL>a < n / d ↔ d * a < n
<VAR>a✝ b c m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a : ℕ<VAR>hdn : 0 ∣ n<GOAL>a < n / 0 ↔ 0 * a < n
<VAR>a✝ b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hdn : d ∣ n<VAR>a : ℕ<VAR>hd : d > 0<GOAL>a < n / d ↔ d * a < n
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E : Set α<VAR>hE : E.Finite<VAR>f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.Base B})<GOAL>{M | M.E ⊆ E}.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E : Set α<VAR>hE : E.Finite<VAR>f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.Base B})<VAR>hf : Function.Injective f<GOAL>{M | M.E ⊆ E}.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E : Set α<VAR>hE : E.Finite<VAR>f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.Base B})<VAR>hf : Function.Injective f<GOAL>(f '' {M | M.E ⊆ E}).Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E : Set α<VAR>hE : E.Finite<VAR>f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.Base B})<VAR>hf : Function.Injective f<GOAL>f '' {M | M.E ⊆ E} ⊆ {b | b ⊆ E} ×ˢ {b | b ⊆ {b | b ⊆ E}}
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>E : Set α<VAR>hE✝ : E.Finite<VAR>f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.Base B})<VAR>hf : Function.Injective f<VAR>M : Matroid α<VAR>hE : M.E ⊆ E<GOAL>f M ∈ {b | b ⊆ E} ×ˢ {b | b ⊆ {b | b ⊆ E}}
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>E : Set α<VAR>hE✝ : E.Finite<VAR>f : Matroid α → Set α × Set (Set α) := fun M => (M.E, {B | M.Base B})<VAR>hf : Function.Injective f<VAR>M : Matroid α<VAR>hE : M.E ⊆ E<GOAL>M.E ⊆ E ∧ ∀ (a : Set α), M.Base a → a ⊆ E
<VAR>x✝ y x : ℝ<GOAL>rexp x < 1 ↔ x < 0