mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.MapIdx
_private.Init.Data.List.MapIdx.0.List.mapIdx.go.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → Array β → Sort u_3) (acc : Array β)
  (h_1 : (acc : Array β) → motive [] acc) (h_2 : (a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc),
  (match [], acc with
    | [], acc => h_1 acc
    | a :: as, acc => h_2 a as acc) =
    h_1 acc
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.span_eq_top_iff_isReproducing : ∀ {R : Type u_7} {M : Type u_8} [inst : Ring R] [inst_1 : LinearOrder R] [AddLeftStrictMono R] [inst_3 : AddCommGroup M]
  [Nontrivial M] [inst_5 : Module R M] {C : ConvexCone R M}, Submodule.span R ↑C = ⊤ ↔ C.IsReproducing
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_neg : ∀ {x : ℝ*}, (-x).Infinitesimal ↔ x.Infinitesimal
-- Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
CategoryTheory.Functor.CoconeTypes.descColimitType_injective_iff_of_isFiltered : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFiltered J]
  {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes),
  Function.Injective (F.descColimitType c) ↔
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' →
        ∃ k f f',
          (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f')) x'
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.mk_toAlgEquivAux : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : K)
  (L : FiniteGaloisIntermediateField k K) (hx' : InfiniteGalois.toAlgEquivAux✝ g x ∈ L.toIntermediateField)
  (hx : x ∈ L.toIntermediateField), ⟨InfiniteGalois.toAlgEquivAux✝ g x, hx'⟩ = ((InfiniteGalois.proj L) g) ⟨x, hx⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
  {Z : C} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal i)
          (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
            (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Topology.Homotopy.Contractible
nullhomotopic_of_indiscrete : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [Nonempty Y]
  [IndiscreteTopology Y] (f : C(X, Y)), f.Nullhomotopic
-- Mathlib.Topology.Algebra.Ring.Basic
instIsTopologicalSemiringMulOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : TopologicalSpace R] [IsTopologicalSemiring R],
  IsTopologicalSemiring Rᵐᵒᵖ
-- Init.Data.Nat.Lemmas
Nat.max_add_right_self : ∀ {a b : ℕ}, max a (a + b) = a + b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).minKey? =
        some (t.minKey?.elim k fun k' => if (compare k k').isLE = true then k else k')
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHomFun.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) (x : α),
  a.ofPermHomFun τ x =
    if hx : g.cycleOf x ∈ g.cycleFactorsFinset then (g ^ Nat.find ⋯) (a (↑τ ⟨g.cycleOf x, hx⟩)) else x
-- Mathlib.CategoryTheory.Presentable.Retracts
CategoryTheory.instIsStableUnderRetractsIsCardinalPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular],
  (CategoryTheory.isCardinalPresentable C κ).IsStableUnderRetracts
-- Mathlib.Tactic.Push
/-- If `true` (default `false`), rewrite `¬ (p ∧ q)` into `¬ p ∨ ¬ q` instead of `p → ¬ q`.  -/
Mathlib.Tactic.Push.Config.distrib : Mathlib.Tactic.Push.Config → Bool
-- Std.Sat.AIG.Basic
/-- An entrypoint into an `AIG`. This can be used to evaluate a circuit, starting at a certain node,
with `AIG.denote` or to construct bigger circuits on top of this specific node.
 -/
