mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.isoMk_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (h : A₀.a ≅ A₁.a)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map h.hom) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str h.hom)
      CategoryTheory.Endofunctor.Algebra.isoMk._auto_1),
  (CategoryTheory.Endofunctor.Algebra.isoMk h w).hom.f = h.hom
-- Mathlib.Analysis.LocallyConvex.WeakSpace
/-- If `e : E →ₗ[𝕜] F` is a linear map between locally convex spaces, and `f ∘ e` is continuous
for every continuous linear functional `f : StrongDual 𝕜 F`, then `e` commutes with the closure on
convex sets.  -/
LinearMap.image_closure_of_convex : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : Module ℝ E] [IsScalarTower ℝ 𝕜 E] [inst_7 : Module ℝ F]
  [IsScalarTower ℝ 𝕜 F] [inst_9 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] [inst_13 : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F]
  [LocallyConvexSpace ℝ F] {s : Set E},
  Convex ℝ s →
    ∀ (e : E →ₗ[𝕜] F), (∀ (f : StrongDual 𝕜 F), Continuous ⇑(e.dualMap ↑f)) → ⇑e '' closure s ⊆ closure (⇑e '' s)
-- Mathlib.Data.Part
Part.dom_iff_mem : ∀ {α : Type u_1} {o : Part α}, o.Dom ↔ ∃ y, y ∈ o
-- Mathlib.Data.List.Basic
List.reverse_cons' : ∀ {α : Type u} (a : α) (l : List α), (a :: l).reverse = l.reverse.concat a
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α} {f : β → β},
  (m.modify k f).getKey! k = if k ∈ m then k else default
-- Mathlib.Topology.Algebra.Monoid
continuous_list_sum : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddMonoid M] [ContinuousAdd M] {f : ι → X → M} (l : List ι),
  (∀ i ∈ l, Continuous (f i)) → Continuous fun a => (List.map (fun i => f i a) l).sum
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDecl.mk.injEq : ∀ (declName : Lean.Name) (keys : Array Lean.Meta.SimpTheoremKey) (declName_1 : Lean.Name)
  (keys_1 : Array Lean.Meta.SimpTheoremKey),
  ({ declName := declName, keys := keys } = { declName := declName_1, keys := keys_1 }) =
    (declName = declName_1 ∧ keys = keys_1)
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_ne_zero_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α}, lcm a b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
/-- **Alias** of `AddTorsor.sConvexComb_eq_affineCombination`.

---

`ConvexSpace.sConvexComb` in an affine space is the affine combination.  -/
AddTorsor.convexCombination_eq_affineCombination : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (s : Convexity.StdSimplex R P), Convexity.sConvexComb s = (Finset.affineCombination R s.weights.support id) ⇑s.weights
-- Mathlib.Analysis.Normed.Field.Lemmas
Filter.map_mul_right_cobounded : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {a : α},
  a ≠ 0 → Filter.map (fun x => x * a) (Bornology.cobounded α) = Bornology.cobounded α
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.mul_assoc : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop}
  (x y z : MonCat.Colimits.Prequotient F), MonCat.Colimits.Relation.below ⋯
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_subset_Iic_union_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iic b ⊆ Set.Iic a ∪ Set.Icc a b
-- Mathlib.Topology.Algebra.Ring.Basic
IsSemitopologicalRing.toIsSemitopologicalSemiring : ∀ {R : Type u_2} {inst : TopologicalSpace R} {inst_1 : NonUnitalNonAssocRing R} [self : IsSemitopologicalRing R],
  IsSemitopologicalSemiring R
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommMonoidWithOneOfAddMonoidHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → AddCommMonoidWithOne (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] →
                      AddCommMonoidWithOne (DirectLimit G f)
