mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `StructuredArrow d F` is filtered for any `d : D`, then `F : C ⥤ D` is final. This is
simply because filtered categories are connected. More profoundly, the converse is also true if
`C` is filtered, see `final_iff_isFiltered_structuredArrow`.  -/
CategoryTheory.Functor.final_of_isFiltered_structuredArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [∀ (d : D), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)], F.Final
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_7.splitter : (motive : Std.Tactic.BVDecide.BVPred → Sort u_1) →
  (pred : Std.Tactic.BVDecide.BVPred) →
    ((w : ℕ) →
        (lhs : Std.Tactic.BVDecide.BVExpr w) →
          (op : Std.Tactic.BVDecide.BVBinPred) →
            (rhs : Std.Tactic.BVDecide.BVExpr w) → motive (Std.Tactic.BVDecide.BVPred.bin lhs op rhs)) →
      ((w : ℕ) →
          (expr : Std.Tactic.BVDecide.BVExpr w) → (idx : ℕ) → motive (Std.Tactic.BVDecide.BVPred.getLsbD expr idx)) →
        motive pred
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.ne_zero_of_mem_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {p a : α},
  p ∈ UniqueFactorizationMonoid.factors a → a ≠ 0
-- Mathlib.Topology.UniformSpace.Separation
Inseparable.nhds_le_uniformity : ∀ {α : Type u} [inst : UniformSpace α] {x y : α}, Inseparable x y → nhds (x, y) ≤ uniformity α
-- Init.Prelude
/-- Bijection between `α` and `PLift α`  -/
PLift.up_down : ∀ {α : Sort u} (b : PLift α), { down := b.down } = b
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousAdd.mk : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M], (Continuous fun p => p.1 + p.2) → ContinuousAdd M
-- Init.Data.Array.Basic
/-- Returns the index of the first element for which `p` returns `true`, or `none` if there is no such
element.

Examples:
* `#[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4`
* `#[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none`
 -/
Array.findIdx? : {α : Type u} → (α → Bool) → Array α → Option ℕ
-- Mathlib.AlgebraicGeometry.SpreadingOut
/-- The germ map at `x` is injective if there exists some affine `U ∋ x`
such that the map `Γ(X, U) ⟶ X_x` is injective  -/
AlgebraicGeometry.Scheme.IsGermInjectiveAt : (X : AlgebraicGeometry.Scheme) → ↥X → Prop
-- Mathlib.Data.Sym.Sym2
Sym2.diagSet_subset_fromRel : ∀ {α : Type u_1} {r : α → α → Prop} (hr : Std.Symm r), Sym2.diagSet ⊆ Sym2.fromRel hr ↔ Std.Refl r
-- Mathlib.Algebra.Lie.Subalgebra
/-- The preimage of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the
domain.  -/
LieSubalgebra.comap : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {L₂ : Type w} →
            [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → (L →ₗ⁅R⁆ L₂) → LieSubalgebra R L₂ → LieSubalgebra R L
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
CategoryTheory.instIsRegularMonoOfNormalMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [I : CategoryTheory.NormalMono f],
  CategoryTheory.IsRegularMono f
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap_eq_bmod : ∀ {x i : ℤ}, 0 ≤ i → (Lean.Grind.IntInterval.co (-i) i).wrap x = x.bmod (2 * i).toNat
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_mul_self : ∀ {α : Type u} [inst : Mul α] [inst_1 : LE α] [CanonicallyOrderedMul α] {a b : α}, a ≤ b * a
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius_zero_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p] (x : R), (iterateFrobenius R p 0) x = x
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_lt_left_iff_neg : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r : k}, a < b → ((AffineMap.lineMap a b) r < a ↔ r < 0)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.forIn'_eq_forIn'_toArray : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toArray init fun a ha acc => f a ⋯ acc
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.add_mem_sup : ∀ {M : Type u_2} [inst : Add M] {S T : AddSubsemigroup M} {x y : M}, x ∈ S → y ∈ T → x + y ∈ S ⊔ T
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.piEquivL_apply : ∀ {𝕜 : Type u_3} [inst : NormedField 𝕜] {E : Type u_7} [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] {ι : Type u_11} (F : ι → Type u_12) [inst_4 : (i : ι) → AddCommGroup (F i)]
  [inst_5 : (i : ι) → Module 𝕜 (F i)] [inst_6 : (i : ι) → TopologicalSpace (F i)]
  [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)]
  (T : (i : ι) → E →Lₚₜ[𝕜] F i) (e : E) (i : ι), ((PointwiseConvergenceCLM.piEquivL 𝕜 E F) T) e i = (T i) e
