mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialToSimplicialAugmented_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ}
  (f : X ⟶ Y),
  (CategoryTheory.cosimplicialToSimplicialAugmented C).map f =
    Quiver.Hom.op { left := CategoryTheory.NatTrans.leftOp f.right, right := f.left.unop, w := ⋯ }
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.step_filter : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {f : β → Bool},
  (Std.Iter.filter f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ =>
      if h' : f out = true then Std.PlausibleIterStep.yield (Std.Iter.filter f it') out ⋯
      else Std.PlausibleIterStep.skip (Std.Iter.filter f it') ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.filter f it') ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.unmop_inv_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ), (β_ X Y).inv.unmop = (β_ Y.unmop X.unmop).inv
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.exists_lt_of_expect_lt : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulMono ℚ≥0 α] {s : Finset ι} {f : ι → α} {a : α},
  s.Nonempty → (s.expect fun i => f i) < a → ∃ x ∈ s, f x < a
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.ω_mul_e : ∀ {ι : 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}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] (i : ↥b.support),
  RootPairing.GeckConstruction.ω b * RootPairing.GeckConstruction.e i =
    RootPairing.GeckConstruction.f i * RootPairing.GeckConstruction.ω b
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?_eq_match.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Lean.Util.Trace
Lean.trace.profiler.output.pp : Lean.Option Bool
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G)
  {a b : F.CoGrothendieck} (f : a ⟶ b), ((CategoryTheory.Pseudofunctor.CoGrothendieck.map α).map f).base = f.base
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  (G : CategoryTheory.Functor D H) (X : C) {Z : H} (h : G.obj (L.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((L.lanUnit.app (L.comp G)).app X)
      (CategoryTheory.CategoryStruct.comp (((L.lanAdjunction H).counit.app G).app (L.obj X)) h) =
    h
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.toStream_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBSet α cmp}, Std.toStream t = (↑t).toStream
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- An inductive constructor for `ℕ`-indexed chain complexes.

You provide explicitly the first two differentials,
then a function which takes two differentials and the fact they compose to zero,
and returns the next object, its differential, and the fact it composes appropriately to zero.

See also `mk'`, which only sees the previous differential in the inductive step.
 -/
ChainComplex.mk : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (X₀ X₁ X₂ : V) →
        (d₀ : X₁ ⟶ X₀) →
          (d₁ : X₂ ⟶ X₁) →
            CategoryTheory.CategoryStruct.comp d₁ d₀ = 0 →
              ((S : CategoryTheory.ShortComplex V) →
                  (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) →
                ChainComplex V ℕ
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Multiplication version.  -/
Finset.ruzsa_triangle_inequality_mul_mul_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] (A B C : Finset G),
  (A * C).card * B.card ≤ (A * B).card * (B * C).card
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.isMatcherLike : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.AnchorRef.mk : ℕ → UInt64 → Lean.Meta.Grind.AnchorRef
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_of_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α} (hx : x ∈ Set.Icc a b),
  Set.projIcc a b h x = ⟨x, hx⟩
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
/-- An additive subsemigroup `H` of `M` determines an additive
subsemigroup `H.op` of the opposite semigroup `Mᵐᵒᵖ`.  -/
AddSubsemigroup.opEquiv : {M : Type u_2} → [inst : Add M] → AddSubsemigroup M ≃o AddSubsemigroup Mᵃᵒᵖ
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.isBasis'_restrict_iff : ∀ {α : Type u_1} {M : Matroid α} {R I X : Set α}, (M.restrict R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousAddCoePrincipal : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {T : Set ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → Add (R i)]
  [inst_3 : ∀ (i : ι), AddMemClass (S i) (R i)] [∀ (i : ι), ContinuousAdd (R i)],
  ContinuousAdd (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) (Filter.principal T))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} {l : List α} {k : α}
  {h' : k ∈ t.insertManyIfNewUnit l}, (t.insertManyIfNewUnit l)[k] = ()
-- Mathlib.Topology.Category.Profinite.Basic
/-- The limit cone `Profinite.limitCone F` is indeed a limit cone.  -/
Profinite.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J Profinite) → CategoryTheory.Limits.IsLimit (Profinite.limitCone F)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] →
          [IsScalarTower R A A] → [SMulCommClass R A A] → CompleteLattice (NonUnitalSubalgebra R A)
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding_map : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {X Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : X ⟶ Y),
  (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).map f =
    CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map f
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
/-- The bijection `(X' ⟶ Y') ≃ (L.obj X ⟶ L.obj Y)` induced by isomorphisms
`eX : L.obj X ≅ X'` and `eY : L.obj Y ≅ Y'`.  -/
CategoryTheory.Localization.Preadditive.homEquiv : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {L : CategoryTheory.Functor C D} →
          {X Y : C} → {X' Y' : D} → (L.obj X ≅ X') → (L.obj Y ≅ Y') → (X' ⟶ Y') ≃ (L.obj X ⟶ L.obj Y)
