mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {T : CategoryTheory.Over A} {X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A}
  (f : (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).obj X ⟶ T),
  (CategoryTheory.overEquivPresheafCostructuredArrow A).inverse.map
      ((CategoryTheory.ConcreteCategory.hom
          ((CategoryTheory.CostructuredArrow.toOverCompYoneda A T).hom.app (Opposite.op X)))
        f) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X)
      (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.overEquivPresheafCostructuredArrow A).unit.app T))
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derived_counit : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂) [inst_4 : L₁.IsLocalization W₁]
  [inst_5 : L₂.IsLocalization W₂] {G' : CategoryTheory.Functor D₁ D₂} {F' : CategoryTheory.Functor D₂ D₁}
  (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [inst_6 : G'.IsLeftDerivedFunctor α W₁]
  [inst_7 : F'.IsRightDerivedFunctor β W₂]
  [inst_8 :
    (G'.comp F').IsLeftDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (L₁.associator G' F').inv (CategoryTheory.Functor.whiskerRight α F')) W₁]
  [inst_9 :
    (F'.comp G').IsRightDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂],
  (adj.derived W₁ W₂ α β).counit = adj.derivedε W₂ α β
-- Mathlib.Algebra.Homology.BifunctorFlip
HomologicalComplex.hasMapBifunctor_flip_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c],
  K₂.HasMapBifunctor K₁ F.flip c ↔ K₁.HasMapBifunctor K₂ F c
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.isZero : Nat.Internal.Linear.Poly → Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
NNReal.pi_ne_zero : NNReal.pi ≠ 0
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.transpose_mem : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R}, A ∈ Matrix.symplecticGroup l R → A.transpose ∈ Matrix.symplecticGroup l R
-- Init.Meta.Defs
/-- Adds an element to the end of a separated array, adding a separator as needed.
 -/
Lean.Syntax.TSepArray.push : {k : Lean.SyntaxNodeKinds} → {sep : String} → Lean.Syntax.TSepArray k sep → Lean.TSyntax k → Lean.Syntax.TSepArray k sep
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.disjoint : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  IsAddQuotientCoveringMap f G → ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g = 0
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
TensorProduct.mapIncl.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid P]
  [inst_2 : AddCommMonoid Q] [inst_3 : Module R P] [inst_4 : Module R Q] (p : Submodule R P) (q : Submodule R Q),
  TensorProduct.mapIncl p q = TensorProduct.map p.subtype q.subtype
-- Mathlib.Algebra.Order.AddGroupWithTop
add_right_inj_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] {a b c : α}, a ≠ ⊤ → (a + b = a + c ↔ b = c)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.getUnsolvedGoalMVarIds : Lean.Elab.Tactic.Grind.GrindTacticM (List Lean.MVarId)
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.sub_one_ne_zero : ∀ {p q : ℝ}, p.HolderConjugate q → p - 1 ≠ 0
-- Mathlib.Data.TwoPointing
TwoPointing.swap_toProd : ∀ {α : Type u_1} (p : TwoPointing α), p.swap.toProd = (p.toProd.2, p.toProd.1)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.one_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A]
  [inst_3 : Star A] (a : A), 1 a = a
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.instCountable_fg_substructures_of_countable : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [Countable M], Countable { S // S.FG }
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.Category.toCategoryStruct : {obj : Type u} → [self : CategoryTheory.Category.{v, u} obj] → CategoryTheory.CategoryStruct.{v, u} obj
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isGE_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (e : X ≅ Y) (n : ℤ) [t.IsGE X n], t.IsGE Y n
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_list_count_of_subset : ∀ {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq M] (m : List M) (s : Finset M),
  m.toFinset ⊆ s → m.prod = ∏ i ∈ s, i ^ List.count i m
-- Mathlib.Algebra.Order.Floor.Div
floorDiv_le_ceilDiv : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [PosSMulReflectLE α β] [inst_6 : FloorDiv α β]
  [inst_7 : CeilDiv α β] {a : α} {b : β}, b ⌊/⌋ a ≤ b ⌈/⌉ a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} {fallback : β k}, m₂.contains k = true → (m₁.diff m₂).getD k fallback = fallback
-- Mathlib.MeasureTheory.Integral.Pi
MeasureTheory.integral_eval : ∀ {ι : Type u_2} [inst : Fintype ι] {X : ι → Type u_3} {mX : (i : ι) → MeasurableSpace (X i)}
  {μ : (i : ι) → MeasureTheory.Measure (X i)} [inst_1 : (i : ι) → NormedAddCommGroup (X i)]
  [inst_2 : (i : ι) → NormedSpace ℝ (X i)] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {i : ι}
  [OpensMeasurableSpace (X i)] [SecondCountableTopology (X i)],
  ∫ (x : (i : ι) → X i), x i ∂MeasureTheory.Measure.pi μ = ∫ (x : X i), x ∂μ i
