mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_intOfNat : ∀ {n n' : ℕ}, Mathlib.Meta.NormNum.IsNat n n' → Mathlib.Meta.NormNum.IsNat (Int.ofNat n) n'
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.inv : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i}
  [inst_2 : (i : ι) → Group (β i)] [∀ (i : ι), ContinuousInv (β i)],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.StronglyAdapted f u⁻¹
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.sdiff : ∀ {α : Type u} {s t : Set α}, s.Finite → (s \ t).Finite
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_eq_neg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  [NonnegSpectrumClass ℝ A] (a : A), a⁻ = -a ↔ a ≤ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.prod_σ_fst : ∀ (X Y : SSet) {n : ℕ} (i : Fin (n + 1))
  (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj (Opposite.op { len := n })),
  ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.SimplicialObject.σ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i))
        z).1 =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i)) z.1
-- Mathlib.Analysis.InnerProductSpace.MulOpposite
MulOpposite.inner_op : ∀ {𝕜 : Type u_1} {H : Type u_2} [inst : Inner 𝕜 H] (x y : H),
  inner 𝕜 (MulOpposite.op x) (MulOpposite.op y) = inner 𝕜 x y
-- Mathlib.Topology.Algebra.ConstMulAction
continuousOn_const_smul_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] [inst_4 : TopologicalSpace β] {f : β → α} {s : Set β} (c : G),
  ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_mod_of_dvd : ∀ (a : Ordinal.{u_4}) {b c : Ordinal.{u_4}}, c ∣ b → a % b % c = a % c
-- Lean.ToLevel
/-- A class to create `Level` expressions that denote particular universe levels in Lean.
`Lean.ToLevel.toLevel.{u}` evaluates to a `Lean.Level` term representing `u`  -/
Lean.ToLevel : Type
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insert k v).getKey k ⋯ = k
-- Mathlib.Topology.NhdsWithin
DenseRange.nhdsWithin_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_5} {f : ι → α},
  DenseRange f → ∀ (x : α), (nhdsWithin x (Set.range f)).NeBot
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none
-- Lean.Meta.Basic
/-- Returns `true` if `mvarId := val` was successfully assigned.
This method uses the same assignment validation performed by `isDefEq`, but it does not check whether the types match.
 -/
Lean.MVarId.checkedAssign : Lean.MVarId → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.Algebra.Group.Basic
/-- A subgroup `S` of an additive topological group `G` acts on `G` properly discontinuously
on the right, if it is discrete in the sense that `S ∩ K` is finite for all compact `K`.
(See also `DiscreteTopology`.)

If `G` is Hausdorff, this can be combined with `t2Space_of_properlyDiscontinuousVAdd_of_t2Space`
to show that the quotient group `G ⧸ S` is Hausdorff.  -/
AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G),
  Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G) → ProperlyDiscontinuousVAdd (↥S.op) G
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries.congr_simp : ∀ (𝕂 : Type u_1) (𝔸 : Type u_2) [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (n : ℕ), NormedSpace.expSeries 𝕂 𝔸 n = NormedSpace.expSeries 𝕂 𝔸 n
-- Batteries.Data.List.Basic
List.replaceFTR.go.eq_2 : ∀ {α : Type u_1} (f : α → Option α) (a : Array α) (x_2 : α) (xs : List α),
  List.replaceFTR.go f (x_2 :: xs) a =
    match f x_2 with
    | none => List.replaceFTR.go f xs (a.push x_2)
    | some a' => a.toListAppend (a' :: xs)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.forgetReflectIsos : (CategoryTheory.forget CommRingCat).ReflectsIsomorphisms
