mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.step_mapM : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {γ : Type w} {f : β → n γ} [inst_1 : Monad n] [inst_2 : MonadAttach n] [LawfulMonad n] [inst_4 : MonadLiftT m n],
  (Std.IterM.mapM f it).step = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let out' ← MonadAttach.attach (f out)
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.mapM f it') ↑out' ⋯))
      | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.mapM f it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Algebra.Algebra.Bilinear
Algebra.coe_lmul_eq_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ⇑(Algebra.lmul R A) = ⇑(LinearMap.mul R A)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.Context : Type
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.toAlexandrovDiscrete : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α], AlexandrovDiscrete α
-- Mathlib.Tactic.Translate.Reorder
/-- Reorder the arguments of a function type using the given `ArgReorder`.  -/
Mathlib.Tactic.Translate.reorderForall : Mathlib.Tactic.Translate.ArgReorder → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor `(F, S) ⥤ (F ⋙ G, G(S))`.  -/
CategoryTheory.CostructuredArrow.post : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {B : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} B] →
            (F : CategoryTheory.Functor B C) →
              (G : CategoryTheory.Functor C D) →
                (S : C) →
                  CategoryTheory.Functor (CategoryTheory.CostructuredArrow F S)
                    (CategoryTheory.CostructuredArrow (F.comp G) (G.obj S))
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmooth_localizationPreserves : RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardSmooth
-- Mathlib.RingTheory.Jacobson.Semiprimary
/-- A ring is semiprimary if its Jacobson radical is nilpotent and its quotient by the
Jacobson radical is semisimple.  -/
IsSemiprimaryRing : (R : Type u_1) → [Ring R] → Prop
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.Context.mk : Lean.Meta.Grind.SymbolPriorities → ℕ → Lean.Meta.Grind.NormalizePattern.Context✝
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `<` on `BitVec`s.  -/
BitVec.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.measurableEquivRealProd_symm_polarCoord_symm_apply : ∀ (p : ℝ × ℝ), Complex.measurableEquivRealProd.symm (↑polarCoord.symm p) = ↑Complex.polarCoord.symm p
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.filterMap.congr_simp : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (f f_1 : α → β → Option γ),
  f = f_1 → ∀ (m m_1 : Std.ExtHashMap α β), m = m_1 → Std.ExtHashMap.filterMap f m = Std.ExtHashMap.filterMap f_1 m_1
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.lift_comp_linearMap : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} (h : IsSymmetricAlgebra f) {A' : Type u_4}
  [inst_5 : CommSemiring A'] [inst_6 : Algebra R A'] (g : M →ₗ[R] A'), ↑(h.lift g) ∘ₗ f = g
-- Lean.Elab.Do.Basic
/-- The elaborator constructing a jump site to the return continuation,
given some return value. The type of this return value determines the type of the jump expression;
this could very well be different than the `resultType` in case an intervening `match` has refined
`resultType`. So `k` must *not* hardcode the type `resultType` into its definition; rather it
should infer the type of the return value argument.
 -/
Lean.Elab.Do.ReturnCont.k : Lean.Elab.Do.ReturnCont → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Std.Data.TreeMap.Basic
/-- Returns `true` if the tree map contains no mappings.  -/
Std.TreeMap.isEmpty : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Bool
-- Std.Async.ContextAsync
Std.Async.ContextAsync.instMonadAsyncAsyncTask : Std.Async.MonadAsync Std.Async.AsyncTask Std.Async.ContextAsync
-- Mathlib.Analysis.Polynomial.Fourier
ContinuousMap.toAEEqFun.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [inst_1 : TopologicalSpace α]
  [inst_2 : BorelSpace α] [inst_3 : TopologicalSpace β] [inst_4 : SecondCountableTopologyEither α β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] (f f_1 : C(α, β)),
  f = f_1 → ContinuousMap.toAEEqFun μ f = ContinuousMap.toAEEqFun μ f_1
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_set_symmDiff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
  a ≠ 0 → a • symmDiff s t = symmDiff (a • s) (a • t)
-- Std.Async.IO
/-- Interface for asynchronous reading operations.
 -/
Std.Async.IO.AsyncRead : Type → Type → Type
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the day of the month to the given `days` value, with any
out-of-range days rolled over to the next month or year as needed.
 -/
Std.Time.DateTime.withDaysRollOver : Std.Time.DateTime → Std.Time.Day.Ordinal → Std.Time.DateTime
-- Init.Data.Vector.Erase
Vector.getElem?_eraseIdx_of_ge : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n) {j : ℕ}, i ≤ j → (xs.eraseIdx i h)[j]? = xs[j + 1]?
-- Std.Time.Date.Unit.Week
/-- `Ordinal` represents a bounded value for weeks of a year, which ranges between 1 and 53.
 -/
Std.Time.Week.OfYear.Ordinal : Type
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.singleDistribMulActionHom.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] [inst_1 : Monoid R] [inst_2 : DistribMulAction R S]
  (a : M),
  AddMonoidAlgebra.singleDistribMulActionHom a =
    { toFun := (↑(AddMonoidAlgebra.singleAddHom a)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Homology.Localization
HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj_assoc : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_4 : c.QFactorsThroughHomotopy C]
  (K : HomologicalComplex C c) (i : ι) {Z : C}
  (h :
    (HomologicalComplexUpToQuasiIso.homologyFunctor C c i).obj
        (HomologicalComplexUpToQuasiIso.Qh.obj ((HomotopyCategory.quotient C c).obj K)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      ((HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh C c i).inv.app ((HomotopyCategory.quotient C c).obj K))
      h =
    CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C c i).hom.app K)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplexUpToQuasiIso.homologyFunctorFactors C c i).inv.app K)
        (CategoryTheory.CategoryStruct.comp
          ((HomologicalComplexUpToQuasiIso.homologyFunctor C c i).map
            ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).inv.app K))
          h))
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift_of_eq_id : ∀ (α : Type u_1), FreeAddGroup.lift FreeAddGroup.of = AddMonoidHom.id (FreeAddGroup α)
-- Mathlib.Topology.Algebra.UniformMulAction
/-- If an additive action is central, then its right action is uniform
continuous when its left action is.  -/
UniformContinuousConstVAdd.op : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : VAdd M X] [inst_2 : VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X]
  [UniformContinuousConstVAdd M X], UniformContinuousConstVAdd Mᵃᵒᵖ X
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] {f g : EsakiaHom α β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Order.Sublattice
Sublattice.prod_top : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L : Sublattice α),
  L.prod ⊤ = Sublattice.comap LatticeHom.fst L
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The natural equivariant map from `n ↪ α` to `m ↪ α` given by an embedding `e : m ↪ n`.  -/
AddActionHom.embMap : (G : Type u_1) →
  (α : Type u_2) →
    [inst : AddGroup G] → [inst_1 : AddAction G α] → {m : Type u_5} → {n : Type u_6} → (m ↪ n) → (n ↪ α) →ₑ[id] m ↪ α