-- Init.Data.Vector.Basic
/-- Extracts the slice of a vector from indices `start` to `stop` (exclusive). If `start ≥ stop`, the
result is empty. If `stop` is greater than the size of the vector, the size is used instead.
 -/
Vector.extract : {α : Type u_1} → {n : ℕ} → Vector α n → (start : optParam ℕ 0) → (stop : optParam ℕ n) → Vector α (min stop n - start)
-- Lean.LocalContext
Lean.LocalContext.getFromUserName! : Lean.LocalContext → Lean.Name → Lean.LocalDecl
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.map_comp_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasCoend F']
  (f : F ⟶ F') {F'' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_4 : CategoryTheory.Limits.HasCoend F''] (g : F' ⟶ F'') {Z : C} (h : CategoryTheory.Limits.coend F'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.map g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.map (CategoryTheory.CategoryStruct.comp f g)) h
-- Mathlib.Algebra.Group.TypeTags.Basic
toMul_nsmul : ∀ {α : Type u} [inst : Monoid α] (n : ℕ) (a : Additive α), Additive.toMul (n • a) = Additive.toMul a ^ n
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.forget_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y : CategoryTheory.AddGrp C} (f : X ⟶ Y), (CategoryTheory.AddGrp.forget C).map f = f.hom.hom
-- Mathlib.Topology.Sets.Opens
/-- The `TopologicalSpace.Opens.carrier _` is an open set.  -/
TopologicalSpace.Opens.is_open' : ∀ {α : Type u_2} [inst : TopologicalSpace α] (self : TopologicalSpace.Opens α), IsOpen self.carrier
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAddCommMonoid.eq_1 : ∀ {R : Type u_1} [inst : AddCommMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S],
  AddOreLocalization.instAddCommMonoid = { toAddMonoid := AddOreLocalization.instAddMonoid, add_comm := ⋯ }
-- Init.Data.UInt.Lemmas
UInt16.add_left_inj : ∀ {a b : UInt16} (c : UInt16), a + c = b + c ↔ a = b
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Iic_castLE : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a : Fin n),
  ∏ i ≤ Fin.castLE h a, f i = ∏ i ≤ a, f (Fin.castLE h i)
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.functorCategory.eq_1 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v, u_2} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (x x_1 : CategoryTheory.Functor J C) (f : x ⟶ x_1),
  W.functorCategory J f = ∀ (j : J), W (f.app j)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.keysArray.isEmpty = t.isEmpty
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fst_one : ∀ {R : Type u_1} {A : Type u_2} [inst : One R] [inst_1 : Zero A], (Unitization.toProd 1).1 = 1
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_dual : ∀ {α : Type u_1} (t : Ordnode α), t.dual.dual = t
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- `bifunctorComp₁₂` can be described in terms of the curryfication of functors.  -/
CategoryTheory.Functor.bifunctorComp₁₂Iso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₁₂ : Type u_3} →
      {C₃ : Type u_4} →
        {E : Type u_9} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_3} C₁₂] →
                  [inst_4 : CategoryTheory.Category.{v_9, u_9} E] →
                    (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) →
                      (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ E)) →
                        CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅
                          CategoryTheory.Functor.curry.obj ((CategoryTheory.Functor.uncurry.obj F₁₂).comp G)
-- Mathlib.Data.Matrix.Composition
Matrix.comp.eq_1 : ∀ (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5),
  Matrix.comp I J K L R =
    { toFun := fun m ik jl => m ik.1 jl.1 ik.2 jl.2, invFun := fun n i j k l => n (i, k) (j, l), left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.RingTheory.Algebraic.Basic
/-- **Alias** of the reverse direction of `IsAlgebraic.inv_iff`. -/
IsAlgebraic.inv : ∀ {R : Type u} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] {x : K},
  IsAlgebraic R x → IsAlgebraic R x⁻¹
