mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
/-- A submodule of full rank of a free finite `ℤ`-module has a finite quotient.
It can't be an instance because of the side condition `Module.finrank ℤ N = Module.finrank ℤ M`.
 -/
Submodule.finiteQuotientOfFreeOfRankEq : ∀ {M : Type u_3} [inst : AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M),
  Module.finrank ℤ ↥N = Module.finrank ℤ M → Finite (M ⧸ N)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.one_eq_eval : ∀ (M : Type u_1) [inst : GroupWithZero M], 1 = Mathlib.Tactic.FieldSimp.NF.eval []
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.self_mem_principalOpen : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] (x : X),
  x ∈ Alexandrov.principalOpen x
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.comp.injEq : ∀ (a a_1 a_2 a_3 : Turing.ToPartrec.Code), (a.comp a_1 = a_2.comp a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instNonAssocRing : {R : Type u_1} → [NonAssocRing R] → NonAssocRing (Lex R)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.subset_adjoin : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A},
  s ⊆ ↑(Algebra.adjoin R s)
-- Init.Data.Range.Polymorphic.Basic
Std.Rxc.size_pos_iff_le : ∀ {α : Type u} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxc.HasSize α]
  [Std.Rxc.LawfulHasSize α] {lo hi : α}, 0 < Std.Rxc.HasSize.size lo hi ↔ lo ≤ hi
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.mem_uniformity : ∀ {α : Type u} [inst : UniformSpace α] {s : Set (CauchyFilter α × CauchyFilter α)},
  s ∈ uniformity (CauchyFilter α) ↔ ∃ t ∈ uniformity α, CauchyFilter.gen t ⊆ s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.Algebra.Order.Floor.Div
floorDiv_of_nonpos : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] {a : α}, a ≤ 0 → ∀ (b : β), b ⌊/⌋ a = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : β → β} {hc : k' ∈ t.modify k f}, (t.modify k f)[k'] = if heq : cmp k k' = Ordering.eq then f t[k] else t[k']
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_iff_tendsto : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L ↔ Filter.Tendsto (fun p => ‖p.1 - p.2‖⁻¹ * ‖f p.1 - f p.2 - (p.1 - p.2) • f'‖) L (nhds 0)
-- Mathlib.RingTheory.Polynomial.Dickson
_private.Mathlib.RingTheory.Polynomial.Dickson.0.Polynomial.dickson.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
/-- `toGrothendieck` and `toPrecoverage` form a Galois connection.  -/
CategoryTheory.Precoverage.toGrothendieck_le_iff_le_toPrecoverage : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] {K : CategoryTheory.Precoverage C}
  {J : CategoryTheory.GrothendieckTopology C}, K.toGrothendieck ≤ J ↔ K ≤ J.toPrecoverage
-- Mathlib.MeasureTheory.Measure.Restrict
/-- This lemma shows that `restrict` and `toOuterMeasure` commute. Note that the LHS has a
restrict on measures and the RHS has a restrict on outer measures.  -/
MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → (μ.restrict s).toOuterMeasure = (MeasureTheory.OuterMeasure.restrict s) μ.toOuterMeasure
-- Mathlib.Tactic.Inhabit
/-- Derives `Inhabited α` from `Nonempty α` without `Classical.choice`
assuming `α` is of type `Prop`.  -/
Lean.Elab.Tactic.nonempty_prop_to_inhabited : (α : Prop) → Nonempty α → Inhabited α
-- Lean.Data.LOption
Lean.LOption.some.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : α), sizeOf (Lean.LOption.some a) = 1 + sizeOf a
-- Mathlib.Order.SuccPred.Basic
Order.pred_covBy : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α), Order.pred a ⋖ a
-- Mathlib.NumberTheory.LSeries.PrimesInAP
ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux.congr_simp : ∀ {q : ℕ} (a a_1 : ZMod q),
  a = a_1 →
    ∀ [inst : NeZero q] (s s_1 : ℂ),
      s = s_1 →
        ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a s =
          ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a_1 s_1
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedSemiring.default : Lean.Meta.Sym.Arith.Semiring
-- Mathlib.Data.Set.Prod
Set.insert_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α}, insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.instInjectiveXIntCochainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.InjectiveResolution X) (n : ℤ),
  CategoryTheory.Injective (R.cochainComplex.X n)
