mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : Inhabited α] [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey! k = m₂.getKey! k
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.shift_app : ∀ {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} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C),
  (CategoryTheory.shiftFunctor D a).map (τ.app X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).inv.app X)
      (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X))
        ((CategoryTheory.Functor.commShiftIso F₂ a).hom.app X))
-- Init.Data.BitVec.Lemmas
BitVec.toInt_sshiftRight' : ∀ {w : ℕ} {x y : BitVec w}, (x.sshiftRight' y).toInt = x.toInt >>> y.toNat
-- Mathlib.Data.Prod.TProd
List.TProd.elim'.congr_simp : ∀ {ι : Type u} {α : ι → Type v} {l : List ι} {inst : DecidableEq ι} [inst_1 : DecidableEq ι] (h : ∀ (i : ι), i ∈ l)
  (v v_1 : List.TProd α l), v = v_1 → ∀ (i : ι), List.TProd.elim' h v i = List.TProd.elim' h v_1 i
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_id_obj : ∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).obj U = U
-- Mathlib.Tactic.NormNum.Ineq
_private.Mathlib.Tactic.NormNum.Ineq.0.Mathlib.Meta.NormNum.evalLT.core.nnratArm : {u : Lean.Level} →
  {α : Q(Type u)} →
    (lα : Q(LT «$α»)) →
      {a b : Q(«$α»)} →
        Mathlib.Meta.NormNum.Result a →
          Mathlib.Meta.NormNum.Result b →
            have e := q(«$a» < «$b»);
            Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.Analysis.Seminorm
/-- The norm of a seminormed group as a seminorm.  -/
normSeminorm : (𝕜 : Type u_3) →
  (E : Type u_7) →
    [inst : NormedField 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → Seminorm 𝕜 E
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- If a short complex `S` has a splitting and `F` is an additive functor, then
`S.map F` also has a splitting.  -/
CategoryTheory.ShortComplex.Splitting.map : {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] →
            {S : CategoryTheory.ShortComplex C} →
              S.Splitting → (F : CategoryTheory.Functor C D) → [inst_4 : F.Additive] → (S.map F).Splitting
-- Mathlib.Analysis.InnerProductSpace.Reproducing
_private.Mathlib.Analysis.InnerProductSpace.Reproducing.0.RKHS.isSelfAdjoint_finsuppSum : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)},
  K.IsHermitian → ∀ (f : X →₀ V →L[𝕜] V), IsSelfAdjoint (f.sum fun i xi => f.sum fun j xj => star xi * K i j * xj)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM.congr_simp : ∀ (α : Type u_1) (E : Type u_2) {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  {T T_1 : Set α → E →L[ℝ] F} (e_T : T = T_1) {C C_1 : ℝ} (e_C : C = C_1)
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT = MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
deriv_const_rpow_id : ∀ {x a : ℝ}, 0 < a → deriv (fun x => a ^ x) x = Real.log a * a ^ x
-- Mathlib.Topology.Inseparable
specializingMap_iff_isClosed_image_closure_singleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → (SpecializingMap f ↔ ∀ (x : X), IsClosed (f '' closure {x}))
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorHom_def'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X₁ Y₁ X₂ Y₂ : C}
  (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y₂) h)
-- Mathlib.RingTheory.Trace.Basic
Module.Basis.traceDual_traceDual : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] [inst_5 : Finite ι] [inst_6 : DecidableEq ι]
  (b : Module.Basis ι K L), b.traceDual.traceDual = b
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.val.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Meta.Match.Pattern.val e) = 1 + sizeOf e
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.continuous_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α], Continuous fun x => {x}
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
/-- **Alias** of the reverse direction of `MeasureTheory.memLp_prodLp_iff`. -/
MeasureTheory.MemLp.of_fst_of_snd_prodLp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)},
  MeasureTheory.MemLp (fun x => (f x).fst) p μ ∧ MeasureTheory.MemLp (fun x => (f x).snd) p μ →
    MeasureTheory.MemLp f p μ
-- Init.Data.Slice.Array.Lemmas
Subarray.array.eq_1 : ∀ {α : Type u_1} (xs : Subarray α), xs.array = xs.internalRepresentation.array
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry_refl : ∀ {X : Type u_1} [inst : MetricSpace X] (D : Delone.DeloneSet X),
  (Delone.DeloneSet.mapIsometry (IsometryEquiv.refl X)) D = D
