mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.zero : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R], Matrix.PosSemidef 0
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sum_f_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S) (i : F.I₀), (E.sum F).f (Sum.inr i) = F.f i
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with subtracting a constant.  -/
iteratedFDerivWithin_comp_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} (n : ℕ) (a : E),
  iteratedFDerivWithin 𝕜 n (fun z => f (z - a)) s x = iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.sup_ringCon : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] (I J : TwoSidedIdeal R), (I ⊔ J).ringCon = I.ringCon ⊔ J.ringCon
-- Mathlib.Data.Fin.Basic
Fin.one_le_of_ne_zero : ∀ {n : ℕ} {k : Fin n}, k ≠ 0 → 1 ≤ k
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.instDiscreteTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [DiscreteTopology M], DiscreteTopology Mᵐᵒᵖ
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.add_sub_add_left : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {c : α}, IsAddUnit c → ∀ (a b : α), c + a - (c + b) = a - b
-- Mathlib.RingTheory.Invariant.Defs
Algebra.isInvariant_iff : ∀ (A : Type u_1) (B : Type u_2) (G : Type u_3) [inst : CommSemiring A] [inst_1 : Semiring B] [inst_2 : Algebra A B]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B],
  Algebra.IsInvariant A B G ↔ ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a, (algebraMap A B) a = b
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_zmod : ∀ (n : ℕ), Nat.card (ZMod n) = n
-- Init.Data.List.Attach
List.pmap_congr_left : ∀ {α : Type u_1} {β : Type u_2} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (l : List α)
  {H₁ : ∀ a ∈ l, p a} {H₂ : ∀ a ∈ l, q a},
  (∀ a ∈ l, ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → List.pmap f l H₁ = List.pmap g l H₂
-- Init.Data.Int.DivMod.Lemmas
Int.sub_bmod_left : ∀ (a : ℕ) (b : ℤ), (↑a - b).bmod a = (-b).bmod a
-- Mathlib.Order.Partition.Basic
/-- See Note [custom simps projection].  -/
Partition.Simps.coe : {α : Type u_1} → [inst : CompleteLattice α] → {s : α} → Partition s → Set α
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ i, c.Rel i j) (i j : ι),
  ¬c.Rel j i → (HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.cofork_ι_app_one : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g],
  (CategoryTheory.Limits.coequalizer.cofork f g).ι.app CategoryTheory.Limits.WalkingParallelPair.one =
    CategoryTheory.Limits.coequalizer.π f g
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.mem_essImage_of_counit_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (A : D)
  [CategoryTheory.IsIso (h.counit.app A)], L.essImage A
-- Mathlib.Data.Finset.SDiff
/-- See also `Finset.inter_sdiff_assoc`.  -/
Finset.sdiff_inter_right_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s \ t ∩ u = (s ∩ u) \ t
-- Mathlib.Logic.Equiv.Defs
Equiv.coe_fn_symm_mk : ∀ {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : Function.LeftInverse g f) (r : Function.RightInverse g f),
  ⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = g
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balance1.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c) z d)
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c)) z d)
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (match RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c, z, d with
    | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c, z, d => h_1 a x b y c z d
    | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c), z, d => h_2 a x b y c z d
    | a, x, b => h_3 a x b) =
    h_1 a x b y c z d
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.

```
Vᵢⱼ ⟶ Uᵢ
 |      |
 ↓      ↓
 Uⱼ ⟶ X
```
 -/
AlgebraicGeometry.SheafedSpace.GlueData.vPullbackConeIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.SheafedSpace.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasLimits C] → (i j : D.J) → CategoryTheory.Limits.IsLimit (D.vPullbackCone i j)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instFaithfulFunctorOppositeAbToPresheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat},
  (PresheafOfModules.toPresheaf R).Faithful
