mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Core
Substring.Raw.mk.inj : ∀ {str : String} {startPos stopPos : String.Pos.Raw} {str_1 : String} {startPos_1 stopPos_1 : String.Pos.Raw},
  { str := str, startPos := startPos, stopPos := stopPos } =
      { str := str_1, startPos := startPos_1, stopPos := stopPos_1 } →
    str = str_1 ∧ startPos = startPos_1 ∧ stopPos = stopPos_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The truncation functor from simplicial objects to truncated simplicial objects.  -/
CategoryTheory.SimplicialObject.truncation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) → CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.SimplicialObject.Truncated C n)
-- Init.Data.Vector.Lemmas
Vector.getElem?_push_size : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α}, (xs.push x)[n]? = some x
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Turn a bijection `e : γ ≃ α` such that we have both `∀ T ∈ 𝔗, e '' T ∈ 𝔖` and
`∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗` into a uniform isomorphism `(γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β)` by pre-composing.  -/
UniformOnFun.congrLeft : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : UniformSpace β] →
        {𝔖 : Set (Set α)} →
          {𝔗 : Set (Set γ)} →
            (e : γ ≃ α) → 𝔗 ⊆ Set.image ⇑e ⁻¹' 𝔖 → 𝔖 ⊆ Set.preimage ⇑e ⁻¹' 𝔗 → UniformOnFun γ β 𝔗 ≃ᵤ UniformOnFun α β 𝔖
-- Mathlib.Control.Functor
Functor.Const.instInhabited : {α : Type u_1} → {β : Type u_2} → [Inhabited α] → Inhabited (Functor.Const α β)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.presburgerFunc.zero : FirstOrder.presburgerFunc 0
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_coe : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M), ↑(extChartAt I x) = ↑I ∘ ↑(chartAt H x)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedResult : Inhabited Lean.Meta.Simp.Result
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.filtration_succ : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  (i : (Module.rank F E).ord.ToType),
  IntermediateField.adjoin F
      (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio (Order.succ i)) =
    IntermediateField.restrictScalars F
      (↥(IntermediateField.adjoin F
            (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
              Set.Iio i)))⟮(Field.Emb.Cardinal.wellOrderedBasis F E) (Field.Emb.Cardinal.leastExt F E i)⟯
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
ConformalAt.congr : ∀ {X : Type u_1} {Y : Type u_2} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y] [inst_2 : NormedSpace ℝ X]
  [inst_3 : NormedSpace ℝ Y] {f g : X → Y} {x : X} {u : Set X},
  x ∈ u → IsOpen u → ConformalAt f x → (∀ x ∈ u, g x = f x) → ConformalAt g x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat],
  J.W.inverseImage (PresheafOfModules.toPresheaf R₀) =
    (CategoryTheory.MorphismProperty.isomorphisms (SheafOfModules R)).inverseImage (PresheafOfModules.sheafification α)
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_irrefl : ∀ {α : Type u_1} {r : α → α → Prop} {sym : Std.Symm r}, Std.Irrefl r ↔ ∀ {z : Sym2 α}, z ∈ Sym2.fromRel sym → ¬z.IsDiag
-- Lean.Data.Json.Basic
/-- Creates a json number from a positive float, panicking if it isn't.
[todo]EdAyers: Currently goes via a string representation, when more float primitives are available
should switch to using those.  -/
_private.Lean.Data.Json.Basic.0.Lean.JsonNumber.fromPositiveFloat! : Float → Lean.JsonNumber
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.baseIso_inv : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {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] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ'),
  (CategoryTheory.Limits.CatCospanTransform.baseIso e).inv = e.inv.base
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.equivPolynomial_single : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_6} [inst_1 : CommRing S] [inst_2 : Algebra R S] (n : ℕ) (x : S),
  PolynomialModule.equivPolynomial (PolynomialModule.single R n x) = (Polynomial.monomial n) x
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_neg_left : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), ⁅-a, b⁆ = -a + ⁅b, a⁆ + a
-- Init.Data.List.MinMax
List.min_eq_iff : ∀ {α : Type u_1} {a : α} [inst : Min α] [inst_1 : LE α] {l : List α} [Std.IsLinearOrder α] [Std.LawfulOrderMin α]
  (hl : l ≠ []), l.min hl = a ↔ a ∈ l ∧ ∀ b ∈ l, a ≤ b
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRoots.eq_1 : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (n : ℕ) (a : R),
  Polynomial.nthRoots n a = (Polynomial.X ^ n - Polynomial.C a).roots
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.SpanningTree.loopOfHom.eq_1 : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {a b : G}
  (p : a ⟶ b),
  IsFreeGroupoid.SpanningTree.loopOfHom T p =
    CategoryTheory.CategoryStruct.comp (IsFreeGroupoid.SpanningTree.treeHom T a)
      (CategoryTheory.CategoryStruct.comp p (CategoryTheory.inv (IsFreeGroupoid.SpanningTree.treeHom T b)))
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instLattice : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [Lattice Y] → [inst_2 : Zero Y] → Lattice (Function.locallyFinsuppWithin U Y)
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.HasIsos.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C},
  (∀ {S T : C} (f : S ⟶ T) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ J.coverings T) → J.HasIsos
