mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Equivalence.mapCommMon_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] (e : C ≌ D)
  [inst_6 : e.functor.Braided] [inst_7 : e.inverse.Braided] [inst_8 : e.IsMonoidal],
  e.mapCommMon.unitIso =
    CategoryTheory.Functor.mapCommMonIdIso.symm ≪≫
      CategoryTheory.Functor.mapCommMonNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapCommMonCompIso
-- Mathlib.CategoryTheory.Limits.Final.Connected
CategoryTheory.isConnected_iff_initial_of_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : Type w} [Unique T]
  (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)), CategoryTheory.IsConnected C ↔ F.Initial
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instCommGroupWithZero : {α : Type u_1} → [CommGroup α] → CommGroupWithZero (WithZero α)
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.exists_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y),
  ∃ Z a b, W₁ a ∧ W₂ b ∧ CategoryTheory.CategoryStruct.comp a b = f ∧ r.degHom f = r.deg Z
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorHom_comp_tensorHom : ∀ {x₁ y₁ z₁ x₂ y₂ z₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂) (g₁ : y₁ ⟶ z₁) (g₂ : y₂ ⟶ z₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
      (CategoryTheory.CategoryStruct.comp f₂ g₂)
-- Mathlib.Order.Interval.Set.Basic
Set.left_mem_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∈ Set.Ico a b ↔ a < b
-- Mathlib.NumberTheory.FunctionField
FunctionField.ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : Algebra (RatFunc F) K] [IsScalarTower (Polynomial F) (RatFunc F) K] [FunctionField F K]
  [Algebra.IsSeparable (RatFunc F) K], IsDedekindDomain ↥(FunctionField.ringOfIntegers F K)
-- Mathlib.Algebra.Order.SuccPred
antitone_of_add_one_le : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : One α]
  [inst_4 : SuccAddOrder α] [IsSuccArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMax a → f (a + 1) ≤ f a) → Antitone f
-- Mathlib.Data.Set.Image
Set.preimage_subset_of_surjOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β},
  Function.Injective f → Set.SurjOn f s t → f ⁻¹' t ⊆ s
-- Mathlib.Topology.LocalAtTarget
Set.restrictPreimage_isClosedEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
  Topology.IsClosedEmbedding f → Topology.IsClosedEmbedding (s.restrictPreimage f)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffAt.add_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {x₀ : M},
  ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) x₀ →
    ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t x⟩) x₀ →
      ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (s + t) x⟩) x₀
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.instHasWidePullbacksOppositeOfHasWidePushouts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasWidePushouts C],
  CategoryTheory.Limits.HasWidePullbacks Cᵒᵖ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.Iterators.Types.Take.instIterator.match_1.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        (it : Std.IterM m β) →
          (motive : it.internalState.inner.Step → Sort u_3) →
            (x : it.internalState.inner.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
                      motive ⟨Std.IterStep.yield it' out, h'⟩) →
                ((it' : Std.IterM m β) →
                    (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
                      motive ⟨Std.IterStep.skip it', h'⟩) →
                  ((h' : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h'⟩) →
                    motive x
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An additive subgroup is closed under subtraction.  -/
sub_mem : ∀ {M : Type u_3} {S : Type u_4} [inst : SubNegMonoid M] [inst_1 : SetLike S M] [hSM : AddSubgroupClass S M] {H : S}
  {x y : M}, x ∈ H → y ∈ H → x - y ∈ H
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.ofLp_single : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] (i : ι) (a : 𝕜),
  (EuclideanSpace.single i a).ofLp = Pi.single i a
-- Mathlib.Data.Fintype.Pi
Fintype.eval_image_piFinset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} (t : (a : α) → Finset (δ a)) (a : α)
  [inst_2 : DecidableEq (δ a)],
  (∀ (b : α), a ≠ b → (t b).Nonempty) → Finset.image (fun f => f a) (Fintype.piFinset t) = t a
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.refl.eq_1 : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : Mul α],
  OrderMonoidIso.refl α = { toMulEquiv := MulEquiv.refl α, map_le_map_iff' := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The map `K.opcycles i ⟶ L.opcycles i` induced by a morphism in `HomologicalComplex`.  -/
HomologicalComplex.opcyclesMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex C c} →
            (K ⟶ L) → (i : ι) → [inst_2 : K.HasHomology i] → [inst_3 : L.HasHomology i] → K.opcycles i ⟶ L.opcycles i