-- Mathlib.Algebra.Lie.Subalgebra
LieEquiv.ofSubalgebras_symm_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (L₁' : LieSubalgebra R L₁) (L₂' : LieSubalgebra R L₂)
  (e : L₁ ≃ₗ⁅R⁆ L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') (x : ↥L₂'),
  ↑((LieEquiv.ofSubalgebras L₁' L₂' e h).symm x) = e.symm ↑x
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
MulHom.map_multiset_ne_zero_prod : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] (f : M →ₙ* N) (s : Multiset M),
  s ≠ 0 → f s.prod = (Multiset.map (⇑f) s).prod
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofNat_lt_top : ∀ {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n < ⊤
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.toAddMonoidHom_mulRight : ∀ (R : Type u_14) {A : Type u_15} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a : A), ↑(LinearMap.mulRight R a) = AddMonoidHom.mulRight a
-- Mathlib.Probability.Independence.ZeroOne
/-- **Kolmogorov's 0-1 law**, kernel version: any event in the tail σ-algebra of an independent
sequence of sub-σ-algebras has probability 0 or 1 almost surely.  -/
ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [inst : SemilatticeInf ι]
  [NoMinOrder ι] [Nonempty ι],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα → ∀ {t : Set Ω}, MeasurableSet t → ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_modify_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {fallback : β k} {f : β k → β k},
  m.WF → (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.gcd_eq_zero_iff : ∀ {d : ℤ} (a : ℤ√d), a.re.gcd a.im = 0 ↔ a = 0
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
AEMeasurable.mk.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {μ μ_1 : MeasureTheory.Measure α}
  (e_μ : μ = μ_1) (f f_1 : α → β) (e_f : f = f_1) (h : AEMeasurable f μ) (a a_1 : α),
  a = a_1 → AEMeasurable.mk f h a = AEMeasurable.mk f_1 ⋯ a_1
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.evalNegHom_X : ∀ {A : Type u_2} [inst : CommRing A], PowerSeries.evalNegHom PowerSeries.X = -PowerSeries.X
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.mk.injEq : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W}
  (toCommaMorphism : CategoryTheory.CommaMorphism X.toComma Y.toComma) (prop_hom_left : Q toCommaMorphism.left)
  (prop_hom_right : W toCommaMorphism.right) (toCommaMorphism_1 : CategoryTheory.CommaMorphism X.toComma Y.toComma)
  (prop_hom_left_1 : Q toCommaMorphism_1.left) (prop_hom_right_1 : W toCommaMorphism_1.right),
  ({ toCommaMorphism := toCommaMorphism, prop_hom_left := prop_hom_left, prop_hom_right := prop_hom_right } =
      { toCommaMorphism := toCommaMorphism_1, prop_hom_left := prop_hom_left_1, prop_hom_right := prop_hom_right_1 }) =
    (toCommaMorphism = toCommaMorphism_1)
-- Init.Data.SInt.Lemmas
Int64.toInt16_add : ∀ (a b : Int64), (a + b).toInt16 = a.toInt16 + b.toInt16
-- Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
/-- Shows that `Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂`.  -/
GenContFract.nums_recurrence : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K] {gp : GenContFract.Pair K} {ppredA predA : K},
  g.s.get? (n + 1) = some gp →
    g.nums n = ppredA → g.nums (n + 1) = predA → g.nums (n + 2) = gp.b * predA + gp.a * ppredA
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.compHausLikeToTop_map : ∀ (P : TopCat → Prop) {X Y : CategoryTheory.InducedCategory TopCat CompHausLike.toTop} (f : X ⟶ Y),
  (CompHausLike.compHausLikeToTop P).map f = f.hom
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.ruleSets.inj : ∀ {rs rs_1 : Aesop.Frontend.RuleSets},
  Aesop.Frontend.Feature.ruleSets rs = Aesop.Frontend.Feature.ruleSets rs_1 → rs = rs_1
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.instHasPushoutInrHomDiscretePUnitOfHasPushoutsAlongOfIsStableUnderCobaseChangeAlong : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) {X Y Z : T}
  (f : Y ⟶ X) (g : Z ⟶ Y) [P.HasPushoutsAlong f] [inst_2 : P.HasPushoutsAlong g] [P.IsStableUnderCobaseChangeAlong g]
  (A : P.Under Q Z), CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr A.hom g) f
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.addLeft_toEquiv : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] (a : α),
  (OrderIso.addLeft a).toEquiv = Equiv.addLeft a
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encodeCode.match_1.splitter : (motive : Nat.Partrec.Code → Sort u_1) →
  (x : Nat.Partrec.Code) →
    (Unit → motive Nat.Partrec.Code.zero) →
      (Unit → motive Nat.Partrec.Code.succ) →
        (Unit → motive Nat.Partrec.Code.left) →
          (Unit → motive Nat.Partrec.Code.right) →
            ((cf cg : Nat.Partrec.Code) → motive (cf.pair cg)) →
              ((cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) →
                ((cf cg : Nat.Partrec.Code) → motive (cf.prec cg)) →
                  ((cf : Nat.Partrec.Code) → motive cf.rfind') → motive x
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- If a function is integrable on a set `s` and vanishes almost everywhere on its complement,
then it is integrable.  -/
MeasureTheory.IntegrableOn.integrable_of_ae_notMem_eq_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α} {ε' : Type u_7}
  [inst : TopologicalSpace ε'] [inst_1 : ENormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ → (∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0) → MeasureTheory.Integrable f μ
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableInf.measurable_const_inf : ∀ {M : Type u_1} {inst : MeasurableSpace M} {inst_1 : Min M} [self : MeasurableInf M] (c : M), Measurable fun x => c ⊓ x
-- Mathlib.Order.CompleteLattice.Basic
iInf_psigma' : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_8} {κ : ι → Sort u_9} (f : (i : ι) → κ i → α),
  ⨅ i, ⨅ j, f i j = ⨅ ij, f ij.fst ij.snd
-- Mathlib.NumberTheory.Modular
/-- Explicit formula for the image of `ModularGroup.fd` in `ℂ`.  -/
ModularGroup.coe_fd : UpperHalfPlane.coe '' ModularGroup.fd = {z | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
-- Mathlib.GroupTheory.OrderOfElement
Nat.cast_card_eq_zero : ∀ (R : Type u_6) [inst : AddGroupWithOne R] [inst_1 : Fintype R], ↑(Fintype.card R) = 0
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDivisionAddCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α],
  OrderDual.instDivisionAddCommMonoid = { toSubtractionMonoid := OrderDual.instSubtractionMonoid, add_comm := ⋯ }
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.inl_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (i : A), (ContinuousAddMonoidHom.inl A B) i = (i, 0)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.vcomp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ ι : F ⟶ G} (Γ : CategoryTheory.Oplax.StrongTrans.Modification η θ)
  (Δ : CategoryTheory.Oplax.StrongTrans.Modification θ ι) (a : B),
  (Γ.vcomp Δ).app a = CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.hole.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Dynamics.FixedPoints.Defs
/-- The set of fixed points of a map `f : α → α`.  -/
Function.fixedPoints : {α : Type u_1} → (α → α) → Set α
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.var.injEq : ∀ (v v_1 : Nat.Internal.Linear.Var), (Nat.Internal.SOM.Expr.var v = Nat.Internal.SOM.Expr.var v_1) = (v = v_1)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).obj c).pt = c.pt
-- Batteries.Data.Fin.Coding
/-- Encode `Quotient s` into `Fin m` where `s` is a decidable setoid on `Fin n`.  -/
Fin.encodeQuotient : {n : ℕ} →
  (s : Setoid (Fin n)) → [inst : DecidableRel ⇑s] → Quotient s → Fin (Fin.countP fun i => decide (Fin.getRepr s i = i))