Std.Sat.AIG.Entrypoint : (α : Type) → [DecidableEq α] → [Hashable α] → Type
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define a `GCDMonoid` structure on a monoid just from the existence of a `gcd`.  -/
gcdMonoidOfExistsGCD : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] → [DecidableEq α] → (∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) → GCDMonoid α
-- Mathlib.RingTheory.SimpleModule.Basic
covBy_iff_quot_is_simple : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A B : Submodule R M},
  A ≤ B → (A ⋖ B ↔ IsSimpleModule R (↥B ⧸ Submodule.comap B.subtype A))
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.prod_fst_snd : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β],
  (AddActionHom.fst M α β).prod (AddActionHom.snd M α β) = AddActionHom.id M
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.Const.alter.eq_1 : ∀ {α : Type u} [inst : BEq α] {β : Type v} (a : α) (f : Option β → Option β),
  Std.DHashMap.Internal.AssocList.Const.alter a f Std.DHashMap.Internal.AssocList.nil =
    match f none with
    | none => Std.DHashMap.Internal.AssocList.nil
    | some b => Std.DHashMap.Internal.AssocList.cons a b Std.DHashMap.Internal.AssocList.nil
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_srem : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec (a.srem b) = ISize.ofBitVec a % ISize.ofBitVec b
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.map_sum : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] {X Y : C} {α : Type u_4}
  (f : α → (X ⟶ Y)) (s : Finset α), F.map (∑ a ∈ s, f a) = ∑ a ∈ s, F.map (f a)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.reindex_updateRow : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq l]
  [inst_1 : DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α) (e : m ≃ l) (f : n ≃ o),
  (Matrix.reindex e f) (A.updateRow i r) = ((Matrix.reindex e f) A).updateRow (e i) fun i => r (f.symm i)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Signature.mk.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr)
  (params : Array (Lean.Compiler.LCNF.Param pu)) (safe : Bool) (name_1 : Lean.Name) (levelParams_1 : List Lean.Name)
  (type_1 : Lean.Expr) (params_1 : Array (Lean.Compiler.LCNF.Param pu)) (safe_1 : Bool),
  ({ name := name, levelParams := levelParams, type := type, params := params, safe := safe } =
      { name := name_1, levelParams := levelParams_1, type := type_1, params := params_1, safe := safe_1 }) =
    (name = name_1 ∧ levelParams = levelParams_1 ∧ type = type_1 ∧ params = params_1 ∧ safe = safe_1)
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given an additive congruence relation `c` on a type `M` with an addition,
the order-preserving bijection between the set of additive congruence relations containing `c` and
the additive congruence relations on the quotient of `M` by `c`.  -/
AddCon.correspondence : {M : Type u_1} → [inst : Add M] → {c : AddCon M} → { d // c ≤ d } ≃o AddCon c.Quotient
-- Mathlib.Topology.Constructions
instDiscreteTopologySubtype : ∀ {X : Type u} {p : X → Prop} [inst : TopologicalSpace X] [DiscreteTopology X], DiscreteTopology (Subtype p)
-- Lean.Elab.Tactic.Omega.Frontend
/-- Construct the `rfl` proof that `lc.eval atoms = e`.  -/
Lean.Elab.Tactic.Omega.mkEvalRflProof : Lean.Expr → Lean.Omega.LinearCombo → Lean.Elab.Tactic.Omega.OmegaM Lean.Expr
-- Mathlib.Tactic.Explode.Datatypes
/-- `Entry.depth` * `│`  -/
Mathlib.Explode.Status.reg : Mathlib.Explode.Status
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.natCast_sInf`. -/
ENat.coe_sInf : ∀ {s : Set ℕ}, s.Nonempty → ↑(sInf s) = ⨅ a ∈ s, ↑a
-- Init.Data.String.PosRaw
String.Pos.Raw.inc_unoffsetBy_inc : ∀ {p q : String.Pos.Raw}, p.inc.unoffsetBy q.inc = p.unoffsetBy q
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {a : α}, Std.Internal.List.containsKey a [] = false
-- Mathlib.Order.Interval.Set.Fin
Fin.image_natAdd_uIcc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m '' Set.uIcc i j = Set.uIcc (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.Analysis.Complex.Angle
/-- Arc-length is always less than a multiple of chord-length.  -/
Complex.angle_le_mul_norm_sub : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → InnerProductGeometry.angle x y ≤ Real.pi / 2 * ‖x - y‖
-- Mathlib.Topology.Compactness.Compact
Set.isCompact_sigma : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : Set ι} {t : (i : ι) → Set (X i)},
  s.Finite → (∀ i ∈ s, IsCompact (t i)) → IsCompact (s.sigma t)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.sectionsFunctor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) {X Y : SheafOfModules R} (f : X ⟶ Y),
  (SheafOfModules.sectionsFunctor R).map f = TypeCat.ofHom (SheafOfModules.sectionsMap f)
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Functor.mapActionCongr_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} W] (G : Type u_3) [inst_2 : Monoid G] {F F' : CategoryTheory.Functor V W}
  (e : F ≅ F'),
  (CategoryTheory.Functor.mapActionCongr G e).hom =
    { app := fun X => (Action.mkIso (e.app X.V) ⋯).hom, naturality := ⋯ }
-- Mathlib.Tactic.NormNum.Core
/-- Traverses the given expression using simp and normalises any numbers it finds.  -/
Mathlib.Meta.NormNum.deriveSimp : Lean.Meta.Simp.Context → optParam Bool true → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.List.Sort.Basic.0.List.mergeSort.match_1.congr_eq_3 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (x : List α) (x_1 : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le) (a b : α) (xs : List α)
  (le : α → α → Bool),
  x = a :: b :: xs →
    x_1 = le →
      (match x, x_1 with
        | [], x => h_1 x
        | [a], x => h_2 a x
        | a :: b :: xs, le => h_3 a b xs le) ≍
        h_3 a b xs le
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.Scheme.Hom.imageι.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Hom.imageι f = (AlgebraicGeometry.Scheme.Hom.ker f).subschemeι
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Two left invariant measures integrate in the same way continuous compactly supported functions,
up to the scalar `haarScalarFactor μ' μ`. See also
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which gives the same result for compact
sets, and `measure_isHaarMeasure_eq_smul_of_isOpen` for open sets.  -/
MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsMulLeftInvariant] {f : G → ℝ},
  Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ
