mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.descOpcycles.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k k_1 : K.X i ⟶ A) (e_k : k = k_1) (j j_1 : ι) (e_j : j = j_1) (hj : c.prev i = j)
  (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0), K.descOpcycles k j hj hk = K.descOpcycles k_1 j_1 ⋯ ⋯
-- Mathlib.Data.Finset.Lattice.Fold
/-- To rewrite from right to left, use `Finset.sup'_comp_eq_image`.  -/
Finset.sup'_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : DecidableEq β] {s : Finset γ}
  {f : γ → β} (hs : (Finset.image f s).Nonempty) (g : β → α), (Finset.image f s).sup' hs g = s.sup' ⋯ (g ∘ f)
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.edist_eq : ∀ {𝕜 : Type u_7} [inst : RCLike 𝕜] {n : Type u_8} [inst_1 : Fintype n] (x y : EuclideanSpace 𝕜 n),
  edist x y = (∑ i, edist (x.ofLp i) (y.ofLp i) ^ 2) ^ (1 / 2)
-- Mathlib.Data.Set.Finite.Basic
Set.BijOn.finite_iff_finite : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} {t : Set β}, Set.BijOn f s t → (s.Finite ↔ t.Finite)
-- Lean.Parser.Attr
Lean.Parser.Attr.extern : Lean.Parser.Parser
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
IsSimplyConnected.isPathConnected : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSimplyConnected s → IsPathConnected s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Init.Data.List.Attach
List.all_subtype : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → l.all f = l.unattach.all g
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- In a Dedekind domain, the prime ideals are the zero ideal together with the prime elements
of the monoid with zero `Ideal A`.  -/
Ideal.isPrime_iff_bot_or_prime : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {P : Ideal A}, P.IsPrime ↔ P = ⊥ ∨ Prime P
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Returns an updated formula f and a bool which indicates whether a contradiction was found in the
process of updating f.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertRupUnits : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.injective_comp_algebraMap : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] {L : Type u_7} [inst_2 : Field L]
  [inst_3 : Algebra A K] [IsFractionRing A K], Function.Injective fun f => f.comp (algebraMap A K)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.self_trans_symm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂),
  e.trans e.symm = ContinuousLinearEquiv.refl R₁ M₁
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.zero_smul : ∀ {R : Type u_1} {R'' : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring R''] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R'' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R'' M] (x : TensorProduct R M N), 0 • x = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, l.contains k = false → k ∈ t.insertManyIfNewUnit l → k ∈ t
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Module.finrank_le_one_iff_top_isPrincipal : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V] [Module.Finite K V], Module.finrank K V ≤ 1 ↔ ⊤.IsPrincipal
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Exception.revertFailure : Lean.MetavarContext → Lean.LocalContext → Array Lean.Expr → String → Lean.MetavarContext.MkBinding.Exception
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Mk₁.map_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {i j k : Fin 2} (hij : i ≤ j)
  (hjk : j ≤ k),
  CategoryTheory.ComposableArrows.Mk₁.map f i k ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.Mk₁.map f i j hij)
      (CategoryTheory.ComposableArrows.Mk₁.map f j k hjk)
-- Init.Data.String.Basic
String.next' : (s : String) → (p : String.Pos.Raw) → ¬String.Pos.Raw.atEnd s p = true → String.Pos.Raw
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift_eq_sum_map : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] {f : α → β} {x : FreeAddGroup α},
  (FreeAddGroup.lift f) x = FreeAddGroup.sum ((FreeAddGroup.map f) x)
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.single_apply : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddZeroClass (f i)] (i : I) (x : f i),
  (AddMonoidHom.single f i) x = Pi.single i x
-- Std.Http.Protocol.H1.Message
/-- Gets the headers of a `Message`.
 -/