-- Mathlib.Algebra.Module.Presentation.Tautological
_private.Mathlib.Algebra.Module.Presentation.Tautological.0.Module.Presentation.tautologicalRelations.match_1.eq_1 : ∀ (A : Type u_2) (M : Type u_1) (motive : Module.Presentation.tautological.R A M → Sort u_3) (m₁ m₂ : M)
  (h_1 : (m₁ m₂ : M) → motive (Module.Presentation.tautological.R.add m₁ m₂))
  (h_2 : (a : A) → (m : M) → motive (Module.Presentation.tautological.R.smul a m)),
  (match Module.Presentation.tautological.R.add m₁ m₂ with
    | Module.Presentation.tautological.R.add m₁ m₂ => h_1 m₁ m₂
    | Module.Presentation.tautological.R.smul a m => h_2 a m) =
    h_1 m₁ m₂
-- Mathlib.FieldTheory.Normal.Closure
/-- `normalClosure F K L` is a valid normal closure if `K/F` is algebraic
and all minimal polynomials of `K/F` splits in `L/F`.  -/
Algebra.IsAlgebraic.isNormalClosure_normalClosure : ∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [Algebra.IsAlgebraic F K],
  (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
    IsNormalClosure F K ↥(IntermediateField.normalClosure F K L)
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `elemExponent_def` using `ExpChar`.  -/
IsPurelyInseparable.elemExponent_def' : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] (a : L),
  a ^ p ^ IsPurelyInseparable.elemExponent K a ∈ (algebraMap K L).range
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a a' : α}, t.get? a = some a' → a' ∈ t
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.addConj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.AddGrpObj G],
  CategoryTheory.AddGrpObj.addConj G =
    CategoryTheory.SemiCartesianMonoidalCategory.fst G G + CategoryTheory.SemiCartesianMonoidalCategory.snd G G +
      -CategoryTheory.SemiCartesianMonoidalCategory.fst G G
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOpId_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.Functor.rightOpId C).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.op X))
-- Mathlib.CategoryTheory.ObjectProperty.Ind
/-- If `C` is finitely accessible and `P` implies finitely presentable, then `X`
satisfies `ind P` if and only if every morphism `Z ⟶ X` from a finitely presentable object
factors via an object satisfying `P`.  -/
CategoryTheory.ObjectProperty.ind_iff_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P ≤ CategoryTheory.ObjectProperty.isFinitelyPresentable C →
    ∀ [CategoryTheory.IsFinitelyAccessibleCategory C] {X : C},
      P.ind X ↔
        ∀ {Z : C} (g : Z ⟶ X) [CategoryTheory.IsFinitelyPresentable Z],
          ∃ W u v, CategoryTheory.CategoryStruct.comp u v = g ∧ P W
-- Mathlib.Algebra.Prime.Defs
Prime.not_dvd_mul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → ∀ {a b : M}, ¬p ∣ a → ¬p ∣ b → ¬p ∣ a * b
-- Mathlib.Algebra.Polynomial.Div
Polynomial.degree_eq_one_of_irreducible_of_root : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} [IsDomain R], Irreducible p → ∀ {x : R}, p.IsRoot x → p.degree = 1
-- Init.Data.Int.DivMod.Basic
_private.Init.Data.Int.DivMod.Basic.0.Int.fdiv.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (m = 0 → False) →
    (match Int.ofNat m, Int.ofNat n with
      | 0, x => h_1 x
      | Int.ofNat m, Int.ofNat n => h_2 m n
      | Int.ofNat m.succ, Int.negSucc n => h_3 m n
      | Int.negSucc a, 0 => h_4 a
      | Int.negSucc m, Int.ofNat n.succ => h_5 m n
      | Int.negSucc m, Int.negSucc n => h_6 m n) =
      h_2 m n