-- Mathlib.RingTheory.Invariant.Basic
IsFractionRing.ker_stabilizerHom : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] (P : Ideal A) (Q : Ideal B)
  [inst_6 : Q.LiesOver P] (K : Type u_4) (L : Type u_5) [inst_7 : Field K] [inst_8 : Field L]
  [inst_9 : Algebra (A ⧸ P) K] [inst_10 : Algebra (B ⧸ Q) L] [inst_11 : Algebra (A ⧸ P) L]
  [inst_12 : IsScalarTower (A ⧸ P) (B ⧸ Q) L] [inst_13 : Algebra K L] [inst_14 : IsScalarTower (A ⧸ P) K L]
  [inst_15 : IsFractionRing (A ⧸ P) K] [inst_16 : IsFractionRing (B ⧸ Q) L],
  (IsFractionRing.stabilizerHom G P Q K L).ker = Ideal.inertia (↥(MulAction.stabilizer G Q)) Q
-- Mathlib.LinearAlgebra.Contraction
/-- If `M` is finite free, the natural map $M^* ⊗ N → Hom(M, N)$ is an
equivalence.  -/
dualTensorHomEquiv : (R : Type u_2) →
  (M : Type u_3) →
    (N : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                [Module.Finite R M] → [Module.Projective R M] → TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N
-- Mathlib.Algebra.Group.Units.Equiv
unitsEquivProdSubtype_apply_coe : ∀ (α : Type u_2) [inst : Monoid α] (u : αˣ), ↑((unitsEquivProdSubtype α) u) = (↑u, ↑u⁻¹)
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_primPart : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R), p.primPart.content = 1
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLE_dec : ∀ {s : String.Slice} {p : String.Pos.Raw} (h : 0 < p), s.posLE p.dec = s.posLT p h
-- Lean.Parser.Basic
Lean.Parser.satisfyFn : (Char → Bool) → optParam String "unexpected character" → Lean.Parser.ParserFn
-- Lean.Parser.Term
Lean.Parser.Term.optSemicolon.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Compactness.Lindelof
/-- If `f : X → Y` is an embedding, the image `f '' s` of a set `s` is Lindelöf
if and only if `s` is Lindelöf.  -/
Topology.IsEmbedding.isLindelof_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  Topology.IsEmbedding f → (IsLindelof s ↔ IsLindelof (f '' s))
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.findM?_eq_findSomeM? : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  [Std.Iterators.Finite α m] {it : Std.IterM m β} {f : β → m (ULift.{w, 0} Bool)},
  it.findM? f =
    it.findSomeM? fun x => do
      let __do_lift ← f x
      pure (if __do_lift.down = true then some x else none)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instAdditiveSingleFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ), (DerivedCategory.singleFunctor C n).Additive