Std.Http.Protocol.H1.Message.Head.headers : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Message.Head dir → Std.Http.Headers
-- Lean.Elab.Do.Control
/-- Build the lifter plan for a body whose effects are summarised by `info`.  -/
Lean.Elab.Do.EffectForwarder.ofCont : Lean.Elab.Do.ControlInfo → Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Elab.Do.EffectForwarder
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.bot_lt_add : ∀ {α : Type u} [inst : Add α] {x y : WithBot α} [inst_1 : LT α], ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y
-- Mathlib.Order.Category.PartOrdEmb
/-- Construct a bundled `PartOrdEmb` from the underlying type and typeclass.  -/
PartOrdEmb.of : (carrier : Type u_1) → [str : PartialOrder carrier] → PartOrdEmb
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- The cardinality of the decomposition group is equal to the ramification index times the
inertia degree.  -/
Ideal.card_stabilizer_eq : ∀ {R : Type u_1} {S : Type u_2} {G : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] [IsDomain R] [IsDomain S]
  [Module.Finite R S] [Module.Flat R S] (p : Ideal R) (P : Ideal S) [P.LiesOver p] [inst_12 : p.IsPrime] [P.IsPrime]
  [PerfectField p.ResidueField], Nat.card ↥(MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_of_get_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k v : α} {w : k ∈ t},
  t.get k w = v → k ∈ t
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.map_injective : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L'), Function.Injective (IntermediateField.map f)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.corec_def : ∀ {F : PFunctor.{uA, uB}} {X : Type u_2} (f : X → ↑F X) (x₀ : X),
  PFunctor.M.corec f x₀ = PFunctor.M.mk (F.map (PFunctor.M.corec f) (f x₀))
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- Given an ideal `I`, `span I` is the smallest two-sided ideal containing `I`.  -/
TwoSidedIdeal.fromIdeal : {R : Type u_1} → [inst : Ring R] → Ideal R →o TwoSidedIdeal R
-- Mathlib.FieldTheory.Minpoly.Basic
/-- A minimal polynomial is irreducible.  -/
minpoly.irreducible : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [IsDomain A]
  [IsDomain B], IsIntegral A x → Irreducible (minpoly A x)
-- Init.Data.Int.DivMod.Lemmas
Int.add_fmod_fmod : ∀ (m n k : ℤ), (m + n.fmod k).fmod k = (m + n).fmod k
-- Init.Data.List.Nat.Range
List.zipIdx_eq_cons_iff : ∀ {α : Type u_1} {x : α × ℕ} {l' : List (α × ℕ)} {l : List α} {k : ℕ},
  l.zipIdx k = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = as.zipIdx (k + 1)
-- Mathlib.Analysis.Normed.Group.Basic
/-- The nonnegative norm seen as an `ENNReal` and
then as a `Real` is equal to the norm.  -/
toReal_coe_nnnorm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), (↑‖a‖₊).toReal = ‖a‖
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.addConjMap_comp_apply : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {g h k : G} {a b c : α} {hg : b = g +ᵥ a}
  {hh : c = h +ᵥ b} {hk : c = k +ᵥ a},
  k = h + g →
    ∀ (x : ↥(SubAddAction.ofStabilizer G a)),
      (SubAddAction.ofStabilizer.conjMap hh) ((SubAddAction.ofStabilizer.conjMap hg) x) =
        (SubAddAction.ofStabilizer.conjMap hk) x
-- Mathlib.FieldTheory.RatFunc.Defs
/-- the coercion to the fraction ring of the polynomial ring  -/
RatFunc.toFractionRing : {K : Type u} → [inst : CommRing K] → RatFunc K → FractionRing (Polynomial K)
-- Mathlib.Analysis.Normed.Group.Constructions
Additive.toNNNorm : {E : Type u_2} → [NNNorm E] → NNNorm (Additive E)
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Measure.integrable_compProd_snd_iff : ∀ {α : Type u_5} {β : Type u_6} {E : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : NormedAddCommGroup E] {κ : ProbabilityTheory.Kernel α β} {μ : MeasureTheory.Measure α} {f : β → E}
  [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ],
  MeasureTheory.AEStronglyMeasurable f (μ.bind ⇑κ) →
    (MeasureTheory.Integrable (fun p => f p.2) (μ.compProd κ) ↔ MeasureTheory.Integrable f (μ.bind ⇑κ))
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjObj.hom_ext_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] {Z : C} {f g : Z ⟶ W.weightedLimObjObj F},
  f = g ↔
    ∀ {j : J} (x : W.obj j),
      CategoryTheory.CategoryStruct.comp f (W.weightedLimObjObjπ F x) =
        CategoryTheory.CategoryStruct.comp g (W.weightedLimObjObjπ F x)
-- Mathlib.Order.Hom.Basic
codisjoint_map_orderIso_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderTop α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderTop β] {a b : α} (f : α ≃o β), Codisjoint (f a) (f b) ↔ Codisjoint a b
-- Mathlib.Analysis.PSeries
NNReal.summable_rpow : ∀ {p : ℝ}, (Summable fun n => ↑n ^ p) ↔ p < -1
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] {g : β → α} {s : Set β} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β] {f : ℕ → β → α},
  HasSumLocallyUniformlyOn f g s → TendstoLocallyUniformlyOn (fun N b => ∑ i ∈ Finset.range N, f i b) g Filter.atTop s
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.of_zag : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ : J},
  CategoryTheory.Zag j₁ j₂ → CategoryTheory.Zigzag j₁ j₂