-- Mathlib.CategoryTheory.Action.Basic
Action.inhabited' : (G : Type u_2) → [inst : Monoid G] → Inhabited (Action (Type u_3) G)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_comp_one_sub_X : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R),
  Polynomial.derivative (p.comp (1 - Polynomial.X)) = -(Polynomial.derivative p).comp (1 - Polynomial.X)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
      (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
        (F.mapComp' f₀₁ f₁₃ f ⋯).inv)
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instIteratorIdSearchStepOfForwardPattern.match_3.eq_2 : ∀ {ρ : Type} (pat : ρ) (s : String.Slice) (it : Std.IterM Id (String.Slice.Pattern.SearchStep s))
  (motive : Option (s.sliceFrom it.internalState.currPos).Pos → Sort u_1)
  (h_1 : (pos : (s.sliceFrom it.internalState.currPos).Pos) → none = some pos → motive (some pos))
  (h_2 : none = none → motive none),
  (match h' : none with
    | some pos => h_1 pos h'
    | none => h_2 h') =
    h_2 ⋯
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.bot_coe : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], ↑⊥ = {0}
-- Init.Data.BitVec.Lemmas
BitVec.append_def : ∀ {v w : ℕ} (x : BitVec v) (y : BitVec w), x ++ y = x.shiftLeftZeroExtend w ||| BitVec.setWidth' ⋯ y
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instIsIsoInvApp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace),
  CategoryTheory.IsIso (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f U)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The setoid on `R × S` used for the Ore localization.  -/
AddOreLocalization.oreEqv : {R : Type u_1} →
  [inst : AddMonoid R] →
    (S : AddSubmonoid R) → [AddOreLocalization.AddOreSet S] → (X : Type u_2) → [AddAction R X] → Setoid (X × ↥S)
-- Std.Time.DateTime.WallTime
Std.Time.instReprWallTime.repr : Std.Time.WallTime → ℕ → Std.Format
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
UpgradedStandardBorel.toTopologicalSpace : {α : Type u_1} → [self : UpgradedStandardBorel α] → TopologicalSpace α
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instRankFiniteMapEmbedding : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RankFinite] {f : α ↪ β}, (M.mapEmbedding f).RankFinite
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.tensorKaehlerEquivBase.congr_simp : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [h : Algebra.IsPushout R S A B],
  KaehlerDifferential.tensorKaehlerEquivBase R S A B = KaehlerDifferential.tensorKaehlerEquivBase R S A B
-- Init.Data.Order.PackageFactories
Std.LinearPreorderPackage.toLawfulOrderOrd : ∀ {α : Type u} [self : Std.LinearPreorderPackage α], Std.LawfulOrderOrd α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k km : α} (hc : k ∈ t), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.NumberTheory.ModularForms.LFunction
/-- Shared Dirichlet-series summability argument for modular and cusp forms.  -/
_private.Mathlib.NumberTheory.ModularForms.LFunction.0.ModularForm.hasSum_Λ_of_qExpansion_isBigO : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [inst_2 : ModularFormClass F Γ k] {r : ℝ},
  0 < s.re →
    r + 1 < s.re →
      ModularForm.Λ hk f s = mellin (fun t => (ModularForm.weakFEPair hk f).f t - (ModularForm.weakFEPair hk f).f₀) s →
        ((fun n => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) =O[Filter.atTop] fun n =>
            ↑n ^ r) →
          HasSum
            (fun n =>
              ↑Real.pi ^ (-s) * Complex.Gamma s *
                  (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) /
                ↑(2 * ↑n / Γ.strictWidthInfty) ^ s)
            (ModularForm.Λ hk f s)
-- Mathlib.Data.ENNReal.Action
ENNReal.instSMulPosMonoNNReal : SMulPosMono NNReal ENNReal
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabel.parts : Array Lean.Lsp.InlayHintLabelPart → Lean.Lsp.InlayHintLabel
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isNatValueTransition : Lean.Meta.Match.Problem → Lean.MetaM Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l →
          ∀ {h : k' ∈ Std.DHashMap.Raw.Const.ofList l},
            Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.Const.ofList l) k' h = v
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_iSup_prop : ∀ {M : Type u_1} [inst : MulOneClass M] {p : Prop} {S : p → Submonoid M} {x : M},
  x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
-- Mathlib.CategoryTheory.Presentable.Dense
CategoryTheory.IsCardinalAccessibleCategory.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ κ_1 : Cardinal.{w}) (e_κ : κ = κ_1)
  [inst_1 : Fact κ.IsRegular],
  CategoryTheory.IsCardinalAccessibleCategory C κ = CategoryTheory.IsCardinalAccessibleCategory C κ_1
-- Lean.Meta.ArgsPacker
/-- Given type `(x : a ⊗' b ⊕' c ⊗' d) → R` (dependent), return types
```
#[(x: a) → (y : b) → R, (x : c) → (y : d) → R]
```
 -/
