mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β) (hf : MeasureTheory.Integrable f μ), MeasureTheory.Integrable.toL1 f hf = MeasureTheory.MemLp.toLp f ⋯
-- Mathlib.Data.Finset.Basic
Multiset.toFinset_eq_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α}, m.toFinset = ∅ ↔ m = 0
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.infSet : {α : Type u_1} → [InfSet α] → InfSet (ULift.{v, u_1} α)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.leIdeal_v_le_of_mem : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [inst_1 : Field K] (v : Valuation K Γ₀)
  {I : Ideal ↥v.integer} {x : ↥v.integer}, x ∈ I → v.leIdeal (v ↑x) ≤ I
-- Mathlib.GroupTheory.Coxeter.Basic
IsCoxeterGroup.mk : ∀ {W : Type u} [inst : Group W], (∃ B M, Nonempty (CoxeterSystem M W)) → IsCoxeterGroup W
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.relMap_unify_equiv : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [IsDirectedOrder ι] [DirectedSystem G fun i j h => ⇑(f i j h)]
  {n : ℕ} (R : L.Relations n) (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i j : ι)
  (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (hj : j ∈ upperBounds (Set.range (Sigma.fst ∘ x))),
  FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x i hi) =
    FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x j hj)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_roc_eq_add : ∀ {m n fallback : ℤ} {i : ℕ}, i < (n - m).toNat → (m<...=n).toList.getD i fallback = m + 1 + ↑i
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.paramDeclIdx : Lean.Elab.Term.CollectPatternVars.Context → ℕ
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Seminormed ring structure on the product of finitely many seminormed rings,
using the sup norm.  -/
Pi.seminormedRing : {ι : Type u_3} → {R : ι → Type u_4} → [Fintype ι] → [(i : ι) → SeminormedRing (R i)] → SeminormedRing ((i : ι) → R i)
-- Lean.Attributes
/-- This is run when the attribute is applied to a declaration `decl`. `stx` is the syntax of the
attribute including arguments.

The handler will be run under `withExporting` iff the declaration is public, i.e. using the same
visibility scope as elaboration of the rest of the declaration signature.
 -/
