ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>P : ClassGroup R → Prop<VAR>h : ∀ (I : (FractionalIdeal R⁰ K)ˣ), P (mk I)<VAR>x : ClassGroup R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>P ↑I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>P : ClassGroup R → Prop<VAR>h : ∀ (I : (FractionalIdeal R⁰ K)ˣ), P (mk I)<VAR>x : ClassGroup R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>this : I = (Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv) ((Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv) I)<GOAL>P ↑I
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>h : IsTorsionFree α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>s.card + t.card - 1 ≤ (s * t).card
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : Nontrivial R<VAR>hR : ringChar R ≠ 2<GOAL>2 ≠ 0
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : Nontrivial R<VAR>hR : ringChar R ≠ 2<GOAL>¬(ringChar R = 1 ∨ ringChar R = 2)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : S.f ≫ k = 0<VAR>inst✝ : S.HasRightHomology<GOAL>h.opcyclesIso.hom ≫ h.descQ k hk = S.descOpcycles k hk
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>w : NormalWord d<GOAL>ReducedWord.prod φ w.toReducedWord • empty = w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure (Measure (Measure α))<GOAL>μ.bind join = μ.join.join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure (Measure (Measure α))<GOAL>μ.bind join = μ.bind fun a => (id a).bind id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure (Measure (Measure α))<GOAL>join = fun a => (id a).bind id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure (Measure (Measure α))<VAR>ν : Measure (Measure α)<GOAL>ν.join = (id ν).bind id
<VAR>a b : ℕ+<GOAL>(Ico a b).card = ↑b - ↑a
<VAR>a b : ℕ+<GOAL>(Ico a b).card = (Ico ↑a ↑b).card
<VAR>a b : ℕ+<GOAL>(Ico a b).card = (map (Embedding.subtype fun n => 0 < n) (Ico a b)).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>p✝ : PMF α<VAR>s✝ t : Set α<VAR>inst✝ : MeasurableSingletonClass α<VAR>p : PMF α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(p.toMeasure.restrict p.support) s = p.toMeasure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>p✝ : PMF α<VAR>s✝ t : Set α<VAR>inst✝ : MeasurableSingletonClass α<VAR>p : PMF α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>p.toMeasure (s ∩ p.support) = p.toMeasure s
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38446, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : X ≅ Y<VAR>U : Opens ↑↑Y<GOAL>(H.hom.c ≫ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) = (𝟙 Y.presheaf).app (op U)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38446, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : X ≅ Y<VAR>U : Opens ↑↑Y<GOAL>H.hom.c.app (op U) ≫ (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) = (𝟙 Y.presheaf).app (op U)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38446, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : X ≅ Y<VAR>U : Opens ↑↑Y<GOAL>(Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) ≫ H.hom.c.app (op U) = (𝟙 ((Presheaf.pushforward C H.hom.base).obj X.presheaf)).app (op U)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38446, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : X ≅ Y<VAR>U : Opens ↑↑Y<GOAL>(Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) ≫ H.hom.c.app (op U) = 𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38446, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : X ≅ Y<VAR>U : Opens ↑↑Y<GOAL>H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) = 𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38446, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : X ≅ Y<VAR>U : Opens ↑↑Y<VAR>eq₁ : (H.hom ≫ H.inv).c.app (op ((Opens.map H.hom.base).obj U)) = (𝟙 X).c.app (op ((Opens.map H.hom.base).obj U)) ≫ X.presheaf.map (eqToHom ⋯)<GOAL>H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) = 𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38446, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : X ≅ Y<VAR>U : Opens ↑↑Y<VAR>eq₁ : (H.hom ≫ H.inv).c.app (op ((Opens.map H.hom.base).obj U)) = (𝟙 X).c.app (op ((Opens.map H.hom.base).obj U)) ≫ X.presheaf.map (eqToHom ⋯)<VAR>eq₂ : Y.presheaf.map (eqToHom ⋯).op ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) = H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫ ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯).op<GOAL>H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) = 𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38446, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : X ≅ Y<VAR>U : Opens ↑↑Y<VAR>eq₁ : H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) = eqToHom ⋯<VAR>eq₂ : Y.presheaf.map (eqToHom ⋯).op ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) = H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫ ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯).op<GOAL>H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) = 𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.38446, u_1} C<VAR>X Y : PresheafedSpace C<VAR>H : X ≅ Y<VAR>U : Opens ↑↑Y<VAR>eq₁ : H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) = eqToHom ⋯<VAR>eq₂ : eqToHom ⋯ ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) = H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫ ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯)<GOAL>H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) = 𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : FiniteDimensional K V₂<VAR>H : finrank K V = finrank K V₂<VAR>f : V →ₗ[K] V₂<GOAL>ker f = ⊥ ↔ range f = ⊤
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>inst✝² : LieRingModule L M✝<VAR>inst✝¹ : LieModule R L M✝<VAR>inst✝ : Subsingleton L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>_h : ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)<GOAL>LieModule.IsNilpotent R L M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>inst✝² : LieRingModule L M✝<VAR>inst✝¹ : LieModule R L M✝<VAR>inst✝ : Subsingleton L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>_h : ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)<GOAL>lowerCentralSeries R L M 1 = ⊥
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieRing L₂<VAR>inst✝⁵ : LieAlgebra R L₂<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>inst✝² : LieRingModule L M✝<VAR>inst✝¹ : LieModule R L M✝<VAR>inst✝ : Subsingleton L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>_h : ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)<GOAL>⊤ = ⊥
<VAR>α : Type u<VAR>inst✝¹ : Mul α<VAR>β : Type v<VAR>inst✝ : Semigroup β<VAR>f✝ f : α →ₙ* β<VAR>x : AssocQuotient α<GOAL>∀ (a b : α), AssocRel α a b → f a = f b
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>S : Submodule R M<VAR>inst✝ : Module.Finite R ↥S<GOAL>1 ≤ finrank R ↥S ↔ S ≠ ⊥
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<GOAL>Odd (m + n) ↔ (Odd m ↔ Even n)
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>h : m = n✝<VAR>n : ℕ<GOAL>m ∣ n ↔ n✝ ∣ n
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero M'<VAR>inst✝ : CommMonoid N<VAR>f : α →₀ M<VAR>y : α<VAR>g : α → M → N<VAR>hyf : y ∈ f.support<GOAL>g y (f y) * (erase y f).prod g = f.prod g
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>s : S<VAR>g : X ⟶ (restrictScalars f).obj Y<VAR>x✝ y✝ : ↑X<GOAL>s • g (x✝ + y✝) = s • g x✝ + s • g y✝
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>s : S<VAR>g : X ⟶ (restrictScalars f).obj Y<VAR>r : R<VAR>x : ↑X<GOAL>{ toFun := fun x => s • g x, map_add' := ⋯ }.toFun (r • x) = (RingHom.id R) r • { toFun := fun x => s • g x, map_add' := ⋯ }.toFun x
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<GOAL>(aeval fun o => o.elim (C Polynomial.X) X).comp (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)) = AlgHom.id R (MvPolynomial S₁ R[X])
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<GOAL>(aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)).comp (aeval fun o => o.elim (C Polynomial.X) X) = AlgHom.id R (MvPolynomial (Option S₁) R)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : Monoid γ<VAR>s₁ s₂ : Finset α<VAR>f g : α → β<VAR>h₁ : s₁ = s₂<VAR>h₂ : ∀ x ∈ s₂, f x = g x<VAR>comm : (↑s₁).Pairwise fun a b => Commute (f a) (f b)<GOAL>s₁.noncommProd f comm = s₂.noncommProd g ⋯
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>b : β<GOAL>b ∈ a⁻¹ • s ↔ a • b ∈ s
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>(L1 ++ L2).length + 2 = (L1 ++ (x, b) :: (x, !b) :: L2).length
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι✝ → α<VAR>hwf : WellFounded fun x x_1 => x > x_1<VAR>ι : Type u_3<VAR>t : ι → α<VAR>ht : Independent t<GOAL>{i | t i ≠ ⊥}.Finite
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι✝ → α<VAR>hwf : WellFounded fun x x_1 => x > x_1<VAR>ι : Type u_3<VAR>t : ι → α<VAR>ht : Independent t<GOAL>(range t).Finite
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<GOAL>a * star a = ↑(a * star a).re
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<GOAL>star a * a = ↑(star a * a).re
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ ≤ b₂<GOAL>Ioc a₁ b₁ ⊆ Ioc a₂ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>e : α ≃ β<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>e.symm (e x) ∈ s
<VAR>p : ℝ≥0∞<VAR>h : p ≤ 1<GOAL>∫ (b : Bool), bif b then 1 else 0 ∂(bernoulli p h).toMeasure = p.toReal
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u : Set α<VAR>x : α<VAR>s t : Set α<GOAL>s \ {x} ⊆ t ↔ s ⊆ insert x t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u : Set α<VAR>x : α<VAR>s t : Set α<GOAL>s \ {x} ⊆ t ↔ s ⊆ {x} ∪ t
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>inst✝ : Monoid M<VAR>a : Mˣ<VAR>x y : M<VAR>h : SemiconjBy (↑a) x y<GOAL>↑a⁻¹ * y = ↑a⁻¹ * (y * ↑a * ↑a⁻¹)
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>inst✝ : Monoid M<VAR>a : Mˣ<VAR>x y : M<VAR>h : SemiconjBy (↑a) x y<GOAL>↑a⁻¹ * (y * ↑a * ↑a⁻¹) = x * ↑a⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>s : Set α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<VAR>h₁ : J ∈ split I i x<VAR>h₂ : y ∈ J<VAR>h₃ : y i ≤ x<GOAL>↑J = ↑I ∩ {y | y i ≤ x}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<VAR>h₁ : J ∈ split I i x<VAR>h₂ : y ∈ J<VAR>h₃ : y i ≤ x<VAR>H : ↑J = ↑I ∩ {y | x < y i}<GOAL>False
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<VAR>h₁ : J ∈ split I i x<VAR>h₂ : y ∈ ↑I ∩ {y | x < y i}<VAR>h₃ : y i ≤ x<VAR>H : ↑J = ↑I ∩ {y | x < y i}<GOAL>False
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : StarAddMonoid α<VAR>M : Matrix m n α<GOAL>Mᴴ = 0 ↔ M = 0
<VAR>α : Type u_1<VAR>f : ℕ → α<GOAL>{f 0} ∪ range (f ∘ succ) = range f
<VAR>P : AffineTargetMorphismProperty<VAR>inst✝ : P.toProperty.RespectsIso<VAR>X Y X' Y' : Scheme<VAR>f : X ⟶ Y<VAR>f' : X' ⟶ Y'<VAR>e : Arrow.mk f ≅ Arrow.mk f'<VAR>h : IsAffine Y<GOAL>P f ↔ P f'
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>a + b = b + a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>a - -b = b + a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>- -a - -b = b + a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>0 - 0 - (0 - a - b) = b + a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>0 - 0 - (-b - a) = b + a
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>a ≡ b [PMOD 0] ↔ a = b
<VAR>A : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} T<VAR>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>inst✝² : Category.{?u.25322, u_1} A'<VAR>inst✝¹ : Category.{?u.25326, u_2} B'<VAR>inst✝ : Category.{?u.25330, u_3} T'<VAR>L : A ⥤ T<VAR>R : B ⥤ T<VAR>L₁ L₂ L₃ : A ⥤ T<VAR>R₁ R₂ R₃ : B ⥤ T<VAR>L' : A' ⥤ T'<VAR>R' : B' ⥤ T'<VAR>F₁ : A ⥤ A'<VAR>F₂ : B ⥤ B'<VAR>F : T ⥤ T'<VAR>α : F₁ ⋙ L' ⟶ L ⋙ F<VAR>β : R ⋙ F ⟶ F₂ ⋙ R'<VAR>X Y : Comma L R<VAR>φ : X ⟶ Y<GOAL>L'.map (F₁.map φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right = (α.app X.left ≫ F.map X.hom ≫ β.app X.right) ≫ R'.map (F₂.map φ.right)
<VAR>A : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} T<VAR>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>inst✝² : Category.{?u.25322, u_1} A'<VAR>inst✝¹ : Category.{?u.25326, u_2} B'<VAR>inst✝ : Category.{?u.25330, u_3} T'<VAR>L : A ⥤ T<VAR>R : B ⥤ T<VAR>L₁ L₂ L₃ : A ⥤ T<VAR>R₁ R₂ R₃ : B ⥤ T<VAR>L' : A' ⥤ T'<VAR>R' : B' ⥤ T'<VAR>F₁ : A ⥤ A'<VAR>F₂ : B ⥤ B'<VAR>F : T ⥤ T'<VAR>α : F₁ ⋙ L' ⟶ L ⋙ F<VAR>β : R ⋙ F ⟶ F₂ ⋙ R'<VAR>X Y : Comma L R<VAR>φ : X ⟶ Y<GOAL>L'.map (F₁.map φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right = α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ R'.map (F₂.map φ.right)
<VAR>A : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} T<VAR>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>inst✝² : Category.{?u.25322, u_1} A'<VAR>inst✝¹ : Category.{?u.25326, u_2} B'<VAR>inst✝ : Category.{?u.25330, u_3} T'<VAR>L : A ⥤ T<VAR>R : B ⥤ T<VAR>L₁ L₂ L₃ : A ⥤ T<VAR>R₁ R₂ R₃ : B ⥤ T<VAR>L' : A' ⥤ T'<VAR>R' : B' ⥤ T'<VAR>F₁ : A ⥤ A'<VAR>F₂ : B ⥤ B'<VAR>F : T ⥤ T'<VAR>α : F₁ ⋙ L' ⟶ L ⋙ F<VAR>β : R ⋙ F ⟶ F₂ ⋙ R'<VAR>X Y : Comma L R<VAR>φ : X ⟶ Y<GOAL>α.app X.left ≫ (L ⋙ F).map φ.left ≫ F.map Y.hom ≫ β.app Y.right = α.app X.left ≫ F.map X.hom ≫ (R ⋙ F).map φ.right ≫ β.app Y.right
<VAR>A : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} T<VAR>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>inst✝² : Category.{?u.25322, u_1} A'<VAR>inst✝¹ : Category.{?u.25326, u_2} B'<VAR>inst✝ : Category.{?u.25330, u_3} T'<VAR>L : A ⥤ T<VAR>R : B ⥤ T<VAR>L₁ L₂ L₃ : A ⥤ T<VAR>R₁ R₂ R₃ : B ⥤ T<VAR>L' : A' ⥤ T'<VAR>R' : B' ⥤ T'<VAR>F₁ : A ⥤ A'<VAR>F₂ : B ⥤ B'<VAR>F : T ⥤ T'<VAR>α : F₁ ⋙ L' ⟶ L ⋙ F<VAR>β : R ⋙ F ⟶ F₂ ⋙ R'<VAR>X Y : Comma L R<VAR>φ : X ⟶ Y<GOAL>α.app X.left ≫ F.map (L.map φ.left) ≫ F.map Y.hom ≫ β.app Y.right = α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m m₁ m₂ : Multiset α<VAR>h : m₁ ≤ m₂<VAR>p : α × ℕ<GOAL>p ∈ m₁.toEnumFinset → p ∈ m₂.toEnumFinset
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m m₁ m₂ : Multiset α<VAR>h : m₁ ≤ m₂<VAR>p : α × ℕ<GOAL>p.2 < count p.1 m₁ → p.2 < count p.1 m₂
<VAR>m n k : ℕ<GOAL>m.psub (n + k) = do let __do_lift ← m.psub n __do_lift.psub k
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : closure s ⊆ s<GOAL>IsClosed s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : closure s ⊆ s<GOAL>IsClosed (closure s)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a x✝¹ : { x // x ∈ s }<VAR>x✝ : x✝¹ ∈ s.attach<GOAL>(a = x✝¹) = (↑a = ↑x✝¹)
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>lle : lift.{u, v} #β' ≤ lift.{v, u} #α<GOAL>Nonempty (α ≃ α ⊕ β')
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>lle : lift.{u, v} #β' ≤ lift.{v, u} #α<GOAL>lift.{max u v, u} #α = lift.{max v u, u} #α + lift.{u, v} #β'
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>lle : lift.{u, v} #β' ≤ lift.{v, u} #α<GOAL>lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<VAR>lle : lift.{u, v} #β' ≤ lift.{v, u} #α<VAR>e : α ≃ α ⊕ β'<VAR>f g : α → β'<VAR>h : (fun f => ⟨fun a => Sum.elim f id (e a), ⋯⟩) f = (fun f => ⟨fun a => Sum.elim f id (e a), ⋯⟩) g<VAR>a : α<GOAL>f a = g a
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β<VAR>h : Surjective (map f)<VAR>x : β<VAR>y : α<VAR>hxy : map f [y] = [x]<GOAL>∃ a, f a = x
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>j j' : J<VAR>x : F.obj j<VAR>x' : F.obj j'<VAR>j'' : J<VAR>f : j ⟶ j''<VAR>f' : j' ⟶ j''<VAR>w : F.map f x = F.map f' x'<GOAL>colimit.ι F j x = colimit.ι F j' x'
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>j j' : J<VAR>x : F.obj j<VAR>x' : F.obj j'<VAR>j'' : J<VAR>f : j ⟶ j''<VAR>f' : j' ⟶ j''<VAR>w : F.map f x = F.map f' x'<GOAL>(F.map f ≫ colimit.ι F j'') x = (F.map f' ≫ colimit.ι F j'') x'
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<GOAL>(a * ⊤).toReal = 0
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : dist p3 p1 = dist p3 p2<VAR>m : P := midpoint ℝ p1 p2<GOAL>∠ p3 (midpoint ℝ p1 p2) p1 = π / 2
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : dist p3 p1 = dist p3 p2<VAR>m : P := midpoint ℝ p1 p2<VAR>h1 : p3 -ᵥ p1 = p3 -ᵥ m - (p1 -ᵥ m)<GOAL>∠ p3 (midpoint ℝ p1 p2) p1 = π / 2
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : dist p3 p1 = dist p3 p2<VAR>m : P := midpoint ℝ p1 p2<VAR>h1 : p3 -ᵥ p1 = p3 -ᵥ m - (p1 -ᵥ m)<VAR>h2 : p3 -ᵥ p2 = p3 -ᵥ m + (p1 -ᵥ m)<GOAL>∠ p3 (midpoint ℝ p1 p2) p1 = π / 2
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>m : P := midpoint ℝ p1 p2<VAR>h : ‖p3 -ᵥ m - (p1 -ᵥ m)‖ = ‖p3 -ᵥ m + (p1 -ᵥ m)‖<VAR>h1 : p3 -ᵥ p1 = p3 -ᵥ m - (p1 -ᵥ m)<VAR>h2 : p3 -ᵥ p2 = p3 -ᵥ m + (p1 -ᵥ m)<GOAL>∠ p3 (midpoint ℝ p1 p2) p1 = π / 2