mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval.eq_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) (ι : C → Type (max u v))
  (t : (X : C) → ι X → F.obj (Opposite.op X)) (x : C)
  (x_1 : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι x),
  CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t x_1 =
    match x, x_1 with
    | X, CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ .(X) i => some (t X i)
    | x, CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i => do
      let __do_lift ← CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t i
      some ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) __do_lift)
    | x, CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h =>
      have vals := fun W r hr => CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t (h r hr);
      if hall : ∀ (W : C) (r : W ⟶ x) (hr : R r), (vals W r hr).isSome = true then
        have y := fun x_2 x hr => (vals x_2 x hr).get ⋯;
        if hy : y.Compatible then some (Exists.choose ⋯) else none
      else none
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_left_comm : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, P ∧ Q ∧ R ⊣⊢ₛ Q ∧ P ∧ R
-- Mathlib.Analysis.Convex.Visible
/-- Two points are visible to each other through a set if no point of that set lies strictly
between them.

By convention, a point `x` sees itself through any set `s`, even when `x ∈ s`.  -/
IsVisible : (𝕜 : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Field 𝕜] →
        [LinearOrder 𝕜] → [inst_2 : AddCommGroup V] → [Module 𝕜 V] → [AddTorsor V P] → Set P → P → P → Prop
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.norm_abs : ∀ {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [CStarRing A] [inst_3 : NormedSpace ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] {a : A}, ‖CFC.abs a‖ = ‖a‖
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- This is false for prime numbers other than 2:
for `p = 3`, `n = 1`, one has `log 3 1 = padicValNat 3 2 = 0`.  -/
Nat.log_ne_padicValNat_succ : ∀ {n : ℕ}, n ≠ 0 → Nat.log 2 n ≠ padicValNat 2 (n + 1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List ((a : α) × β a)} {k : α}, (Std.DTreeMap.ofList l cmp).contains k = (List.map Sigma.fst l).contains k
-- Mathlib.Logic.Relation
Relation.TransGen.head : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α}, r a b → Relation.TransGen r b c → Relation.TransGen r a c
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.instCommMonoid : {𝕜 : Type u_1} → [inst : SeminormedCommRing 𝕜] → [NormOneClass 𝕜] → CommMonoid ↑(Metric.closedBall 0 1)
-- Init.Data.Fin.Basic
Fin.instShiftRight : {n : ℕ} → ShiftRight (Fin n)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get!.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t t_1 : Std.DTreeMap.Internal.Impl α β),
  t = t_1 → ∀ (k : α) [inst_2 : Inhabited (β k)], t.get! k = t_1.get! k
-- Mathlib.Order.Interval.Multiset
Multiset.Ioi.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α), Multiset.Ioi a = (Finset.Ioi a).val
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_C_mul_X_pow : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R],
  (Polynomial.C a * Polynomial.X ^ n).divX = if n = 0 then 0 else Polynomial.C a * Polynomial.X ^ (n - 1)