-- Mathlib.Topology.NhdsWithin
pure_sup_nhdsNE : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), pure a ⊔ nhdsWithin a {a}ᶜ = nhds a
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_Ici_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedGT α] (i : α),
  ((Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2) →
    Cardinal.aleph0 ≤ Cardinal.mk α → Cardinal.mk ↑(Set.Ici i) < Cardinal.mk α
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.isPartialFixpoint : Lean.Elab.PartialFixpointType → Bool
-- Mathlib.Algebra.Homology.Additive
/-- If additive functors are related by an isomorphism `F ⋙ G ≅ H`, this is
the corresponding isomorphism for the induced functors on categories
of homological complexes.  -/
CategoryTheory.Functor.mapHomologicalComplexCompIso : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {W : Type u_2} →
          [inst_2 : CategoryTheory.Category.{v_1, u_2} W] →
            [inst_3 : CategoryTheory.Preadditive W] →
              {W' : Type u_5} →
                [inst_4 : CategoryTheory.Category.{u_6, u_5} W'] →
                  [inst_5 : CategoryTheory.Preadditive W'] →
                    {F : CategoryTheory.Functor V W} →
                      {G : CategoryTheory.Functor W W'} →
                        {H : CategoryTheory.Functor V W'} →
                          (F.comp G ≅ H) →
                            [inst_6 : F.Additive] →
                              [inst_7 : G.Additive] →
                                [inst_8 : H.Additive] →
                                  (c : ComplexShape ι) →
                                    (F.mapHomologicalComplex c).comp (G.mapHomologicalComplex c) ≅
                                      H.mapHomologicalComplex c
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : D) {y z : C} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x (CategoryTheory.inv f))
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x z)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.comp_apply : ∀ {R : Type u} [inst : CommRing R] {A B C : CommAlgCat R} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_inj_iff : ∀ {R : Type u} (x y : Tropical R), Tropical.untrop x = Tropical.untrop y ↔ x = y
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.map_sub : ∀ {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 : E →ₛₗ.[σ] F)
  (x y : ↥f.domain), ↑f (x - y) = ↑f x - ↑f y
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonalEquivFin_symm_apply_coe : ∀ (n : ℕ) (x : Fin (n + 1)), ↑((Finset.Nat.antidiagonalEquivFin n).symm x) = (↑x, n - ↑x)
-- Mathlib.Topology.Algebra.UniformConvergence
instAddCommGroupUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup β],
  instAddCommGroupUniformFun = { toAddGroup := instAddGroupUniformFun, add_comm := ⋯ }
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addSimproc.inj : ∀ {«simproc» : Lean.Name} {post : Bool} {simproc_1 : Lean.Name} {post_1 : Bool},
  Lean.Elab.Tactic.ElabSimpArgResult.addSimproc «simproc» post =
      Lean.Elab.Tactic.ElabSimpArgResult.addSimproc simproc_1 post_1 →
    «simproc» = simproc_1 ∧ post = post_1
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.concat_comp_IccInclusionLeft : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E]
  {f : C(↑(Set.Icc a b), E)} {g : C(↑(Set.Icc b c), E)},
  f ⊤ = g ⊥ → (f.concat g).comp ContinuousMap.IccInclusionLeft = f
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderTriple.toNNReal_iff : ∀ {p q : ENNReal} (r : ENNReal),
  0 < p.toNNReal → 0 < q.toNNReal → (p.toNNReal.HolderTriple q.toNNReal r.toNNReal ↔ p.HolderTriple q r)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.refl : ∀ {F : Type u → Type v} [q : QPF F] (x : (QPF.P F).W), QPF.Wequiv x x
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_congr_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ⊆ t ∪ u → t ⊆ s ∪ u → s ∪ u = t ∪ u
-- Mathlib.NumberTheory.Modular
/-- Explicit formula for the image of `ModularGroup.fdo` in `ℂ`.  -/
ModularGroup.coe_fdo : UpperHalfPlane.coe '' ModularGroup.fdo = {z | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.lt_sin : ∀ {x : ℝ}, x < 0 → x < Real.sin x
-- Init.Data.SInt.Lemmas
Int16.le_trans : ∀ {a b c : Int16}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Control.Bitraversable.Instances
Bitraversable.isLawfulTraversable : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t] {α : Type u}, LawfulTraversable (t α)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexFuel.eq_2 : ∀ (fuel_2 : ℕ),
  Lean.Grind.CommRing.Mon.revlexFuel fuel_2.succ Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit = Ordering.eq
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.ι_ne_algebraMap : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] [Nontrivial R] (x : X) (r : R),
  FreeAlgebra.ι R x ≠ (algebraMap R (FreeAlgebra R X)) r
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.whiskeringRight₂_map_app_app_app : ∀ (B : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (D : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)}
  (f : X ⟶ Y) (X_1 : CategoryTheory.Functor B C) (Y_1 : CategoryTheory.Functor B D) (c : B),
  ((((CategoryTheory.Functor.whiskeringRight₂ B C D E).map f).app X_1).app Y_1).app c =
    (f.app (X_1.obj c)).app (Y_1.obj c)