Lean.Meta.ArgsPacker.curryType : Lean.Meta.ArgsPacker → Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.perm_symm_mapsTo_of_mapsTo : ∀ {α : Type u} (f : Equiv.Perm α) {s : Set α} [Finite ↑s], Set.MapsTo (⇑f) s s → Set.MapsTo (⇑(Equiv.symm f)) s s
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.lift_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
  [inst_2 : Fintype J] {f : J → C} [inst_3 : CategoryTheory.Limits.HasBiproduct f] {T U : C} {g : (j : J) → T ⟶ f j}
  {h : (j : J) → f j ⟶ U} {Z : C} (h_1 : U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc h) h_1) =
    CategoryTheory.CategoryStruct.comp (∑ j, CategoryTheory.CategoryStruct.comp (g j) (h j)) h_1
-- Mathlib.Topology.Order.LowerUpperTopology
/-- A recursor for `WithUpper`. Use as `induction x`.  -/
Topology.WithUpper.rec : {α : Type u_1} →
  {motive : Topology.WithUpper α → Sort u_3} →
    ((a : α) → motive (Topology.WithUpper.toUpper a)) → (a : Topology.WithUpper α) → motive a
-- Mathlib.Analysis.Normed.Ring.Int
Int.nnnorm_natCast : ∀ (n : ℕ), ‖↑n‖₊ = ↑n
-- Mathlib.Topology.ClusterPt
clusterPt_iff_lift'_closure' : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, ClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot
-- Mathlib.Analysis.Normed.Group.Basic
indiscreteTopology_iff_forall_norm_eq_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_neq_empty : ∀ (α : Type u_4) [inst : Fintype α] [Nonempty α], Finset.univ ≠ ∅
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.descentData_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (D : F.DescentData' sq sq₃) (i : ι), D.descentData.obj i = D.obj i
-- Mathlib.Tactic.CongrExclamation
/-- Like `implies_congr` but provides an additional assumption to the second hypothesis.
This is a non-dependent version of `pi_congr` that allows the domains to be different.  -/
_private.Mathlib.Tactic.CongrExclamation.0.implies_congr' : ∀ {α α' : Sort u} {β β' : Sort v}, α = α' → (∀ (a : α'), β = β') → (α → β) = (α' → β')
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.coatomic_of_top_compact : ∀ {α : Type u_2} [inst : CompleteLattice α], IsCompactElement ⊤ → IsCoatomic α
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.isRoot_prod : ∀ {R : Type u_2} [inst : CommSemiring R] [IsDomain R] {ι : Type u_1} (s : Finset ι) (p : ι → Polynomial R) (x : R),
  (∏ j ∈ s, p j).IsRoot x ↔ ∃ i ∈ s, (p i).IsRoot x
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.mk.injEq : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (map : SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
  (δ_castSucc_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map = g.map)
      SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam)
  (δ_succ_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map = fg.map)
      SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam)
  (δ_succ_succ_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map = f.map)
      SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam)
  (δ_map_of_lt :
    autoParam (∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam)
  (δ_map_of_gt :
    autoParam
      (∀ (j : Fin (n + 2)),
        i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam)
  (map_1 : SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
  (δ_castSucc_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map_1 = g.map)
      SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam)
  (δ_succ_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map_1 = fg.map)
      SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam)
  (δ_succ_succ_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map_1 = f.map)
      SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam)
  (δ_map_of_lt_1 :
    autoParam (∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam)
  (δ_map_of_gt_1 :
    autoParam
      (∀ (j : Fin (n + 2)),
        i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam),
  ({ map := map, δ_castSucc_castSucc_map := δ_castSucc_castSucc_map, δ_succ_castSucc_map := δ_succ_castSucc_map,
        δ_succ_succ_map := δ_succ_succ_map, δ_map_of_lt := δ_map_of_lt, δ_map_of_gt := δ_map_of_gt } =
      { map := map_1, δ_castSucc_castSucc_map := δ_castSucc_castSucc_map_1,
        δ_succ_castSucc_map := δ_succ_castSucc_map_1, δ_succ_succ_map := δ_succ_succ_map_1,
        δ_map_of_lt := δ_map_of_lt_1, δ_map_of_gt := δ_map_of_gt_1 }) =
    (map = map_1)
-- Init.Control.Lawful.Instances
EStateM.run_modifyGet : ∀ {σ α ε : Type u_1} (f : σ → α × σ) (s : σ), (modifyGet f).run s = EStateM.Result.ok (f s).1 (f s).2
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → Bool} {k fallback : α},
  t.WF → (Std.DTreeMap.Raw.filter (fun k x => f k) t).getKeyD k fallback = (Option.filter f (t.getKey? k)).getD fallback
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.base_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g : X ⟶ Y} (α : CategoryTheory.CatEnrichedOrdinary.homEquiv f ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv g),
  CategoryTheory.CatEnrichedOrdinary.Hom.base (CategoryTheory.CatEnrichedOrdinary.Hom.mk α) = α
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_apply : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V) (s : Set X),
  μ.variation s = (MeasureTheory.preVariation (fun x => ‖μ x‖ₑ) ⋯ ⋯) s
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- the cochain complex involved in the resolution  -/
CategoryTheory.InjectiveResolution.cocomplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} → CategoryTheory.InjectiveResolution Z → CochainComplex C ℕ
-- Mathlib.FieldTheory.Relrank
IntermediateField.inf_relrank_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E),
  (A ⊓ B).relrank B = A.relrank B
-- Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory
/-- `QCat` obtains a `Cat`-enriched ordinary category structure by applying `hoFunctor` to the
hom objects in its `SSet`-enriched ordinary structure.  -/
SSet.QCat.catEnrichedOrdinaryCategory : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat SSet.QCat
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- **Alias** of `CategoryTheory.PreZeroHypercover.comp_h₀`. -/
AlgebraicGeometry.Scheme.Cover.comp_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y Z : CategoryTheory.PreZeroHypercover S}
  (f : X.Hom Y) (g : Y.Hom Z) (i : X.I₀),
  (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.fold_filterMap : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : Monad m] [inst_3 : Std.Internal.Do.Assertion Pred] [inst_4 : Std.Internal.Do.Assertion EPred]
  [inst_5 : Std.Internal.Do.WPMonad m Pred EPred] [inst_6 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m]
  {f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.fold
        (fun d b =>
          match f b with
          | some c => g d c
          | x => d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.IterM.filterMap f it) ⦃ Q; eQ ⦄
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.instOneTermRing : (α : Type u_2) → One (FirstOrder.Language.ring.Term α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  {f : (a : α) → β a → Bool} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl = true →
    Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.Data.Ordmap.Ordset
Ordnode.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Ordnode.map f Ordnode.nil = Ordnode.nil
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- If `v` is an injective family of vectors such that `f ∘ v` is linearly independent, then `v`
    spans a submodule disjoint from the kernel of `f`.
TODO : `LinearIndepOn` version.  -/
Submodule.range_ker_disjoint : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] {f : M →ₗ[R] M'},
  LinearIndependent R (⇑f ∘ v) → Disjoint (Submodule.span R (Set.range v)) f.ker
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.evaluation_obj : ∀ (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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (a : A) (F : CategoryTheory.SingleFunctors C D A),
  (CategoryTheory.SingleFunctors.evaluation C D a).obj F = F.functor a
-- Mathlib.Data.Set.Card
Set.exists_eq_insert_iff_ncard : ∀ {α : Type u_1} {s t : Set α},
  autoParam s.Finite Set.exists_eq_insert_iff_ncard._auto_1 →
    ((∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.of_forall_get?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ (k : α), t₁.get? k = t₂.get? k) → t₁.Equiv t₂
-- Mathlib.RingTheory.Ideal.Basic
Ideal.instIsTwoSidedForallPi : ∀ {ι : Type u_1} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] (I : (i : ι) → Ideal (R i))
  [∀ (i : ι), (I i).IsTwoSided], (Ideal.pi I).IsTwoSided
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_empty : ∀ {α : Type u_1} [inst : EDist α], ∅.einfsep = ⊤
-- Mathlib.Order.PFilter
Order.PFilter.mk.sizeOf_spec : ∀ {P : Type u_1} [inst : Preorder P] [inst_1 : SizeOf P] (dual : Order.Ideal Pᵒᵈ),
  sizeOf { dual := dual } = 1 + sizeOf dual
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasDerivAt.const_smul` -/
HasDerivAt.fun_const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  HasDerivAt f f' x → HasDerivAt (fun i => c • f i) (c • f') x