-- Mathlib.Data.Sym.Sym2
Sym2.fromRelOrderIso_symm_apply_coe : ∀ (α : Type u_1) (s : Set (Sym2 α)) (x y : α), ↑((RelIso.symm (Sym2.fromRelOrderIso α)) s) x y = Sym2.ToRel s x y
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.ext' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X Y : T.Algebra)
  (f g : X ⟶ Y), f.f = g.f → f = g
-- Mathlib.Topology.Category.TopCat.Adjunctions
TopCat.instIsLeftAdjointForgetContinuousMapCarrier : (CategoryTheory.forget TopCat).IsLeftAdjoint
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.forM : {m : Type w → Type w'} →
  [Monad m] →
    {α : Type u_1} →
      {β : Type u_2} →
        {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → (α → β → m PUnit.{w + 1}) → m PUnit.{w + 1}
-- Mathlib.Topology.Perfect
/-- The intersection of a preperfect set and an open set is preperfect.  -/
Preperfect.open_inter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C U : Set α}, Preperfect C → IsOpen U → Preperfect (U ∩ C)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getPowThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.Algebra.Torsor.Basic
vsub_vadd_comm : ∀ {G : Type u_1} {P : Type u_2} [inst : AddCommGroup G] [inst_1 : AddTorsor G P] (p₁ p₂ p₃ : P),
  (p₁ -ᵥ p₂) +ᵥ p₃ = (p₃ -ᵥ p₂) +ᵥ p₁
-- Mathlib.Algebra.DirectSum.Internal
/-- The subsemiring `A 0` of `R`.  -/
SetLike.GradeZero.subsemiring : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : SetLike σ R] → [AddSubmonoidClass σ R] → (A : ι → σ) → [SetLike.GradedMonoid A] → Subsemiring R
-- Mathlib.Algebra.Order.Sub.Defs
tsub_eq_of_eq_add_rev : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a = b + c → a - b = c
-- Init.Data.OfScientific
/-- Converts an integer into the closest-possible 64-bit floating-point number, or positive or negative
infinite floating-point value if the range of `Float` is exceeded.
 -/
Float.ofInt : ℤ → Float
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.instIsSolvableOfFinite : ∀ {G : Type u_1} [inst : Group G] [Finite G] [IsZGroup G], Group.IsSolvable G
-- Mathlib.Logic.Function.Basic
Function.bijective_iff_existsUnique : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β), Function.Bijective f ↔ ∀ (b : β), ∃! a, f a = b
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.instRingObjForgetRingHomCarrier : {R : RingCat} → Ring ((CategoryTheory.forget RingCat).obj R)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {A : C} (toPrecylinder : HomotopicalAlgebra.Precylinder A)
  (weakEquivalence_π :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrecylinder.π)
      HomotopicalAlgebra.Cylinder.weakEquivalence_π._autoParam)
  (toPrecylinder_1 : HomotopicalAlgebra.Precylinder A)
  (weakEquivalence_π_1 :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrecylinder_1.π)
      HomotopicalAlgebra.Cylinder.weakEquivalence_π._autoParam),
  ({ toPrecylinder := toPrecylinder, weakEquivalence_π := weakEquivalence_π } =
      { toPrecylinder := toPrecylinder_1, weakEquivalence_π := weakEquivalence_π_1 }) =
    (toPrecylinder = toPrecylinder_1)
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.nonempty_neLocus_iff : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] {f g : α →₀ N},
  (f.neLocus g).Nonempty ↔ f ≠ g
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.indep_aug : ∀ {α : Type u_2} (self : IndepMatroid α) ⦃I B : Set α⦄,
  self.Indep I → ¬Maximal self.Indep I → Maximal self.Indep B → ∃ x ∈ B \ I, self.Indep (insert x I)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.getValueByPosition : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadLiftT (ST IO.RealWorld) m] → [MonadLiftT BaseIO m] → ℕ → Std.AtomicT (Std.Bounded.State✝ α) m (Option α)