-- Aesop.Forward.Match
/-- Returns `true` if the match contains the given hyp.  -/
Aesop.Match.containsHyp : Lean.FVarId → Aesop.Match → Bool
-- Lean.Meta.Tactic.Grind.EMatch
/-- Returns `true` if the function `pFn` of a pattern is equivalent to the function `eFn`.
Recall that we ignore universe levels in patterns.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.eqvFunctions : Lean.Expr → Lean.Expr → Bool
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.mk.injEq : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (obj : (j : J) → CategoryTheory.Limits.Cocone (F.obj j))
  (map : {j j' : J} → (f : j ⟶ j') → obj j ⟶ (CategoryTheory.Limits.Cocone.precompose (F.map f)).obj (obj j'))
  (id :
    autoParam (∀ (j : J), (map (CategoryTheory.CategoryStruct.id j)).hom = CategoryTheory.CategoryStruct.id (obj j).pt)
      CategoryTheory.Limits.DiagramOfCocones.id._autoParam)
  (comp :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (map f).hom (map g).hom)
      CategoryTheory.Limits.DiagramOfCocones.comp._autoParam)
  (obj_1 : (j : J) → CategoryTheory.Limits.Cocone (F.obj j))
  (map_1 : {j j' : J} → (f : j ⟶ j') → obj_1 j ⟶ (CategoryTheory.Limits.Cocone.precompose (F.map f)).obj (obj_1 j'))
  (id_1 :
    autoParam
      (∀ (j : J), (map_1 (CategoryTheory.CategoryStruct.id j)).hom = CategoryTheory.CategoryStruct.id (obj_1 j).pt)
      CategoryTheory.Limits.DiagramOfCocones.id._autoParam)
  (comp_1 :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map_1 (CategoryTheory.CategoryStruct.comp f g)).hom =
          CategoryTheory.CategoryStruct.comp (map_1 f).hom (map_1 g).hom)
      CategoryTheory.Limits.DiagramOfCocones.comp._autoParam),
  ({ obj := obj, map := map, id := id, comp := comp } = { obj := obj_1, map := map_1, id := id_1, comp := comp_1 }) =
    (obj = obj_1 ∧ map ≍ map_1)
-- Mathlib.GroupTheory.Congruence.Opposite
/-- The multiplicative congruences on `M` bijects to the multiplicative congruences on `Mᵐᵒᵖ`
 -/
Con.orderIsoOp : {M : Type u_1} → [inst : Mul M] → Con M ≃o Con Mᵐᵒᵖ
-- Mathlib.Order.Defs.Unbundled
MaximalFor.eq_1 : ∀ {ι : Sort u_1} {α : Type u_2} [inst : LE α] (P : ι → Prop) (f : ι → α) (i : ι),
  MaximalFor P f i = (P i ∧ ∀ ⦃j : ι⦄, P j → f i ≤ f j → f j ≤ f i)
-- Mathlib.Data.Rat.Floor
Int.mod_nat_eq_sub_mul_floor_rat_div : ∀ {n : ℤ} {d : ℕ}, n % ↑d = n - ↑d * ⌊↑n / ↑d⌋
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.singleton_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (x : PUnit.{w + 1}),
  (CategoryTheory.PreZeroHypercover.singleton f).f x = f
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.succ_lt_iff : ∀ {α : Type u_1} {a b : α} [inst : PartialOrder α] [inst_1 : SuccOrder α],
  Order.IsSuccPrelimit b → (Order.succ a < b ↔ a < b)
-- Mathlib.Topology.Algebra.Algebra
Algebra.elemental.instCommSemiringSubtypeMemSubalgebraOfT2Space : (R : Type u_1) →
  [inst : CommSemiring R] →
    {A : Type u} →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : IsSemitopologicalSemiring A] → [T2Space A] → {x : A} → CommSemiring ↥(Algebra.elemental R x)
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_generatePiSystem : ∀ {α : Type u_1} (S : Set (Set α)), IsPiSystem (generatePiSystem S)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPairIsoMk_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (p : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
  (q : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) q.hom =
        CategoryTheory.CategoryStruct.comp p.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
      CategoryTheory.Limits.parallelPairIsoMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) q.hom =
        CategoryTheory.CategoryStruct.comp p.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
      CategoryTheory.Limits.parallelPairIsoMk._auto_3)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.parallelPairIsoMk p q hl hr).inv.app X =
    (CategoryTheory.Limits.WalkingParallelPair.rec p q X).inv