-- Mathlib.Topology.Connected.LocallyConnected
isOpen_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] [LocallyConnectedSpace α] {x : α}, IsOpen (connectedComponent x)
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.integral_llr_tilted_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable f μ →
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
        MeasureTheory.Integrable (fun x => Real.exp (f x)) μ →
          AEMeasurable f ν →
            ∫ (x : α), MeasureTheory.llr (μ.tilted f) ν x ∂μ =
              ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + ∫ (x : α), f x ∂μ - Real.log (∫ (x : α), Real.exp (f x) ∂μ)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iio_add_Iic_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b : α),
  Set.Iio a + Set.Iic b ⊆ Set.Iio (a + b)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂) {Z : CategoryTheory.ShortComplex C}
  (h : S₂.L₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.f₀ (CategoryTheory.CategoryStruct.comp S₂.v₀₁ h) =
    CategoryTheory.CategoryStruct.comp S₁.v₀₁ (CategoryTheory.CategoryStruct.comp self.f₁ h)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A finite nontrivial connected graph contains a vertex that leaves the graph connected if
removed.  -/
SimpleGraph.Connected.exists_connected_induce_compl_singleton_of_finite_nontrivial : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nontrivial V], G.Connected → ∃ v, (SimpleGraph.induce {v}ᶜ G).Connected
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.iff_of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocal K] {X : C} (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.dual_insert : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair] (x : M) (s : Set M),
  ProperCone.dual p (insert x s) = ProperCone.dual p {x} ⊓ ProperCone.dual p s
-- Mathlib.RingTheory.AdicCompletion.RingHom
/-- A variant of `IsAdicComplete.liftRingHom`. Only takes `f n : R →+* S ⧸ I ^ (a n)`
from a strictly increasing sequence `a n`.
 -/
