mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso : ∀ {Y Z : AlgebraicGeometry.LocallyRingedSpace} (g : Y ⟶ Z) [CategoryTheory.IsIso g],
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion g
-- Aesop.Index
Aesop.Index.unindexed : {α : Type} → Aesop.Index α → Lean.PHashSet (Aesop.Rule α)
-- Mathlib.Data.Fin.Parity
Fin.even_iff_of_even : ∀ {n : ℕ} {k : Fin n}, Even n → (Even k ↔ Even ↑k)
-- Lean.Parser.Types
Lean.Parser.ParserCache.mk.inj : ∀ {tokenCache : Lean.Parser.TokenCacheEntry}
  {parserCache : Std.HashMap Lean.Parser.ParserCacheKey Lean.Parser.ParserCacheEntry}
  {tokenCache_1 : Lean.Parser.TokenCacheEntry}
  {parserCache_1 : Std.HashMap Lean.Parser.ParserCacheKey Lean.Parser.ParserCacheEntry},
  { tokenCache := tokenCache, parserCache := parserCache } =
      { tokenCache := tokenCache_1, parserCache := parserCache_1 } →
    tokenCache = tokenCache_1 ∧ parserCache = parserCache_1
-- Mathlib.Order.WithBotTop
/-- The canonical inclusion `ι → WithBotTop ι`. Registered as a coercion.  -/
WithBotTop.coe : {ι : Type u_1} → ι → WithBotTop ι
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
/-- Force `P ≤ sourceLocalClosure K P`.  -/
CategoryTheory.MorphismProperty.sourceLocalClosure.of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C} {X Y : C} (f : X ⟶ Y),
  P f → CategoryTheory.MorphismProperty.sourceLocalClosure K P f