-- Mathlib.Order.Bounds.Basic
/-- If `s` has a greatest lower bound, then it is bounded below.  -/
IsGLB.bddBelow : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsGLB s a → BddBelow s
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- The pointwise topology on `MvPowerSeries`  -/
MvPowerSeries.WithPiTopology.instTopologicalSpace : {σ : Type u_1} → (R : Type u_2) → [TopologicalSpace R] → TopologicalSpace (MvPowerSeries σ R)
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.instStar : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → [CompleteSpace E] → Star (E →ₗ.[𝕜] E)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.mk.injEq : ∀ (carrier : Type u) [str : AddMonoid carrier] (carrier_1 : Type u) (str_1 : AddMonoid carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.nextCoeff_pow : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → ∀ (n : ℕ), (p ^ n).nextCoeff = n • p.nextCoeff
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.of_injOn : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} {t : Set β}, Set.MapsTo f s t → Set.InjOn f s → t.Finite → s.Finite
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The chosen cowedge for each functor `Jᵒᵖ ⥤ J ⥤ C`.  -/
CategoryTheory.Limits.ChosenCoendsOfShape.cowedge : {J : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} J} →
    {C : Type u_2} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} C} →
        [self : CategoryTheory.Limits.ChosenCoendsOfShape J C] →
          (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) → CategoryTheory.Limits.Cowedge F
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.isPreconnected_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y),
  IsPreconnected (⇑h ⁻¹' s) ↔ IsPreconnected s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, a ∈ t.insertIfNew k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Init.Grind.AC
Lean.Grind.AC.diseq_erase0 : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  {x : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)} (lhs rhs lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_erase0_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Seq.denote ctx lhs ≠ Lean.Grind.AC.Seq.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' ≠ Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.divisionMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : Inv M₁]
  [inst_4 : Div M₁] [inst_5 : Pow M₁ ℤ] [inst_6 : DivisionMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Injective.divisionMonoid f hf one mul inv div npow zpow =
    { toDivInvMonoid := Function.Injective.divInvMonoid f hf one mul inv div npow zpow, inv_inv := ⋯, mul_inv_rev := ⋯,
      inv_eq_of_mul := ⋯ }
-- Init.Data.Option.Lemmas
Option.bind_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β}, o.bind f = none ↔ ∀ (a : α), o = some a → f a = none
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instSemilatticeSup : {E : Type u_3} → [inst : AddGroup E] → SemilatticeSup (NonarchAddGroupSeminorm E)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.stdPart_map : ∀ {x : ℝ*} {r : ℝ} {f : ℝ → ℝ},
  ContinuousAt f r → Filter.Germ.Tendsto x (nhds r) → (Filter.Germ.map f x).Tendsto (nhds (f r))
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.Scheme.compactSpace_of_isLimit : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)],
  CompactSpace ↥c.pt
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.val_addUnitsEquivAddUnitsType_apply_coe : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (x : ↥S.addUnits),
  ↑↑(S.addUnitsEquivAddUnitsType x) = (AddUnits.coeHom M) ↑x
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.hom_ext_iff : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] {f g : ExteriorAlgebra R M →ₐ[R] A},
  f = g ↔ f.toLinearMap ∘ₗ ExteriorAlgebra.ι R = g.toLinearMap ∘ₗ ExteriorAlgebra.ι R
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.rightHomologyMap_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology]
  [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.rightHomologyMap (φ + φ') =
    CategoryTheory.ShortComplex.rightHomologyMap φ + CategoryTheory.ShortComplex.rightHomologyMap φ'
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ_natDegree_eq_θ_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → (RatFunc.Luroth.Φ✝ E).natDegree = (RatFunc.Luroth.θ✝ E).natDegree
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → ∀ {h' : k' ∈ Std.DTreeMap.Const.unitOfList l cmp}, (Std.DTreeMap.Const.unitOfList l cmp).getKey k' h' = k
-- Mathlib.Data.Set.Restrict
Set.MapsTo.val_restrict_apply : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) (x : ↑s),
  ↑(Set.MapsTo.restrict f s t h x) = f ↑x
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrLeft_trans_prodComm : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂),
  (Equiv.prodCongrLeft e).trans (Equiv.prodComm β₂ α₁) = (Equiv.prodComm β₁ α₁).trans (Equiv.prodCongrRight e)
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftableCocone.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cocone (K.comp F)}
  {liftedCocone : CategoryTheory.Limits.Cocone K} {validLift : F.mapCocone liftedCocone ≅ c}
  {liftedCocone_1 : CategoryTheory.Limits.Cocone K} {validLift_1 : F.mapCocone liftedCocone_1 ≅ c},
  { liftedCocone := liftedCocone, validLift := validLift } =
      { liftedCocone := liftedCocone_1, validLift := validLift_1 } →
    liftedCocone = liftedCocone_1 ∧ validLift ≍ validLift_1
