mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_eq_getLast?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey? = t.keys.getLast?
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.toArray_flattenAfter : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m (Std.IterM m β)] [inst_5 : Std.Iterator α₂ m β]
  [Std.Iterators.Finite α m] [Std.Iterators.Finite α₂ m] {it₁ : Std.IterM m (Std.IterM m β)}
  {it₂ : Option (Std.IterM m β)},
  (Std.IterM.flattenAfter✝ it₁ it₂).toArray =
    match it₂ with
    | none => Array.flatten <$> (Std.IterM.mapM (fun it₂ => it₂.toArray) it₁).toArray
    | some it₂ => do
      let __do_lift ← it₂.toArray
      let __do_lift_1 ← Array.flatten <$> (Std.IterM.mapM (fun it₂ => it₂.toArray) it₁).toArray
      pure (__do_lift ++ __do_lift_1)
-- Mathlib.Computability.EpsilonNFA
εNFA.instZero : {α : Type u} → {σ : Type v} → Zero (εNFA α σ)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toContinuousAddMonoidHom_neg : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_8 : IsTopologicalAddGroup M₂]
  (f : M →SL[σ₁₂] M₂), ↑(-f) = -↑f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → (aig : Std.Sat.AIG α) → BitVec w → (curr : ℕ) → aig.RefVec curr → curr ≤ w → aig.RefVec w
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Meta.Grind.Params.insertCasesTypes : Lean.Meta.Grind.Params → Lean.Name → Bool → Lean.Meta.Grind.Params
-- Mathlib.Data.Sign.Defs
SignType.instLinearOrder : LinearOrder SignType
-- Mathlib.Data.ENNReal.Real
ENNReal.ofNat_le_ofReal : ∀ {n : ℕ} [inst : n.AtLeastTwo] {p : ℝ}, OfNat.ofNat n ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p
-- Mathlib.Dynamics.Flow
Flow.IsSemiconjugacy.cont : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  {β : Type u_3} [inst_3 : TopologicalSpace β] {π : α → β} {ϕ : Flow τ α} {ψ : Flow τ β},
  Flow.IsSemiconjugacy π ϕ ψ → Continuous π
-- Mathlib.Order.Minimal
image_antitone_setOfPred_minimal_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) →
    f '' {x | Minimal (fun x => x ∈ s) x} = {x | Maximal (fun x => x ∈ f '' s) x}
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsSymm.eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsSymm → ∀ (x y : M), (B x) y = (B y) x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.foldlM_eq_foldlM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : δ → α → m δ} {init : δ}, Std.TreeSet.Raw.foldlM f init t = List.foldlM f init t.toList
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_cons_some : ∀ {α : Type u_1} {β : Type v} (f : α → Option β) (a : α) (s : Multiset α) {b : β},
  f a = some b → Multiset.filterMap f (a ::ₘ s) = b ::ₘ Multiset.filterMap f s
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_monomial : ∀ {R : Type u_1} [inst : CommSemiring R] (n : ℕ) (f : Polynomial R),
  Polynomial.Bivariate.swap ((Polynomial.monomial n) f) =
    Polynomial.map Polynomial.C f * Polynomial.C (Polynomial.X ^ n)
-- Mathlib.Topology.MetricSpace.Algebra
TendstoLocallyUniformly.smul₀_of_isBoundedUnder : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] {X : Type u_3} {ι : Type u_4} [inst_6 : TopologicalSpace X]
  {F : ι → X → α} {G : ι → X → β} {f : X → α} {g : X → β} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l →
      (∀ (x : X), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x) fun y => dist (f y) 0) →
        (∀ (x : X), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x) fun y => dist (g y) 0) →
          TendstoLocallyUniformly (F • G) (f • g) l
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- Two `R`-linear maps from `Finsupp X M` which agree on each `single x y` agree everywhere.

We formulate this fact using equality of linear maps `φ.comp (lsingle a)` and `ψ.comp (lsingle a)`
so that the `ext` tactic can apply a type-specific extensionality lemma to prove equality of these
maps. E.g., if `M = R`, then it suffices to verify `φ (single a 1) = ψ (single a 1)`.  -/
Finsupp.lhom_ext' : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ₁₂ : R →+* R₂}
  ⦃φ ψ : (α →₀ M) →ₛₗ[σ₁₂] N⦄, (∀ (a : α), φ ∘ₛₗ Finsupp.lsingle a = ψ ∘ₛₗ Finsupp.lsingle a) → φ = ψ
-- Mathlib.Topology.MetricSpace.Cover
Metric.isCover_iff_subset_cthickening : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X],
  IsClosed N → (Metric.IsCover ε s N ↔ s ⊆ Metric.cthickening (↑ε) N)