-- Mathlib.Algebra.Module.Injective
/-- If `x ∈ M ⊔ ⟨y⟩`, then `x = m + r • y`, `fst` pick an arbitrary such `m`.  -/
Module.Baer.ExtensionOfMaxAdjoin.fst : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) →
                        {f : M →ₗ[R] Q} →
                          [inst_7 : Fact (Function.Injective ⇑i)] →
                            {y : N} →
                              ↥(Module.Baer.supExtensionOfMaxSingleton i f y) → ↥(Module.Baer.extensionOfMax i f).domain
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.IsFiniteType.mk : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {σ : M.GeneratingSections},
  autoParam (Finite σ.I) SheafOfModules.GeneratingSections.IsFiniteType.finite._autoParam → σ.IsFiniteType
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.diagramFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (X : C) {X_1 Y : CategoryTheory.Functor Cᵒᵖ D} (η : X_1 ⟶ Y), (J.diagramFunctor D X).map η = J.diagramNatTrans η X
-- Mathlib.Topology.Hom.ContinuousEval
ContinuousEval.toContinuousEvalConst : ∀ {F : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : FunLike F X Y] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [ContinuousEval F X Y], ContinuousEvalConst F X Y
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁.subseq s₂` checks whether `s₁` is a subsequence of `s₂`
 -/
Lean.Grind.AC.Seq.subseq : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.SubseqResult
-- Mathlib.Condensed.Light.Sequence
CompHausLike.mk.congr_simp : ∀ {P : TopCat → Prop} (toTop toTop_1 : TopCat) (e_toTop : toTop = toTop_1) [is_compact : CompactSpace ↑toTop]
  [is_hausdorff : T2Space ↑toTop] (prop : P toTop),
  { toTop := toTop, is_compact := is_compact, is_hausdorff := is_hausdorff, prop := prop } =
    { toTop := toTop_1, is_compact := ⋯, is_hausdorff := ⋯, prop := ⋯ }
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_pow_p_pow_self : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ),
  (Perfection.coeffMonoidHom M p n) f ^ p ^ n = (Perfection.coeffMonoidHom M p 0) f
-- Mathlib.Order.SuccPred.Basic
Order.Ioc_pred_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioc (Order.pred b) a = Set.Icc b a
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.ExtTreeMap.getEntryGED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α × β → α × β
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An orbit of a normal subgroup is a block  -/
MulAction.IsBlock.orbit_of_normal : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {N : Subgroup G} [N.Normal] (a : X),
  MulAction.IsBlock G (MulAction.orbit (↥N) a)
-- Lean.Expr
Lean.instHashableFVarId.hash : Lean.FVarId → UInt64
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The rewrite tactic string that performs the rewrite  -/
Mathlib.Tactic.LibraryRewrite.RewriteInterface.tactic : Mathlib.Tactic.LibraryRewrite.RewriteInterface → String
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- A DVR is a valuation ring.  -/
of_isDiscreteValuationRing : ∀ (A : Type u) [inst : CommRing A] [inst_1 : IsDomain A] [IsDiscreteValuationRing A], ValuationRing A
-- Init.PropLemmas
and_congr_left' : ∀ {a b c : Prop}, (a ↔ b) → (a ∧ c ↔ b ∧ c)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDeclarationParams.toJson : Lean.Lsp.DeclarationParams → Lean.Json
-- Mathlib.Order.Antichain
isStrongAntichain_insert : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  IsStrongAntichain r (insert a s) ↔ IsStrongAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ∀ (c : α), ¬r a c ∨ ¬r b c
-- Mathlib.Data.List.Nodup
List.Nodup.append : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.Nodup → l₂.Nodup → l₁.Disjoint l₂ → (l₁ ++ l₂).Nodup
-- Mathlib.Algebra.Lie.Subalgebra
instCoeLieSubalgebraSubmodule : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Coe (LieSubalgebra R L) (Submodule R L)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.eq_normS_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Bool
-- Mathlib.CategoryTheory.Adjunction.Unique
/-- If `F` and `F'` are both left adjoint to `G`, then they are naturally isomorphic.  -/
CategoryTheory.Adjunction.leftAdjointUniq : {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] →
        {F F' : CategoryTheory.Functor C D} → {G : CategoryTheory.Functor D C} → (F ⊣ G) → (F' ⊣ G) → (F ≅ F')
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.flatten.match_1.eq_2 : ∀ {α : Type u_1} (motive : List (List α) → Sort u_2) (l : List α) (L : List (List α)) (h_1 : Unit → motive [])
  (h_2 : (l : List α) → (L : List (List α)) → motive (l :: L)),
  (match l :: L with
    | [] => h_1 ()
    | l :: L => h_2 l L) =
    h_2 l L
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.IterM.step_drop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : 0 = 0 → motive 0) (h_2 : (k : ℕ) → 0 = k.succ → motive k.succ),
  (match h' : 0 with
    | 0 => h_1 h'
    | k.succ => h_2 k h') =
    h_1 ⋯
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` iff `range 𝓕` is equicontinuous at `x₀`,
i.e the family `(↑) : range F → X → α` is equicontinuous at `x₀`.  -/
equicontinuousAt_iff_range : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} {x₀ : X},
  EquicontinuousAt F x₀ ↔ EquicontinuousAt Subtype.val x₀
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_le_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k km : α} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ (hc : Std.Internal.List.containsKey k l = true),
      (Std.Internal.List.maxKey? l).get ⋯ = km → (compare k km).isLE = true
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Meta.Grind.Params.containsEMatch : Lean.Meta.Grind.Params → Lean.Name → Bool
-- Mathlib.Data.Nat.ModEq
AddCommGroup.modEq_iff_natModEq : ∀ {a b n : ℕ}, a ≡ b [PMOD n] ↔ a ≡ b [MOD n]
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_fun_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      (∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n) (f i) s x) →
        iteratedDerivWithin n (fun x => ∑ i ∈ I, f i x) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.isAffineHom_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y],
  AlgebraicGeometry.IsAffineHom f
-- Mathlib.ModelTheory.PartialEquiv
/-- The cofinal set of finite equivalences with a given element in their domain.  -/
FirstOrder.Language.IsExtensionPair.definedAtLeft : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → L.IsExtensionPair M N → M → Order.Cofinal (L.FGEquiv M N)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {fallback : β k'} {f : β k → β k},
  (m.modify k f).getD k' fallback =
    if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback else m.getD k' fallback
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.transPartialEquiv_source : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f' : PartialEquiv β γ),
  (e.transPartialEquiv f').source = ⇑e ⁻¹' f'.source
-- Mathlib.GroupTheory.Complement
/-- The correct way to unfold `IsComplement` for `SetLike`s such as `AddSubgroup`s  -/
AddSubgroup.isComplement_iff_bijective : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_2} [inst_1 : SetLike S G] (s t : S),
  AddSubgroup.IsComplement ↑s ↑t ↔ Function.Bijective fun x => ↑x.1 + ↑x.2
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.instIsWellFoundedElemNIIAncestralRel : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular], IsWellFounded (↑P.II) P.AncestralRel
-- Init.Data.ToString.Basic
instToStringFormat : ToString Std.Format
-- Init.Data.Vector.Lemmas
Vector.mem_append_right : ∀ {α : Type u_1} {n m : ℕ} {a : α} (xs : Vector α n) {ys : Vector α m}, a ∈ ys → a ∈ xs ++ ys
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- Subsemiring closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`.  -/
NonUnitalSubsemiring.closure_mono : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] ⦃s t : Set R⦄,
  s ⊆ t → NonUnitalSubsemiring.closure s ≤ NonUnitalSubsemiring.closure t
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.negRev : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0to1.tr.match_3.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} (motive : Turing.TM0to1.Λ' Γ Λ → Sort u_3) (d : Turing.Dir) (q : Λ)
  (h_1 : (q : Λ) → motive (Turing.TM0to1.Λ'.normal q))
  (h_2 : (d : Turing.Dir) → (q : Λ) → motive (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.move d) q))
  (h_3 : (a : Γ) → (q : Λ) → motive (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.write a) q)),
  (match Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.move d) q with
    | Turing.TM0to1.Λ'.normal q => h_1 q
    | Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.move d) q => h_2 d q
    | Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.write a) q => h_3 a q) =
    h_2 d q
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.BinaryCofan.isVanKampen_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y),
  CategoryTheory.IsVanKampenColimit c ↔
    ∀ {X' Y' : C} (c' : CategoryTheory.Limits.BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      CategoryTheory.CategoryStruct.comp αX c.inl = CategoryTheory.CategoryStruct.comp c'.inl f →
        CategoryTheory.CategoryStruct.comp αY c.inr = CategoryTheory.CategoryStruct.comp c'.inr f →
          (Nonempty (CategoryTheory.Limits.IsColimit c') ↔
            CategoryTheory.IsPullback c'.inl αX f c.inl ∧ CategoryTheory.IsPullback c'.inr αY f c.inr)
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.projectionL_add_projectionL_eq_id : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q),
  p.projectionL q h + q.projectionL p ⋯ = ContinuousLinearMap.id R M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.PackedBitVec.mk.inj : ∀ {w : ℕ} {bv : BitVec w} {w_1 : ℕ} {bv_1 : BitVec w_1},
  { w := w, bv := bv } = { w := w_1, bv := bv_1 } → w = w_1 ∧ bv ≍ bv_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {fallback : β}, t.contains a = false → t.getD a fallback = fallback
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.supNorm_eq_zero_iff : ∀ {A : Type u_1} [inst : NormedRing A] (p : Polynomial A), p.supNorm = 0 ↔ p = 0
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.toPlus_comp_plusCompIso_inv : ∀ {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] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F],
  CategoryTheory.CategoryStruct.comp (J.toPlus (P.comp F)) (J.plusCompIso F P).inv =
    CategoryTheory.Functor.whiskerRight (J.toPlus P) F
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv.eq_4 : ∀ (m n : ℕ), (Int.negSucc m).tdiv (Int.negSucc n) = Int.ofNat (m.succ / n.succ)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- See `SimpleGraph.cliqueFree_of_chromaticNumber_lt` for a tighter bound.  -/
SimpleGraph.cliqueFree_of_card_lt : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} [inst : Fintype α], Fintype.card α < n → G.CliqueFree n
-- Mathlib.Analysis.SpecialFunctions.JapaneseBracket
closedBall_rpow_sub_one_eq_empty_aux : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] {r t : ℝ}, 0 < r → 1 < t → Metric.closedBall 0 (t ^ (-r⁻¹) - 1) = ∅
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a → ∀ (s : σ), MvPowerSeries.subst a (MvPowerSeries.X s) = a s
-- Lean.DocString.Extension
Lean.ElabInline.custom.sizeOf_spec : ∀ (val : Dynamic), sizeOf (Lean.ElabInline.custom val) = 1 + sizeOf val
-- Init.SimpLemmas
have_body_congr_dep' : ∀ {α : Sort u} {β : α → Sort v} (a : α) {f f' : (x : α) → β x}, (∀ (x : α), f x = f' x) → f a = f' a
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- In a compactly generated space `X`, a set `s` is closed when `s ∩ K` is
closed for every compact set `K`.  -/
CompactlyGeneratedSpace.isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X},
  (∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)) → IsClosed s
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {k : α},
  k ∈ m.keys ↔ k ∈ m