-- Init.Data.Array.GetLit
Array.toArrayLit.eq_1 : ∀ {α : Type u_1} (xs : Array α) (n : ℕ) (hsz : xs.size = n),
  xs.toArrayLit n hsz = (xs.toListLitAux n hsz n ⋯ []).toArray
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionContext.mk.inj : ∀ {diagnostics : Array Lean.Lsp.Diagnostic} {only? : Option (Array Lean.Lsp.CodeActionKind)}
  {triggerKind? : Option Lean.Lsp.CodeActionTriggerKind} {diagnostics_1 : Array Lean.Lsp.Diagnostic}
  {only?_1 : Option (Array Lean.Lsp.CodeActionKind)} {triggerKind?_1 : Option Lean.Lsp.CodeActionTriggerKind},
  { diagnostics := diagnostics, only? := only?, triggerKind? := triggerKind? } =
      { diagnostics := diagnostics_1, only? := only?_1, triggerKind? := triggerKind?_1 } →
    diagnostics = diagnostics_1 ∧ only? = only?_1 ∧ triggerKind? = triggerKind?_1
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.append.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((bs : List α) → motive [] bs) → ((a : α) → (as bs : List α) → motive (a :: as) bs) → motive x x_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).size + (↑m₂).size = (↑(m₁.union m₂)).size + (↑(m₁.inter m₂)).size
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalIntStx : Lean.Term → Lean.Elab.TermElabM (ℤ × Lean.Expr)
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encodeCode.match_1.eq_1 : ∀ (motive : Nat.Partrec.Code → Sort u_1) (h_1 : Unit → motive Nat.Partrec.Code.zero)
  (h_2 : Unit → motive Nat.Partrec.Code.succ) (h_3 : Unit → motive Nat.Partrec.Code.left)
  (h_4 : Unit → motive Nat.Partrec.Code.right) (h_5 : (cf cg : Nat.Partrec.Code) → motive (cf.pair cg))
  (h_6 : (cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) (h_7 : (cf cg : Nat.Partrec.Code) → motive (cf.prec cg))
  (h_8 : (cf : Nat.Partrec.Code) → motive cf.rfind'),
  (match Nat.Partrec.Code.zero with
    | Nat.Partrec.Code.zero => h_1 ()
    | Nat.Partrec.Code.succ => h_2 ()
    | Nat.Partrec.Code.left => h_3 ()
    | Nat.Partrec.Code.right => h_4 ()
    | cf.pair cg => h_5 cf cg
    | cf.comp cg => h_6 cf cg
    | cf.prec cg => h_7 cf cg
    | cf.rfind' => h_8 cf) =
    h_1 ()
-- Mathlib.Data.Int.Log
Int.log_of_right_le_zero : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ) {r : R}, r ≤ 0 → Int.log b r = 0
-- Mathlib.Data.Complex.Basic
Complex.mul_re : ∀ (z w : ℂ), (z * w).re = z.re * w.re - z.im * w.im
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.comp_τr_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {a_1 b_1 c : a ⟶ b}
  (x : CategoryTheory.Bicategory.Adj.Hom₂ a_1 b_1) (y : CategoryTheory.Bicategory.Adj.Hom₂ b_1 c) {Z : b.obj ⟶ a.obj}
  (h : a_1.r ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x y).τr h =
    CategoryTheory.CategoryStruct.comp y.τr (CategoryTheory.CategoryStruct.comp x.τr h)
-- Init.Prelude
/-- Marker for type dependency that has been erased by the code generator.  -/
lcAny : Type
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (p : Ideal S) [inst_4 : p.IsPrime] [Algebra.WeaklyQuasiFiniteAt R p],
  ∃ S', (Subalgebra.toSubmodule S').FG ∧ ∃ r, ↑r ∉ p ∧ Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
-- Mathlib.Data.Int.CardIntervalMod
Int.Ico_filter_dvd_eq : ∀ (a b : ℤ) {r : ℤ} (hr : 0 < r),
  {x ∈ Finset.Ico a b | r ∣ x} = Finset.map { toFun := fun x => x * r, inj' := ⋯ } (Finset.Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_eq_zero_of_le_left : ∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, H ≤ K → K.relIndex L = 0 → H.relIndex L = 0
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- The colon preradical from Stenström, defined as the pullback of `Φ.π : 𝟭 C ⟶ Φ.quotient` along
`Φ.quotient.whiskerLeft Ψ.ι ≫ Φ.quotient.rightUnitor.hom : Φ.quotient ⋙ Ψ.r ⟶ Φ.quotient`  -/
CategoryTheory.Abelian.Preradical.colon : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [CategoryTheory.Abelian C] →
      CategoryTheory.Abelian.Preradical C → CategoryTheory.Abelian.Preradical C → CategoryTheory.Abelian.Preradical C
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileM.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : MonadAttach m] {P : β → m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (MonadAttach.CanReturn (P out)) → Sort u_3) (hP : MonadAttach.CanReturn (P out) { down := true })
  (h_1 : (hP : MonadAttach.CanReturn (P out) { down := true }) → motive ⟨{ down := true }, hP⟩)
  (h_2 : (hP : MonadAttach.CanReturn (P out) { down := false }) → motive ⟨{ down := false }, hP⟩),
  (match ⟨{ down := true }, hP⟩ with
    | ⟨{ down := true }, hP⟩ => h_1 hP
    | ⟨{ down := false }, hP⟩ => h_2 hP) =
    h_1 hP
-- Mathlib.Topology.Sets.VietorisTopology
Topology.IsOpenEmbedding.compacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsOpenEmbedding f), Topology.IsOpenEmbedding (TopologicalSpace.Compacts.map f ⋯)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.mem_fixingAddSubgroup_union_iff : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {g : M},
  g ∈ fixingAddSubgroup M (s ∪ t) ↔ g ∈ fixingAddSubgroup M s ∧ g ∈ fixingAddSubgroup M t
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.whiskerRight_comm_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ : CategoryTheory.Center C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Center C) (U : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj U (X₂.tensorObj Y).fst ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.f Y.fst)
        U)
      (CategoryTheory.CategoryStruct.comp ((X₂.tensorObj Y).snd.β U).hom h) =
    CategoryTheory.CategoryStruct.comp ((X₁.tensorObj Y).snd.β U).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.f Y.fst))
        h)