Lean.AttributeImpl.add : Lean.AttributeImpl → Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.trans_apply : ∀ {G : Type u_1} {H : Type u_2} {K : Type u_3} [inst : Add G] [inst_1 : Add H] [inst_2 : Add K] {a : G} {b : H} {c : K}
  (e₁ : AddConstEquiv G H a b) (e₂ : AddConstEquiv H K b c) (a_1 : G), (e₁.trans e₂) a_1 = e₂ (e₁ a_1)
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- The affine space over an affine base is isomorphic to the spectrum of the polynomial ring.  -/
AlgebraicGeometry.AffineSpace.SpecIso : (n : Type u) →
  (R : CommRingCat) →
    AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ≅
      AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n ↑R))
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.addConj_symm_apply`. -/
AddAut.conj_symm_apply : ∀ {G : Type u_3} [inst : AddGroup G] (g h : G), (AddEquiv.symm (AddAut.addConj g)) h = -g + h + g
-- Mathlib.Topology.Order.DenselyOrdered
/-- The closure of the interval `(-∞, a)` is the interval `(-∞, a]`.  -/
closure_Iio : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] (a : α)
  [NoMinOrder α], closure (Set.Iio a) = Set.Iic a
-- Mathlib.Tactic.Linter.TextBased
/-- Produce output suitable for Github error annotations: in particular,
duplicate the file path, line number and error code  -/
Mathlib.Linter.TextBased.ErrorFormat.github : Mathlib.Linter.TextBased.ErrorFormat
-- Mathlib.Topology.Order.WithTop
TopologicalSpace.instOrderTopologyWithTop : ∀ {ι : Type u_1} [inst : Preorder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι], OrderTopology (WithTop ι)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a negative multiple of a vector and a vector.  -/
InnerProductGeometry.angle_smul_left_of_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V) {r : ℝ},
  r < 0 → InnerProductGeometry.angle (r • x) y = InnerProductGeometry.angle (-x) y
-- Mathlib.Order.Nucleus
Nucleus.mk.sizeOf_spec : ∀ {X : Type u_2} [inst : SemilatticeInf X] [inst_1 : SizeOf X] (toInfHom : InfHom X X)
  (idempotent' : ∀ (x : X), toInfHom.toFun (toInfHom.toFun x) ≤ toInfHom.toFun x)
  (le_apply' : ∀ (x : X), x ≤ toInfHom.toFun x),
  sizeOf { toInfHom := toInfHom, idempotent' := idempotent', le_apply' := le_apply' } = 1 + sizeOf toInfHom
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_sub_int : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddGroupWithOne G]
  [inst_2 : AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ), f (x - ↑n) = f x - ↑n
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.intCast_real_norm : ∀ (x : GaussianInt), ↑(Zsqrtd.norm x) = Complex.normSq (GaussianInt.toComplex x)
-- Mathlib.Algebra.Algebra.Operations
Submodule.restrictScalars_mul : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : SMul A B] [inst_4 : Module A C] [inst_5 : Module B C] [inst_6 : IsScalarTower A C C]
  [inst_7 : IsScalarTower B C C] [inst_8 : IsScalarTower A B C] {I J : Submodule B C},
  Submodule.restrictScalars A (I * J) = Submodule.restrictScalars A I * Submodule.restrictScalars A J
-- Std.Http.Protocol.H1
/-- Parses one request start-line in server mode and initializes `reader.messageHead`
for header parsing.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processReceivingStartLine : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving →
  Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_le : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k fallback : α},
        (compare (Std.Internal.List.maxKeyD l fallback) k).isLE = true ↔
          ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Swap the second and third objects in `(X₁ ⊗ X₂) ⊗ (Y₁ ⊗ Y₂)`. This is used to strength the
tensor product functor from `C × C` to `C` as a monoidal functor.  -/
CategoryTheory.MonoidalCategory.tensorμ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        (X₁ X₂ Y₁ Y₂ : C) →
          CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
              (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂) ⟶
            CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsCyclotomicExtension.Rat.finrank : ∀ (k : ℕ) (K : Type u) [inst : Field K] [inst_1 : CharZero K] [NeZero k] [IsCyclotomicExtension {k} ℚ K],
  Module.finrank ℚ K = k.totient
-- Mathlib.Algebra.Module.ZLattice.Basic
instIsZLatticeRealSpan : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : Finite ι]
  (b : Module.Basis ι ℝ E), IsZLattice ℝ (Submodule.span ℤ (Set.range ⇑b))
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RoiSlice.instToIterator : {α : Type u_1} →
  {β : α → Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.RoiSliceData α β)) Id (Std.DTreeMap.Internal.Zipper α β)
        ((a : α) × β a)
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂Functor_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] {X Y : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  (φ : X ⟶ Y), CategoryTheory.bifunctorComp₁₂Functor.map φ = CategoryTheory.bifunctorComp₁₂FunctorMap φ
-- Mathlib.Logic.Equiv.Set
Equiv.Set.univPi_apply_coe : ∀ {α : Type u_3} {β : α → Type u_4} (s : (a : α) → Set (β a)) (f : ↑(Set.univ.pi s)) (a : α),
  ↑((Equiv.Set.univPi s) f a) = ↑f a
-- Init.Control.Basic
Alternative.toApplicative : {f : Type u → Type v} → [self : Alternative f] → Applicative f
-- Mathlib.Data.Fin.SuccPred
/-- Embedding `i : Fin n` into `Fin (n + 1)` with a hole around `p : Fin (n + 1)`
embeds `i` by `castSucc` when the resulting `i.castSucc < p`.  -/
Fin.succAbove_of_castSucc_lt : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), i.castSucc < p → p.succAbove i = i.castSucc
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.map_of : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (p : Polynomial R)
  (q : Polynomial S) (h : q ∣ Polynomial.map f p) (r : R),
  (AdjoinRoot.map f p q h) ((AdjoinRoot.of p) r) = (AdjoinRoot.of q) (f r)
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- For a presheaf of the form `yoneda.obj W`, a compatible family of elements on a sieve
is the same as a co-cone over the sieve. Constructing a co-cone from a compatible family works for
any presieve, as does constructing a family of elements from a co-cone. Showing compatibility of the
family needs the sieve condition.
Note: This is related to `CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily`
 -/
CategoryTheory.Presieve.compatibleYonedaFamily_toCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      (R : CategoryTheory.Presieve X) →
        (W : C) →
          (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.yoneda.obj W) R) →
            x.Compatible → CategoryTheory.Limits.Cocone R.diagram
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.natural.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {β : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (β i)]
  [inst_1 : ∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)] [mβ : (i : ι) → MeasurableSpace (β i)]
  [inst_2 : ∀ (i : ι), BorelSpace (β i)] [inst_3 : Preorder ι] (u : (i : ι) → Ω → β i)
  (hum : ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)),
  MeasureTheory.Filtration.natural u hum =
    { seq := fun i => ⨆ j, ⨆ (_ : j ≤ i), MeasurableSpace.comap (u j) (mβ j), mono' := ⋯, le' := ⋯ }
-- Init.Data.String.Modify
String.Pos.offset_toModifyOfLE : ∀ {s : String} {q p : s.Pos} {f : Char → Char} {hp : p ≠ s.endPos} {hpq : q ≤ p},
  (q.toModifyOfLE p f hp hpq).offset = q.offset
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.HasProd.mk : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G},
  (∃ ρ, ∀ (s : Set X) (t : Set Y), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B (μ s)) (ν t)) → μ.HasProd ν B
-- Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Multiset.le_prod_of_submultiplicative_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : CommMonoidWithZero β] [inst_2 : PartialOrder β]
  [PosMulMono β] (f : α → β),
  (∀ (a : α), 0 ≤ f a) →
    f 1 ≤ 1 → (∀ (a b : α), f (a * b) ≤ f a * f b) → ∀ (s : Multiset α), f s.prod ≤ (Multiset.map f s).prod
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_ret_comp : ∀ (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)) =
    Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.trNormal f k
-- Mathlib.Logic.Function.Basic
Pi.map_id : ∀ {ι : Type u_3} {α : ι → Type u_4}, (Pi.map fun i => id) = id
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Arbitrary coloring with two colors for a tree  -/
SimpleGraph.IsTree.coloringTwo : {V : Type u_1} → {G : SimpleGraph V} → G.IsTree → G.Coloring (Fin 2)
-- Mathlib.Order.Filter.Bases.Finite
/-- If `s : ι → Set α` is an indexed family of sets, then finite intersections of `s i` form a basis
of `⨅ i, 𝓟 (s i)`.  -/
Filter.hasBasis_iInf_principal_finite : ∀ {α : Type u_1} {ι : Type u_6} (s : ι → Set α),
  (⨅ i, Filter.principal (s i)).HasBasis (fun t => t.Finite) fun t => ⋂ i ∈ t, s i
-- Mathlib.Algebra.Module.Submodule.IterateMapComap
/-- If `f` is surjective, `i` is injective, and there exists some `m` such that
`LinearMap.iterateMapComap f i m K = LinearMap.iterateMapComap f i (m + 1) K`,
then the kernel of `f` is contained in `K`.
This is a corollary of `LinearMap.iterateMapComap_eq_succ` and `LinearMap.ker_le_comap`.
As a special case, if one can take `K` to be zero,
then `f` is injective. This is the key result for establishing the strong rank condition
for Noetherian rings.  -/
LinearMap.ker_le_of_iterateMapComap_eq_succ : ∀ {R : Type u_1} {N : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f i : N →ₗ[R] M) (K : Submodule R N) (m : ℕ),
  f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K → Function.Surjective ⇑f → Function.Injective ⇑i → f.ker ≤ K
-- Lean.Data.KVMap
Lean.DataValue.ofInt.injEq : ∀ (v v_1 : ℤ), (Lean.DataValue.ofInt v = Lean.DataValue.ofInt v_1) = (v = v_1)
-- Mathlib.Tactic.Core
/-- Get the array of `FVarId`s in the local context of the given `goal`.

If `ids` is specified, elaborate them in the local context of the given goal to obtain the array of
`FVarId`s.

If `includeImplementationDetails` is `false` (the default), we filter out implementation details
(`implDecl`s and `auxDecl`s) from the resulting list of `FVarId`s.  -/
Lean.Elab.Tactic.getFVarIdsAt : Lean.MVarId →
  optParam (Option (Array Lean.Syntax)) none → optParam Bool false → Lean.Elab.Tactic.TacticM (Array Lean.FVarId)
-- Batteries.Util.ProofWanted
/-- This proof would be a welcome contribution to the library!

The syntax of `theorem_wanted` declarations is just like that of `theorem`. Without `:=` and a
proof body it records a wanted theorem; with one it records a partial proof that still depends on
other wanted lemmas. Lean checks that `theorem_wanted` declarations are well-formed (e.g. it
ensures that all the mentioned names are in scope, and that the theorem statement is a valid
proposition), and records a private placeholder declaration of type `... → ProofWanted statement`.

Modifiers (such as `@[simp]`) are accepted for syntactic compatibility with `theorem` but are
currently ignored.

`proof_wanted` is a synonym for `theorem_wanted`.

Inside another `theorem_wanted` or `def_wanted`, write `❰foo❱` to reference an earlier
`theorem_wanted` or `def_wanted` named `foo`. The bracket may appear in the statement or
the body, and each distinct reference becomes a fresh parameter binder of the matching type. For
parametrised `foo : ∀ args, ProofWanted _`, the binder type is itself Π-quantified, so `❰foo❱ x
y` applies the parameter to `x y`. `❰foo❱` only resolves names within the current file, since
the placeholders are `private`.

A body must reference at least one `❰…❱` (in the statement or the body); otherwise the body is
a complete proof and the declaration should be a `theorem`.

Typical usage:
```
-- A parameterless wanted fact:
theorem_wanted size_of_two_pushes_onto_empty :
    ((#[] : Array Nat).push 1 |>.push 2).size = 2

-- Referencing an earlier `theorem_wanted` inside a statement (here in the `Fin`
-- bound proof, which rewrites by the wanted fact):
theorem_wanted first_index_after_two_pushes :
    (⟨0, by rw [❰size_of_two_pushes_onto_empty❱]; decide⟩
      : Fin ((#[] : Array Nat).push 1 |>.push 2).size).val = 0

-- A parametrised wanted fact:
theorem_wanted size_after_two_pushes {α : Type _} (a : Array α) (x y : α) :
    ((a.push x).push y).size = a.size + 2

-- Referencing the parametrised wanted with arguments: `❰foo❱ a x y`.
theorem_wanted index_after_two_pushes {α : Type _} (a : Array α) (x y : α) :
    (⟨a.size, by rw [❰size_after_two_pushes❱ a x y]; omega⟩
      : Fin ((a.push x).push y).size).val = a.size

-- A partial proof may be supplied with `:= body`, deferring the harder step via `❰…❱`:
theorem_wanted size_after_three_pushes {α : Type _} (a : Array α) (x y z : α) :
    (((a.push x).push y).push z).size = a.size + 3 := by
  rw [Array.size_push, ❰size_after_two_pushes❱ a x y]
```
 -/
theorem_wanted : Lean.Parser.Parser
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_ne_zero : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α] {q : ℚ≥0}, ↑q ≠ 0 ↔ q ≠ 0
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding_target : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z)
  (hf : Topology.IsOpenEmbedding f), (e.lift_openEmbedding hf).target = e.target
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.moduleTk.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Power.toExpr : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
/-- Let `F` and `G` be two diagrams indexed by a connected `I`, and `X` and `Y` be two cones over
`F` and `G` respectively, with maps `α : F ⟶ G` and `f : X ⟶ Y` that commutes with the cone maps.
Suppose `X = Y x[G i] F i` for all `i` and `Y = lim G`, then `X = lim F`.
 -/
CategoryTheory.Limits.isLimitOfIsPullbackOfIsConnected : {I : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} I] →
      [CategoryTheory.IsConnected I] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} C] →
          {F G : CategoryTheory.Functor I C} →
            (α : F ⟶ G) →
              (cF : CategoryTheory.Limits.Cone F) →
                (cG : CategoryTheory.Limits.Cone G) →
                  (f : (CategoryTheory.Limits.Cone.postcompose α).obj cF ⟶ cG) →
                    (∀ (i : I), CategoryTheory.IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)) →
                      CategoryTheory.Limits.IsLimit cG → CategoryTheory.Limits.IsLimit cF
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.cofibration_iff : ∀ {X Y : SSet} (f : X ⟶ Y), HomotopicalAlgebra.Cofibration f ↔ CategoryTheory.Mono f
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.part_iff₂ : ∀ {f : ℕ → ℕ →. ℕ}, (Nat.Partrec' fun v => f v.head v.tail.head) ↔ Partrec₂ f
-- Mathlib.Order.Basic
lt_or_gt_iff_ne' : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, b < a ∨ a < b ↔ a ≠ b
-- Std.Sync.CancellationToken
Std.CancellationToken.mk.sizeOf_spec : ∀ (state : Std.Mutex Std.CancellationToken.State), sizeOf { state := state } = 1 + sizeOf state
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.tendsto_pow_atTop_nhds_top_iff : ∀ {r : ENNReal}, Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds ⊤) ↔ 1 < r
-- Mathlib.RingTheory.QuotSMulTop
/-- Tensoring on the right and applying `QuotSMulTop · r` commute.  -/
QuotSMulTop.quotSMulTopTensorEquivQuotSMulTop : {R : Type u_2} →
  [inst : CommRing R] →
    (r : R) →
      (M : Type u_1) →
        (M' : Type u_3) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup M'] →
                [inst_4 : Module R M'] → TensorProduct R (QuotSMulTop r M') M ≃ₗ[R] QuotSMulTop r (TensorProduct R M' M)
-- Mathlib.Analysis.Distribution.TemperateGrowth
ContinuousLinearMap.hasTemperateGrowth : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : E →L[ℝ] F), Function.HasTemperateGrowth ⇑f
-- Mathlib.Algebra.Quandle
ShelfHom.mk.inj : ∀ {S₁ : Type u_1} {S₂ : Type u_2} {inst : Shelf S₁} {inst_1 : Shelf S₂} {toFun : S₁ → S₂}
  {map_act' : ∀ {x y : S₁}, toFun (Shelf.act x y) = Shelf.act (toFun x) (toFun y)} {toFun_1 : S₁ → S₂}
  {map_act'_1 : ∀ {x y : S₁}, toFun_1 (Shelf.act x y) = Shelf.act (toFun_1 x) (toFun_1 y)},
  { toFun := toFun, map_act' := map_act' } = { toFun := toFun_1, map_act' := map_act'_1 } → toFun = toFun_1
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.comap_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F)
  {U V : Submodule 𝕜 F}, Submodule.comap (↑↑↑f) U ⟂ Submodule.comap (↑↑↑f) V ↔ U ⟂ V
-- Mathlib.Combinatorics.Configuration
Configuration.HasLines.exists_bijective_of_card_eq : ∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [Configuration.HasLines P L] [inst_2 : Fintype P]
  [inst_3 : Fintype L],
  Fintype.card P = Fintype.card L →
    ∃ f, Function.Bijective f ∧ ∀ (l : L), Configuration.pointCount P l = Configuration.lineCount L (f l)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- `π` considered as a nonnegative real.  -/
NNReal.pi : NNReal
-- Mathlib.Topology.Bases
TopologicalSpace.SecondCountableTopology.mk' : ∀ {α : Type u_1} {b : Set (Set α)}, b.Countable → SecondCountableTopology α
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.appHom.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α α_1 : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj),
  α = α_1 →
    ∀ [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K] (X : D),
      CategoryTheory.Functor.IsCoverDense.Types.appHom α X = CategoryTheory.Functor.IsCoverDense.Types.appHom α_1 X
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousWithinAt.inv₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  {f : α → G₀} {s : Set α} {a : α} [inst_4 : TopologicalSpace α],
  ContinuousWithinAt f s a → f a ≠ 0 → ContinuousWithinAt f⁻¹ s a
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
AddCommMonCat.Hom.Simps.hom : (X Y : AddCommMonCat) → X.Hom Y → ↑X →+ ↑Y
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `Equivalence.stdSymm`. -/
Equivalence.symmetric : ∀ {α : Sort u_1} (r : α → α → Prop), Equivalence r → Std.Symm r
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.mem_span_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {s : Set R} {x : R},
  x ∈ TwoSidedIdeal.span s ↔ ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I
-- Std.Do.PostCond
/-- An assertion about the possible exceptions in `ps` that never holds.
 -/
Std.Do.ExceptConds.false : {ps : Std.Do.PostShape} → Std.Do.ExceptConds ps
-- Lean.Server.References
/-- Yields locations and parent declaration for all references referring to `ident`.  -/
Lean.Server.References.referringTo : Lean.Server.References → Lean.Lsp.RefIdent → optParam Bool true → Array Lean.Server.References.DocumentRefInfo