-- Mathlib.Algebra.Group.Center
Set.inv_mem_center : ∀ {M : Type u_1} [inst : DivisionMonoid M] {a : M}, a ∈ Set.center M → a⁻¹ ∈ Set.center M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_add_le : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  (a b : R), ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isOpenPosMeasure : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → TopologicalSpace (α i)] [∀ (i : ι), (μ i).IsOpenPosMeasure],
  (MeasureTheory.Measure.pi μ).IsOpenPosMeasure
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.indicator_of_notMem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : Zero R] {U : Set X} (f : LocallyConstant X R)
  {a : X} (hU : IsClopen U), a ∉ U → (f.indicator hU) a = 0
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The diagram of the multiforks attached to `data : F.PreOneHypercoverDenseData X`.  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {A : Type u'} →
            [inst_2 : CategoryTheory.Category.{v', u'} A] →
              {X : C} →
                (data : F.PreOneHypercoverDenseData X) →
                  CategoryTheory.Functor C₀ᵒᵖ A → CategoryTheory.Limits.MulticospanIndex data.multicospanShape A
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterM.match_1.eq_2 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (ULift.{u_1, 0} Bool)} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (hf : MonadAttach.CanReturn (f out) { down := true })
  (h_1 : (hf : MonadAttach.CanReturn (f out) { down := false }) → motive ⟨{ down := false }, hf⟩)
  (h_2 : (hf : MonadAttach.CanReturn (f out) { down := true }) → motive ⟨{ down := true }, hf⟩),
  (match ⟨{ down := true }, hf⟩ with
    | ⟨{ down := false }, hf⟩ => h_1 hf
    | ⟨{ down := true }, hf⟩ => h_2 hf) =
    h_2 hf
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_functor_map_toFun : ∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), (Bipointed.swapEquiv.functor.map f).toFun a = f.toFun a
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compChangeOfVariables_blocksFun : ∀ (m M N : ℕ) {i : (n : ℕ) × (Fin n → ℕ)} (hi : i ∈ FormalMultilinearSeries.compPartialSumSource m M N) (j : Fin i.fst),
  (FormalMultilinearSeries.compChangeOfVariables m M N i hi).snd.blocksFun ⟨↑j, ⋯⟩ = i.snd j
-- Mathlib.Data.Set.Finite.Basic
Set.infinite_of_finite_compl : ∀ {α : Type u} [Infinite α] {s : Set α}, sᶜ.Finite → s.Infinite
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.greatestFib.eq_1 : ∀ (n : ℕ), n.greatestFib = Nat.findGreatest (fun k => Nat.fib k ≤ n) (n + 1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.deriv_arccos : deriv Real.arccos = fun x => -(1 / √(1 - x ^ 2))
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instNonUnitalRing : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalRing A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : NonUnitalSemiring B] →
                  [inst_6 : Module R B] →
                    [SMulCommClass R B B] → [IsScalarTower R B B] → NonUnitalRing (TensorProduct R A B)
-- Mathlib.Order.Interval.Set.SurjOn
surjOn_Icc_of_monotone_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Surjective f → ∀ {a b : α}, a ≤ b → Set.SurjOn f (Set.Icc a b) (Set.Icc (f a) (f b))
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.zero_posPart : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasureTheory.JordanDecomposition.posPart 0 = 0
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.Hom.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {V W : QuadraticModuleCat R} (toIsometry' toIsometry'_1 : V.form →qᵢ W.form),
  ({ toIsometry' := toIsometry' } = { toIsometry' := toIsometry'_1 }) = (toIsometry' = toIsometry'_1)
-- Mathlib.Topology.Constructions
MapClusterPt.prodMap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {α : Type u_5} {β : Type u_6}
  {f : α → X} {g : β → Y} {la : Filter α} {lb : Filter β} {x : X} {y : Y},
  MapClusterPt x la f → MapClusterPt y lb g → MapClusterPt (x, y) (la ×ˢ lb) (Prod.map f g)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.zero_ult' : ∀ {w : ℕ} (a : BitVec w), (0#w).ult a = !a == 0#w
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The group associated to a split extension is isomorphic to a semidirect product.  -/
GroupExtension.Splitting.semidirectProductMulEquiv : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] →
      [inst_1 : Group G] →
        {E : Type u_3} → [inst_2 : Group E] → {S : GroupExtension N E G} → (s : S.Splitting) → N ⋊[s.conjAct] G ≃* E