-- Mathlib.Data.NNRat.Defs
NNRat.divNat.eq_1 : ∀ (n d : ℕ), NNRat.divNat n d = ⟨Rat.divInt ↑n ↑d, ⋯⟩
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_singleton : ∀ {α : Type u_2} {x : Bornology α} {x_1 : α}, Bornology.IsBounded {x_1}
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_le_eccent : ∀ {α : Type u_1} {G : SimpleGraph α} {u : α}, G.radius ≤ G.eccent u
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
PresheafOfModules.sheafification.congr_simp : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α α_1 : R₀ ⟶ R.obj) (e_α : α = α_1)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat],
  PresheafOfModules.sheafification α = PresheafOfModules.sheafification α_1
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.adjoin_range_ι : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Algebra.adjoin R (Set.range ⇑(TensorAlgebra.ι R)) = ⊤
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.singleton_inter_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → {a} ∩ s = ∅
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.EToCycles.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂), X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂ = X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Algebra.Ring.Defs
/-- Zero is a left absorbing element for multiplication  -/
NonUnitalNonAssocSemiring.zero_mul : ∀ {α : Type u} [self : NonUnitalNonAssocSemiring α] (a : α), 0 * a = 0
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.isNonloop_of_mem_closure : ∀ {α : Type u_1} {M : Matroid α} {e f : α}, M.IsNonloop e → e ∈ M.closure {f} → M.IsNonloop f
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.limMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [W.IsStableUnderLimitsOfShape J] {X Y : CategoryTheory.Functor J C}
  (f : X ⟶ Y) [inst_3 : CategoryTheory.Limits.HasLimit X] [inst_4 : CategoryTheory.Limits.HasLimit Y],
  W.functorCategory J f → W (CategoryTheory.Limits.limMap f)
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.State.mk.sizeOf_spec : ∀ (params : Array Lean.Meta.Grind.TParam) (anchors : Array Lean.Meta.Grind.TAnchor✝) (hasSorry : Bool),
  sizeOf { params := params, anchors := anchors, hasSorry := hasSorry } =
    1 + sizeOf params + sizeOf anchors + sizeOf hasSorry
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedLength_eq_derivedLengthOfIdeal : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  LieAlgebra.derivedLength R ↥I = LieAlgebra.derivedLengthOfIdeal R L I
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
/-- The sum of two left fractions with the same denominator.  -/
CategoryTheory.MorphismProperty.LeftFraction₂.add : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₂ X Y → W.LeftFraction X Y
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.add_assoc : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F ((x.add y).add z) (x.add (y.add z))
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Given a surjective local homeomorphism `f : M → M'`, endow `M'` with a `ChartedSpace` structure
by pushing forward the `ChartedSpace` structure from `M`.  -/
IsLocalHomeomorph.chartedSpace : {H : Type u} →
  {M : Type u_2} →
    {M' : Type u_3} →
      [inst : TopologicalSpace M] →
        [inst_1 : TopologicalSpace M'] →
          [inst_2 : TopologicalSpace H] →
            [ChartedSpace H M] → {f : M → M'} → IsLocalHomeomorph f → Function.Surjective f → ChartedSpace H M'
-- Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions
/-- The `n`th convergent of the `GenContFract.of ξ` agrees with `ξ.convergent n`.  -/
Real.convs_eq_convergent : ∀ (ξ : ℝ) (n : ℕ), (GenContFract.of ξ).convs n = ↑(ξ.convergent n)
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comapEquiv_symm_coe : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R),
  ⇑(MvPolynomial.comapEquiv f).symm = MvPolynomial.comap ↑f.symm
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right_add_left : ∀ (m n k : ℕ), (k * m + n).gcd m = n.gcd m
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_of_liftPropWithinAt : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P → ChartedSpace.LiftPropWithinAt P g s x → s ∈ nhds x → ChartedSpace.LiftPropAt P g x
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `fallback` if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryGTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α × β → α × β
-- Mathlib.Order.Filter.Map
Filter.map_neBot_iff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {F : Filter α}, (Filter.map f F).NeBot ↔ F.NeBot
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_and : ∀ {v i : ℕ} {x y : BitVec v}, (x &&& y).getLsbD i = (x.getLsbD i && y.getLsbD i)
-- Mathlib.Algebra.GradedMonoid
/-- A version of `List.coe_dProd_set_like` with `Subtype.mk`.  -/
SetLike.list_dProd_eq : ∀ {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [inst : SetLike S R] [inst_1 : Monoid R]
  [inst_2 : AddMonoid ι] (A : ι → S) [inst_3 : SetLike.GradedMonoid A] (fι : α → ι) (fA : (a : α) → ↥(A (fι a)))
  (l : List α), l.dProd fι fA = ⟨(List.map (fun a => ↑(fA a)) l).prod, ⋯⟩
-- Mathlib.Topology.Separation.Regular
regularSpace_TFAE : ∀ (X : Type u) [inst : TopologicalSpace X],
  [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (nhdsSet s) (nhds x),
      ∀ (x : X) (s : Set X), Disjoint (nhdsSet s) (nhds x) ↔ x ∉ closure s,
      ∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s, ∀ (x : X), (nhds x).lift' closure ≤ nhds x,
      ∀ (x : X), (nhds x).lift' closure = nhds x].TFAE
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.mul_rpow_eq_ite : ∀ (x y : ENNReal) (z : ℝ), (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The map `LinearMap.rTensorHom` which sends `f ↦ f ⊗ 1` as a morphism of algebras.  -/
Module.End.rTensorAlgHom : (R : Type u_1) →
  (M : Type u_2) →
    (N : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → Module.End R M →ₐ[R] Module.End R (TensorProduct R M N)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.apply_skipWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos} {h : pos.skipWhile P ≠ s.endPos},
  ¬P ((pos.skipWhile P).get h)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_preΨ'_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {n : ℕ},
  ↑n ≠ 0 → (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) ≠ 0
-- Batteries.Data.PairingHeap
/-- `O(1)`. Merge two heaps. Ignore siblings.  -/
Batteries.PairingHeapImp.Heap.merge : {α : Type u_1} →
  (α → α → Bool) → Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α
-- Mathlib.Tactic.Linter.EmptyLine
/-- `filterMap stx f` takes as input a `Syntax` `stx` and a function `f : Syntax → α`.
It produces the array of the `some` values that `f` takes while traversing `stx`.

See `filterMapM` for a non-monadic version.
 -/
Lean.Syntax.filterMap : {α : Type} → Lean.Syntax → (Lean.Syntax → Option α) → Array α
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.shift : USize
-- Mathlib.Data.List.Rotate
/-- `IsRotated l₁ l₂` or `l₁ ~r l₂` asserts that `l₁` and `l₂` are cyclic permutations
of each other. This is defined by claiming that `∃ n, l.rotate n = l'`.  -/
List.IsRotated : {α : Type u} → List α → List α → Prop
-- Mathlib.Data.Matrix.Reflection
_private.Mathlib.Data.Matrix.Reflection.0.Matrix.transposeᵣ.match_1.splitter : {α : Type u_1} →
  (motive : (x x_1 : ℕ) → Matrix (Fin x) (Fin x_1) α → Sort u_2) →
    (x x_1 : ℕ) →
      (x_2 : Matrix (Fin x) (Fin x_1) α) →
        ((x : ℕ) → (x_3 : Matrix (Fin x) (Fin 0) α) → motive x 0 x_3) →
          ((x n : ℕ) → (A : Matrix (Fin x) (Fin (n + 1)) α) → motive x n.succ A) → motive x x_1 x_2
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.neg_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (-f) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp f g) h
-- Mathlib.Order.Hom.Lattice
LatticeHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (g : LatticeHom βᵒᵈ γᵒᵈ) (f : LatticeHom αᵒᵈ βᵒᵈ),
  LatticeHom.dual.symm (g.comp f) = (LatticeHom.dual.symm g).comp (LatticeHom.dual.symm f)
-- Batteries.Lean.EStateM
EStateM.Result.map_eq_ok : ∀ {ε σ α β : Type u_1} {f : α → β} {x : EStateM.Result ε σ α} {b : β} {s : σ},
  EStateM.Result.map f x = EStateM.Result.ok b s ↔ ∃ a, x = EStateM.Result.ok a s ∧ b = f a
-- Mathlib.ModelTheory.Skolem
/-- The structure assigning each function symbol of `L.skolem₁` to a skolem function generated with
choice.  -/
FirstOrder.Language.skolem₁Structure : {L : FirstOrder.Language} → {M : Type w} → [Nonempty M] → [L.Structure M] → L.skolem₁.Structure M
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_toLinearMapₛₗ₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] {σ₁ : R →+* R} [inst_7 : Fintype n]
  [inst_8 : Fintype m] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁)
  (b₂ : Module.Basis m R M₂) (M : Matrix n m N₂), (LinearMap.toMatrix₂ b₁ b₂) ((Matrix.toLinearMapₛₗ₂ σ₁ b₁ b₂) M) = M
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp : CategoryTheory.ConcreteCategory FiniteAddGrp.{u_1} fun x1 x2 => ↑x1.toAddGrp →+ ↑x2.toAddGrp
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.isPullback_iff_map_coyoneda_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  sq.IsPullback ↔ ∀ (X : Cᵒᵖ), (sq.map (CategoryTheory.coyoneda.obj X)).IsPullback
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₃_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.a₃ = 0
-- Mathlib.Order.Hom.Bounded
BoundedOrderHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : LE α] [inst_1 : LE β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] [inst_4 : FunLike F α β]
  [toRelHomClass : RelHomClass F (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2],
  (∀ (f : F), f ⊤ = ⊤) → (∀ (f : F), f ⊥ = ⊥) → BoundedOrderHomClass F α β
-- Mathlib.Data.List.Cycle
/-- The coercion from `List α` to `Cycle α`  -/
Cycle.ofList : {α : Type u_1} → List α → Cycle α
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The forgetful functor from `𝒪ₓ`-modules to presheaves of abelian groups.  -/
AlgebraicGeometry.Scheme.Modules.toPresheaf : (X : AlgebraicGeometry.Scheme) → CategoryTheory.Functor X.Modules (TopCat.Presheaf Ab ↑X.toPresheafedSpace)
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- If two continuous functions are a.e. equal, then they are equal.  -/
MeasureTheory.Measure.eq_of_ae_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {m : MeasurableSpace X} [inst_1 : TopologicalSpace Y]
  [T2Space Y] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {f g : X → Y},
  f =ᵐ[μ] g → Continuous f → Continuous g → f = g
-- Lean.Data.Lsp.Utf16
/-- Gets the LSP range of syntax `stx`.  -/
Lean.FileMap.lspRangeOfStx? : Lean.FileMap → Lean.Syntax → optParam Bool false → Option Lean.Lsp.Range
-- Mathlib.RingTheory.Ideal.Maps
/-- Any ring isomorphism induces an order isomorphism of ideals.  -/
RingEquiv.idealComapOrderIso : {R : Type u_1} → {S : Type u_2} → [inst : Semiring R] → [inst_1 : Semiring S] → R ≃+* S → Ideal S ≃o Ideal R
-- Init.Data.Int.Order
Int.not_ofNat_neg : ∀ (n : ℕ), ¬↑n < 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
PresheafOfModules.pullback_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R)
  {G : CategoryTheory.Functor D E} {T : CategoryTheory.Functor Eᵒᵖ RingCat} (ψ : R ⟶ G.op.comp T)
  [inst_4 : (PresheafOfModules.pushforward φ).IsRightAdjoint]
  [inst_5 : (PresheafOfModules.pushforward ψ).IsRightAdjoint] {T' : CategoryTheory.Functor E'ᵒᵖ RingCat}
  {G' : CategoryTheory.Functor E E'} (ψ' : T ⟶ G'.op.comp T')
  [inst_6 : (PresheafOfModules.pushforward ψ').IsRightAdjoint],
  (PresheafOfModules.pullback φ).isoWhiskerLeft (PresheafOfModules.pullbackComp ψ ψ') ≪≫
      PresheafOfModules.pullbackComp φ (CategoryTheory.CategoryStruct.comp ψ (G.op.whiskerLeft ψ')) =
    ((PresheafOfModules.pullback φ).associator (PresheafOfModules.pullback ψ) (PresheafOfModules.pullback ψ')).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (PresheafOfModules.pullbackComp φ ψ) (PresheafOfModules.pullback ψ') ≪≫
        PresheafOfModules.pullbackComp (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ)) ψ'
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorObj.eq_3 : ∀ (m : AugmentedSimplexCategory),
  (m = CategoryTheory.WithInitial.star → False) → m.tensorObj CategoryTheory.WithInitial.star = m
-- Mathlib.Data.Set.Sigma
Set.sigma_univ_range_eq : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : ι → Type u_6} {f : (i : ι) → α i → β i},
  (Set.univ.sigma fun i => Set.range (f i)) = Set.range fun x => ⟨x.fst, f x.fst x.snd⟩
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.quot_one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat),
  Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) CommRingCat.Colimits.Prequotient.one = 1
-- Init.Data.Range.Polymorphic.PRange
/-- This type class allows taking the intersection of a left-unbounded right-closed range with a
left-closed right-open range, resulting in another left-closed right-open range.
 -/
Std.Ric.HasRcoIntersection : Type w → Type w
-- Mathlib.Topology.UniformSpace.Basic
/-- The union of an entourage of the diagonal in each set of a disjoint union is again an entourage
of the diagonal.  -/
union_mem_uniformity_sum : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {a : SetRel α α},
  a ∈ uniformity α →
    ∀ {b : SetRel β β},
      b ∈ uniformity β → Prod.map Sum.inl Sum.inl '' a ∪ Prod.map Sum.inr Sum.inr '' b ∈ uniformity (α ⊕ β)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.hasColimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C
-- Mathlib.Util.Superscript
Mathlib.Tactic.subscriptTerm.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVec.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {w : ℕ}
  {refs : Vector Std.Sat.AIG.Fanin w} {hrefs : ∀ {i : ℕ} (h : i < w), refs[i].gate < aig.decls.size}
  {refs_1 : Vector Std.Sat.AIG.Fanin w} {hrefs_1 : ∀ {i : ℕ} (h : i < w), refs_1[i].gate < aig.decls.size},
  { refs := refs, hrefs := hrefs } = { refs := refs_1, hrefs := hrefs_1 } → refs = refs_1
-- Mathlib.Probability.Notation
/-- `𝔼[f | m]` is the conditional expectation of `f` with respect to `m`.  -/
ProbabilityTheory.«term𝔼[_|_]» : Lean.ParserDescr
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.iff_of_surjective : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Function.Surjective ⇑(algebraMap R S) → (Algebra.FormallyEtale R S ↔ IsIdempotentElem (RingHom.ker (algebraMap R S)))
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_enorm_lt_one : ∀ (α : Type u_2) [inst : NontriviallyNormedField α], ∃ x, 0 < ‖x‖ₑ ∧ ‖x‖ₑ < 1
-- Mathlib.Topology.MetricSpace.Equicontinuity
/-- Reformulation of `equicontinuousAt_iff_pair` for families of functions taking values in a
(pseudo) metric space.  -/
Metric.equicontinuousAt_iff_pair : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : TopologicalSpace β]
  {F : ι → β → α} {x₀ : β},
  EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- The head type  -/
PFunctor.A : PFunctor.{uA, uB} → Type uA
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableAt.mdifferentiableWithinAt : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt f x → MDiffAt[s] f x
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- The set in `countablePartition α n` to which `a : α` belongs.  -/
MeasurableSpace.countablePartitionSet : {α : Type u_1} → [m : MeasurableSpace α] → [h : MeasurableSpace.CountablyGenerated α] → ℕ → α → Set α
-- Batteries.Data.Nat.Lemmas
Nat.recDiagOn_succ_succ : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 n → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1))
  (m n : ℕ),
  Nat.recDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ =
    succ_succ m n (Nat.recDiagOn m n zero_zero zero_succ succ_zero succ_succ)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- The universal property of a strongly Cartesian morphism.

This lemma is more flexible with respect to non-definitional equalities than the field
`universal_property'` of `IsStronglyCartesian`.  -/
CategoryTheory.Functor.IsStronglyCartesian.universal_property : ∀ {𝒮 : 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 φ] {R' : 𝒮}
  {a' : 𝒳} (g : R' ⟶ R) (f' : R' ⟶ S),
  f' = CategoryTheory.CategoryStruct.comp g f →
    ∀ (φ' : a' ⟶ b) [p.IsHomLift f' φ'], ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.instMonoidWithZeroHomClassLocalizationMap : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N],
  MonoidWithZeroHomClass (S.LocalizationMap N) M N
-- Mathlib.Order.Hom.Lattice
SupHom.id_apply : ∀ {α : Type u_2} [inst : Max α] (a : α), (SupHom.id α) a = a
-- Mathlib.CategoryTheory.Types.Basic
/-- A one-field structure wrapping a function between types.  -/
TypeCat.Fun : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Init.Data.SInt.Lemmas
Int8.neg_mul_neg : ∀ (a b : Int8), -a * -b = a * b
-- Mathlib.Logic.Embedding.Basic
/-- If `f : α ↪ α'` is an embedding and `g : Π a, β α ↪ β' (f α)` is a family
of embeddings, then `Sigma.map f g` is an embedding.  -/
Function.Embedding.sigmaMap : {α : Type u_1} →
  {α' : Type u_2} →
    {β : α → Type u_3} →
      {β' : α' → Type u_4} → (f : α ↪ α') → ((a : α) → β a ↪ β' (f a)) → (a : α) × β a ↪ (a' : α') × β' a'
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.addCommMonoid : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddCommMonoid (β i)] → AddCommMonoid (Π₀ (i : ι), β i)
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.braiding_inv_hom : ∀ {R : Type u} [inst : CommRing R] (A B : CommAlgCat R),
  CommAlgCat.Hom.hom (β_ A B).inv = ↑(Algebra.TensorProduct.comm R ↑B ↑A)
-- Mathlib.FieldTheory.Normal.Basic
isSolvable_of_isScalarTower : ∀ (F : Type u_1) [inst : Field F] (K₁ : Type u_3) [inst_1 : Field K₁] [inst_2 : Algebra F K₁] (E : Type u_6)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra K₁ E] [IsScalarTower F K₁ E] [Normal F K₁]
  [h1 : Group.IsSolvable Gal(K₁/F)] [h2 : Group.IsSolvable Gal(E/K₁)], Group.IsSolvable Gal(E/F)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- The tilde construction is functorial.  -/
AlgebraicGeometry.tilde.map : {R : CommRingCat} → {M N : ModuleCat ↑R} → (M ⟶ N) → (AlgebraicGeometry.tilde M ⟶ AlgebraicGeometry.tilde N)