-- Init.Data.Ord.Basic
Ordering.isGT_lt : Ordering.lt.isGT = false
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α} {f : Option β → Option β},
  (Std.ExtDHashMap.Const.alter m k f).getKey! k =
    if (f (Std.ExtDHashMap.Const.get? m k)).isSome = true then k else default
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimAltInfo.mk.sizeOf_spec : ∀ (name : Lean.Name) (declName? : Option Lean.Name) (numFields : ℕ) (provesMotive : Bool),
  sizeOf { name := name, declName? := declName?, numFields := numFields, provesMotive := provesMotive } =
    1 + sizeOf name + sizeOf declName? + sizeOf numFields + sizeOf provesMotive
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.toEquiv_inclusion_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N} (h : f ≤ g) (x : ↥f.dom),
  g.toEquiv ((FirstOrder.Language.Substructure.inclusion ⋯) x) =
    (FirstOrder.Language.Substructure.inclusion ⋯) (f.toEquiv x)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.tr_respects : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {Λ : Type u_2} [inst_1 : Inhabited Λ] (M : Turing.TM0.Machine Γ Λ),
  StateTransition.Respects (Turing.TM0.step M) (Turing.TM1.step (Turing.TM0to1.tr M)) fun a b =>
    Turing.TM0to1.trCfg M a = b
-- Mathlib.Order.MinMax
instLawfulOrderSup_mathlib : ∀ {α : Type u} [inst : LinearOrder α], Std.LawfulOrderSup α
-- Mathlib.Algebra.Algebra.Defs
/-- `mul_comm` for `Algebra`s when one element is from the base ring.  -/
Algebra.commutes : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R) (x : A),
  (algebraMap R A) r * x = x * (algebraMap R A) r
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.finsuppAntidiag.eq_1 : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] (s : Finset ι) (n : μ),
  s.finsuppAntidiag n =
    Finset.map { toFun := fun f => { support := {x ∈ s | ↑f x ≠ 0}, toFun := ↑f, mem_support_toFun := ⋯ }, inj' := ⋯ }
      (s.piAntidiag n).attach
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.truth_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ),
  (CategoryTheory.Presheaf.truth C).app X = TypeCat.ofHom fun x => ⊤
-- Mathlib.Data.Fintype.EquivFin
Function.Embedding.exists_of_card_le_finset : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] {s : Finset β}, Fintype.card α ≤ s.card → ∃ f, Set.range ⇑f ⊆ ↑s
-- Std.Data.TreeSet.Basic
Std.TreeSet.mk : {α : Type u} → {cmp : autoParam (α → α → Ordering) Std.TreeSet._auto_1} → Std.TreeMap α Unit cmp → Std.TreeSet α cmp
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.descShortComplex_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (f : S₁ ⟶ S₂) {Z : CochainComplex C ℤ} (h : S₂.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.descShortComplex S₂) h) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.descShortComplex S₁)
      (CategoryTheory.CategoryStruct.comp f.τ₃ h)
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.DHashMap.Const.toList.eq_1 : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} (m : Std.DHashMap α fun x => β),
  Std.DHashMap.Const.toList m = Std.DHashMap.Raw.Const.toList m.inner
-- Mathlib.LinearAlgebra.Dimension.Localization
IsBaseChange.finrank_eq : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {T : Type uT}
  [inst_3 : CommRing T] [NoZeroDivisors T] [inst_5 : Algebra R T] [FaithfulSMul R T] {P : Type uP}
  [inst_7 : AddCommGroup P] [inst_8 : Module R P] [inst_9 : Module T P] [inst_10 : IsScalarTower R T P] {g : M →ₗ[R] P},
  IsBaseChange T g → Module.finrank T P = Module.finrank R M