-- Mathlib.Topology.Separation.CompletelyRegular
isInducing_stoneCechUnit : ∀ {X : Type u} [inst : TopologicalSpace X] [CompletelyRegularSpace X], Topology.IsInducing stoneCechUnit
-- Init.Data.Array.InsertIdx
Array.eraseIdx_insertIdx_self : ∀ {α : Type u} {a : α} {i : ℕ} {xs : Array α} (h : i ≤ xs.size), (xs.insertIdx i a h).eraseIdx i ⋯ = xs
-- Mathlib.Algebra.Field.Basic
OrderDual.instDivisionRing : {K : Type u_1} → [DivisionRing K] → DivisionRing Kᵒᵈ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α},
  Std.DTreeMap.Internal.Impl.Const.get? (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)) k =
    if k ∈ t ∨ l.contains k = true then some () else none
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMap_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [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₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J)
  [inst_4 :
    ∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
      (X₃ : CategoryTheory.GradedObject I₃ C₃),
      ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  (X₁ : CategoryTheory.GradedObject I₁ C₁),
  (CategoryTheory.GradedObject.mapTrifunctorMap F p).obj X₁ =
    CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- **Riesz's theorem**: a locally compact topological vector space is finite-dimensional.  -/
FiniteDimensional.of_locallyCompactSpace : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_5} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [WeaklyLocallyCompactSpace E], FiniteDimensional 𝕜 E
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set ↑s},
  MeasureTheory.NullMeasurableSet s μ → MeasurableSet t → MeasureTheory.NullMeasurableSet (Subtype.val '' t) μ
-- Mathlib.RingTheory.Ideal.Operations
Ideal.uniqueUnits : {R : Type u} → [inst : CommSemiring R] → Unique (Ideal R)ˣ