mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Basic
/-- **Alias** of `Convex.setOfPred_const_imp`. -/
Convex.setOf_const_imp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {P : Prop}, Convex 𝕜 s → Convex 𝕜 {x | P → x ∈ s}
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_toNat_eq_finrank : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] (A : Matrix m n R),
  A.eRank.toNat = Module.finrank R ↥(Submodule.span R (Set.range A.col))
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `f ◁ η`.  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft : (Type → Type) → Type
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.polynomialEquiv_symm : ∀ (R : Type u) [inst : CommRing R] (P : Polynomial R),
  (KaehlerDifferential.polynomialEquiv R).symm P = P • (KaehlerDifferential.D R (Polynomial R)) Polynomial.X
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k fallback : α},
  (Std.TreeMap.filterMap f t).getKeyD k fallback = ((t.getKey? k).pfilter fun x h' => (f x t[x]).isSome).getD fallback
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ RingCat SemiRingCat
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.fromLoop_symm_toLoop : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] {i : N}
  {p : ↑(GenLoop N X x)}, GenLoop.fromLoop i (Path.symm (GenLoop.toLoop i p)) = GenLoop.symmAt i p
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.add_subset_closure : ∀ {M : Type u_3} [inst : AddMonoid M] {s t u : Set M}, s ⊆ u → t ⊆ u → s + t ⊆ ↑(AddSubmonoid.closure u)
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable within `S` at `y ∈ S`, then the
slope of any secant line with right endpoint at `y` is strictly less than the derivative of `f`
within `S` at `y`.

This is fractionally weaker than `StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio` but simpler to
apply under a `DifferentiableOn S` hypothesis.  -/
StrictConvexOn.slope_lt_of_hasDerivWithinAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' S y → slope f x y < f'
-- Mathlib.Analysis.Seminorm
Seminorm.mk : {𝕜 : Type u_12} →
  {E : Type u_13} →
    [inst : SeminormedRing 𝕜] →
      [inst_1 : AddGroup E] →
        [inst_2 : SMul 𝕜 E] →
          (toAddGroupSeminorm : AddGroupSeminorm E) →
            (∀ (a : 𝕜) (x : E), toAddGroupSeminorm.toFun (a • x) = ‖a‖ * toAddGroupSeminorm.toFun x) → Seminorm 𝕜 E