-- Mathlib.Algebra.Group.Defs
neg_add_cancel_comm_assoc : ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + (b + a) = b
-- Mathlib.Data.Set.Countable
/-- **Alias** of `Set.countable_ofPred_finite_subset`.

---

The set of finite subsets of a countable set is countable.  -/
Set.countable_setOf_finite_subset : ∀ {α : Type u} {s : Set α}, s.Countable → {t | t.Finite ∧ t ⊆ s}.Countable
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.μ_def : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] (i : I) (X Y : (i : I) → C i),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Pi.eval C i) X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (X i) (Y i))
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.filtered_colim_preservesFiniteLimits_of_types : ∀ {K : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} K] [inst_1 : Small.{v, u₂} K] [CategoryTheory.IsFiltered K],
  CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_restrictScalars : ∀ (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂),
  ⇑(↑R f) = ⇑f
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mono_set : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b c d : ℝ}
  {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f μ a b → Set.uIcc c d ⊆ Set.uIcc a b → IntervalIntegrable f μ c d
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_ite_compl`. -/
Set.restrict_ite_compl : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [inst : (x : α) → Decidable (x ∈ s)],
  (sᶜ.domRestrict fun a => if a ∈ s then f a else g a) = sᶜ.domRestrict g
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D] (L : CategoryTheory.Functor C₂ D) [inst_3 : L.IsLocalization W₂]
  {X₂ : C₂} {X₃ : D} (y : L.obj X₂ ⟶ X₃) {R R' : Φ.RightResolution X₂} (φ : R ⟶ R'),
  (CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution Φ L y).map φ =
    CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.homMk φ.f ⋯) ⋯
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_eval_eq_descFactorial : ∀ (R : Type u) [inst : Ring R] (n k : ℕ), Polynomial.eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
-- Mathlib.SetTheory.Ordinal.Notation
/-- `NFBelow o b` says that `o` is a normal form ordinal notation satisfying `repr o < ω ^ b`.  -/
ONote.NFBelow : ONote → Ordinal.{0} → Prop
-- Mathlib.Algebra.Group.Units.Defs
/-- Units have decidable equality if the base `Monoid` has decidable equality.  -/
Units.instDecidableEq : {α : Type u} → [inst : Monoid α] → [DecidableEq α] → DecidableEq αˣ
-- Plausible.Testable
_private.Plausible.Testable.0.Plausible.instEvalExprConfiguration.evalExpr : Lean.Expr → Lean.MetaM Plausible.Configuration
-- Mathlib.Algebra.Group.Hom.Defs
/-- `OneHomClass F M N` states that `F` is a type of one-preserving homomorphisms.
You should extend this typeclass when you extend `OneHom`.
 -/
OneHomClass : (F : Type u_10) → (M : outParam (Type u_11)) → (N : outParam (Type u_12)) → [One M] → [One N] → [FunLike F M N] → Prop
-- Std.Do.PostCond
/-- Conjunction of postconditions.

This is defined pointwise, as the conjunction of the assertions about the return value and the
conjunctions of the assertions about each potential exception.
 -/
Std.Do.«term_∧ₚ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Separation.Basic
R0Space.closure_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R0Space X] (x : X), closure {x} = (nhds x).ker
-- Mathlib.Data.Fin.Basic
Fin.val_natCast : ∀ (a n : ℕ) [inst : NeZero n], ↑↑a = a % n
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.coe_id : ∀ {M : Type u_10} [inst : One M], ⇑(OneHom.id M) = id
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Helper function for reducing `x <<< i` and `x >>> i` where `i` is a bitvector literal,
into one that is a natural number literal.
 -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.reduceShiftWithBitVecLit : Lean.Name → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α] {l : List α} {k : α},
  l.contains k = false → (Std.DHashMap.Const.unitOfList l).getKey! k = default
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.D₁.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
  [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] (j j' : ι₄),
  HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' =
    HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j'
-- Mathlib.Order.SupIndep
Finset.SupIndep.le_sup_iff : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s t : Finset ι} {f : ι → α} {i : ι},
  s.SupIndep f → t ⊆ s → i ∈ s → (∀ (i : ι), f i ≠ ⊥) → (f i ≤ t.sup f ↔ i ∈ t)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.isValidForSlice : ∀ {pat s : String.Slice},
  pat.isEmpty = false →
    ∀ {pos : String.Pos.Raw},
      String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat.copy.toByteArray s.copy.toByteArray
          pat.utf8ByteSize pos.byteIdx →
        String.Pos.Raw.IsValidForSlice s (pos.unoffsetBy pat.rawEndPos) → String.Pos.Raw.IsValidForSlice s pos
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- Category structure on `Hom a b`. In this file, we will use `Hom a b` for `a b : B`
(precisely, `FreeBicategory.Hom a b`) instead of the definitionally equal expression
`a ⟶ b` for `a b : FreeBicategory B`. The main reason is that we have to annoyingly write
`@Quiver.Hom (FreeBicategory B) _ a b` to get the latter expression when given `a b : B`.  -/
CategoryTheory.FreeBicategory.homCategory' : {B : Type u} →
  [inst : Quiver B] → (a b : B) → CategoryTheory.Category.{max u v, max u v} (CategoryTheory.FreeBicategory.Hom a b)
-- Init.Data.UInt.Lemmas
UInt32.mul_def : ∀ (a b : UInt32), a * b = { toBitVec := a.toBitVec * b.toBitVec }
-- Init.Data.List.Find
List.findIdx_map : ∀ {α : Type u_1} {β : Type u_2} (xs : List α) (f : α → β) (p : β → Bool),
  List.findIdx p (List.map f xs) = List.findIdx (p ∘ f) xs
-- Batteries.Data.UnionFind.Basic
_private.Batteries.Data.UnionFind.Basic.0.Batteries.UnionFind.findAux.match_1.splitter : (self : Batteries.UnionFind) →
  (motive : Batteries.UnionFind.FindAux self.size → Sort u_1) →
    (x : Batteries.UnionFind.FindAux self.size) →
      ((arr₁ : Array Batteries.UFNode) →
          (root : Fin self.size) → (H : arr₁.size = self.size) → motive { s := arr₁, root := root, size_eq := H }) →
        motive x
-- Lean.Util.MonadCache
/-- Similar to `MonadCacheT`, but using `StateT` instead of `StateRefT`  -/
Lean.MonadStateCacheT : (α : Type) → Type → (Type → Type) → [BEq α] → [Hashable α] → Type → Type
-- Mathlib.Algebra.Group.Subsemigroup.Basic
MulHom.coe_ofDense : ∀ {M : Type u_1} {N : Type u_2} [inst : Semigroup M] [inst_1 : Semigroup N] {s : Set M} (f : M → N)
  (hs : Subsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y), ⇑(MulHom.ofDense f hs hmul) = f
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.w_mk_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y X' Y' : T} {f : X ⟶ Y} {g : X' ⟶ Y'}
  (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {Z : T} (h : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
-- Mathlib.GroupTheory.MonoidLocalization.DivPairs
Submonoid.mem_divPairs : ∀ {M : Type u_1} {G : Type u_2} [inst : CommMonoid M] [inst_1 : CommGroup G] {f : ⊤.LocalizationMap G} {s : Submonoid G}
  {x : M × M}, x ∈ Submonoid.divPairs f s ↔ f x.1 / f x.2 ∈ s
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.indexingMode? : Aesop.RuleBuilderOptions → Option Aesop.IndexingMode
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.coeFn_def : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω), ⇑μ = fun s => (↑μ s).toNNReal
-- Mathlib.Algebra.Group.Units.Defs
Units.inv_mul_of_eq : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, ↑u = a → ↑u⁻¹ * a = 1
-- Mathlib.Algebra.Order.Nonneg.Module
Nonneg.mk_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : SMul R S] (a : R) (ha : 0 ≤ a)
  (x : S), ⟨a, ha⟩ • x = a • x
-- Mathlib.Data.Set.Image
Set.preimage_singleton_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {y : β}, f ⁻¹' {y} = ∅ ↔ y ∉ Set.range f
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.ofIsoWeakLimit_lift : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F}
  (P : CategoryTheory.Limits.IsWeakLimit r) (i : r ≅ t) (s : CategoryTheory.Limits.Cone F),
  (P.ofIsoWeakLimit i).lift s = CategoryTheory.CategoryStruct.comp (P.lift s) i.hom.hom
-- Mathlib.Order.Atoms
Set.isSimpleOrder_Iic_iff_isAtom : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsSimpleOrder ↑(Set.Iic a) ↔ IsAtom a