-- Lean.Environment
Lean.Kernel.Exception.unknownConstant.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name),
  sizeOf (Lean.Kernel.Exception.unknownConstant env name) = 1 + sizeOf env + sizeOf name
-- Mathlib.Combinatorics.Colex
Finset.Colex.erase_le_erase : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a b : α} [inst_1 : DecidableEq α],
  a ∈ s → b ∈ s → (toColex (s.erase a) ≤ toColex (s.erase b) ↔ b ≤ a)
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.instInhabitedAction.default : {β : Type u} → {α : Type v} → Std.Tactic.BVDecide.LRAT.Action β α
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} {homₚ : (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i}
  {hom : (i : ι) → HP.H i ⟶ HP'.H i}
  {iso_comm :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (HP.iso i).hom (TopPair.incl.whiskerLeft (homₚ i)) =
          CategoryTheory.CategoryStruct.comp (hom i) (HP'.iso i).hom)
      TopPair.HomologyPretheory.Hom.iso_comm._autoParam}
  {w :
    autoParam
      (∀ (i j : ι),
        CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (hom j)) =
          CategoryTheory.CategoryStruct.comp (homₚ i) (HP'.δ i j))
      TopPair.HomologyPretheory.Hom.w._autoParam}
  {homₚ_1 : (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i} {hom_1 : (i : ι) → HP.H i ⟶ HP'.H i}
  {iso_comm_1 :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (HP.iso i).hom (TopPair.incl.whiskerLeft (homₚ_1 i)) =
          CategoryTheory.CategoryStruct.comp (hom_1 i) (HP'.iso i).hom)
      TopPair.HomologyPretheory.Hom.iso_comm._autoParam}
  {w_1 :
    autoParam
      (∀ (i j : ι),
        CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (hom_1 j)) =
          CategoryTheory.CategoryStruct.comp (homₚ_1 i) (HP'.δ i j))
      TopPair.HomologyPretheory.Hom.w._autoParam},
  { homₚ := homₚ, hom := hom, iso_comm := iso_comm, w := w } =
      { homₚ := homₚ_1, hom := hom_1, iso_comm := iso_comm_1, w := w_1 } →
    homₚ = homₚ_1 ∧ hom = hom_1
-- Mathlib.Data.Nat.Totient
Nat.odd_totient_iff_eq_one : ∀ {n : ℕ}, Odd n.totient ↔ n.totient = 1
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log_smul' : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_4 : PartialOrder A] [StarOrderedRing A]
  [NonnegSpectrumClass ℝ A] {r : ℝ} (a : A),
  0 < r →
    autoParam (IsStrictlyPositive a) CFC.log_smul'._auto_1 → CFC.log (r • a) = (algebraMap ℝ A) (Real.log r) + CFC.log a
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C)
  {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso X t).inv.left =
    CategoryTheory.CategoryStruct.id (X.right ⟹ W)
-- Mathlib.Tactic.Algebraize
Mathlib.Tactic.Algebraize.Config.mk.sizeOf_spec : ∀ (properties : Bool), sizeOf { properties := properties } = 1 + sizeOf properties
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
/-- Convert from the base-changed clifford algebra to the clifford algebra over a base-changed
module.  -/
CliffordAlgebra.ofBaseChange : {R : Type u_1} →
  (A : Type u_2) →
    {V : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R V] →
                [inst_5 : Invertible 2] →
                  (Q : QuadraticForm R V) →
                    TensorProduct R A (CliffordAlgebra Q) →ₐ[A] CliffordAlgebra (QuadraticForm.baseChange A Q)
-- Mathlib.Order.Filter.Basic
Filter.frequently_sup : ∀ {α : Type u} {p : α → Prop} {f g : Filter α},
  (∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Fintype.piFinset_add : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Add (α i)] (s t : (i : ι) → Finset (α i)),
  (Fintype.piFinset fun i => s i + t i) = Fintype.piFinset s + Fintype.piFinset t
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.doubleCoset_eq_of_mem : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {a b : G},
  b ∈ DoubleCoset.doubleCoset a ↑H ↑K → DoubleCoset.doubleCoset b ↑H ↑K = DoubleCoset.doubleCoset a ↑H ↑K
-- Mathlib.Analysis.Complex.Norm
Complex.lim_im : ∀ (f : CauSeq ℂ fun x => ‖x‖), (Complex.cauSeqIm f).lim = f.lim.im
-- Mathlib.Data.Set.Function
Set.LeftInvOn.image_image' : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : α → β} {f' : β → α},
  Set.LeftInvOn f' f s → s₁ ⊆ s → f' '' f '' s₁ = s₁
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₂ → (m₁ \ m₂).get? k = none
-- Mathlib.Algebra.Category.Grp.Basic
_private.Mathlib.Algebra.Category.Grp.Basic.0.AddCommGrpCat.Hom.mk : {A B : AddCommGrpCat} → (↑A →+ ↑B) → A.Hom B
-- Mathlib.Logic.Equiv.List
_private.Mathlib.Logic.Equiv.List.0.Encodable.encodeList.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match [] with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_1 ()
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_some_getD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, a ∈ t → t[a]? = some (t.getD a fallback)
-- Std.Http.Server.Config
/-- Maximum number of bytes consumed while parsing one chunk-size line with extensions (default: 8192 bytes).
 -/
Std.Http.Config.maxChunkLineLength : Std.Http.Config → ℕ
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instSMulSubtypeMem_1 : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {S : IntermediateField K L} →
            {E : Type u_4} → [inst_3 : Field E] → [inst_4 : Algebra L E] → (T : IntermediateField (↥S) E) → SMul ↥S ↥T
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.isEmpty.eq_1 : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α] (r : Std.Rcc α),
  r.isEmpty = decide ¬r.lower ≤ r.upper
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α) (f : β → β), (t₁.modify k f).Equiv (t₂.modify k f)
-- Mathlib.Order.Filter.Cofinite
le_cofinite_iff_boundary : ∀ {α : Type u_2} {f : Filter α}, f ≤ Filter.cofinite ↔ Coheyting.boundary f = f
-- Init.Data.Order.Classes
/-- This typeclass states that being less or equal to `Max.max a b` is equivalent to being less or
equal to both `a` and `b`.
 -/
Std.LawfulOrderSup : (α : Type u) → [Max α] → [LE α] → Prop
-- Mathlib.Algebra.Group.Subgroup.Defs
HasMemOrInvMem.mem_of_inv_notMem : ∀ {S : Type u_3} {G : Type u_4} [inst : Inv G] [inst_1 : SetLike S G] (s : S) [HasMemOrInvMem s] (x : G),
  x⁻¹ ∉ s → x ∈ s
-- Mathlib.Algebra.Group.End
_private.Mathlib.Algebra.Group.End.0.Equiv.Perm.inv_aux : ∀ {α : Type u_4} {p : α → Prop} {f : Equiv.Perm α}, (∀ (x : α), p (f x) ↔ p x) ↔ ∀ (x : α), p (f⁻¹ x) ↔ p x
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
/-- If the underlying map of a morphism is inducing and has closed range, then it is affine.  -/
AlgebraicGeometry.isAffineHom_of_isInducing : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  Topology.IsInducing ⇑f → IsClosed (Set.range ⇑f) → AlgebraicGeometry.IsAffineHom f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k)[k]? = none
-- Lean.Elab.Tactic.Omega.OmegaM
Lean.Elab.Tactic.Omega.Context.mk.inj : ∀ {cfg cfg_1 : Lean.Meta.Omega.OmegaConfig}, { cfg := cfg } = { cfg := cfg_1 } → cfg = cfg_1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesCokernel.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.Limits.PreservesCokernel.iso G f = CategoryTheory.Limits.PreservesCokernel.iso G f
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.mk.injEq : ∀ {B : Type u_1} {M : CoxeterMatrix B} {W : Type u_2} [inst : Group W] (mulEquiv mulEquiv_1 : W ≃* M.Group),
  ({ mulEquiv := mulEquiv } = { mulEquiv := mulEquiv_1 }) = (mulEquiv = mulEquiv_1)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.comap_id : ∀ {A : Type u_1} {σ : Type u_4} {ι : Type u_7} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  {I : HomogeneousIdeal 𝒜}, HomogeneousIdeal.comap (GradedRingHom.id 𝒜) I = I
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyGE!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKeyGE! k = t₂.getKeyGE! k
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.ysq_dvd_yy : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.yn a1 n * Pell.yn a1 n ∣ Pell.yn a1 (n * Pell.yn a1 n)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.mul_def : ∀ {k : Type u_1} {G : Type u_2} [inst : Mul G] [inst_1 : SMul G k] [inst_2 : NonUnitalNonAssocSemiring k]
  {f g : SkewMonoidAlgebra k G},
  f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => SkewMonoidAlgebra.single (a₁ * a₂) (b₁ * a₁ • b₂)
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int32.ofInt 48 = 48`
* `Int32.ofInt (-129) = -129`
* `Int32.ofInt 70000 = 70000`
* `Int32.ofInt (-40000) = -40000`
* `Int32.ofInt 2147483648 = -2147483648`
* `Int32.ofInt (-2147483649) = 2147483647`
 -/
Int32.ofInt : ℤ → Int32
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.toEquiv_piCongrRight : ∀ {ι : Type u_7} {Y₁ : ι → Type u_8} {Y₂ : ι → Type u_9} [inst : (i : ι) → TopologicalSpace (Y₁ i)]
  [inst_1 : (i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i),
  (Homeomorph.piCongrRight F).toEquiv = Equiv.piCongrRight fun i => (F i).toEquiv
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.zero_opow : ∀ {a : Ordinal.{u_1}}, a ≠ 0 → 0 ^ a = 0
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.exists_mk : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α ⧸ s → Prop}, (∃ x, C x) ↔ ∃ x, C ↑x
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_associator_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  Bicategory.Opposite.op2 (CategoryTheory.Bicategory.associator f g h).hom =
    (CategoryTheory.Bicategory.associator h.op g.op f.op).symm.hom
-- Init.Data.UInt.Bitwise
UInt8.shiftLeft_or : ∀ {a b c : UInt8}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
IsStrongFEPair.symm_Λ_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → P.symm.Λ = mellin P.g
-- Mathlib.Data.List.Basic
List.getLastI.eq_4 : ∀ {α : Type u_1} [inst : Inhabited α] (head head_1 : α) (l : List α),
  (l = [] → False) → (head :: head_1 :: l).getLastI = l.getLastI
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
hasSum_jacobiTheta₂_term : ∀ (z : ℂ) {τ : ℂ}, 0 < τ.im → HasSum (fun n => jacobiTheta₂_term n z τ) (jacobiTheta₂ z τ)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Given `p` a polynomial being inserted into `lowers`, `uppers`, or `diseqs`,
get its leading variable `y`, and adds `y` as an occurrence for the remaining variables in `p`.
 -/
Lean.Grind.Linarith.Poly.updateOccs : Lean.Grind.Linarith.Poly → Lean.Meta.Grind.Arith.Linear.LinearM Unit
-- Lean.Data.KVMap
/-- Update a `Bool` entry based on its current value.  -/
Lean.KVMap.updateBool : Lean.KVMap → Lean.Name → (Bool → Bool) → Lean.KVMap
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- A family with at most one point is affinely independent.  -/
affineIndependent_of_subsingleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [Subsingleton ι] (p : ι → P), AffineIndependent k p
-- Std.Time.Format.Modifier
Std.Time.instInhabitedFraction.default : Std.Time.Fraction
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.mem_op : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {x : Rᵐᵒᵖ} {S : Subsemiring R}, x ∈ S.op ↔ MulOpposite.unop x ∈ S
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_equiv_comp : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring T] (f : R →+* S)
  (e : S ≃+* T), RingHom.ker (e.toRingHom.comp f) = RingHom.ker f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.addMonoid.eq_1 : ∀ {α : Type u_2} [inst : AddMonoid α],
  Set.addMonoid =
    { toAddSemigroup := Set.addSemigroup, toZero := Set.addZeroClass.toZero, zero_add := ⋯, add_zero := ⋯,
      toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The equivalence between `ContinuousLinearMapWOT` and `ContinuousLinearMap`.  -/
ContinuousLinearMapWOT.equiv : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] → [inst_7 : Module 𝕜₂ F] → (E →SWOT[σ] F) ≃ (E →SL[σ] F)
-- Init.System.IOError
IO.Error.mkHardwareFault : UInt32 → String → IO.Error
-- Mathlib.Topology.SeparatedMap
IsLocallyInjective.isOpen_eqLocus : ∀ {X : Type u_1} {Y : Type u_2} {A : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace A] {f : X → Y}
  {g₁ g₂ : A → X}, Continuous g₁ → Continuous g₂ → IsLocallyInjective f → f ∘ g₁ = f ∘ g₂ → IsOpen {a | g₁ a = g₂ a}
-- Mathlib.GroupTheory.Commutator.Basic
one_mem_commutatorSet : ∀ (G : Type u_1) [inst : Group G], 1 ∈ commutatorSet G
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.aemeasurable_of_aemeasurable_exp_mul : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α} {t : ℝ},
  t ≠ 0 → AEMeasurable (fun x => Real.exp (t * f x)) μ → AEMeasurable f μ
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.eq_1 : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] (A : Matrix n n α), A.IsHermitian = (A.conjTranspose = A)
-- Init.Data.String.Basic
String.Pos.Raw.IsValid.append_left : ∀ {t : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid t p → ∀ (s : String), String.Pos.Raw.IsValid (s ++ t) (s + p)