-- Init.Data.Array.DecidableEq
Array.isEqv_self : ∀ {α : Type u_1} [inst : DecidableEq α] (xs : Array α), (xs.isEqv xs fun x1 x2 => decide (x1 = x2)) = true
-- Mathlib.Algebra.Homology.Homotopy
/-- A homotopy showing that composing the backward and forward maps is homotopic to the identity
on D  -/
HomotopyEquiv.homotopyInvHomId : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            (self : HomotopyEquiv C D) →
              Homotopy (CategoryTheory.CategoryStruct.comp self.inv self.hom) (CategoryTheory.CategoryStruct.id D)
-- Init.Data.List.Nat.TakeDrop
List.drop_append_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, List.drop l₁.length (l₁ ++ l₂) = l₂
-- Mathlib.Algebra.Category.Ring.Under.Basic
/-- Make a morphism in `Under R` from an algebra map.  -/
AlgHom.toUnder : {R : CommRingCat} →
  {A B : Type u} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra (↑R) A] → [inst_3 : Algebra (↑R) B] → (A →ₐ[↑R] B) → (R.mkUnder A ⟶ R.mkUnder B)
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.coeff_one_zeroX : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R), (PowerSeries.coeff 1) F.zeroX = 1
-- Mathlib.Tactic.Linarith.Parsing
/-- We introduce a local instance allowing addition of `TreeMap`s,
removing any keys with value zero.
We don't need to prove anything about this addition, as it is only used in meta code.
 -/
instAddTreeMapOfZeroOfDecidableEq_mathlib : {α : Type u_1} →
  {β : Type u_2} → {c : α → α → Ordering} → [Add β] → [Zero β] → [DecidableEq β] → Add (Std.TreeMap α β c)
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateResetImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → ℕ → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Lean.Elab.PreDefinition.FixedParams
/-- We observe a possibly valid edge.
 -/
Lean.Elab.FixedParams.Info.setCallerParam : ℕ → ℕ → ℕ → ℕ → Lean.Elab.FixedParams.Info → Lean.Elab.FixedParams.Info
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.fold_map : ∀ {α β γ δ : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {f : β → γ} {g : δ → γ → δ} {init : δ} {it : Std.Iter β},
  Std.Iter.fold g init (Std.Iter.map f it) = Std.Iter.fold (fun d b => g d (f b)) init it
-- ProofWidgets.Component.Basic
ProofWidgets.Component.mk.injEq : ∀ {Props : Type} (toModule : Lean.Widget.Module) («export» : String) (toModule_1 : Lean.Widget.Module)
  (export_1 : String),
  ({ toModule := toModule, «export» := «export» } = { toModule := toModule_1, «export» := export_1 }) =
    (toModule = toModule_1 ∧ «export» = export_1)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getKey!_eq_getKey! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α] {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.getKey! a = Std.Internal.List.getKey! a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.instLargeCategory : CategoryTheory.LargeCategory ωCPO
-- Mathlib.Topology.Closure
exists_isClosed_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {p : Set X → Prop}, (∃ t, IsClosed t ∧ p t) ↔ ∃ t, p (closure t)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.injective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), Function.Injective ⇑e
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
        (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))) =
    CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f)
      (CategoryTheory.Limits.pullback.map
        (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
        (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
        (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
        (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)
-- Lean.Attributes
Lean.AttributeImplCore.mk : autoParam Lean.Name Lean.AttributeImplCore.ref._autoParam →
  Lean.Name → String → Lean.AttributeApplicationTime → Lean.AttributeImplCore
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.natCast_mul_natCast_cpow : ∀ (m n : ℕ) (s : ℂ), (↑m * ↑n) ^ s = ↑m ^ s * ↑n ^ s
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
monoEquivOfFin.congr_simp : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : LinearOrder α] {k : ℕ} (h : Fintype.card α = k),
  monoEquivOfFin α h = monoEquivOfFin α h
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instPowUSizeUintNumBits : Lean.Grind.ToInt.Pow USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Given `A : AddCommGrpCat` and a ring morphism `R →+* End A`, this is a type synonym
for `A`, on which we shall define a structure of `R`-module.  -/
ModuleCat.mkOfSMul' : {R : Type u} → [inst : Ring R] → {A : AddCommGrpCat} → (R →+* CategoryTheory.End A) → AddCommGrpCat
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULiftHom.up_map_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.ULiftHom.up.map f).down = f
-- Mathlib.Data.Num.Bitwise
NzsNum.msb.sizeOf_spec : ∀ (a : Bool), sizeOf (NzsNum.msb a) = 1 + sizeOf a
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.merge' : ∀ {α : Type u_1} {le : α → α → Bool} {s₁ s₂ : Batteries.BinomialHeap.Imp.Heap α} {n : ℕ},
  Batteries.BinomialHeap.Imp.Heap.WF le n s₁ →
    Batteries.BinomialHeap.Imp.Heap.WF le n s₂ →
      Batteries.BinomialHeap.Imp.Heap.WF le n (Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂) ∧
        ((s₁.rankGT n ↔ s₂.rankGT n) → (Batteries.BinomialHeap.Imp.Heap.merge le s₁ s₂).rankGT n)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.inter_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.inter t₂ = t₁ ∩ t₂
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Bimon C} {f g : X ⟶ Y},
  f.hom.hom = g.hom.hom → f = g
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.mk.injEq : ∀ (cancelledByCancelRequest cancelledByEdit : IO.CancelToken)
  (requestCancellationPromise editCancellationPromise : IO.Promise Unit)
  (cancelledByCancelRequest_1 cancelledByEdit_1 : IO.CancelToken)
  (requestCancellationPromise_1 editCancellationPromise_1 : IO.Promise Unit),
  ({ cancelledByCancelRequest := cancelledByCancelRequest, cancelledByEdit := cancelledByEdit,
        requestCancellationPromise := requestCancellationPromise, editCancellationPromise := editCancellationPromise } =
      { cancelledByCancelRequest := cancelledByCancelRequest_1, cancelledByEdit := cancelledByEdit_1,
        requestCancellationPromise := requestCancellationPromise_1,
        editCancellationPromise := editCancellationPromise_1 }) =
    (cancelledByCancelRequest = cancelledByCancelRequest_1 ∧
      cancelledByEdit = cancelledByEdit_1 ∧
        requestCancellationPromise = requestCancellationPromise_1 ∧ editCancellationPromise = editCancellationPromise_1)
-- Mathlib.Control.Traversable.Lemmas
Traversable.naturality' : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F G : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] [inst_4 : Applicative G] [LawfulApplicative G] {α : Type u} (η : ApplicativeTransformation F G)
  (x : t (F α)), (fun {α} => η.app α) (sequence x) = sequence ((fun {α} => η.app α) <$> x)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_comm : ∀ (x y : ℕ), x ||| y = y ||| x
-- Mathlib.Algebra.Module.SpanRank
Submodule.FG.generators_ncard : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.FG → p.generators.ncard = p.spanFinrank
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.coe_equivFnOfDiscrete : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : DiscreteTopology α],
  ⇑ContinuousMap.equivFnOfDiscrete = DFunLike.coe