-- Batteries.Data.Array.Scan
Array.scanr_eq_scanrM : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α},
  Array.scanr f init as = (Array.scanrM (fun x1 x2 => pure (f x1 x2)) init as).run
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] {f : γ → E},
  MeasureTheory.Integrable f ((η.comp κ) a) → ∫ (z : γ), f z ∂(η.comp κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalGroup.t1Space : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [ContinuousMul G], IsClosed {1} → T1Space G
-- Mathlib.Tactic.Linter.DocString
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.getDeclModifiers.eq_def : ∀ (x : Lean.Syntax),
  Mathlib.Linter.getDeclModifiers x =
    match x with
    | s@h:(Lean.Syntax.node info kind args) =>
      (if (kind == `Lean.Parser.Command.declModifiers) = true then #[s] else #[]) ++
        Array.flatMap Mathlib.Linter.getDeclModifiers args
    | x => #[]
-- Aesop.Util.Tactic.Ext
Aesop.straightLineExt : Lean.MVarId → Lean.MetaM Aesop.ExtResult
-- Aesop.Builder.Basic
Aesop.RuleBuilderInput : Type
-- Mathlib.Analysis.SpecialFunctions.Bernstein
/-- The Bernstein polynomials, as continuous functions on `[0,1]`.
 -/
bernstein : ℕ → ℕ → C(↑unitInterval, ℝ)
-- Mathlib.Geometry.Convex.Cone.Dual
/-- Any set is a subset of its double dual cone.  -/
PointedCone.subset_dual_dual : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {s : Set M}, s ⊆ ↑(PointedCone.dual p.flip ↑(PointedCone.dual p s))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_eq_some_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.maxKey? = some t.maxKey!
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.renameEquiv_refl : ∀ {σ : Type u_1} (R : Type u_4) [inst : CommSemiring R], MvPolynomial.renameEquiv R (Equiv.refl σ) = AlgEquiv.refl
-- Std.Http.Data.Status
/-- 418 I'm a teapot
 -/
Std.Http.Status.imATeapot : Std.Http.Status
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.of_V : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (X : Type w) [inst_2 : AddCommGroup X]
  [inst_3 : Module k X] (ρ : Representation k G X), ↑(Rep.of ρ) = X
-- Init.Tactics
/-- `replace h := e` is like `have h := e`, but it removes a previous hypothesis
of the same name as this one if possible. For example, if the state is:

```lean
f : α → β
h : α
⊢ goal
```

Then after `replace h := f h` the state will be:

```lean
f : α → β
h : β
⊢ goal
```

whereas `have h := f h` would result in:

```lean
f : α → β
h† : α
h : β
⊢ goal
```

The tactic `specialize h a₁ ... aₙ` is a way to write `replace h := h a₁ ... aₙ`,
automatically inferring which hypothesis should be replaced.

The `replace` tactic can be used to simulate Rocq's `apply at` tactic.


Extensions:

 * `replace h : t`, without a subsequent proof, creates a new main goal `case h : ... ⊢ t`.
   This form is considered deprecated in Mathlib: use `replace h : t := _` instead. -/
Lean.Parser.Tactic.replace : Lean.ParserDescr
-- Mathlib.Data.Nat.Choose.Dvd
Nat.Prime.coprime_choose_of_lt : ∀ {p a b : ℕ}, Nat.Prime p → b < p → a ≤ b → p.Coprime (b.choose a)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.centralizer_le : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (s t : Set A),
  s ⊆ t → StarSubalgebra.centralizer R t ≤ StarSubalgebra.centralizer R s
-- Mathlib.Algebra.CharP.LinearMaps
/-- For a division ring `D` with center `k`, the ring of `k`-linear endomorphisms
of `D` has the same characteristic as `D`  -/
instCharPLinearMapSubtypeMemSubringCenterId : ∀ {D : Type u_1} [inst : DivisionRing D] {p : ℕ} [CharP D p], CharP (D →ₗ[↥(Subring.center D)] D) p
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.instRxiHasSize_eq : ISize.instRxiHasSize = HasModel.instRxiHasSize✝
-- Mathlib.Topology.PartialHomeomorph.Basic
Topology.IsEmbedding.toPartialHomeomorph_right_inv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsEmbedding f) [inst_2 : Nonempty X] {x : Y},
  x ∈ Set.range f → f (↑(Topology.IsEmbedding.toPartialHomeomorph f h).symm x) = x
-- Mathlib.CategoryTheory.EssentialImage
/-- Applying an essentially surjective functor to a preimage of `Y` yields an object that is
isomorphic to `Y`.  -/
CategoryTheory.Functor.objObjPreimageIso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → [inst_2 : F.EssSurj] → (Y : D) → F.obj (F.objPreimage Y) ≅ Y
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_le_re_and_im_le`. -/
Complex.frontier_setOf_le_re_and_im_le : ∀ (a b : ℝ), frontier {z | a ≤ z.re ∧ z.im ≤ b} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype_inv_snd_apply : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z)
  (x : { p // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))
      ((CategoryTheory.ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype f g).inv) x) =
    (↑x).2
-- Mathlib.Algebra.Field.Rat
NNRat.coe_div : ∀ (p q : ℚ≥0), ↑(p / q) = ↑p / ↑q
-- Mathlib.Algebra.Polynomial.Lifts
/-- If `p` lifts and `(r : R)` then `r • p` lifts.  -/
Polynomial.smul_mem_lifts : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : Semiring S] [inst_2 : Algebra R S] {p : Polynomial S}
  (r : R), p ∈ Polynomial.lifts (algebraMap R S) → r • p ∈ Polynomial.lifts (algebraMap R S)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.toNatTrans_mateEquiv : ∀ {C D E F : CategoryTheory.Cat} {G : C ⟶ E} {H : D ⟶ F} {L₁ : C ⟶ D} {R₁ : D ⟶ C} {L₂ : E ⟶ F} {R₂ : F ⟶ E}
  (adj₁ : CategoryTheory.Bicategory.Adjunction L₁ R₁) (adj₂ : CategoryTheory.Bicategory.Adjunction L₂ R₂)
  (f : CategoryTheory.CategoryStruct.comp G L₂ ⟶ CategoryTheory.CategoryStruct.comp L₁ H),
  ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) f).toNatTrans =
    (CategoryTheory.mateEquiv (CategoryTheory.Adjunction.ofCat adj₁) (CategoryTheory.Adjunction.ofCat adj₂))
      f.toNatTrans
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.map_injective : ∀ {R : Type u} [inst : CommRing R] {A : Type v} [inst_1 : CommRing A] {φ : R →+* A},
  Function.Injective ⇑φ → Function.Injective fun C => C.map φ
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans : ∀ (K : Type u_4) {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {κ : Type w} (E : Type z)
  [inst_3 : Field E] [inst_4 : Algebra K E] [inst_5 : Module.Finite K L] [Algebra.IsSeparable K L] [IsAlgClosed E]
  (b : κ → L),
  (Algebra.traceMatrix K b).map ⇑(algebraMap K E) =
    Algebra.embeddingsMatrix K E b * (Algebra.embeddingsMatrix K E b).transpose
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckBinrel : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Equivalence.map_injective_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : C ≌ D) (P : C),
  CategoryTheory.Injective (F.functor.obj P) ↔ CategoryTheory.Injective P
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instInhabitedDiseqCnstr : Inhabited Lean.Meta.Grind.Arith.Linear.DiseqCnstr
-- Mathlib.LinearAlgebra.Pi
Fin.consLinearEquiv_apply : ∀ (R : Type u) {n : ℕ} (M : Fin n.succ → Type u_1) [inst : Semiring R] [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)]
  [inst_2 : (i : Fin n.succ) → Module R (M i)] (a : M 0 × ((i : Fin n) → M i.succ)) (i : Fin (n + 1)),
  (Fin.consLinearEquiv R M) a i = (Fin.consEquiv M).toFun a i