-- Init.Data.Int.Linear
Int.Internal.Linear.neg_fold : ∀ (a : ℤ), a.neg = -a
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.le_prefixFunction : ∀ {pat : ByteArray} {stackPos needlePos : ℕ}
  (h : String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat needlePos stackPos) (h₀ : 0 < stackPos),
  needlePos ≤ stackPos - 1 →
    needlePos ≤ String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat (stackPos - 1) ⋯
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trList.eq_def : ∀ (x : List ℕ),
  Turing.PartrecToTM2.trList x =
    match x with
    | [] => []
    | n :: ns => Turing.PartrecToTM2.trNat n ++ Turing.PartrecToTM2.Γ'.cons :: Turing.PartrecToTM2.trList ns
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonAddHom_apply : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] (a : α), Finset.singletonAddHom a = {a}
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.rightUnitor_hom_app : ∀ {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)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        (CategoryTheory.Localization.Monoidal.ε' L W ε).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Localization.Monoidal.μ L W ε X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Composition (in the target) of a bounded continuous function with a Lipschitz map again
gives a bounded continuous function.  -/
BoundedContinuousFunction.comp : {α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      [inst : TopologicalSpace α] →
        [inst_1 : PseudoMetricSpace β] →
          [inst_2 : PseudoMetricSpace γ] →
            (G : β → γ) →
              {C : NNReal} → LipschitzWith C G → BoundedContinuousFunction α β → BoundedContinuousFunction α γ
-- Init.Data.Vector.Attach
/-- Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
`Vector {x // P x} n` is the same as the input `Vector α n`.
 -/
_private.Init.Data.Vector.Attach.0.Vector.attachWithImpl : {α : Type u_1} → {n : ℕ} → (xs : Vector α n) → (P : α → Prop) → (∀ x ∈ xs, P x) → Vector { x // P x } n
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Topology.IsEmbedding.toHomeomorphOfSurjective.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f f_1 : X → Y}
  (e_f : f = f_1) (hf : Topology.IsEmbedding f) (hsurj : Function.Surjective f),
  hf.toHomeomorphOfSurjective hsurj = ⋯.toHomeomorphOfSurjective ⋯
-- Mathlib.Order.RelClasses
instIsNonstrictStrictOrderGeGt : ∀ {α : Type u} [inst : Preorder α], IsNonstrictStrictOrder α (fun x1 x2 => x2 ≤ x1) fun x1 x2 => x2 < x1
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_of_pow_mul_eq : ∀ {p n k l : ℕ}, n ≠ 0 → p ^ k * l = n → ¬p ∣ l → p.maxPowDvdDiv n = (k, l)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l → (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).getKey! k' = k
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₃.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W x)] {Y' : C} (f f' f'' : X ⟶ Y') (s : Y ⟶ Y')
  (hs : W s),
  sizeOf { Y' := Y', f := f, f' := f', f'' := f'', s := s, hs := hs } =
    1 + sizeOf Y' + sizeOf f + sizeOf f' + sizeOf f'' + sizeOf s + sizeOf hs
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instMul : {R : Type u_1} → {A : Type u_2} → [Mul R] → [Add A] → [Mul A] → [SMul R A] → Mul (Unitization R A)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.symm_g : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (a : ℝ), P.symm.g a = P.f a
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
/-- `λ` is the Carmichael function, also known as the reduced totient function,
defined as the exponent of the unit group of `ZMod n`.  -/
ArithmeticFunction.carmichael : ArithmeticFunction ℕ
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `FaithfulSMul` across an `Equiv`.

See `FaithfulSMul.of_injective` for the general statement not about transferring.  -/
Equiv.faithfulSMul : ∀ (M : Type u_1) {α : Type u_4} {β : Type u_5} [inst : SMul M β] (e : α ≃ β) [FaithfulSMul M β], FaithfulSMul M α
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_eq_bot_iff : ∀ {G : Type u_1} [inst : Group G] {k : Set G}, Subgroup.closure k = ⊥ ↔ k ⊆ {1}
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieAlgebra.toSMulCommClass : ∀ {R : Type u_1} {inst : CommRing R} {L : Type u_2} {inst_1 : RightPreLieRing L} [self : RightPreLieAlgebra R L],
  SMulCommClass R L L
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.coe_bot : ∀ {M : Type u_1} [inst : Mul M], ↑⊥ = ∅
-- Batteries.Data.DList.Lemmas
Batteries.DList.toList_push : ∀ {α : Type u_1} (x : α) (l : Batteries.DList α), (l.push x).toList = l.toList ++ [x]
-- Mathlib.Data.Set.Lattice
Set.biUnion_lt_eq_iUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [NoMaxOrder α] {s : α → Set β}, ⋃ n, ⋃ m, ⋃ (_ : m < n), s m = ⋃ n, s n
-- Mathlib.RingTheory.Etale.Weakly
Algebra.WeaklyEtale.flat : ∀ {R : Type u_3} {S : Type u_4} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  [self : Algebra.WeaklyEtale R S], Module.Flat R S
-- Init.Data.List.Basic
List.dropLast_singleton : ∀ {α : Type u_1} {x : α}, [x].dropLast = []
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.domRestrict_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (K : Subgroup G) (f : G →* N),
  (f.domRestrict K).range = Subgroup.map f K
-- Init.Data.UInt.Lemmas
USize.toUInt16_ofFin : ∀ (n : Fin USize.size), (USize.ofFin n).toUInt16 = UInt16.ofNat ↑n
-- Mathlib.Tactic.IntervalCases
/-- The result of `interval_cases` is a list of goals,
one for each integer value between the bounds.  -/
Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal : Type