ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>IH : ∀ m < n, 0 < m → (bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0<VAR>hn : 0 < n<GOAL>(1 - ∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>IH : ∀ m < n, 0 < m → (bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0<VAR>hn : 0 < n<GOAL>C ⅟↑p ^ n - (∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>IH : ∀ m < n, 0 < m → (bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0<VAR>hn : 0 < n<GOAL>C ⅟↑p ^ n - C ↑p ^ 0 * (bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) * C ⅟↑p ^ n = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>IH : ∀ m < n, 0 < m → (bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0<VAR>hn : 0 < n<GOAL>∀ b ∈ Finset.range n, b ≠ 0 → C ↑p ^ b * (bind₁ fun k => 1) (xInTermsOfW p ℚ b) ^ p ^ (n - b) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>IH : ∀ m < n, 0 < m → (bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0<VAR>hn : 0 < n<GOAL>0 ∉ Finset.range n → C ↑p ^ 0 * (bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>h : Function.Surjective ⇑(algebraMap R S)<GOAL>Subsingleton (Ω[S⁄R])
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>h : Function.Surjective ⇑(algebraMap R S)<GOAL>⊤ ≤ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>h : Function.Surjective ⇑(algebraMap R S)<GOAL>Set.range ⇑(D R S) ⊆ ↑⊥
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<GOAL>Continuous convexBodySumFun
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>w : InfinitePlace K<GOAL>w ∈ Finset.univ → Continuous fun a => ↑w.mult * (normAtPlace w) a
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>w : InfinitePlace K<VAR>hw : w.IsReal<GOAL>w ∈ Finset.univ → Continuous fun a => ↑w.mult * (normAtPlace w) a
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>w : InfinitePlace K<VAR>hw : w.IsComplex<GOAL>w ∈ Finset.univ → Continuous fun a => ↑w.mult * (normAtPlace w) a
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal<VAR>f : C(X, ℝ≥0)<GOAL>φ f = ψ f
<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>a b : ℕ<GOAL>↑(a.descFactorial b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer S b)
<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>a b : ℕ<GOAL>↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
<VAR>S : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasShift C S<VAR>inst✝ : (shiftFunctor C 1).PreservesZeroMorphisms<VAR>X Y : DifferentialObject S C<VAR>f : X ≅ Y<GOAL>f.hom.f ≫ f.inv.f = 𝟙 X.obj
<VAR>S : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasShift C S<VAR>inst✝ : (shiftFunctor C 1).PreservesZeroMorphisms<VAR>X Y : DifferentialObject S C<VAR>f : X ≅ Y<GOAL>f.inv.f ≫ f.hom.f = 𝟙 Y.obj
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι'✝ : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι'✝ → Prop<VAR>s' : ι'✝ → Set α<VAR>i' : ι'✝<VAR>ι : Sort u_6<VAR>ι' : ι → Type u_7<VAR>l : ι → Filter α<VAR>p : (i : ι) → ι' i → Prop<VAR>s : (i : ι) → ι' i → Set α<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<VAR>t : Set α<GOAL>t ∈ ⨆ i, l i ↔ ∃ i, (∀ (i_1 : ι), p i_1 (i i_1)) ∧ ⋃ i_1, s i_1 (i i_1) ⊆ t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>σ : Type u_4<VAR>inst✝¹ : Mul M<VAR>inst✝ : Mul N<VAR>f : M →ₙ* N<VAR>S : Subsemigroup N<VAR>h : S ≤ f.srange<GOAL>map f (comap f S) = S
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝¹ : Mul M<VAR>inst✝ : Mul N<VAR>f : M →ₙ* N<VAR>hf : ∀ (x y : M), Commute (f x) (f y)<VAR>x y : M<GOAL>(op ∘ ⇑f) (x * y) = (op ∘ ⇑f) x * (op ∘ ⇑f) y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<GOAL>AntitoneOn (dist x) (Iic x)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a : Ordinal.{max u v}<VAR>ha : ∀ (i : ι), f i a ≤ a<GOAL>∃ o, derivFamily f o = a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a : Ordinal.{max u v}<VAR>ha : ∀ (i : ι), f i a ≤ a<GOAL>∀ (o : Ordinal.{max u v}), a ≤ derivFamily f o → ∃ o, derivFamily f o = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y✝ : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n<VAR>hg0 : Summable fun n => g n y₀<VAR>y : 𝕜<GOAL>HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : HasZeroMorphisms V<VAR>α : Type u_2<VAR>inst✝² : AddRightCancelSemigroup α<VAR>inst✝¹ : One α<VAR>inst✝ : DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X n ⟶ X (n + 1)<VAR>sq : ∀ (n : α), d n ≫ d (n + 1) = 0<VAR>j : α<GOAL>(if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<GOAL>adjoint (id 𝕜 E) = id 𝕜 E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<GOAL>id 𝕜 E = adjoint (id 𝕜 E)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<GOAL>∀ (x y : E), ⟪(id 𝕜 E) x, y⟫_𝕜 = ⟪x, (id 𝕜 E) y⟫_𝕜
<VAR>xl xr : Type u<VAR>x x' : PGame<GOAL>x ≤ x.insertLeft x'
<VAR>xl xr : Type u<VAR>x x' : PGame<GOAL>(∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ (x.insertLeft x').moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ x.insertLeft x') ∧ ∀ (j : (x.insertLeft x').RightMoves), (∃ i, x ≤ ((x.insertLeft x').moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ (x.insertLeft x').moveRight j
<VAR>α : Type u_1<VAR>n : ℤ<GOAL>n.sign = ↑(SignType.sign n)
<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 : M<VAR>p : TangentBundle I M<VAR>hs : UniqueMDiffWithinAt I s p.proj<GOAL>{ proj := p.proj, snd := (mfderivWithin I I id s p.proj) p.snd } = p
<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 : M<VAR>p : TangentBundle I M<VAR>hs : UniqueMDiffWithinAt I s p.proj<GOAL>{ proj := p.proj, snd := (ContinuousLinearMap.id 𝕜 (TangentSpace I p.proj)) p.snd } = p
<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 : M<VAR>p : TangentBundle I M<VAR>hs : UniqueMDiffWithinAt I s p.proj<GOAL>UniqueMDiffWithinAt I s p.proj
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<VAR>h : c < ℵ₀<GOAL>∃ n, c = ↑n
<VAR>α β : Type u<VAR>c : Cardinal.{0}<VAR>h' : c < #ℕ<VAR>h : lift.{u_1, 0} c < ℵ₀<GOAL>∃ n, lift.{u_1, 0} c = ↑n
<VAR>α β : Type u<VAR>S : Set ℕ<VAR>h' : #↑S < #ℕ<VAR>h : lift.{u_1, 0} #↑S < ℵ₀<GOAL>∃ n, lift.{u_1, 0} #↑S = ↑n
<VAR>α β : Type u<VAR>S : Set ℕ<VAR>h' : #↑S < #ℕ<VAR>h : lift.{u_1, 0} #↑S < ℵ₀<GOAL>S.Finite
<VAR>α β : Type u<VAR>S : Set ℕ<VAR>h : lift.{u_1, 0} #↑S < ℵ₀<VAR>h' : ¬S.Finite<GOAL>#ℕ ≤ #↑S
<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>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f' : α → γ → δ'<VAR>g' : δ' → β → ε<VAR>h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b<GOAL>image2 f (image2 g s t) u = image2 g' (image2 f' s u) t
<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>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f' : α → γ → δ'<VAR>g' : δ' → β → ε<VAR>h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b<GOAL>image2 f (image2 (fun a b => g b a) t s) u = image2 (fun a b => g' b a) t (image2 f' s u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>s : β → β → Prop<VAR>a : α<VAR>h : ¬r a a<GOAL>∀ {a_1 b : β}, Prod.Lex r s ({ toFun := Prod.mk a, inj' := ⋯ } a_1) ({ toFun := Prod.mk a, inj' := ⋯ } b) ↔ s a_1 b
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>κ : Type u_6<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : DecidableEq M<VAR>s : Finset M<VAR>b : Basis { x // x ∈ s } A M<VAR>f : M →ₗ[A] M<VAR>this : ∃ s, Nonempty (Basis { x // x ∈ s } A M)<GOAL>LinearMap.det f = ((toMatrix b b) f).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f g : Filter α<VAR>s : Set α<GOAL>IsBounded r (𝓟 s) ↔ ∃ t, ∀ x ∈ s, r x t
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₁ : ∀ (l : ι), ¬c.Rel l k₁<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₁ : ∀ (l : ι), ¬c.Rel l k₁<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x => 0) = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a✝ a₁ a₂ : α<VAR>b : β<VAR>inst✝ : DecidablePred fun x => x = b<VAR>a : α<GOAL>(∏' (b' : β), if b' = b then a else 1) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a✝ a₁ a₂ : α<VAR>b : β<VAR>inst✝ : DecidablePred fun x => x = b<VAR>a : α<GOAL>(if b = b then a else 1) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a✝ a₁ a₂ : α<VAR>b : β<VAR>inst✝ : DecidablePred fun x => x = b<VAR>a : α<GOAL>∀ (b' : β), b' ≠ b → (if b' = b then a else 1) = 1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : lift.{v, u} o.card < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord<VAR>a : Ordinal.{max u v}<GOAL>lift.{v, u} #(Quotient.out o).α < c
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>motive : (u v : V) → G.Walk u v → Sort u_1<VAR>Hnil : {u : V} → motive u u nil<VAR>Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>⋯ ▸ concatRecAux Hnil Hconcat (p.concat h).reverse = Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>motive : (u v : V) → G.Walk u v → Sort u_1<VAR>Hnil : {u : V} → motive u u nil<VAR>Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>HEq (⋯ ▸ concatRecAux Hnil Hconcat (p.concat h).reverse) (Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse))
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>motive : (u v : V) → G.Walk u v → Sort u_1<VAR>Hnil : {u : V} → motive u u nil<VAR>Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>HEq (concatRecAux Hnil Hconcat (p.concat h).reverse) (Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse))
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>motive : (u v : V) → G.Walk u v → Sort u_1<VAR>Hnil : {u : V} → motive u u nil<VAR>Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>HEq (concatRecAux Hnil Hconcat (p.concat h).reverse) (concatRecAux Hnil Hconcat (cons ⋯ p.reverse))
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>motive : (u v : V) → G.Walk u v → Sort u_1<VAR>Hnil : {u : V} → motive u u nil<VAR>Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)<VAR>u v w : V<VAR>p : G.Walk u v<VAR>h : G.Adj v w<GOAL>HEq (concatRecAux Hnil Hconcat (cons ⋯ p.reverse)) (Hconcat p h (⋯ ▸ concatRecAux Hnil Hconcat p.reverse))
<VAR>α : Type u_1<VAR>G✝ : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>S : Set G<VAR>x : G<GOAL>x ∈ closure S⁻¹ ↔ x⁻¹ ∈ closure S
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<GOAL>↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>q : Associates N<VAR>hq : q ∈ normalizedFactors n<VAR>hq' : Associated (↑(d ⟨p, ⋯⟩)) q<GOAL>↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>q : Associates N<VAR>hq : q ∈ normalizedFactors n<VAR>hq' : ↑(d ⟨p, ⋯⟩) = q<GOAL>↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n
<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>X : TopCat<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : ConcreteCategory C<VAR>F : Presheaf C X<VAR>U V W : Opens ↑X<VAR>e₁ : U ≤ V<VAR>e₂ : V ≤ W<VAR>x : (forget C).obj (F.obj (op W))<GOAL>(F.map (homOfLE e₁).op) ((F.map (homOfLE e₂).op) x) = (F.map (homOfLE ⋯).op) x
<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>X : TopCat<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : ConcreteCategory C<VAR>F : Presheaf C X<VAR>U V W : Opens ↑X<VAR>e₁ : U ≤ V<VAR>e₂ : V ≤ W<VAR>x : (forget C).obj (F.obj (op W))<GOAL>(F.map ((homOfLE e₂).op ≫ (homOfLE e₁).op)) x = (F.map (homOfLE ⋯).op) x
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>f : F<GOAL>∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>f : F<VAR>K : Set α<VAR>hK₁ : IsCompact K<VAR>hK₂ : Kᶜ ⊆ ⇑f ⁻¹' closedBall 0 1<GOAL>∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>f : F<VAR>K : Set α<VAR>hK₁ : IsCompact K<VAR>hK₂ : Kᶜ ⊆ ⇑f ⁻¹' closedBall 0 1<VAR>C : ℝ<VAR>hC : ⇑f '' K ⊆ closedBall 0 C<GOAL>∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>f : F<VAR>K : Set α<VAR>hK₁ : IsCompact K<VAR>hK₂ : Kᶜ ⊆ ⇑f ⁻¹' closedBall 0 1<VAR>C : ℝ<VAR>hC : ⇑f '' K ⊆ closedBall 0 C<VAR>x y : α<VAR>this : ∀ (x : α), f x ∈ closedBall 0 (max C 1)<GOAL>dist (f x) (f y) ≤ max C 1 + max C 1
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex (update x i a) < toLex x ↔ a < x i
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex (update x i a) < toLex x → a < x i
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i : ι<VAR>a : β i<VAR>j : ι<VAR>hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → toLex (update x i a) j_1 = toLex x j_1<VAR>h : update x i a j < x j<GOAL>a < x i
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>j : ι<VAR>a : β j<VAR>hj : ∀ (j_1 : ι), (fun x x_1 => x < x_1) j_1 j → toLex (update x j a) j_1 = toLex x j_1<VAR>h : update x j a j < x j<GOAL>a < x j
<VAR>a b c d : Ordinal.{u}<GOAL>a ⨳ b ⨳ c ≤ d ↔ ∀ a' < a, ∀ b' < b, ∀ c' < c, a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
<VAR>a b c d : Ordinal.{u}<GOAL>¬a ⨳ b ⨳ c ≤ d ↔ ¬∀ a' < a, ∀ b' < b, ∀ c' < c, a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>inst✝ : One γ<VAR>c : α<VAR>f : β → γ<VAR>x : β<GOAL>(x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f