-- Aesop.Rule.Forward
Aesop.instBEqForwardRulePriority : BEq Aesop.ForwardRulePriority
-- Mathlib.CategoryTheory.EffectiveEpi.Extensive
CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.FinitaryPreExtensive D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteCoproducts F] [F.ReflectsEffectiveEpis],
  F.ReflectsFiniteEffectiveEpiFamilies
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sigmaOfIsColimit_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d), (E.sigmaOfIsColimit hc hd).toPreZeroHypercover = E.sigmaOfIsColimit hc
-- Init.Data.Array.Lemmas
Array.set_replicate_self : ∀ {n : ℕ} {α : Type u_1} {a : α} {i : ℕ} {h : i < (Array.replicate n a).size},
  (Array.replicate n a).set i a h = Array.replicate n a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonAddMonoidHom_apply : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddZeroClass α] (a : α), Finset.singletonAddMonoidHom a = {a}
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_comp_swap : ∀ (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  (Monoid.Coprod.swap M N).comp (Monoid.Coprod.swap N M) = MonoidHom.id (Monoid.Coprod N M)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
iteratedFDerivWithin_comp_of_eventually_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {g : F → G} {x : E}
  {n : WithTop ℕ∞} {t : Set F},
  ContDiffWithinAt 𝕜 n g t (f x) →
    ContDiffWithinAt 𝕜 n f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            (∀ᶠ (y : E) in nhdsWithin x s, f y ∈ t) →
              ∀ {i : ℕ},
                ↑i ≤ n →
                  iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
                    (ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.mk : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  Continuous ⇑Topology.WithGeneratedByTopology.equiv.symm → Topology.IsGeneratedBy X Y
-- Mathlib.Analysis.Distribution.TestFunction
/-- The underlying function. Use coercion instead.  -/
TestFunction.toFun : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → {n : ℕ∞} → TestFunction Ω F n → E → F
-- Mathlib.Logic.Basic
/-- Provide modus tollens (`mt`) as dot notation for implications.  -/
Function.mt : ∀ {a b : Prop}, (a → b) → ¬b → ¬a
-- Init.Data.Array.Lemmas
Array.size_swapAt! : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {v : α}, (xs.swapAt! i v).2.size = xs.size
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instIsCocontinuousOverObjPostOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (K : CategoryTheory.GrothendieckTopology D)
  (F : CategoryTheory.Functor C D) (X : C) [F.IsCocontinuous J K],
  (CategoryTheory.Over.post F).IsCocontinuous (J.over X) (K.over (F.obj X))
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_subset_zeroLocus_iff : ∀ {R : Type u} [inst : CommSemiring R] (I J : Ideal R),
  PrimeSpectrum.zeroLocus ↑I ⊆ PrimeSpectrum.zeroLocus ↑J ↔ J ≤ I.radical
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.zero_vadd_self_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] (X : C) [inst_3 : CategoryTheory.AddModObj M X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.zero X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h
-- Mathlib.Algebra.Group.Action.Hom
/-- A monoid homomorphism between two monoids M and N can be equivalently specified by a
multiplicative action of M on N that is compatible with the multiplication on N.  -/
monoidHomEquivMulActionIsScalarTower : (M : Type u_4) → (N : Type u_5) → [inst : Monoid M] → [inst_1 : Monoid N] → (M →* N) ≃ { _inst // IsScalarTower M N N }
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.instSliceableRioSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.instSliceableRioSlice._auto_1) →
      Std.Rio.Sliceable (Std.DTreeMap α β cmp) α (Std.DTreeMap.Internal.RioSlice α β)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.IsPullback.of_equiv : ∀ {sq₁ : CategoryTheory.Square (Type v)} {sq₂ : CategoryTheory.Square (Type u)} (e₁ : sq₁.X₁ ≃ sq₂.X₁)
  (e₂ : sq₁.X₂ ≃ sq₂.X₂) (e₃ : sq₁.X₃ ≃ sq₂.X₃) (e₄ : sq₁.X₄ ≃ sq₂.X₄),
  ⇑e₂ ∘ ⇑(CategoryTheory.ConcreteCategory.hom sq₁.f₁₂) = ⇑(CategoryTheory.ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁ →
    ⇑e₃ ∘ ⇑(CategoryTheory.ConcreteCategory.hom sq₁.f₁₃) = ⇑(CategoryTheory.ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁ →
      ⇑e₄ ∘ ⇑(CategoryTheory.ConcreteCategory.hom sq₁.f₂₄) = ⇑(CategoryTheory.ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂ →
        ⇑e₄ ∘ ⇑(CategoryTheory.ConcreteCategory.hom sq₁.f₃₄) = ⇑(CategoryTheory.ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃ →
          sq₁.IsPullback → sq₂.IsPullback
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.mapPair_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
  (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left })
  (g :
    F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.right }),
  (CategoryTheory.Limits.mapPair f g).app { as := CategoryTheory.Limits.WalkingPair.left } = f
-- Mathlib.RingTheory.Extension.Generators
/-- The canonical homomorphism of extensions from the universal extension `R[S] → S`
(given by `Generators.self R S`) to any extension `P` defined via the designated section `P.σ`.  -/
Algebra.Extension.defaultHom : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → (Algebra.Generators.self R S).toExtension.Hom P
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.productIso_hom_comp_eval : ∀ {J : Type v} (F : J → Type (max v u)) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.productIso F).hom (TypeCat.ofHom fun f => f j) =
    CategoryTheory.Limits.Pi.π F j
-- Std.Sat.AIG.RelabelNat
/-- Map an `Entrypoint` with arbitrary atom identifiers to one that uses `Nat` as atom identifiers.
This is useful for preparing an `AIG` for CNF translation if it doesn't already use `Nat`
identifiers.
 -/
Std.Sat.AIG.Entrypoint.relabelNat : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → Std.Sat.AIG.Entrypoint α → Std.Sat.AIG.Entrypoint ℕ
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The tensor product map of two linear isometries is a linear isometry. In particular, this is
the linear isometry version of `TensorProduct.map f g` when `f` and `g` are linear isometries.  -/
TensorProduct.mapIsometry : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        {H : Type u_5} →
          [inst : RCLike 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : InnerProductSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : InnerProductSpace 𝕜 F] →
                    [inst_5 : NormedAddCommGroup G] →
                      [inst_6 : InnerProductSpace 𝕜 G] →
                        [inst_7 : NormedAddCommGroup H] →
                          [inst_8 : InnerProductSpace 𝕜 H] →
                            (E →ₗᵢ[𝕜] G) → (F →ₗᵢ[𝕜] H) → TensorProduct 𝕜 E F →ₗᵢ[𝕜] TensorProduct 𝕜 G H
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_le_add_natCast_right_iff : ∀ {a b : WithBot ℕ∞} {c : ℕ}, a + ↑c ≤ b + ↑c ↔ a ≤ b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_lt_of_nonneg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, b < c → 0 ≤ a → b < c + a
-- Init.Core
PULift.up.inj : ∀ {α : Sort s} {down down_1 : α}, { down := down } = { down := down_1 } → down = down_1
-- Mathlib.Topology.MetricSpace.IsometricSMul
ULift.isIsometricSMul' : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X],
  IsIsometricSMul M (ULift.{u_2, w} X)
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y}
  (toMapFactorizationData :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f)
  (r : toMapFactorizationData.Z ⟶ X)
  (i_r :
    autoParam (CategoryTheory.CategoryStruct.comp toMapFactorizationData.i r = CategoryTheory.CategoryStruct.id X)
      HomotopicalAlgebra.FibrantBrownFactorization.i_r._autoParam)
  (fibration_r :
    autoParam (HomotopicalAlgebra.Fibration r) HomotopicalAlgebra.FibrantBrownFactorization.fibration_r._autoParam)
  (toMapFactorizationData_1 :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f)
  (r_1 : toMapFactorizationData_1.Z ⟶ X)
  (i_r_1 :
    autoParam (CategoryTheory.CategoryStruct.comp toMapFactorizationData_1.i r_1 = CategoryTheory.CategoryStruct.id X)
      HomotopicalAlgebra.FibrantBrownFactorization.i_r._autoParam)
  (fibration_r_1 :
    autoParam (HomotopicalAlgebra.Fibration r_1) HomotopicalAlgebra.FibrantBrownFactorization.fibration_r._autoParam),
  ({ toMapFactorizationData := toMapFactorizationData, r := r, i_r := i_r, fibration_r := fibration_r } =
      { toMapFactorizationData := toMapFactorizationData_1, r := r_1, i_r := i_r_1, fibration_r := fibration_r_1 }) =
    (toMapFactorizationData = toMapFactorizationData_1 ∧ r ≍ r_1)
-- Mathlib.AlgebraicTopology.Reedy.Basic
/-- The degree of a morphism for a Reedy structure. It is defined as the degree of
the intermediate object in the Reedy factorization, but it is also the smallest
degree of an intermediate object in a factorization, see the lemma `degHom_le`.  -/
HomotopicalAlgebra.ReedyStructure.degHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      [inst_1 : W₁.IsMultiplicative] →
        [inst_2 : W₂.IsMultiplicative] →
          {α : Type u_2} →
            [inst_3 : LinearOrder α] →
              [inst_4 : OrderBot α] →
                [inst_5 : SuccOrder α] →
                  [inst_6 : WellFoundedLT α] → HomotopicalAlgebra.ReedyStructure W₁ W₂ α → {X Y : C} → (X ⟶ Y) → α
-- Mathlib.Algebra.Group.Defs
AddCancelMonoid.mk : {M : Type u} →
  [toAddLeftCancelMonoid : AddLeftCancelMonoid M] → [toIsRightCancelAdd : IsRightCancelAdd M] → AddCancelMonoid M
-- Mathlib.Data.Multiset.Basic
Multiset.strongDownwardInduction.eq_1 : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} {n : ℕ}
  (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Multiset α),
  Multiset.strongDownwardInduction H s = H s fun {t} ht _h => Multiset.strongDownwardInduction H t ht