IsAdicComplete.StrictMono.liftRingHom : {R : Type u_1} →
  {S : Type u_2} →
    [inst : NonAssocSemiring R] →
      [inst_1 : CommRing S] →
        (I : Ideal S) →
          {a : ℕ → ℕ} →
            (ha : StrictMono a) →
              (f : (n : ℕ) → R →+* S ⧸ I ^ a n) →
                (∀ {m : ℕ}, (Ideal.Quotient.factorPow I ⋯).comp (f (m + 1)) = f m) → [IsAdicComplete I S] → R →+* S
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.comp_of_right_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  {f g : Module.Dual R V} {v : V},
  f v = 0 → LinearMap.transvection f v ∘ₗ LinearMap.transvection g v = LinearMap.transvection (f + g) v
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsRefl.domRestrict : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsRefl → ∀ (p : Submodule R₁ M₁), (B.domRestrict₁₂ p p).IsRefl
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.closure_inv : ∀ {G : Type u_2} [inst : Group G] (s : Set G), Submonoid.closure s⁻¹ = (Submonoid.closure s)⁻¹
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.instTransForallIsThetaIsBigO : {α : Type u_1} →
  {E : Type u_3} →
    {G : Type u_5} →
      {F' : Type u_7} →
        [inst : Norm E] →
          [inst_1 : Norm G] →
            [inst_2 : SeminormedAddCommGroup F'] →
              {l : Filter α} → Trans (Asymptotics.IsTheta l) (Asymptotics.IsBigO l) (Asymptotics.IsBigO l)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.preservesLimit_cospan_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    (CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F ↔
      CategoryTheory.IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g))
-- Mathlib.Topology.DenseEmbedding
/-- The range of a dense inducing map is a dense set.  -/
IsDenseInducing.dense : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  IsDenseInducing i → DenseRange i
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_sumElim : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι → M)
  (g : κ → M), ∑ x ∈ s.disjSum t, Sum.elim f g x = ∑ x ∈ s, f x + ∑ x ∈ t, g x
-- Mathlib.Algebra.Torsor.Basic
Pi.instTorsor.eq_1 : ∀ {I : Type u} {fg : I → Type v} [inst : (i : I) → Group (fg i)] {fp : I → Type w}
  [inst_1 : (i : I) → Torsor (fg i) (fp i)],
  Pi.instTorsor =
    { toMulAction := Pi.mulAction', sdiv := fun p₁ p₂ i => p₁ i /ₛ p₂ i, nonempty := ⋯, sdiv_smul' := ⋯,
      smul_sdiv' := ⋯ }
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.LawfulUpwardEnumerableLeast?.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α],
  (∀ (a : α), ∃ init, Std.PRange.least? = some init ∧ Std.PRange.UpwardEnumerable.LE init a) →
    Std.PRange.LawfulUpwardEnumerableLeast? α
-- Init.Data.List.Scan.Lemmas
List.getElem?_scanr_of_lt : ∀ {α : Type u_1} {β : Type u_2} {i : ℕ} {b : β} {l : List α} {f : α → β → β},
  i < l.length + 1 → (List.scanr f b l)[i]? = some (List.foldr f b (List.drop i l))
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
/-- Baby version of the Whitney weak embedding theorem: if `M` admits a finite covering by
supports of bump functions, then for some `n` it can be embedded into the `n`-dimensional
Euclidean space.  -/
exists_embedding_euclidean_of_compact : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH}
  [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [CompactSpace M],
  ∃ n e,
    ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧
      Topology.IsClosedEmbedding e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv% e x)
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot_lt_iff : ∀ {n a b : ℕ}, n ≠ 0 → (n.nthRoot a < b ↔ a < b ^ n)
-- Init.Data.Range.Polymorphic.Fin
Fin.instLawfulUpwardEnumerable : ∀ {n : ℕ}, Std.PRange.LawfulUpwardEnumerable (Fin n)
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh.eq_1 : ∀ (x : ℝ), Real.cosh x = (Complex.cosh ↑x).re
-- Mathlib.Order.DirSupClosed
dirSupInacc_compl : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], DirSupInacc sᶜ ↔ DirSupClosed s
-- Mathlib.Topology.Constructions
isClosedMap_ofAdd : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosedMap ⇑Multiplicative.ofAdd
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.IsUniform.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P P_1 : Finpartition A),
  P = P_1 →
    ∀ (G G_1 : SimpleGraph α),
      G = G_1 →
        ∀ {inst_3 : DecidableRel G.Adj} [inst_4 : DecidableRel G_1.Adj] (ε ε_1 : 𝕜),
          ε = ε_1 → P.IsUniform G ε = P_1.IsUniform G_1 ε_1
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.one_mul : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R'), 1 * χ = χ
-- Init.Data.Int.LemmasAux
/-- This is a generalization of `a ≤ c` and `b ≤ d` implying `a * b ≤ c * d` for natural numbers,
appropriately generalized to integers when `b` is nonnegative and `c` is nonpositive.
 -/