-- Mathlib.Tactic.Hint
/-- Register a new hint tactic.  -/
Mathlib.Tactic.Hint.addHint : ℕ → Lean.TSyntax `tactic → Lean.CoreM Unit
-- Mathlib.Topology.UniformSpace.Defs
nhds_eq_comap_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {x : α}, nhds x = Filter.comap (Prod.mk x) (uniformity α)
-- Lean.Parser.Term
Lean.Parser.Term.letPatDecl.parenthesizer : optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- The constant coefficient is continuous  -/
PowerSeries.WithPiTopology.continuous_constantCoeff : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Semiring R], Continuous ⇑PowerSeries.constantCoeff
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalTower_comp_algebraMap : ∀ {R : Type u} {S : Type v} {A' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring A'] [inst_2 : CommSemiring S]
  [inst_3 : Algebra S R] [inst_4 : Algebra S A'] (g : R →ₐ[S] A') (y : A'),
  (↑(Polynomial.aevalTower g y)).comp (algebraMap R (Polynomial R)) = ↑g
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.Const.toList_eq_toListModel_map : ∀ {α : Type u} {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  Std.DHashMap.Raw.Const.toList m =
    List.map
      (fun x =>
        match x with
        | ⟨k, v⟩ => (k, v))
      (Std.DHashMap.Internal.toListModel m.buckets)
-- Mathlib.Topology.Order
/-- The smallest topological space containing the collection `g` of basic sets  -/
TopologicalSpace.generateFrom : {α : Type u} → Set (Set α) → TopologicalSpace α
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given `CommMonoid`s `M, P`, Localization maps `f : M →* N, k : P →* Q` for Submonoids
`S, T` respectively, and `g : M →* P` such that `g(S) ⊆ T`, `f x = f y` implies
`k (g x) = k (g y)`.  -/
Submonoid.LocalizationMap.comp_eq_of_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} {Q : Type u_4}
  [inst_3 : CommMonoid Q], (∀ (y : ↥S), g ↑y ∈ T) → ∀ (k : T.LocalizationMap Q) {x y : M}, f x = f y → k (g x) = k (g y)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.outer_le_length : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) (s : Set R),
  f.outer s ≤ f.length s
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₄_of_isCharTwoJEqZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2], W.c₄ = 0
-- Mathlib.Data.Set.Prod
Set.prod_subset_prod_iff' : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β}, (s ×ˢ t).Nonempty → (s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁)
-- Init.Data.List.Monadic
List.filterMapM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : α → Prop}
  {xs : List (Subtype P)} {f : α → m (Option β)},
  List.filterMapM f xs.unattach =
    List.filterMapM
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- The homset equivalence which helps show that `R` is a right adjoint.  -/
CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {U : CategoryTheory.Functor B C} →
              {F : CategoryTheory.Functor C B} →
                (R : CategoryTheory.Functor A B) →
                  (F' : CategoryTheory.Functor C A) →
                    (adj₁ : F ⊣ U) →
                      (adj₂ : F' ⊣ R.comp U) →
                        [inst_3 : CategoryTheory.Limits.HasReflexiveCoequalizers A] →
                          ((X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)) →
                            (Y : A) →
                              (X : B) →
                                (CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) ≃
                                  (X ⟶ R.obj Y)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α},
  l.contains k = false → (Std.DHashMap.Const.unitOfList l).getKeyD k fallback = fallback
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map_zero : ∀ {α β : Type u} (f : α → β), f <$> 0 = 0
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (D : F.DescentData' sq sq₃) (i₁ i₂ : ι),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom (CategoryTheory.CategoryStruct.comp (sq i₁ i₂).p₂ (f i₂))
      (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯ =
    D.hom i₁ i₂
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.pos_iff_ne_zero : ∀ {p : DyckWord}, 0 < p ↔ p ≠ 0
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_eq_zero : ∀ {r : ENNReal}, ⌊r⌋ₑ = 0 ↔ r < 1
-- Init.Data.Array.Lemmas
Array.map_flatMap : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {g : α → Array β} {xs : Array α},
  Array.map f (Array.flatMap g xs) = Array.flatMap (fun a => Array.map f (g a)) xs
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.isCartesian_of_isStronglyCartesian : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ],
  p.IsCartesian f φ
-- Init.Data.Rat.Lemmas
Rat.intCast_pos : ∀ {a : ℤ}, 0 < ↑a ↔ 0 < a
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : CategoryTheory.Comonad C} →
      (A : C) →
        (a : A ⟶ G.obj A) →
          autoParam (CategoryTheory.CategoryStruct.comp a (G.ε.app A) = CategoryTheory.CategoryStruct.id A)
              CategoryTheory.Comonad.Coalgebra.counit._autoParam →
            autoParam
                (CategoryTheory.CategoryStruct.comp a (G.δ.app A) = CategoryTheory.CategoryStruct.comp a (G.map a))
                CategoryTheory.Comonad.Coalgebra.coassoc._autoParam →
              G.Coalgebra
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasFDerivWithinAt.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Real.sin (f x)) (Real.cos (f x) • f') s x
-- Aesop.RulePattern.Cache
/-- A cache for the rule pattern index.  -/
Aesop.RulePatternCache : Type
-- Mathlib.LinearAlgebra.AffineSpace.Independent
affineIndependent_equiv : ∀ {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} {ι' : Type u_5} (e : ι ≃ ι') {p : ι' → P},
  AffineIndependent k (p ∘ ⇑e) ↔ AffineIndependent k p
-- Batteries.Recycling.RBTree.WF
/-- The `balance1` function repairs the balance invariant when the first argument is red-red.  -/
RBTree.RBNode.RedRed.balance1 : ∀ {α : Type u_1} {p : Prop} {n : ℕ} {c : RBTree.RBColor} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.RedRed p l n → r.Balanced c n → ∃ c, (l.balance1 v r).Balanced c (n + 1)
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
RatFunc.liftAlgHom.congr_simp : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} {S : Type u_3} [inst_2 : Field L]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S (Polynomial K)] [inst_5 : Algebra S L] (φ φ_1 : Polynomial K →ₐ[S] L)
  (e_φ : φ = φ_1) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)),
  RatFunc.liftAlgHom φ hφ = RatFunc.liftAlgHom φ_1 ⋯
-- Mathlib.Order.WellQuasiOrder
/-- A well quasi-order or WQO is a relation such that any infinite sequence contains an infinite
monotonic subsequence, or equivalently, two elements `f m` and `f n` with `m < n` and
`r (f m) (f n)`.

For a preorder, this is equivalent to having a well-founded order with no infinite antichains.

Despite the nomenclature, we don't require the relation to be preordered. Moreover, a well
quasi-order will not in general be a well-order.  -/
WellQuasiOrdered : {α : Type u_1} → (α → α → Prop) → Prop
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.unop_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.LeftHomologyData), h.unop.ι = h.π.unop
-- Mathlib.Order.WithBot
WithBot.map_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.Injective (WithBot.map f)
-- Mathlib.Data.LawfulXor.Equiv
/-- `XorOp.xor` as a permutation.  -/
Equiv.xor : {α : Type u_1} → [inst : XorOp α] → [inst_1 : Zero α] → [LawfulXor α] → α → Equiv.Perm α
-- Lean.Compiler.IR.Format
Lean.IR.instToFormatLitVal : Std.ToFormat Lean.IR.LitVal
-- Mathlib.Analysis.Normed.Group.Continuity
mem_closure_zero_iff_norm : ∀ {E : Type u_4} [inst : SeminormedAddGroup E] {x : E}, x ∈ closure {0} ↔ ‖x‖ = 0
-- Mathlib.Topology.UnitInterval
unitInterval.div_mem : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → x ≤ y → x / y ∈ unitInterval
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isNNRat_zpow_neg : ∀ {α : Type u_1} [inst : DivisionSemiring α] {a : α} {b : ℤ} {nb num den : ℕ},
  Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb) →
    Mathlib.Meta.NormNum.IsNNRat (a ^ nb)⁻¹ num den → Mathlib.Meta.NormNum.IsNNRat (a ^ b) num den
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] (m n : ℕ) (h : n < m),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.SequentialProduct.cone f).π.app (Opposite.op m))
      (CategoryTheory.Limits.Pi.π (fun i => if x : i < m then M i else N i) n) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π M n) (CategoryTheory.eqToHom ⋯)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsAndPureAnd : ∀ {p q : Prop} (σs : List (Type u_1)), Std.Do.SPred.Tactic.IsAnd ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝
-- Mathlib.Data.Finset.Card
Finset.image.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β) (s : Finset α),
  Finset.image f s = (Multiset.map f s.val).toFinset
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isColimit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  (F G : CategoryTheory.Functor D C),
  (CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit F G).isColimit =
    CategoryTheory.Limits.evaluationJointlyReflectsColimits (CategoryTheory.Limits.pointwiseBinaryBicone F G).toCocone
      fun d =>
      (CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso
          (CategoryTheory.Limits.pairComp F G ((CategoryTheory.evaluation D C).obj d)).symm
          (CategoryTheory.Limits.BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone
          (((CategoryTheory.evaluation D C).obj d).mapCocone (CategoryTheory.Limits.pointwiseBinaryBicone F G).toCocone)
          (CategoryTheory.Limits.Cocone.ext
            (CategoryTheory.Iso.refl
              ((CategoryTheory.Limits.Cocone.precompose
                      (CategoryTheory.Limits.pairComp F G ((CategoryTheory.evaluation D C).obj d)).symm.inv).obj
                  (CategoryTheory.Limits.BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt)
            ⋯))
        (CategoryTheory.Limits.BinaryBiproduct.isColimit (F.obj d) (G.obj d))
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.eval_app : ∀ (S₁ S₂ : CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u)) (f : S₁ ⟶ S₂) (α : Type u)
  (s : S₁.obj.obj (Opposite.op α)) (x : α),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.eval S₂.obj α ((CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op α))) s)))
      x =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op PUnit.{u + 1})))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eval S₁.obj α s)) x)
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.length_iter : ∀ {β : Type w} {n : ℕ} {xs : Vector β n}, xs.iter.length = n
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.mem_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (α i)] {f : Π₀ (i : ι), Finset (α i)} {g : Π₀ (i : ι), α i},
  g ∈ f.pi ↔ ∀ (i : ι), g i ∈ f i