-- Mathlib.Order.Minimal
/-- **Alias** of `Minimal.notMem_of_prop_sdiff_singleton`. -/
Minimal.notMem_of_prop_diff_singleton : ∀ {α : Type u_2} {x : α} {P : Set α → Prop} {s : Set α}, Minimal P s → P (s \ {x}) → x ∉ s
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDivInvMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : DivInvMonoid Mᵐᵒᵖ], DomMulAct.instDivInvMonoidOfMulOpposite = inst
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.isPlot_const : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {n : ℕ} {x : X}, Diffeology.IsPlot fun x_1 => x
-- Mathlib.Order.RelIso.Basic
RelIso.surjective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), Function.Surjective ⇑e
-- Mathlib.Logic.Equiv.Set
Equiv.set_forall_iff : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) {p : Set α → Prop}, (∀ (a : Set α), p a) ↔ ∀ (a : Set β), p (⇑e ⁻¹' a)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- If `f b = 1` for all `b ∈ t`, then the product of `f a` with `a ∈ s` is the same as the
product of `f a` with `a ∈ s ∖ t`.  -/
tprod_setElem_eq_tprod_setElem_sdiff : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (s t : Set β),
  (∀ b ∈ t, f b = 1) → ∏' (a : ↑s), f ↑a = ∏' (a : ↑(s \ t)), f ↑a
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.toPresentation_relation : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S) (a : Fin (Nat.succ 1)),
  P.toPresentation.relation a =
    ![(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f),
        (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.g) * MvPolynomial.X 1 - 1]
      a
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_add_eq_right : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x y : K},
  0 < ArchimedeanClass.mk x → ArchimedeanClass.stdPart (x + y) = ArchimedeanClass.stdPart y
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
/-- This function is used in lemmas about iterator equivalence (`Iter.Equiv` and `IterM.Equiv`).

If the given step contains a successor iterator, replaces the iterator with the quotient of its
bundled version.
 -/
Std.IterStep.bundledQuotient : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [Std.Iterator α m β] →
        [inst : Monad m] →
          [inst_1 : LawfulMonad m] → Std.IterStep (Std.IterM m β) β → Std.IterStep (Quot (Std.BundledIterM.Equiv m β)) β
-- Lean.Data.Json.Parser
Lean.Json.Parser.anyCore : Std.Internal.Parsec.String.Parser Lean.Json
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.sub_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f g : E →ₛₗ.[σ] F)
  (x : ↥(f.domain ⊓ g.domain)), ↑(f - g) x = ↑f ⟨↑x, ⋯⟩ - ↑g ⟨↑x, ⋯⟩
-- Init.Data.List.Pairwise
List.pairwise_filterMap : ∀ {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {f : β → Option α} {l : List β},
  List.Pairwise R (List.filterMap f l) ↔
    List.Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac : Lean.Grind.AC.Seq →
  Lean.Grind.AC.Seq →
    Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Trie.node.injEq : ∀ {α : Type} (values : Array α) (star : Lean.Meta.LazyDiscrTree.TrieIndex)
  (children : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex)
  (pending : Array (Lean.Meta.LazyDiscrTree.LazyEntry α)) (values_1 : Array α)
  (star_1 : Lean.Meta.LazyDiscrTree.TrieIndex)
  (children_1 : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex)
  (pending_1 : Array (Lean.Meta.LazyDiscrTree.LazyEntry α)),
  ({ values := values, star := star, children := children, pending := pending } =
      { values := values_1, star := star_1, children := children_1, pending := pending_1 }) =
    (values = values_1 ∧ star = star_1 ∧ children = children_1 ∧ pending = pending_1)
-- Lean.Parser.Command
Lean.Parser.Command.exit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors equals minus the unoriented angle if the sign is
negative.  -/
Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign = -1 → o.oangle x y = -↑(InnerProductGeometry.angle x y)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃}
  (h : CategoryTheory.CategoryStruct.comp (F.map f₀₁) (CategoryTheory.CategoryStruct.comp (F.map f₁₂) (F.map f₂₃)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) h) =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom h))
-- Mathlib.Algebra.Order.Module.Defs
PosSMulStrictMono.lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] (f : β → γ) [inst_5 : Zero α] [PosSMulStrictMono α γ],
  (∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) → (∀ (a : α) (b : β), f (a • b) = a • f b) → PosSMulStrictMono α β
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `norm_le_norm_add_norm_sub'`. -/
norm_le_insert' : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (u v : E), ‖u‖ ≤ ‖v‖ + ‖u - v‖
-- Mathlib.Algebra.Group.Basic
mul_eq_one_iff_inv_eq : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a * b = 1 ↔ a⁻¹ = b
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.hab : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  (self : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f),
  CategoryTheory.CategoryStruct.comp (self.c.π.app self.i) self.a =
    CategoryTheory.CategoryStruct.comp (self.c.π.app self.i) self.b