Int.mul_le_mul_of_le_of_le_of_nonneg_of_nonpos : ∀ {a b c d : ℤ}, a ≤ c → d ≤ b → 0 ≤ b → c ≤ 0 → a * b ≤ c * d
-- Aesop.Search.ExpandSafePrefix
Aesop.SafeExpansionM.State.mk.injEq : ∀ (numRapps numRapps_1 : ℕ), ({ numRapps := numRapps } = { numRapps := numRapps_1 }) = (numRapps = numRapps_1)
-- Mathlib.Algebra.Jordan.Basic
_private.Mathlib.Algebra.Jordan.Basic.0.aux2 : ∀ {A : Type u_1} [inst : NonUnitalNonAssocCommRing A] [IsCommJordan A] {a b c : A},
  ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (a * a)⁆ + ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * b)⁆ +
                ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (c * c)⁆ +
              ⁅AddMonoid.End.mulLeft a, 2 • AddMonoid.End.mulLeft (a * b)⁆ +
            ⁅AddMonoid.End.mulLeft a, 2 • AddMonoid.End.mulLeft (c * a)⁆ +
          ⁅AddMonoid.End.mulLeft a, 2 • AddMonoid.End.mulLeft (b * c)⁆ +
        (⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (a * a)⁆ +
                  ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (b * b)⁆ +
                ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * c)⁆ +
              ⁅AddMonoid.End.mulLeft b, 2 • AddMonoid.End.mulLeft (a * b)⁆ +
            ⁅AddMonoid.End.mulLeft b, 2 • AddMonoid.End.mulLeft (c * a)⁆ +
          ⁅AddMonoid.End.mulLeft b, 2 • AddMonoid.End.mulLeft (b * c)⁆) +
      (⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * a)⁆ +
                ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (b * b)⁆ +
              ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (c * c)⁆ +
            ⁅AddMonoid.End.mulLeft c, 2 • AddMonoid.End.mulLeft (a * b)⁆ +
          ⁅AddMonoid.End.mulLeft c, 2 • AddMonoid.End.mulLeft (c * a)⁆ +
        ⁅AddMonoid.End.mulLeft c, 2 • AddMonoid.End.mulLeft (b * c)⁆) =
    ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * b)⁆ +
              ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (a * a)⁆ +
            2 •
              (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (a * b)⁆ +
                ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (a * b)⁆) +
          (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (c * c)⁆ +
              ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * a)⁆ +
            2 •
              (⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (c * a)⁆ +
                ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (c * a)⁆)) +
        (⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * c)⁆ +
            ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (b * b)⁆ +
          2 •
            (⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (b * c)⁆ +
              ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (b * c)⁆)) +
      (2 • ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * c)⁆ +
          2 • ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * a)⁆ +
        2 • ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * b)⁆)
-- Mathlib.Order.SemiconjSup
IsOrderRightAdjoint.orderIso_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {g : β → α}, IsOrderRightAdjoint f g → ∀ (e : β ≃o γ), IsOrderRightAdjoint (⇑e ∘ f) (g ∘ ⇑e.symm)