-- Std.Time.Zoned.Database.Windows
/-- Fetches the timezone at a timestamp.
 -/
Std.Time.Database.Windows.getLocalTimeZoneIdentifierAt : Int64 → IO String
-- Mathlib.Order.Basic
Prod.mk_lt_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a₁ a₂ : α} {b₁ b₂ : β},
  (a₁, b₁) < (a₂, b₂) ↔ a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasureTheory.measurableSet_generateFrom_singleton_iff : ∀ {α : Type u_1} {s t : Set α}, MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = Set.univ
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_mapAccumr_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {s₁ : σ₁}
  {s₂ : σ₂} (xs : List.Vector α n) (ys : List.Vector β n) (f₁ : γ → β → σ₁ → σ₁ × ζ) (f₂ : α → σ₂ → σ₂ × γ),
  List.Vector.mapAccumr₂ f₁ (List.Vector.mapAccumr f₂ xs s₂).2 ys s₁ =
    have m :=
      List.Vector.mapAccumr₂
        (fun x y s =>
          have r₂ := f₂ x s.2;
          have r₁ := f₁ r₂.2 y s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_eq_of_support_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  Function.support f ⊆ s → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂μ
-- Init.Data.Format.Basic
/-- Checks whether the given format contains no characters.  -/
Std.Format.isEmpty : Std.Format → Bool
-- Mathlib.Order.BooleanAlgebra.Basic
/-- A bounded generalized Boolean algebra is a Boolean algebra.  -/
GeneralizedBooleanAlgebra.toBooleanAlgebra : {α : Type u} → [inst : GeneralizedBooleanAlgebra α] → [OrderTop α] → BooleanAlgebra α
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.refl : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y), CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.toAddMonObj : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} →
      {X : C} → [self : CategoryTheory.AddGrpObj X] → CategoryTheory.AddMonObj X