-- Mathlib.Analysis.Convex.Basic
convex_uIcc : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : LinearOrder β] [IsOrderedAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulMono 𝕜 β] (r s : β),
  Convex 𝕜 (Set.uIcc r s)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.sub.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.IsPrimitive.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R), p.IsPrimitive = ∀ (r : R), Polynomial.C r ∣ p → IsUnit r
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.includeRight_apply : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (a : B), (GradedTensorProduct.includeRight 𝒜 ℬ) a = 1 ᵍ⊗ₜ[R] a
-- Init.Meta.Defs
Lean.Syntax.setInfo : Lean.SourceInfo → Lean.Syntax → Lean.Syntax
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.isStableUnderBaseChangeAgainst_top_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.IsStableUnderBaseChangeAgainst ⊤ ↔ P.IsStableUnderBaseChange
-- Mathlib.RingTheory.Ideal.Over
Ideal.isPrime_of_liesOver : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [P.LiesOver p] [P.IsPrime], p.IsPrime
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The `MonoidHom` from a profinite group `P` to the projective limit of its quotients by
open normal subgroups ordered by inclusion  -/
ProfiniteGrp.toLimitFun : (P : ProfiniteGrp.{u}) → ↑P.toProfinite.toTop →* ↑(ProfiniteGrp.limit P.diagram).toProfinite.toTop
-- Mathlib.Analysis.Analytic.Basic
hasFPowerSeriesWithinAt_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFPowerSeriesWithinAt f p Set.univ x ↔ HasFPowerSeriesAt f p x
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.inv_lt_one_iff`.

---

Uses `left` co(ntra)variant.  -/
inv_lt_one' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a : α}, a⁻¹ < 1 ↔ 1 < a
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_eq_if : ∀ {m n : ℤ}, (m...=n).toList = if m ≤ n then m :: ((m + 1)...=n).toList else []
-- Mathlib.Topology.Category.TopPair
/-- The inclusion functor is left adjoint to the projection to the first component.  -/
TopPair.inclAdjProj₁ : TopPair.incl ⊣ TopPair.proj₁
-- Init.Data.Vector.Lemmas
Vector.toArray_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β → γ} {as : Vector α n} {bs : Vector β n},
  (Vector.zipWith f as bs).toArray = Array.zipWith f as.toArray bs.toArray
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.finset_sup_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : SemilatticeSup β]
  [inst_2 : OrderBot β] {f : γ → MeasureTheory.SimpleFunc α β} (s : Finset γ) (a : α),
  (s.sup f) a = s.sup fun c => (f c) a
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.hasDerivAt_sigmoid : ∀ (x : ℝ), HasDerivAt Real.sigmoid (x.sigmoid * (1 - x.sigmoid)) x
-- Mathlib.Analysis.Normed.Module.FiniteDimension
LinearMap.exists_antilipschitzWith : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F), f.ker = ⊥ → ∃ K > 0, AntilipschitzWith K ⇑f
-- Mathlib.Order.Fin.Basic
/-- `predAbove` is injective at the pivot  -/
Fin.predAbove_left_injective : ∀ {n : ℕ}, Function.Injective Fin.predAbove
-- Mathlib.GroupTheory.SchurZassenhaus
/-- **Schur-Zassenhaus** for normal subgroups:
If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
subgroup `K` which is a (right) complement of `H`.  -/
Subgroup.exists_right_complement'_of_coprime : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ElimStatus.failure.inj : ∀ {ts ts_1 : List Lean.Expr},
  Mathlib.Tactic.Choose.ElimStatus.failure ts = Mathlib.Tactic.Choose.ElimStatus.failure ts_1 → ts = ts_1
-- Mathlib.Data.Nat.Log
Nat.log_pow : ∀ {b : ℕ}, 1 < b → ∀ (x : ℕ), Nat.log b (b ^ x) = x
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion₂_sub : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Sub α] (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋃ i, ⋃ j, s i j) - t = ⋃ i, ⋃ j, s i j - t
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The canonical quotient map `FreeTensorAlgebra R A →ₐ[R] FreeProduct R A`,
as an `R`-algebra homomorphism  -/
LinearAlgebra.FreeProduct.mkAlgHom : {I : Type u} →
  [inst : DecidableEq I] →
    (R : Type v) →
      [inst_1 : CommSemiring R] →
        (A : I → Type w) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] →
              LinearAlgebra.FreeProduct.FreeTensorAlgebra R A →ₐ[R] LinearAlgebra.FreeProduct R A
-- Lean.MetavarContext
/-- Set of unassigned metavariables being abstracted.  -/
Lean.MetavarContext.MkBinding.Context.mvarIdsToAbstract : Lean.MetavarContext.MkBinding.Context → Lean.MVarIdSet
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
GaloisConnection.l_ciSup_set_of_directedOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompletePartialOrderSup α]
  [inst_1 : ConditionallyCompletePartialOrderSup β] {l : α → β} {u : β → α},
  GaloisConnection l u →
    ∀ {s : Set γ} {f : γ → α},
      DirectedOn (fun x1 x2 => x1 ≤ x2) (f '' s) → BddAbove (f '' s) → s.Nonempty → l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_shiftLeftZeroExtend : ∀ {w n : ℕ} {x : BitVec w}, (x.shiftLeftZeroExtend n).toNat = x.toNat <<< n
-- Mathlib.Tactic.Ring.Common
/-- The value represented by `e`. Should not be zero.  -/
Mathlib.Tactic.Ring.RatCoeff.value : {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.RatCoeff e → ℚ
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- If `w` is a nontorsion weight function, then a multivariate polynomial has weighted total
degree zero if and only if for every `m ∈ p.support` and `x : σ`, `m x = 0`.  -/
MvPolynomial.weightedTotalDegree_eq_zero_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : LinearOrder M] [inst_3 : OrderBot M] [CanonicallyOrderedAdd M] {w : σ → M},
  MvPolynomial.NonTorsionWeight w →
    ∀ (p : MvPolynomial σ R), MvPolynomial.weightedTotalDegree w p = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0