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>G : Type u_5<VAR>inst✝⁷ : Ring 𝕜<VAR>inst✝⁶ : Ring 𝕜₂<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : SeminormedAddCommGroup F<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜₂ F<VAR>σ : 𝕜 →+* 𝕜₂<VAR>f✝ : E →ₛₗ[σ] F<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>inst✝¹ : RingHomInvPair σ σ₂₁<VAR>inst✝ : RingHomInvPair σ₂₁ σ<VAR>a : ℝ<VAR>ha : 0 < a<VAR>f : E ≃ₛₗ[σ] F<VAR>hf : ∀ (x : E), ‖f x‖ = a * ‖x‖<VAR>y : F<GOAL>‖f.symm y‖ = a⁻¹ * ‖y‖
<VAR>α : Type u_1<VAR>s t : Multiset α<VAR>a : α<VAR>h : s ⋖ t<GOAL>card s ⋖ card t
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a✝ a : α<VAR>h : s ⋖ a ::ₘ s<GOAL>card s ⋖ card (a ::ₘ s)
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a✝ a : α<VAR>h : s ⋖ a ::ₘ s<GOAL>card s ⋖ card s + 1
<VAR>α : Type u_1<VAR>f : Perm α<VAR>n : ℤ<VAR>x : α<GOAL>f ((f ^ n) x) = (f ^ n) x ↔ f x = x
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : CancelMonoidWithZero M₀<VAR>a b c : M₀<GOAL>a * b = a * c ↔ b = c ∨ a = 0
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>inst✝ : DecidableEq K<VAR>hn : ¬n = 0<GOAL>primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>inst✝ : DecidableEq K<VAR>hn : ¬n = 0<VAR>hpos : 0 < n<GOAL>primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>inst✝ : DecidableEq K<VAR>hn : ¬n = 0<VAR>hpos : 0 < n<VAR>x : K<VAR>hx : x ∈ primitiveRoots n K<GOAL>x ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>inst✝ : DecidableEq K<VAR>hn : ¬n = 0<VAR>hpos : 0 < n<VAR>m : ℕ<VAR>left✝ : m < n<VAR>hcop : m.Coprime n<VAR>hx : μ ^ m ∈ primitiveRoots n K<GOAL>μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>inst✝ : DecidableEq K<VAR>hn : ¬n = 0<VAR>hpos : 0 < n<VAR>m : ℕ<VAR>left✝ : m < n<VAR>hcop : m.Coprime n<VAR>hx : μ ^ m ∈ primitiveRoots n K<GOAL>μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>inst✝ : DecidableEq K<VAR>hn : ¬n = 0<VAR>hpos : 0 < n<VAR>m : ℕ<VAR>left✝ : m < n<VAR>hcop : m.Coprime n<VAR>hx : μ ^ m ∈ primitiveRoots n K<GOAL>μ ^ m ∈ (map (Int.castRingHom K) (minpoly ℤ μ)).roots ↔ (map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>inst✝ : DecidableEq K<VAR>hn : ¬n = 0<VAR>hpos : 0 < n<VAR>m : ℕ<VAR>left✝ : m < n<VAR>hcop : m.Coprime n<VAR>hx : μ ^ m ∈ primitiveRoots n K<GOAL>map (Int.castRingHom K) (minpoly ℤ μ) ≠ 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>hN : ¬N = 0<GOAL>upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>hN : ¬N = 0<GOAL>upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ, {n | upperCrossingTime a b f N n ω < N}.indicator 1 i + ∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ, {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>hN : ¬N = 0<VAR>h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1<GOAL>upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ, {n | upperCrossingTime a b f N n ω < N}.indicator 1 i + ∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ, {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>hN : ¬N = 0<VAR>h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1<VAR>h₂ : ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0<GOAL>upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ, {n | upperCrossingTime a b f N n ω < N}.indicator 1 i + ∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ, {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>s : Set ℝ<VAR>f f' : ℝ → ℝ<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>g : ℝ → F<GOAL>∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, |f' x| • g (f x)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : ↥s<GOAL>↑((orthogonalProjection s) ↑p) = ↑p
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : ↥s<GOAL>↑p ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>s : Set α<VAR>x : α<VAR>inst✝² : Group H<VAR>inst✝¹ : MulAction H α<VAR>inst✝ : SMulCommClass H G α<VAR>g : H<GOAL>fundamentalFrontier G (g • s) = g • fundamentalFrontier G s
<VAR>α : Type u<VAR>ι : Sort v<VAR>t : ι → TopologicalSpace α<VAR>s : Set α<GOAL>IsClosed s ↔ ∀ (i : ι), IsClosed s
<VAR>C₁ : Type u₁<VAR>inst✝¹¹ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝¹⁰ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁹ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁸ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝⁷ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝⁶ : L₂.IsLocalization W₂<VAR>W : ?m.49815<VAR>X Y Z : C₁<VAR>inst✝⁵ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝⁴ : HasSmallLocalizedHom W₁ Y Z<VAR>inst✝³ : HasSmallLocalizedHom W₁ X Z<VAR>inst✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>inst✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)<VAR>f : SmallHom W₁ X Y<VAR>g : SmallHom W₁ Y Z<GOAL>Φ.smallHomMap (f.comp g) = (Φ.smallHomMap f).comp (Φ.smallHomMap g)
<VAR>C₁ : Type u₁<VAR>inst✝¹¹ : Category.{v₁, u₁} C₁<VAR>W₁ : MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>inst✝¹⁰ : Category.{v₂, u₂} C₂<VAR>W₂ : MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>inst✝⁹ : Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>inst✝⁸ : Category.{v₄, u₄} D₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝⁷ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝⁶ : L₂.IsLocalization W₂<VAR>W : ?m.49815<VAR>X Y Z : C₁<VAR>inst✝⁵ : HasSmallLocalizedHom W₁ X Y<VAR>inst✝⁴ : HasSmallLocalizedHom W₁ Y Z<VAR>inst✝³ : HasSmallLocalizedHom W₁ X Z<VAR>inst✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>inst✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)<VAR>inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)<VAR>f : SmallHom W₁ X Y<VAR>g : SmallHom W₁ Y Z<GOAL>(SmallHom.equiv W₂ W₂.Q) (Φ.smallHomMap (f.comp g)) = (SmallHom.equiv W₂ W₂.Q) ((Φ.smallHomMap f).comp (Φ.smallHomMap g))
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<GOAL>(X.prodIsoProd Y).hom ≫ prodFst = prod.fst
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y : TopCat<GOAL>prodFst = (X.prodBinaryFan Y).fst
<VAR>θ₁ θ₂ : Angle<GOAL>(θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin
<VAR>θ₂ : Angle<VAR>x✝ : ℝ<GOAL>(↑x✝ + θ₂).sin = (↑x✝).sin * θ₂.cos + (↑x✝).cos * θ₂.sin
<VAR>x✝¹ x✝ : ℝ<GOAL>(↑x✝¹ + ↑x✝).sin = (↑x✝¹).sin * (↑x✝).cos + (↑x✝¹).cos * (↑x✝).sin
<VAR>n : ℕ<GOAL>fib (n + 2) - fib (n + 1) = fib n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrderTop α<VAR>inst✝ : DecidableEq α<VAR>a a✝ : α<GOAL>a✝ ∈ (Ici a).erase a ↔ a✝ ∈ Ioi a
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<GOAL>const a = a :: const a
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<GOAL>∀ (n : ℕ), (const a).get n = (a :: const a).get n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x : M<VAR>y : N<GOAL>(LinearMap.snd R M N) (x, y) = 0 ↔ (x, y) ∈ Set.range ⇑(LinearMap.inl R M N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : T2Space α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : T2Space α<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>K : Set α<VAR>hKA : K ⊆ A<VAR>hKc : IsCompact K<VAR>hK : μ A < μ K + ε<GOAL>∃ K ⊆ A, IsCompact K ∧ μ (A \ K) < ε
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>inst✝ : HasEqualizer f g<GOAL>(equalizerSubobject f g).arrow ≫ f = (equalizerSubobject f g).arrow ≫ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<VAR>h : 0 < l.length<VAR>head✝ : α<VAR>tail✝ : List α<VAR>x✝ : 0 < (head✝ :: tail✝).length<GOAL>(head✝ :: tail✝).maximum ≠ ⊥
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>f : Perm α<VAR>g : Perm β<VAR>e : α ≃ β<VAR>h : ∀ (x : α), e (f x) = g (e x)<GOAL>sign f = sign g
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>f : Perm α<VAR>g : Perm β<VAR>e : α ≃ β<VAR>h : ∀ (x : α), e (f x) = g (e x)<VAR>hg : g = (e.symm.trans f).trans e<GOAL>sign f = sign g
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : CommMonoidWithZero M₀<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<GOAL>(∏ i : ι, if p i then 1 else 0) = if ∀ (i : ι), p i then 1 else 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>i : ι<GOAL>b.reindexRange ⟨b i, ⋯⟩ = ↑⟨b i, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y : α<VAR>hy : y ∈ (swap x (f x) * f).support<GOAL>y ∈ f.support ∧ y ≠ x
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y : α<VAR>hy : (if f y = x then f x else if y = x then x else f y) ≠ y<GOAL>f y ≠ y ∧ y ≠ x
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>⟪x, (o.rotation ↑(π / 2)) x⟫_ℝ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹¹ : LinearOrder α<VAR>inst✝¹⁰ : LinearOrder β<VAR>inst✝⁹ : Countable α<VAR>inst✝⁸ : DenselyOrdered α<VAR>inst✝⁷ : NoMinOrder α<VAR>inst✝⁶ : NoMaxOrder α<VAR>inst✝⁵ : Nonempty α<VAR>inst✝⁴ : Countable β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<GOAL>Nonempty (α ≃o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹¹ : LinearOrder α<VAR>inst✝¹⁰ : LinearOrder β<VAR>inst✝⁹ : Countable α<VAR>inst✝⁸ : DenselyOrdered α<VAR>inst✝⁷ : NoMinOrder α<VAR>inst✝⁶ : NoMaxOrder α<VAR>inst✝⁵ : Nonempty α<VAR>inst✝⁴ : Countable β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>val✝ : Encodable α<GOAL>Nonempty (α ≃o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹¹ : LinearOrder α<VAR>inst✝¹⁰ : LinearOrder β<VAR>inst✝⁹ : Countable α<VAR>inst✝⁸ : DenselyOrdered α<VAR>inst✝⁷ : NoMinOrder α<VAR>inst✝⁶ : NoMaxOrder α<VAR>inst✝⁵ : Nonempty α<VAR>inst✝⁴ : Countable β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>val✝¹ : Encodable α<VAR>val✝ : Encodable β<GOAL>Nonempty (α ≃o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹¹ : LinearOrder α<VAR>inst✝¹⁰ : LinearOrder β<VAR>inst✝⁹ : Countable α<VAR>inst✝⁸ : DenselyOrdered α<VAR>inst✝⁷ : NoMinOrder α<VAR>inst✝⁶ : NoMaxOrder α<VAR>inst✝⁵ : Nonempty α<VAR>inst✝⁴ : Countable β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>val✝¹ : Encodable α<VAR>val✝ : Encodable β<VAR>to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)<VAR>our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal<GOAL>Nonempty (α ≃o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹¹ : LinearOrder α<VAR>inst✝¹⁰ : LinearOrder β<VAR>inst✝⁹ : Countable α<VAR>inst✝⁸ : DenselyOrdered α<VAR>inst✝⁷ : NoMinOrder α<VAR>inst✝⁶ : NoMaxOrder α<VAR>inst✝⁵ : Nonempty α<VAR>inst✝⁴ : Countable β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>val✝¹ : Encodable α<VAR>val✝ : Encodable β<VAR>to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)<VAR>our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal<VAR>F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯<GOAL>Nonempty (α ≃o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹¹ : LinearOrder α<VAR>inst✝¹⁰ : LinearOrder β<VAR>inst✝⁹ : Countable α<VAR>inst✝⁸ : DenselyOrdered α<VAR>inst✝⁷ : NoMinOrder α<VAR>inst✝⁶ : NoMaxOrder α<VAR>inst✝⁵ : Nonempty α<VAR>inst✝⁴ : Countable β<VAR>inst✝³ : DenselyOrdered β<VAR>inst✝² : NoMinOrder β<VAR>inst✝¹ : NoMaxOrder β<VAR>inst✝ : Nonempty β<VAR>val✝¹ : Encodable α<VAR>val✝ : Encodable β<VAR>to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p => Sum.recOn p (definedAtLeft β) (definedAtRight α)<VAR>our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal<VAR>F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯<VAR>G : (b : β) → { a // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun b => invOfIdeal b our_ideal ⋯<GOAL>Nonempty (α ≃o β)
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<GOAL>(↑(alternatization a)).domCoprod ↑(alternatization b) = ∑ σa : Perm ιa, ∑ σb : Perm ιb, Perm.sign σa • Perm.sign σb • (domDomCongr σa a).domCoprod (domDomCongr σb b)
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<GOAL>domCoprod' ((∑ σ : Perm ιa, Perm.sign σ • domDomCongr σ a) ⊗ₜ[R'] ∑ σ : Perm ιb, Perm.sign σ • domDomCongr σ b) = ∑ x : Perm ιa, ∑ x_1 : Perm ιb, Perm.sign x • Perm.sign x_1 • domCoprod' (domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b)
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>inst✝¹⁰ : Fintype ιa<VAR>inst✝⁹ : Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommGroup N₁<VAR>inst✝⁶ : Module R' N₁<VAR>inst✝⁵ : AddCommGroup N₂<VAR>inst✝⁴ : Module R' N₂<VAR>inst✝³ : AddCommMonoid Mᵢ<VAR>inst✝² : Module R' Mᵢ<VAR>inst✝¹ : DecidableEq ιa<VAR>inst✝ : DecidableEq ιb<VAR>a : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<GOAL>∑ x : Perm ιa, ∑ x_1 : Perm ιb, domCoprod' (Perm.sign x • Perm.sign x_1 • domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b) = ∑ x : Perm ιa, ∑ x_1 : Perm ιb, Perm.sign x • Perm.sign x_1 • domCoprod' (domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b)
<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>s : Set (Set α)<GOAL>(FilterBasis.ofSets s).filter = generate s
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝² : HasCokernel f✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasCokernel f<VAR>inst✝ : IsIso g<GOAL>f ≫ g ≫ cokernel.π (f ≫ g) = 0
<VAR>V : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup V<VAR>inst✝ : NormedSpace ℝ V<VAR>K L : ConvexBody V<GOAL>EMetric.hausdorffEdist ↑K ↑L = edist K L
<VAR>V : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup V<VAR>inst✝ : NormedSpace ℝ V<VAR>K L : ConvexBody V<GOAL>EMetric.hausdorffEdist ↑K ↑L = ENNReal.ofReal (dist K L)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>motive : (⨂[R] (i : ι), s i) → Prop<VAR>z : ⨂[R] (i : ι), s i<VAR>tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)<VAR>add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)<GOAL>motive z
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>motive : (⨂[R] (i : ι), s i) → Prop<VAR>z : ⨂[R] (i : ι), s i<VAR>tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)<VAR>add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)<VAR>C0 : motive 0<GOAL>motive z
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>motive : (⨂[R] (i : ι), s i) → Prop<VAR>z : ⨂[R] (i : ι), s i<VAR>tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)<VAR>add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)<VAR>C0 : motive 0<VAR>x : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))<GOAL>∀ (x : R × ((i : ι) → (fun i => s i) i)) (xs : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))), motive ↑xs → motive ↑(FreeAddMonoid.of x + xs)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>motive : (⨂[R] (i : ι), s i) → Prop<VAR>z : ⨂[R] (i : ι), s i<VAR>tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)<VAR>add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)<VAR>C0 : motive 0<VAR>x : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))<GOAL>∀ (x : R × ((i : ι) → s i)) (xs : FreeAddMonoid (R × ((i : ι) → s i))), motive ↑xs → motive (↑(FreeAddMonoid.of x) + ↑xs)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X : Set α<GOAL>∀ (x : α), (∀ (t : Set α), M.Flat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.Flat a → x ∈ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝⁴ : GroupWithZero G₀<VAR>inst✝³ : TopologicalSpace G₀<VAR>inst✝² : HasContinuousInv₀ G₀<VAR>inst✝¹ : ContinuousMul G₀<VAR>f✝ g✝ : α → G₀<VAR>inst✝ : T1Space G₀<VAR>f g : α → G₀<VAR>l : Filter α<VAR>x y : G₀<VAR>hg : Tendsto g l (𝓝 y)<VAR>hy : y ≠ 0<GOAL>Tendsto (fun n => f n * g n) l (𝓝 (x * y)) ↔ Tendsto f l (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝⁴ : GroupWithZero G₀<VAR>inst✝³ : TopologicalSpace G₀<VAR>inst✝² : HasContinuousInv₀ G₀<VAR>inst✝¹ : ContinuousMul G₀<VAR>f✝ g✝ : α → G₀<VAR>inst✝ : T1Space G₀<VAR>f g : α → G₀<VAR>l : Filter α<VAR>x y : G₀<VAR>hg : Tendsto g l (𝓝 y)<VAR>hy : y ≠ 0<VAR>hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))<GOAL>Tendsto f l (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝⁴ : GroupWithZero G₀<VAR>inst✝³ : TopologicalSpace G₀<VAR>inst✝² : HasContinuousInv₀ G₀<VAR>inst✝¹ : ContinuousMul G₀<VAR>f✝ g✝ : α → G₀<VAR>inst✝ : T1Space G₀<VAR>f g : α → G₀<VAR>l : Filter α<VAR>x y : G₀<VAR>hg : Tendsto g l (𝓝 y)<VAR>hy : y ≠ 0<VAR>hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))<GOAL>Tendsto f l (𝓝 (x * y / y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝⁴ : GroupWithZero G₀<VAR>inst✝³ : TopologicalSpace G₀<VAR>inst✝² : HasContinuousInv₀ G₀<VAR>inst✝¹ : ContinuousMul G₀<VAR>f✝ g✝ : α → G₀<VAR>inst✝ : T1Space G₀<VAR>f g : α → G₀<VAR>l : Filter α<VAR>x y : G₀<VAR>hg : Tendsto g l (𝓝 y)<VAR>hy : y ≠ 0<VAR>hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))<GOAL>(fun n => f n * g n) / g =ᶠ[l] f