-- Std.Sat.CNF.Basic
Std.Sat.CNF.VarMem.eq_1 : ∀ {α : Type u_1} (v : α) (f : Std.Sat.CNF α), Std.Sat.CNF.VarMem v f = ∃ c ∈ f.clauses, Std.Sat.CNF.Clause.Mem v c
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.isOpenMap_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (S : Submodule R M) [ContinuousAdd M], IsOpenMap ⇑S.mkQ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_mul_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α] [MulLeftStrictMono α] {b c : α}, b < c → ∀ (a : α), a * b < a * c
-- Mathlib.Dynamics.Ergodic.Conservative
MeasureTheory.Conservative.of_absolutelyContinuous : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {μ ν : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    ν.AbsolutelyContinuous μ → MeasureTheory.Measure.QuasiMeasurePreserving f ν ν → MeasureTheory.Conservative f ν
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g)
        (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.commRing : {R : Type u} → [inst : CommRing R] → (self : CommHopfAlgCat R) → CommRing ↑self
-- Mathlib.Data.Fin.Basic
Fin.min_val : ∀ {n : ℕ} {a : Fin n}, min (↑a) n = ↑a
-- Aesop.RuleSet
Aesop.LocalRuleSet.unindex : Aesop.LocalRuleSet → (Aesop.RuleName → Bool) → Aesop.LocalRuleSet