-- Mathlib.CategoryTheory.Filtered.Small
/-- The first part of a factoring of a functor from a small category to a filtered category through
a small filtered category.  -/
CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoring : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          (F : CategoryTheory.Functor D C) →
            CategoryTheory.Functor D (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instCategory.eq_1 : AddCommGrpCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := AddMonoidHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @AddCommGrpCat.instCategory._proof_1,
    comp_id := @AddCommGrpCat.instCategory._proof_2, assoc := @AddCommGrpCat.instCategory._proof_3 }
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.self : ∀ (R : Type u_1) [inst : Semiring R], Module.Finite R R
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- Restricting scalars along a composition is isomorphic to the composition
of restriction of scalars.  -/
AlgCat.restrictScalarsComp' : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            (f : R →+* S) →
              (g : S →+* T) →
                (gf : R →+* T) →
                  gf = g.comp f →
                    (AlgCat.restrictScalars gf ≅ (AlgCat.restrictScalars g).comp (AlgCat.restrictScalars f))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_mul_lt_iff₀` for a version with multiplication on the other side.  -/
inv_mul_lt_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (c⁻¹ * b < a ↔ b < a * c)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instIsCancelMul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Mul M] [IsCancelMul M], IsCancelMul (l.Germ M)
-- Mathlib.Algebra.Group.Commute.Basic
SemiconjBy.function_semiconj_mul_left : ∀ {G : Type u_1} [inst : Semigroup G] {a b c : G},
  SemiconjBy a b c → Function.Semiconj (fun x => a * x) (fun x => b * x) fun x => c * x
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sheaf.pushforwardOverMapIso_inv_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] (F : CategoryTheory.Sheaf J A) {X Y : C} (f : X ⟶ Y)
  (X_1 : (CategoryTheory.Over X)ᵒᵖ),
  (F.pushforwardOverMapIso f).inv.hom.app X_1 =
    CategoryTheory.CategoryStruct.id (F.obj.obj (Opposite.op (Opposite.unop X_1).left))
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.toPresheafedSpace : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → AlgebraicGeometry.SheafedSpace C → AlgebraicGeometry.PresheafedSpace C
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.instHasImagesSheafType : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C},
  CategoryTheory.Limits.HasImages (CategoryTheory.Sheaf J (Type (max v u)))
-- Mathlib.Analysis.Convex.Mul
ConcaveOn.mul_convexOn' : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E] [inst_6 : AddCommGroup G] [inst_7 : Module 𝕜 G]
  [inst_8 : Module 𝕜 E] {s : Set G} [IsOrderedModule 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f g : G → E},
  ConcaveOn 𝕜 s f →
    ConvexOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → f x ≤ 0) → (∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x) → AntivaryOn f g s → ConcaveOn 𝕜 s (f • g)
-- Lean.Elab.ParseImportsFast
/-- Simpler and faster version of `parseImports`. We use it to implement Lake.
 -/
Lean.parseImports' : String → String → IO Lean.ModuleHeader
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.compare_maxKeyD_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β} {fallback : α}, cmp ((t.modify k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.Order.Filter.AtTopBot.Finite
/-- If `u` is a sequence which is unbounded above,
then after any point, it reaches a value strictly greater than all previous values.
 -/
Filter.high_scores : ∀ {β : Type u_4} [inst : LinearOrder β] [NoMaxOrder β] {u : ℕ → β},
  Filter.Tendsto u Filter.atTop Filter.atTop → ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u k < u n
-- Mathlib.Algebra.Lie.Character
LieAlgebra.lieCharacterEquivLinearDual_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : IsLieAbelian L]
  (χ : LieAlgebra.LieCharacter R L), LieAlgebra.lieCharacterEquivLinearDual χ = ↑χ
-- Mathlib.SetTheory.Cardinal.Free
FreeCommRing.eq_1 : ∀ (α : Type u), FreeCommRing α = FreeAbelianGroup (Multiplicative (Multiset α))
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.isFixedPt_piMap : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i},
  Function.IsFixedPt (Pi.map f) x ↔ ∀ (i : ι), Function.IsFixedPt (f i) (x i)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Given a triangle, and a fourth point such that twice the angle between two points of the
triangle at that fourth point equals twice the third angle of the triangle, the fourth point
lies in the circumsphere of the triangle.  -/
Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {t : Affine.Triangle ℝ P} {p : P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        2 • EuclideanGeometry.oangle (t.points i₁) p (t.points i₃) =
            2 • EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃) →
          p ∈ Affine.Simplex.circumsphere t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Inv : Std.Tactic.BVDecide.BVExpr.Assignment →
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) → Std.Tactic.BVDecide.BVExpr.Cache aig → Prop
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.ι_obj_lift_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X Y : C}
  (f : X ⟶ Y), P.ι.map ((P.lift F hF).map f) = F.map f
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.forall_apply_eq_apply_iff : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α},
  P.IsRepFun f → ∀ (a : α), (∀ (x : α), f a = f x ↔ a = x) ∨ ∀ (x : α), f a = f x ↔ P.Rel a x
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.invStructInv_homInvId : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} (I : hom.InvStruct),
  I.invStructInv.homInvId = I.invHomId
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isLE_of_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (p q : ℤ),
  autoParam (p ≤ q) CategoryTheory.Triangulated.TStructure.isLE_of_le._auto_1 → ∀ [t.IsLE X p], t.IsLE X q
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a `G`-representation `A` on which a normal subgroup `S ≤ G` acts trivially, the
induced map `H₁(G, A) ⟶ H₁(G ⧸ S, A)` is an epimorphism.  -/
groupHomology.H1CoresCoinfOfTrivial_g_epi : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal]
  [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)],
  CategoryTheory.Epi (groupHomology.H1CoresCoinfOfTrivial A S).g
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.instSMulNatTerm : {α : Type u_1} → SMul ℕ (FirstOrder.Language.presburger.Term α)
-- Init.Data.Option.Basic
instLEOption : {α : Type u_1} → [LE α] → LE (Option α)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.id.match_1.eq_2 : ∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → Sort u_2)
  (h_1 : (a : C) → motive (CategoryTheory.WithInitial.of a)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.smul_eball : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal), c • Metric.eball x r = Metric.eball (c • x) r
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Local notation for `starRingEnd _`  -/
_private.Mathlib.Analysis.InnerProductSpace.Defs.0.InnerProductSpace.Core.«term_†» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.equalizer_ι_isLocalHom : ∀ (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CommRingCat),
  IsLocalHom (CommRingCat.Hom.hom (CategoryTheory.Limits.limit.π F CategoryTheory.Limits.WalkingParallelPair.zero))
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_rel₁ : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M}
  {R : L.Relations 1} {t : L.Term (α ⊕ Fin l)},
  (R.boundedFormula₁ t).Realize v xs ↔
    FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize (Sum.elim v xs) t]
-- Mathlib.FieldTheory.PerfectClosure
/-- Embedding of `K` into `PerfectClosure K p`  -/
PerfectClosure.of : (K : Type u) →
  [inst : CommRing K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → K →+* PerfectClosure K p
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.IsStrictSegal.mk : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)},
  (∀ (m : ℕ) (h : autoParam (m ≤ n + 1) SSet.Truncated.IsStrictSegal._auto_1), Function.Bijective (X.spine m h)) →
    X.IsStrictSegal
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.FunctorToTypes.naturality_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type u_1)}
  {G : CategoryTheory.Functor C (Type u_2)} (e : (j : C) → F.obj j ≃ G.obj j),
  (∀ {j j' : C} (f : j ⟶ j'),
      ⇑(e j') ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) =
        ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)) →
    ∀ {j j' : C} (f : j ⟶ j'),
      ⇑(e j').symm ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) =
        ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_top_iff : ∀ {α : Type u_1} {r : α → α → Prop} {sym : Std.Symm r}, Sym2.fromRel sym = Set.univ ↔ r = ⊤
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalNameExpr : Lean.Expr → Lean.MetaM Lean.Name
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositions_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsStableUnderTransfiniteComposition], CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u} W ≤ W
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.ext : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] {f g : M [⋀^ι]→L[R] N}, (∀ (x : ι → M), f x = g x) → f = g
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The `finrank` of the direct sum is the sum of the `finrank`s.  -/
Module.finrank_directSum : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι] (M : ι → Type w)
  [inst_3 : (i : ι) → AddCommMonoid (M i)] [inst_4 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)]
  [∀ (i : ι), Module.Finite R (M i)], Module.finrank R (DirectSum ι fun i => M i) = ∑ i, Module.finrank R (M i)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- Implementation detail for `optionEquivLeft`. Use `MvPowerSeries.optionEquivLeft` instead.  -/
_private.Mathlib.RingTheory.MvPowerSeries.Equiv.0.MvPowerSeries.optionFunLeft : (σ : Type u_1) → (R : Type u_2) → [CommSemiring R] → MvPowerSeries (Option σ) R → PowerSeries (MvPowerSeries σ R)
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `I` is a prime ideal of `R[X]` and `pX ∈ I` is a non-constant polynomial,
then the map `R →+* R[x]/I` descends to an integral map when localizing at `pX.leadingCoeff`.
In particular `X` is integral because it satisfies `pX`, and constants are trivially integral,
so integrality of the entire extension follows by closure under addition and multiplication.  -/
Polynomial.isIntegral_isLocalization_polynomial_quotient : ∀ {R : Type u_1} [inst : CommRing R] {Rₘ : Type u_3} {Sₘ : Type u_4} [inst_1 : CommRing Rₘ] [inst_2 : CommRing Sₘ]
  (P : Ideal (Polynomial R)),
  ∀ pX ∈ P,
    ∀ [inst_3 : Algebra (R ⧸ Ideal.comap Polynomial.C P) Rₘ]
      [inst_4 :
        IsLocalization.Away (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff Rₘ]
      [inst_5 : Algebra (Polynomial R ⧸ P) Sₘ]
      [inst_6 :
        IsLocalization
          (Submonoid.map (Ideal.quotientMap P Polynomial.C ⋯)
            (Submonoid.powers (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff))
          Sₘ],
      (IsLocalization.map Sₘ (Ideal.quotientMap P Polynomial.C ⋯) ⋯).IsIntegral
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The natural isomorphism between pushforward of the composition and the composition of
pushforward functors.  -/
CategoryTheory.ExponentiableMorphism.pushforwardComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J K : C} →
      (f : I ⟶ J) →
        (g : J ⟶ K) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong f] →
            [inst_2 : CategoryTheory.ChosenPullbacksAlong g] →
              [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)] →
                [inst_4 : CategoryTheory.ExponentiableMorphism f] →
                  [inst_5 : CategoryTheory.ExponentiableMorphism g] →
                    [inst_6 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.comp f g)] →
                      CategoryTheory.ExponentiableMorphism.pushforward (CategoryTheory.CategoryStruct.comp f g) ≅
                        (CategoryTheory.ExponentiableMorphism.pushforward f).comp
                          (CategoryTheory.ExponentiableMorphism.pushforward g)
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.foldM.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (α × Batteries.PairingHeapImp.Heap α) → Sort u_2) (hd : α)
  (tl : Batteries.PairingHeapImp.Heap α) (h_1 : some (hd, tl) = none → motive none)
  (h_2 :
    (hd_1 : α) →
      (tl_1 : Batteries.PairingHeapImp.Heap α) → some (hd, tl) = some (hd_1, tl_1) → motive (some (hd_1, tl_1))),
  (match eq : some (hd, tl) with
    | none => h_1 eq
    | some (hd_1, tl_1) => h_2 hd_1 tl_1 eq) =
    h_2 hd tl ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombinationLineMapWeights_apply_left : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] {i j : ι},
  i ≠ j → ∀ (c : k), Finset.affineCombinationLineMapWeights i j c i = 1 - c
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.id_comp : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (F : L →ᴸ L'), (FirstOrder.Language.LHom.id L').comp F = F
-- Lean.Elab.Coinductive
Lean.Elab.Command.removeFunctorPostfix : Lean.Name → Lean.Name
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.mapIso_hom : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y : CategoryTheory.GradedObject I C} (e : X ≅ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p] (i : J),
  (CategoryTheory.GradedObject.mapIso e p).hom i = CategoryTheory.GradedObject.mapMap e.hom p i
-- Mathlib.Logic.Equiv.Prod
Equiv.sumArrowEquivProdArrow_symm_apply_inl : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α → γ) (g : β → γ) (a : α),
  (Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inl a) = f a
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_nsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.operation_pure : ∀ {m : Type w → Type w'} [inst : Monad m] {α : Type w} {x : α}, (pure x).operation = pure ⟨x, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
exp_neg_mul_sq_isLittleO_exp_neg : ∀ {b : ℝ}, 0 < b → (fun x => Real.exp (-b * x ^ 2)) =o[Filter.atTop] fun x => Real.exp (-x)
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.prod_Icc_factorial : ∀ (n : ℕ), ∏ x ∈ Finset.Icc 1 n, x.factorial = n.superFactorial
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.CotangentSpace.compEquiv.eq_1 : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  Algebra.Generators.CotangentSpace.compEquiv Q P =
    (Q.comp P).cotangentSpaceBasis.repr.trans
      (Q.cotangentSpaceBasis.prod (Module.Basis.baseChange T P.cotangentSpaceBasis)).repr.symm
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.map_exact : ∀ {R : Type u_2} [inst : CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} {M'' : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] [inst_5 : AddCommGroup M'']
  [inst_6 : Module R M''] {f : M →ₗ[R] M'} {g : M' →ₗ[R] M''},
  Function.Exact ⇑f ⇑g → Function.Surjective ⇑g → Function.Exact ⇑((QuotSMulTop.map r) f) ⇑((QuotSMulTop.map r) g)
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.isRight_left : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {d : δ},
  Sum.LiftRel r s x (Sum.inr d) → x.isRight = true
-- Mathlib.Algebra.Polynomial.Div
/-- Division by a monic polynomial doesn't change the leading coefficient.  -/
Polynomial.leadingCoeff_divByMonic_of_monic : ∀ {R : Type u} [inst : CommRing R] {p q : Polynomial R},
  q.Monic → q.degree ≤ p.degree → (p /ₘ q).leadingCoeff = p.leadingCoeff
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.eq_1 : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (g : ι → β)
  (s : Set ι), AntivaryOn f g s = ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → g i < g j → f j ≤ f i
-- Mathlib.Data.Matrix.Reflection
Matrix.transposeᵣ.eq_1 : ∀ {α : Type u_1} (x : ℕ) (x_4 : Matrix (Fin x) (Fin 0) α), x_4.transposeᵣ = Matrix.of ![]
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.Dual.eq_of_ker_eq_of_apply_eq : ∀ {K : Type u_1} {V₁ : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [FiniteDimensional K V₁] {f g : Module.Dual K V₁} (x : V₁),
  LinearMap.ker f = LinearMap.ker g → f x = g x → f x ≠ 0 → f = g
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.hasBasis_nhds_prod : ∀ {α : Type ua} [inst : UniformSpace α] (x y : α),
  (nhds (x, y)).HasBasis (fun s => s ∈ uniformity α ∧ SetRel.IsSymm s) fun s =>
    UniformSpace.ball x s ×ˢ UniformSpace.ball y s
-- Init.GetElem
Fin.getElem?_fin : ∀ {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → ℕ → Prop} {n : ℕ} [h : GetElem? Cont ℕ Elem Dom] (a : Cont)
  (i : Fin n), a[i]? = a[↑i]?
-- Mathlib.Order.Hom.Set
OrderIso.image_eq_preimage_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (s : Set α), ⇑e '' s = ⇑e.symm ⁻¹' s
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.mk.injEq : ∀ {α : Type u_1} {s : Set α} (toFun : ℕ → Set α) (finite' : ∀ (n : ℕ), Finite ↑(toFun n))
  (subset_succ' : ∀ (n : ℕ), toFun n ⊆ toFun (n + 1)) (iUnion_eq' : ⋃ n, toFun n = s) (toFun_1 : ℕ → Set α)
  (finite'_1 : ∀ (n : ℕ), Finite ↑(toFun_1 n)) (subset_succ'_1 : ∀ (n : ℕ), toFun_1 n ⊆ toFun_1 (n + 1))
  (iUnion_eq'_1 : ⋃ n, toFun_1 n = s),
  ({ toFun := toFun, finite' := finite', subset_succ' := subset_succ', iUnion_eq' := iUnion_eq' } =
      { toFun := toFun_1, finite' := finite'_1, subset_succ' := subset_succ'_1, iUnion_eq' := iUnion_eq'_1 }) =
    (toFun = toFun_1)