-- Mathlib.GroupTheory.Commutator.Basic
/-- If g is conjugate to `2 • g`, then `g` is an additive commutator  -/
mem_addCommutatorSet_of_isAddConj_sq : ∀ (G : Type u_1) [inst : AddGroup G] {g : G}, IsAddConj g (2 • g) → g ∈ addCommutatorSet G
-- Mathlib.Analysis.Convex.EGauge
Set.MapsTo.egauge_le : ∀ (𝕜 : Type u_1) [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] {s : Set E} {E' : Type u_3} {F : Type u_4}
  [inst_2 : SMul 𝕜 E'] [inst_3 : FunLike F E E'] [MulActionHomClass F 𝕜 E E'] (f : F) {t : Set E'},
  Set.MapsTo (⇑f) s t → ∀ (x : E), egauge 𝕜 t (f x) ≤ egauge 𝕜 s x
-- Mathlib.Analysis.Normed.Group.Uniform
locallyLipschitzOn_inv_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E} {s : Set α},
  LocallyLipschitzOn s f⁻¹ ↔ LocallyLipschitzOn s f
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
/-- The connecting homomorphism in the long exact sequence attached to a homological
functor and a distinguished triangle.  -/
CategoryTheory.Functor.homologySequenceδ : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.HasShift C ℤ] →
        [inst_2 : CategoryTheory.Category.{v_3, u_3} A] →
          (F : CategoryTheory.Functor C A) →
            [inst_3 : F.ShiftSequence ℤ] →
              (T : CategoryTheory.Pretriangulated.Triangle C) →
                (n₀ n₁ : ℤ) → n₀ + 1 = n₁ → ((F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₁)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
coe_set_eq_zero : ∀ {G : Type u_2} [inst : AddGroup G] {s : AddSubgroup G}, ↑s = 0 ↔ s = ⊥
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.ofNat_le_cast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {m n : ℕ} [inst_5 : m.AtLeastTwo], OfNat.ofNat m ≤ ↑n ↔ OfNat.ofNat m ≤ n
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.divRight_symm_apply : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (x b : G),
  (Homeomorph.divRight x).symm b = b * x