-- Init.Data.Range.Polymorphic.Stream
Std.PRange.instToStreamRioIterIteratorOfUpwardEnumerableOfLeast? : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → [Std.PRange.Least? α] → Std.ToStream (Std.Rio α) (Std.Iter α)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.quasiCompact_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.QuasiCompact f]
  [AlgebraicGeometry.QuasiCompact g], AlgebraicGeometry.QuasiCompact (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableAt.finsum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {x₀ : B} {ι : Type u_9}
  {t : ι → (x : B) → E x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), MDiffAt (T% t) x₀) → (MDiffAt fun x => ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieAlgebra.toIsScalarTower : ∀ {R : Type u_1} {inst : CommRing R} {L : Type u_2} {inst_1 : RightPreLieRing L} [self : RightPreLieAlgebra R L],
  IsScalarTower R L L
-- Mathlib.Topology.Constructions
IsOpen.trans : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {t : Set ↑s}, IsOpen t → IsOpen s → IsOpen (Subtype.val '' t)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_cons_eq_insertManyIfNewUnit! : ∀ {α : Type u} {instOrd : Ord α} {hd : α} {tl : List α},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty (hd :: tl) ⋯) =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit!
        (Std.DTreeMap.Internal.Impl.insertIfNew! hd () Std.DTreeMap.Internal.Impl.empty) tl)