-- Mathlib.Topology.Inseparable
/-- **Alias** of the reverse direction of `stableUnderSpecialization_compl_iff`. -/
StableUnderGeneralization.compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, StableUnderGeneralization s → StableUnderSpecialization sᶜ
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_one : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)], WittVector.ghostFun✝ 1 = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_preΨ₄ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 2 ≠ 0 → W.preΨ₄.natDegree = 6
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instLeast?Nat : Std.PRange.Least? ℕ
-- Mathlib.RingTheory.Polynomial.Pochhammer
Nat.cast_factorial : ∀ (S : Type u_1) [inst : Semiring S] (a : ℕ), ↑a.factorial = Polynomial.eval 1 (ascPochhammer S a)
-- Mathlib.Order.BooleanAlgebra.Set
Set.insert_sdiff_subset : ∀ {α : Type u_1} {s t : Set α} {a : α}, insert a s \ t ⊆ insert a (s \ t)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_zero : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (p : Submodule R M) [inst_6 : RingHomSurjective σ₁₂], Submodule.map 0 p = ⊥
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.ConfigWithKey.mk.injEq : ∀ (config : Lean.Meta.Config) (key : UInt64) (config_1 : Lean.Meta.Config) (key_1 : UInt64),
  ({ config := config, key := key } = { config := config_1, key := key_1 }) = (config = config_1 ∧ key = key_1)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Isomorphisms from identities in ℕ.  -/
CategoryTheory.SimplicialObject.eqToIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      {n m : ℕ} → n = m → (X.obj (Opposite.op { len := n }) ≅ X.obj (Opposite.op { len := m }))
-- Mathlib.Topology.NhdsKer
nhdsSet_nhdsKer : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s : Set X), nhdsSet (nhdsKer s) = nhdsSet s
-- Mathlib.LinearAlgebra.Matrix.RowCol
/-- Update, i.e. replace the `j`th column of matrix `A` with the values in `b`.  -/
Matrix.updateCol : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [DecidableEq n] → Matrix m n α → n → (m → α) → Matrix m n α
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
borel_eq_generateFrom_Iio : ∀ (α : Type u_1) [inst : TopologicalSpace α] [SecondCountableTopology α] [inst_2 : LinearOrder α] [OrderTopology α],
  borel α = MeasurableSpace.generateFrom (Set.range Set.Iio)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  (DoubleQuot.quotQuotEquivQuotSupₐ R I J).symm.toRingEquiv = (DoubleQuot.quotQuotEquivQuotSup I J).symm
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- Goals before the flexible tactic  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData.goals : Mathlib.Linter.Flexible.StainData✝ → List Lean.MVarId
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp]
  {k : α}, k ∈ t.keys ↔ k ∈ t
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.equivOfEq_symm : ∀ {F : Type u_4} [inst : Field F] {E : Type u_5} [inst_1 : Field E] [inst_2 : Algebra F E] {S T : IntermediateField F E}
  (h : S = T), (IntermediateField.equivOfEq h).symm = IntermediateField.equivOfEq ⋯
-- Mathlib.CategoryTheory.SingleObj
/-- There is a 1-1 correspondence between monoid homomorphisms `M → N` and functors between the
corresponding single-object categories. It means that `SingleObj` is a fully faithful functor.  -/
CategoryTheory.SingleObj.mapHom : (M : Type u) →
  [inst : Monoid M] →
    (N : Type v) →
      [inst_1 : Monoid N] → (M →* N) ≃ CategoryTheory.Functor (CategoryTheory.SingleObj M) (CategoryTheory.SingleObj N)
-- Mathlib.Algebra.Ring.Periodic
Multiset.periodic_prod : ∀ {α : Type u_1} {β : Type u_2} {c : α} [inst : Add α] [inst_1 : CommMonoid β] (s : Multiset (α → β)),
  (∀ f ∈ s, Function.Periodic f c) → Function.Periodic s.prod c
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.homEquiv_apply : ∀ {R S : CommRingCat} (f : AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R),
  AlgebraicGeometry.Spec.homEquiv f = AlgebraicGeometry.Spec.preimage f
-- Mathlib.Topology.UnitInterval
unitInterval.toNNReal_zero : unitInterval.toNNReal 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cos θ` to the
value `sin ((n + 1) * θ) / sin θ`.  -/
Polynomial.Chebyshev.U_real_cos : ∀ (θ : ℝ) (n : ℤ), Polynomial.eval (Real.cos θ) (Polynomial.Chebyshev.U ℝ n) * Real.sin θ = Real.sin ((↑n + 1) * θ)
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
_private.Mathlib.CategoryTheory.Limits.Shapes.Countable.0.CategoryTheory.Limits.IsCofiltered.preorder_of_cofiltered_countable : (J : Type u_3) →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsCofiltered J] →
      [CategoryTheory.CountableCategory J] →
        ProofWanted (∃ I x, ∃ (_ : Countable I) (_ : CategoryTheory.IsCofiltered I), ∃ F, F.Initial)