-- Mathlib.Logic.Embedding.Set
subtypeOrEquiv_symm_inr : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] (h : Disjoint p q) (x : { x // q x }),
  (subtypeOrEquiv p q h).symm (Sum.inr x) = ⟨↑x, ⋯⟩
-- Mathlib.Data.Nat.Cast.Commute
Nat.commute_cast : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (x : α) (n : ℕ), Commute x ↑n
-- Mathlib.Algebra.Group.Action.Faithful
/-- `Mul.toSMulMulOpposite` is faithful when multiplication is left cancellative  -/
instFaithfulSMulMulOppositeOfIsLeftCancelMul : ∀ (R : Type u_4) [inst : Mul R] [IsLeftCancelMul R], FaithfulSMul Rᵐᵒᵖ R
-- Mathlib.Logic.OpClass
/-- `LeftCommutative op` where `op : α → β → β` says that `op` is a left-commutative operation,
i.e. `op a₁ (op a₂ b) = op a₂ (op a₁ b)`.  -/
LeftCommutative : {α : Sort u} → {β : Sort v} → (α → β → β) → Prop
-- Init.Data.Nat.Lemmas
Nat.add_eq_zero : ∀ {m n : ℕ}, m + n = 0 ↔ m = 0 ∧ n = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, Std.DTreeMap.Internal.Impl.contains (t.maxKey he) t = true
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.trans_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E),
  (f.trans g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ -y + x` is quasi-measure-preserving.  -/
MeasureTheory.quasiMeasurePreserving_neg_add_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => -p.2 + p.1) (μ.prod ν) μ
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.union_C0C1_eq : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2), Profinite.NobelingProof.C0 C ho ∪ Profinite.NobelingProof.C1 C ho = C
-- Mathlib.Data.QPF.Univariate.Basic
/-- A qpf is said to be uniform if every polynomial functor
representing a single value all have the same range.  -/
QPF.IsUniform : {F : Type u → Type u} → [q : QPF F] → Prop
-- Mathlib.Topology.Closure
interior_sInter_subset : ∀ {X : Type u} [inst : TopologicalSpace X] (S : Set (Set X)), interior (⋂₀ S) ⊆ ⋂ s ∈ S, interior s
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_eq_nil_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeGroup α}, x.toWord = [] ↔ x = 1
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Waiter.root.sizeOf_spec : sizeOf Lean.Meta.SynthInstance.Waiter.root = 1
-- Mathlib.Algebra.Polynomial.Degree.Domain
Polynomial.natDegree_mul : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R},
  p ≠ 0 → q ≠ 0 → (p * q).natDegree = p.natDegree + q.natDegree
-- Mathlib.CategoryTheory.Opposites
/-- Compatibility of `Functor.op` with respect to functor composition.  -/
CategoryTheory.Functor.opComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
            (F : CategoryTheory.Functor C D) → (G : CategoryTheory.Functor D E) → (F.comp G).op ≅ F.op.comp G.op
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_eq_ofNat : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Semiring α] [inst_2 : StarRing α] {M : Matrix n n α}
  {d : ℕ} [inst_3 : d.AtLeastTwo], M.conjTranspose = OfNat.ofNat d ↔ M = OfNat.ofNat d
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_zero : ∀ (b : ℕ), b.digits 0 = []
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.iterate_le_nfp : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}) (a : Ordinal.{u_1}) (n : ℕ), f^[n] a ≤ Ordinal.nfp f a
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- `M` acts pretransitively on `α` if for any `x y` there is `g` such that `g • x = y`.
A transitive action should furthermore have `α` nonempty.  -/
MulAction.IsPretransitive : (M : Type u_5) → (α : Type u_6) → [SMul M α] → Prop
-- Mathlib.Order.Filter.Bases.Basic
instInhabitedFilterBasisNat : Inhabited (FilterBasis ℕ)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.mk.inj : ∀ {n length : ℕ} {partSize : Fin length → ℕ} {partSize_pos : ∀ (m : Fin length), 0 < partSize m}
  {emb : (m : Fin length) → Fin (partSize m) → Fin n} {emb_strictMono : ∀ (m : Fin length), StrictMono (emb m)}
  {parts_strictMono : StrictMono fun m => emb m ⟨partSize m - 1, ⋯⟩}
  {disjoint : Set.univ.PairwiseDisjoint fun m => Set.range (emb m)} {cover : ∀ (x : Fin n), ∃ m, x ∈ Set.range (emb m)}
  {length_1 : ℕ} {partSize_1 : Fin length_1 → ℕ} {partSize_pos_1 : ∀ (m : Fin length_1), 0 < partSize_1 m}
  {emb_1 : (m : Fin length_1) → Fin (partSize_1 m) → Fin n}
  {emb_strictMono_1 : ∀ (m : Fin length_1), StrictMono (emb_1 m)}
  {parts_strictMono_1 : StrictMono fun m => emb_1 m ⟨partSize_1 m - 1, ⋯⟩}
  {disjoint_1 : Set.univ.PairwiseDisjoint fun m => Set.range (emb_1 m)}
  {cover_1 : ∀ (x : Fin n), ∃ m, x ∈ Set.range (emb_1 m)},
  { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb, emb_strictMono := emb_strictMono,
        parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover } =
      { length := length_1, partSize := partSize_1, partSize_pos := partSize_pos_1, emb := emb_1,
        emb_strictMono := emb_strictMono_1, parts_strictMono := parts_strictMono_1, disjoint := disjoint_1,
        cover := cover_1 } →
    length = length_1 ∧ partSize ≍ partSize_1 ∧ emb ≍ emb_1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The adjunction between `Y.IdealSheafData` and `(Over Y)ᵒᵖ` given by taking kernels.  -/
AlgebraicGeometry.Scheme.kerAdjunction : (Y : AlgebraicGeometry.Scheme) → (AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor Y).rightOp ⊣ Y.kerFunctor
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.code.takeContentsFn : ℕ → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Init.Data.UInt.Bitwise
UInt8.ofBitVec_and : ∀ (a b : BitVec 8), { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
-- Mathlib.Data.Nat.Find
/-- `Nat.findGreatest P n` is the largest `i ≤ n` such that `P i` holds, or `0` if no such `i`
exists  -/
Nat.findGreatest : (P : ℕ → Prop) → [DecidablePred P] → ℕ → ℕ
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_apply_eq_zero_iff`. -/
Submodule.IsCompl.projection_apply_eq_zero_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) {x : E}, (p.projection q hpq) x = 0 ↔ x ∈ q
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.complexMGF_mul_I : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AEMeasurable X μ →
    ∀ (t : ℝ),
      ProbabilityTheory.complexMGF X μ (↑t * Complex.I) = MeasureTheory.charFun (MeasureTheory.Measure.map X μ) t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.zero.sizeOf_spec : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : SizeOf R],
  sizeOf WeierstrassCurve.Affine.Point.zero = 1
-- Mathlib.Order.Lattice
sup_eq_sup_iff_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_singleton_intCast : ∀ {R : Type u} [inst : NonAssocRing R] (n : ℤ), Subring.closure {↑n} = ⊥
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.coroot_mem_span_int : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base) (i : ι),
  P.coroot i ∈ Submodule.span ℤ (⇑P.coroot '' ↑b.support)