-- Init.Data.List.Find
List.findIdx_cons : ∀ {α : Type u_1} {p : α → Bool} {b : α} {l : List α}, List.findIdx p (b :: l) = bif p b then 0 else List.findIdx p l + 1
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_sub_left : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (v₁ v₂ : V), midpoint R v₁ v₂ - v₁ = ⅟2 • (v₂ - v₁)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun_iff_iIndep : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {β : ι → Type u_7} (m : (x : ι) → MeasurableSpace (β x))
  (f : (x : ι) → Ω → β x) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndepFun f μ ↔ ProbabilityTheory.iIndep (fun x => MeasurableSpace.comap (f x) (m x)) μ
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] {R : Type u_2}
  [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R C] (o : CategoryTheory.HomOrthogonal s) {α β : Type}
  [inst_5 : Finite α] [inst_6 : Finite β] {f : α → ι} {g : β → ι}
  (a : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))),
  o.matrixDecompositionLinearEquiv.symm a = o.matrixDecompositionAddEquiv.invFun a
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOnNhd.pow`

---

Powers of analytic functions (into a normed `𝕜`-algebra) are analytic.  -/
AnalyticOnNhd.fun_pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A}
  {s : Set E}, AnalyticOnNhd 𝕜 f s → ∀ (n : ℕ), AnalyticOnNhd 𝕜 (fun i => f i ^ n) s
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extendedHom'_apply : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  (I : FractionalIdeal M K), (FractionalIdeal.extendedHom' L hf) I = FractionalIdeal.extended L hf I
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinderEvents.eq_1 : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] (Δ : Set ι),
  MeasureTheory.cylinderEvents Δ = ⨆ i ∈ Δ, MeasurableSpace.comap (fun σ => σ i) (m i)
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_sub_apply : ∀ (f g : ℕ → ℂ) (s : ℂ) (n : ℕ), LSeries.term (f - g) s n = LSeries.term f s n - LSeries.term g s n
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCodetector_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsCodetector G ↔
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
      (∀ (h : X ⟶ G), ∃! h', CategoryTheory.CategoryStruct.comp f h' = h) → CategoryTheory.IsIso f
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.match_19.splitter : (aig : Std.Sat.AIG ℕ) →
  (upper : ℕ) →
    (h : upper < aig.decls.size) →
      (lhs rhs : Std.Sat.AIG.Fanin) →
        (this : lhs.gate < upper ∧ rhs.gate < upper) →
          (lstate : Std.Sat.AIG.toCNF.State✝ aig) →
            (motive : { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ lstate out rhs.gate ⋯ } → Sort u_1) →
              (x : { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ lstate out rhs.gate ⋯ }) →
                ((rstate : Std.Sat.AIG.toCNF.State✝ aig) →
                    (hrstate : Std.Sat.AIG.toCNF.State.IsExtensionBy✝ lstate rstate rhs.gate ⋯) →
                      motive ⟨rstate, hrstate⟩) →
                  motive x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.xRep_eq_xRep_iff : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {P Q : W.Point}, P.xRep = Q.xRep ↔ P = Q ∨ P = -Q
-- Init.Data.Slice.List.Iterator
List.instToStringListSlice : {α : Type u} → [ToString α] → ToString (ListSlice α)
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- **Alias** of `HilbertBasis.hasSum_orthogonalProjectionOnto`. -/
HilbertBasis.hasSum_orthogonalProjection : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [inst_3 : CompleteSpace ↥U] (b : HilbertBasis ι 𝕜 ↥U) (x : E),
  HasSum (fun i => inner 𝕜 (↑(b i)) x • b i) (U.orthogonalProjectionOnto x)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_top : ∀ {α : Type u_2} [inst : TopologicalSpace α], ↑⊤ = Set.univ
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Equiv.Perm.prod_comp : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (σ : Equiv.Perm ι) (s : Finset ι) (f : ι → M),
  {a | σ a ≠ a} ⊆ ↑s → ∏ x ∈ s, f (σ x) = ∏ x ∈ s, f x
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.ι_comp_map : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {W₁ : Type u_6} {W₂ : Type u_7} [inst_2 : SeminormedAddCommGroup W₁] [inst_3 : SeminormedAddCommGroup W₂]
  {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂}
  {ψ : NormedAddGroupHom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ),
  (NormedAddGroupHom.Equalizer.ι f₂ g₂).comp (NormedAddGroupHom.Equalizer.map φ ψ hf hg) =
    φ.comp (NormedAddGroupHom.Equalizer.ι f₁ g₁)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- The type of type (I) simplices for the pairing  -/
SSet.prodStdSimplex.pairingCore.Type₁ : {m : ℕ} → Fin (m + 1) → ℕ → Type u
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformEmbedding.of_comp_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {g : β → γ}, IsUniformEmbedding g → ∀ {f : α → β}, IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f
-- Init.PropLemmas
and_right_comm : ∀ {a b c : Prop}, (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- Functor that gets the set of objects of a groupoid. It is not
called `forget`, because it is not a faithful functor.  -/
CategoryTheory.Grpd.objects : CategoryTheory.Functor CategoryTheory.Grpd (Type u)
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get_out_bound : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (s : aig.RefVec len) (idx : ℕ)
  (alt : aig.Ref), len ≤ idx → s.getD idx alt = alt
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.mk.injEq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {X₁ : C₁}
  (w : Φ.functor.obj X₁ ⟶ X₂) (hw : W₂ w) (X₁_1 : C₁) (w_1 : Φ.functor.obj X₁_1 ⟶ X₂) (hw_1 : W₂ w_1),
  ({ X₁ := X₁, w := w, hw := hw } = { X₁ := X₁_1, w := w_1, hw := hw_1 }) = (X₁ = X₁_1 ∧ w ≍ w_1)
-- Mathlib.Order.Filter.Map
Filter.map_inj : ∀ {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β},
  Function.Injective m → (Filter.map m f = Filter.map m g ↔ f = g)
-- Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
/-- Let `c₁` (resp. `c₂`) be a cokernel cofork for a morphism `f₁ : X₁ ⟶ Y₁`
in a category `C₁` (resp. `f₂ : X₂ ⟶ Y₂` in `C₂`). Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C`,
this is the cokernel cofork with point `(F.obj c₁.pt).obj c₂.pt` for
the obvious morphism `(F.obj X₁).obj Y₂ ⨿ (F.obj Y₁).obj X₂ ⟶ (F.obj Y₁).obj Y₂`.  -/
CategoryTheory.Limits.CokernelCofork.mapBifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C : 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} C] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  {X₁ Y₁ : C₁} →
                    {f₁ : X₁ ⟶ Y₁} →
                      (c₁ : CategoryTheory.Limits.CokernelCofork f₁) →
                        {X₂ Y₂ : C₂} →
                          {f₂ : X₂ ⟶ Y₂} →
                            CategoryTheory.Limits.CokernelCofork f₂ →
                              (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                                [(F.obj c₁.pt).PreservesZeroMorphisms] →
                                  [F.PreservesZeroMorphisms] →
                                    [inst_8 :
                                        CategoryTheory.Limits.HasBinaryCoproduct ((F.obj X₁).obj Y₂)
                                          ((F.obj Y₁).obj X₂)] →
                                      CategoryTheory.Limits.CokernelCofork
                                        (CategoryTheory.Limits.coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
-- Lean.Data.Json.Parser
Lean.Json.Parser.hexChar : Std.Internal.Parsec.String.Parser UInt16
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- A special case of `Set.image_finsetProd_pi` for `Finset.univ`.  -/
Set.image_fintype_prod_pi : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : Fintype ι] (S : ι → Set α),
  (fun f => ∏ i, f i) '' Set.univ.pi S = ∏ i, S i
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.ι_comp_map : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (s : A),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen ℬ (f s)).ι (AlgebraicGeometry.Proj.map f hf) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.resLE (AlgebraicGeometry.Proj.map f hf) (AlgebraicGeometry.Proj.basicOpen 𝒜 s)
        ((TopologicalSpace.Opens.map (AlgebraicGeometry.Proj.map f hf).base).obj (AlgebraicGeometry.Proj.basicOpen 𝒜 s))
        ⋯)
      (AlgebraicGeometry.Proj.basicOpen 𝒜 s).ι
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₂_of_isCharTwoJEqZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF], W.a₂ = 0
-- Lean.Declaration
Lean.instInhabitedConstructorVal : Inhabited Lean.ConstructorVal
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homology_sc'_eq_homology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (j : ι) [inst_2 : K.HasHomology j]
  [inst_3 : (K.sc' (c.prev j) j (c.next j)).HasHomology], (K.sc' (c.prev j) j (c.next j)).homology = K.homology j
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.coe_toIntertwiningMap : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ), ⇑↑φ = ⇑φ
-- Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
Module.Finite.multilinearMap : ∀ {ι : Type u_1} {R : Type u_2} {M₂ : Type u_3} {M₁ : ι → Type u_4} [Finite ι] [inst : CommRing R]
  [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂] [Module.Finite R M₂] [Module.Free R M₂]
  [inst_5 : (i : ι) → AddCommGroup (M₁ i)] [inst_6 : (i : ι) → Module R (M₁ i)] [∀ (i : ι), Module.Finite R (M₁ i)]
  [∀ (i : ι), Module.Free R (M₁ i)], Module.Finite R (MultilinearMap R M₁ M₂)