-- Lean.Server.References
/-- Declarations in the module of the ILean.  -/
Lean.Server.LoadedILean.decls : Lean.Server.LoadedILean → Lean.Lsp.Decls
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_le_size_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List (α × β)}, t.size ≤ (t.insertMany l).size
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.algebra₂ : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (self : Algebra.Extension R S) → Algebra self.Ring S
-- Mathlib.Data.Set.Function
Function.Semiconj.bijOn_range : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {f : α → β},
  Function.Semiconj f fa fb → Function.Bijective fa → Function.Injective f → Set.BijOn fb (Set.range f) (Set.range f)
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Evaluate option accessor, using subterm-specific options if set.  -/
Lean.PrettyPrinter.Delaborator.getPPOption : {α : Type} → (Lean.Options → α) → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Algebra.Ring.Prod
RingEquiv.coe_prodComm : ∀ {R : Type u_1} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  ⇑RingEquiv.prodComm = Prod.swap
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.Swap.equivalence_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Sum.Swap.equivalence C D).functor = CategoryTheory.Sum.swap C D
-- Init.Core
/-- Subset relation: `a ⊆ b`  

Conventions for notations in identifiers:

 * The recommended spelling of `⊆` in identifiers is `subset`. -/
HasSubset.Subset : {α : Type u} → [self : HasSubset α] → α → α → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskeringLeft_preservesColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (J : Type u) [inst_3 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasColimitsOfShape J D] (F : CategoryTheory.Functor C E),
  CategoryTheory.Limits.PreservesColimitsOfShape J ((CategoryTheory.Functor.whiskeringLeft C E D).obj F)
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.IsPointed.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (M : AddSubmonoid G), M.IsPointed = ∀ x ∈ M, -x ∈ M → x = 0
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.prodFan_pt : ∀ (A B : CommRingCat), (A.prodFan B).pt = CommRingCat.of (↑A × ↑B)
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          {P : CategoryTheory.ProjectiveResolution Z} →
            {Z' : C} →
              {P' : CategoryTheory.ProjectiveResolution Z'} →
                {f : Z ⟶ Z'} →
                  (hom : P.complex ⟶ P'.complex) →
                    CategoryTheory.CategoryStruct.comp (hom.f 0) (P'.π.f 0) =
                        CategoryTheory.CategoryStruct.comp (P.π.f 0) (((ChainComplex.single₀ C).map f).f 0) →
                      P.Hom P' f
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Indep.cardinalMk_le_cRk_of_subset : ∀ {α : Type u} {M : Matroid α} {I X : Set α}, M.Indep I → I ⊆ X → Cardinal.mk ↑I ≤ M.cRk X
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.hasForget₂ : (P : TopCat → Prop) → CategoryTheory.HasForget₂ (CompHausLike P) TopCat
-- Mathlib.Tactic.FunProp.ToBatteries
/-- For an element of a product type (of size `n`) `xs` create an array of all possible projections
i.e. `#[xs.1, xs.2.1, xs.2.2.1, ..., xs.2..2]`  -/
Mathlib.Meta.FunProp.mkProdSplitElem : Lean.Expr → ℕ → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zipWith_cons_cons : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {x : α} {s : Stream'.Seq α} {x' : β} {s' : Stream'.Seq β},
  Stream'.Seq.zipWith f (Stream'.Seq.cons x s) (Stream'.Seq.cons x' s') =
    Stream'.Seq.cons (f x x') (Stream'.Seq.zipWith f s s')
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.post_post : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasLimit (F.comp G)] {E : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} E]
  (H : CategoryTheory.Functor D E) [h : CategoryTheory.Limits.HasLimit ((F.comp G).comp H)],
  CategoryTheory.CategoryStruct.comp (H.map (CategoryTheory.Limits.limit.post F G))
      (CategoryTheory.Limits.limit.post (F.comp G) H) =
    CategoryTheory.Limits.limit.post F (G.comp H)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ_three : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ψ 3 = Polynomial.C W.Ψ₃
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.shrink₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsStableUnderTransfiniteComposition], W.IsStableUnderTransfiniteComposition
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.insert_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α} {a : α},
  s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂
-- Aesop.Script.CtorNames
Aesop.CtorNames.toInductionAlt : Aesop.CtorNames → Array Lean.Syntax.Tactic → Lean.TSyntax `Lean.Parser.Tactic.inductionAlt
-- Mathlib.RingTheory.Binomial
Polynomial.ascPochhammer_smeval_cast : ∀ (R : Type u_1) [inst : Semiring R] {S : Type u_2} [inst_1 : NonAssocSemiring S] [inst_2 : Pow S ℕ]
  [inst_3 : Module R S] [IsScalarTower R S S] [NatPowAssoc S] (x : S) (n : ℕ),
  (ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_eq_left_iff : ∀ {x : NNReal} {y : ℝ}, x ^ y = x ↔ x = 1 ∨ y = 1 ∨ x = 0 ∧ y ≠ 0
-- Mathlib.Order.Interval.Finset.Defs
Finset.coe_Iic : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α), ↑(Finset.Iic a) = Set.Iic a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_eq_of_continuous_of_map_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  [ContinuousMap.UniqueHom R A] (φ : C(↑(spectrum R a), R) →⋆ₐ[R] A),
  Continuous ⇑φ → φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a → cfcHom ha = φ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.union.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t₁ t₁_1 : Std.ExtTreeMap α β cmp),
  t₁ = t₁_1 → ∀ (t₂ t₂_1 : Std.ExtTreeMap α β cmp), t₂ = t₂_1 → t₁.union t₂ = t₁_1.union t₂_1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.ofInv_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (s : Y ⟶ X) (hs : W s),
  (CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).f = CategoryTheory.CategoryStruct.id X
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.any_filterMap : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {f : β → Option β'} {p : β' → Bool},
  Std.IterM.any p (Std.IterM.filterMap f it) =
    Std.IterM.any
      (fun x =>
        match f x with
        | some fx => p fx
        | none => false)
      it
-- Aesop.RuleTac.Cases
Aesop.CasesTarget'.patterns : Array (Lean.Expr × Lean.Meta.SavedState) → Aesop.CasesTarget'
-- Mathlib.Data.Set.UnionLift
/-- Glue together functions defined on each of a collection `S` of sets that cover a type. See
also `Set.iUnionLift`.  -/
Set.liftCover : {α : Type u_1} →
  {ι : Sort u_2} →
    {β : Sort u_3} →
      (S : ι → Set α) →
        (f : (i : ι) → ↑(S i) → β) →
          (∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) →
            Set.iUnion S = Set.univ → α → β
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.IterM.forIn_eq_foldM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β}
  {init : γ} {f : β → γ → m (ForInStep γ)},
  forIn it init f =
    ForInStep.value <$>
      Std.Iter.foldM
        (fun c b =>
          match c with
          | ForInStep.yield c => f b c
          | ForInStep.done c => pure (ForInStep.done c))
        (ForInStep.yield init) it
-- Mathlib.Tactic.GCongr.ForwardAttr
_private.Mathlib.Tactic.GCongr.ForwardAttr.0.Mathlib.Tactic.GCongr.mkForwardExt.unsafe_impl_2 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Tactic.GCongr.ForwardExt
-- Init.Data.UInt.Lemmas
USize.add_sub_cancel : ∀ (a b : USize), a + b - b = a
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineSpan_face_le : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1),
  affineSpan k (Set.range (s.face h).points) ≤ affineSpan k (Set.range s.points)
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.lift'_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulZeroOneClass β] {f : α →* β},
  Function.Surjective ⇑f → Function.Surjective ⇑(WithZero.lift' f)
-- Mathlib.Tactic.Linter.Whitespace
/-- `unlintedNodes` contains the `SyntaxNodeKind`s for which there is no clear formatting preference:
if they appear in surface syntax, the linter will ignore formatting.

Currently, the unlined nodes are mostly related to `Subtype`, `Set` and `Finset` notation and
list notation.
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.unlintedNodes : Array Lean.Name
-- Mathlib.Order.Bounds.OrderIso
OrderIso.isLUB_image' : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set α} {x : α},
  IsLUB (⇑f '' s) (f x) ↔ IsLUB s x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s : Finset α} (a : α),
  {a} - s = Finset.image (fun x => a - x) s
-- Lean.Elab.Tactic.Induction
/-- We may have at most one `| _ => ...` (wildcard alternative), and it must not set variable names.
The idea is to make sure users do not write unstructured tactics.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.checkAltsOfOptInductionAlts : Lean.Syntax → Lean.Elab.Tactic.TacticM Unit