-- Mathlib.Data.Set.Basic
Set.sep_false : ∀ {α : Type u} {s : Set α}, {x | x ∈ s ∧ False} = ∅
-- Mathlib.Analysis.Convex.Visible
/-- **Alias** of the forward direction of `isVisible_comm`. -/
IsVisible.symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsOrderedRing 𝕜]
  [inst_3 : AddCommGroup V] [inst_4 : Module 𝕜 V] [inst_5 : AddTorsor V P] {s : Set P} {x y : P},
  IsVisible 𝕜 s x y → IsVisible 𝕜 s y x
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.parserOfStack.parenthesizer : ℕ → optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Std.Http.Data.Headers
Std.Http.Headers.instToString : ToString Std.Http.Headers
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.mkPositivityExt.unsafe_1 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_pi_div_two_sub : ∀ (x : ℂ), Complex.sin (↑Real.pi / 2 - x) = Complex.cos x
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMulOneClass.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : MulOneClass M] [inst_2 : ContinuousMul M],
  SeparationQuotient.instMulOneClass =
    { toOne := SeparationQuotient.instOne, toMul := SeparationQuotient.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] [F.IsCardinalAccessible κ]
  (J : Type w) [inst_4 : CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ],
  CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_modify_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {k : α} {f : β → β},
  m.WF → (m.modify k f).getKey! k = if k ∈ m then k else default
-- Mathlib.Order.Disjoint
Prod.codisjoint_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] {x y : α × β}, Codisjoint x y ↔ Codisjoint x.1 y.1 ∧ Codisjoint x.2 y.2
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.sInter_sdiff_singleton_univ`. -/
Set.sInter_diff_singleton_univ : ∀ {α : Type u_1} (s : Set (Set α)), ⋂₀ (s \ {Set.univ}) = ⋂₀ s
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SavedState.mk.injEq : ∀ (term : Lean.Elab.Term.SavedState) (tactic : Lean.Elab.Tactic.Grind.State) (term_1 : Lean.Elab.Term.SavedState)
  (tactic_1 : Lean.Elab.Tactic.Grind.State),
  ({ term := term, tactic := tactic } = { term := term_1, tactic := tactic_1 }) = (term = term_1 ∧ tactic = tactic_1)
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_sub_Ico_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  Multiset.Ico a b - Multiset.Ico c b = Multiset.Ico a (min b c)
-- Mathlib.Lean.Meta.Simp
/-- Gets all simp-attributes given to declaration `decl`.  -/
Lean.Meta.getAllSimpAttrs : Lean.Name → Lean.CoreM (Array Lean.Name)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.convexCombPair.eq_def : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (x y : M),
  Convexity.convexCombPair s t hs ht hst x y = Convexity.sConvexComb (Convexity.StdSimplex.duple x y hs ht hst)
-- Mathlib.Tactic.NormNum.Core
/-- Each `norm_num` extension is labelled with a collection of patterns
which determine the expressions to which it should be applied.  -/
Mathlib.Meta.NormNum.Entry : Type
-- Std.Do.SPred.Laws
Std.Do.SPred.instTransEntails : {σs : List (Type u)} → Trans Std.Do.SPred.entails Std.Do.SPred.entails Std.Do.SPred.entails