mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
mdifferentiableAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : M → M') (x : M),
  MDiffAt f x ↔
    ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (Set.range ↑I) (↑(extChartAt I x) x)
-- Init.Data.Nat.Lemmas
Nat.one_pow : ∀ (n : ℕ), 1 ^ n = 1
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- The difference of two Hurwitz zeta functions is differentiable everywhere.  -/
HurwitzZeta.differentiable_hurwitzZeta_sub_hurwitzZeta : ∀ (a b : UnitAddCircle), Differentiable ℂ fun s => HurwitzZeta.hurwitzZeta a s - HurwitzZeta.hurwitzZeta b s
-- Init.Data.Option.Lemmas
Option.all_true : ∀ {α : Type u_1} {o : Option α}, Option.all (fun x => true) o = true
-- Mathlib.CategoryTheory.Adjunction.Restrict
CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'}
  {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful)
  (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) (X : C),
  iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X) =
    CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X))
      (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (comm2.hom.app (L.obj X)))
-- Std.Data.TreeMap.Raw.Lemmas
/-- Variant of `getElem_map` that holds without `LawfulEqCmp`.  -/
Std.TreeMap.Raw.getElem_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.TreeMap.Raw.map f t} (h : t.WF),
  (Std.TreeMap.Raw.map f t)[k] = f (t.getKey k ⋯) t[k]
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.toPerfPair_flip_conj_coreflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  P.flip.toPerfPair.conj ↑(P.coreflection i) = (↑(P.reflection i)).dualMap
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (n : ℤ) [K.IsStrictlyGE (n + 1)]
  [L.IsStrictlyGE n],
  (CochainComplex.mappingCone (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K)) ⊞ L).IsStrictlyGE n
-- Mathlib.Data.Fin.VecNotation
_private.Mathlib.Data.Fin.VecNotation.0.PiFin.mkLiteralQ.loop.eq_def : ∀ {u : Lean.Level} {α : Q(Type u)} {n : ℕ} (elems : Fin n → Q(«$α»)) (i : ℕ) (rest : Q(Fin «$i» → «$α»)),
  PiFin.mkLiteralQ.loop✝ elems i rest =
    if h : i < n then
      PiFin.mkLiteralQ.loop✝ elems (i + 1)
        (have a := elems ⟨i, h⟩.rev;
        q(Matrix.vecCons «$a» «$rest»))
    else rest
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.alt.congr_simp : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} (m m_1 : ι → M) (e_m : m = m_1) (i i_1 : ι) (e_i : i = i_1) (j j_1 : ι)
  (e_j : j = j_1) (hm : m i = m j) (hij : i ≠ j),
  exteriorPower.presentation.Rels.alt m i j hm hij = exteriorPower.presentation.Rels.alt m_1 i_1 j_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The inclusion into the second summand of a binary biproduct.  -/
CategoryTheory.Limits.biprod.inr : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → Y ⟶ X ⊞ Y
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.forget₂_map_pushforward_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) {U V : Cᵒᵖ} (f : U ⟶ V) (M : PresheafOfModules R),
  (CategoryTheory.forget₂ (ModuleCat ↑(S.obj U)) Ab).map (((PresheafOfModules.pushforward φ).obj M).map f) =
    M.presheaf.map (F.map f.unop).op
-- Mathlib.Data.Matrix.Basis
LinearEquiv.congrLeft.eq_1 : ∀ (M : Type u_5) {M₂ : Type u_7} {M₃ : Type u_8} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] {R : Type u_9} (S : Type u_10) [inst_3 : Semiring R] [inst_4 : Semiring S]
  [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : Module R M] [inst_8 : Module S M]
  [inst_9 : SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃),
  LinearEquiv.congrLeft M S e =
    { toFun := (e.arrowCongrAddEquiv (LinearEquiv.refl R M)).toFun, map_add' := ⋯, map_smul' := ⋯,
      invFun := (e.arrowCongrAddEquiv (LinearEquiv.refl R M)).invFun, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.Icc_sdiff_left`. -/
Set.Icc_diff_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Icc a b \ {a} = Set.Ioc a b
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Expr.toPoly.go.match_1.splitter : (motive : Nat.Internal.Linear.Expr → Sort u_1) →
  (x : Nat.Internal.Linear.Expr) →
    ((k : ℕ) → motive (Nat.Internal.Linear.Expr.num k)) →
      ((i : Nat.Internal.Linear.Var) → motive (Nat.Internal.Linear.Expr.var i)) →
        ((a b : Nat.Internal.Linear.Expr) → motive (a.add b)) →
          ((k : ℕ) → (a : Nat.Internal.Linear.Expr) → motive (Nat.Internal.Linear.Expr.mulL k a)) →
            ((a : Nat.Internal.Linear.Expr) → (k : ℕ) → motive (a.mulR k)) → motive x
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂ : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ}
  (s :
    CategoryTheory.Limits.Cone
      ((CategoryTheory.StructuredArrow.proj (Opposite.op { len := n }) (SimplexCategory.Truncated.inclusion 2).op).comp
        ((SimplexCategory.Truncated.inclusion 2).op.comp X)))
  (x : s.pt) (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op))
      (SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift sx s x) =
    (CategoryTheory.ConcreteCategory.hom
        (s.π.app
          (SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂ (SimplexCategory.mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij)
            SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁._proof_1)))
      x
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.SameCycle.cycleOf_apply : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [inst : DecidableRel f.SameCycle], f.SameCycle x y → (f.cycleOf x) y = f y
-- Mathlib.Topology.Homotopy.Basic
/-- Given `ContinuousMap.Homotopy f₀ f₁` and `ContinuousMap.Homotopy f₁ f₂`, we can define a
`ContinuousMap.Homotopy f₀ f₂` by putting the first homotopy on `[0, 1/2]` and the second
on `[1/2, 1]`.
 -/
ContinuousMap.Homotopy.trans : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f₀ f₁ f₂ : C(X, Y)} → f₀.Homotopy f₁ → f₁.Homotopy f₂ → f₀.Homotopy f₂
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?_eq_getEntryGE?ₘ' : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGE? k t = Std.DTreeMap.Internal.Impl.getEntryGE?ₘ' k t
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.isCyclic_units_iff_of_odd : ∀ {n : ℕ}, Odd n → (IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m)
-- Mathlib.Order.Shrink
instSuccOrderShrink.eq_1 : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] [inst_2 : SuccOrder α],
  instSuccOrderShrink = SuccOrder.ofOrderIso (orderIsoShrink α)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.orelse.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.instInhabitedState.default : Lean.ParseImports.State
-- Mathlib.Data.Finset.Sups
Finset.image_subset_sups_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α} {b : α},
  b ∈ t → Finset.image (fun x => x ⊔ b) s ⊆ s ⊻ t
-- Aesop.Script.TacticState
Aesop.Script.TacticState.mk.inj : ∀ {visibleGoals : Array Aesop.GoalWithMVars} {invisibleGoals : Std.HashSet Lean.MVarId}
  {visibleGoals_1 : Array Aesop.GoalWithMVars} {invisibleGoals_1 : Std.HashSet Lean.MVarId},
  { visibleGoals := visibleGoals, invisibleGoals := invisibleGoals } =
      { visibleGoals := visibleGoals_1, invisibleGoals := invisibleGoals_1 } →
    visibleGoals = visibleGoals_1 ∧ invisibleGoals = invisibleGoals_1
-- Mathlib.Probability.ProbabilityMassFunction.Binomial
PMF.binomial_apply_last : ∀ (p : NNReal) (h : p ≤ 1) (n : ℕ), (PMF.binomial p h n) (Fin.last n) = ↑p ^ n
-- Mathlib.Data.ZMod.QuotientGroup
/-- The quotient `(ℤ ∙ a) ⧸ (stabilizer b)` is cyclic of order `minimalPeriod (a +ᵥ ·) b`.  -/
AddAction.zmultiplesQuotientStabilizerEquiv : {α : Type u_3} →
  {β : Type u_4} →
    [inst : AddGroup α] →
      (a : α) →
        [inst_1 : AddAction α β] →
          (b : β) →
            ↥(AddSubgroup.zmultiples a) ⧸ AddAction.stabilizer (↥(AddSubgroup.zmultiples a)) b ≃+
              ZMod (Function.minimalPeriod (fun x => a +ᵥ x) b)
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- An operator is positive iff it is self-adjoint and `0 ≤ ⟪T x, x⟫`.

For the version with `IsSymmetric` instead of `IsSelfAdjoint`, see
`ContinuousLinearMap.isPositive_iff`.  -/
ContinuousLinearMap.isPositive_iff' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (T : E →L[𝕜] E), T.IsPositive ↔ IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ inner 𝕜 (T x) x
-- Mathlib.Algebra.Algebra.Operations
Submodule.instAddCommMonoidWithOne : {R : Type u} →
  [inst : Semiring R] →
    {A : Type v} → [inst_1 : Semiring A] → [inst_2 : Module R A] → AddCommMonoidWithOne (Submodule R A)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_trans : ∀ {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module S M] [inst_7 : Module S N] [inst_8 : LinearMap.CompatibleSMul M N R S] {T : Type u_20}
  [inst_9 : Semiring T] [inst_10 : Module T M] [inst_11 : Module T N] [inst_12 : LinearMap.CompatibleSMul M N S T]
  [inst_13 : LinearMap.CompatibleSMul M N R T] (f : M →ₗ[T] N), ↑R (↑S f) = ↑R f
-- Init.Data.UInt.Lemmas
instAssociativeUInt8HAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.const_mul_left : ∀ {α : Type u_1} {F : Type u_4} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedRing R] {g : α → F} {l : Filter α}
  {f : α → R}, f =o[l] g → ∀ (c : R), (fun x => c * f x) =o[l] g
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.mkEvalTactic' : Lean.Name →
  Lean.Meta.Grind.Params →
    Lean.Elab.TermElabM
      (Lean.Meta.Grind.Goal → Lean.TSyntax `grind → Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.Goal))
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivial.linearMapAt_trivialization : ∀ (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace B] (x : B),
  Bundle.Trivialization.linearMapAt 𝕜 (Bundle.Trivial.trivialization B F) x = LinearMap.id
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- Bessel's inequality for finite sums.  -/
Orthonormal.sum_inner_products_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} (x : E) {v : ι → E} {s : Finset ι}, Orthonormal 𝕜 v → ∑ i ∈ s, ‖inner 𝕜 (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) (a : B) (X : ↑(F.obj a)),
  (α.naturality (CategoryTheory.CategoryStruct.id a)).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((α.app a).toFunctor.map ((F.mapId a).hom.toNatTrans.app X))
      ((G.mapId a).inv.toNatTrans.app ((α.app a).toFunctor.obj X))
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
AddMonoidAlgebra.cardinalMk_of_infinite : ∀ (R M : Type u) [inst : Semiring R] [Infinite M] [Nontrivial R],
  Cardinal.mk (AddMonoidAlgebra R M) = max (Cardinal.mk R) (Cardinal.mk M)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.ShortComplex.ShortExact.extClass.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact), hS.extClass = hS.extClass
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (a : X ⟶ Y) {Z : ↑(F.obj b₂)}
  (h : (F.map fg).toFunctor.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map fg).toFunctor.map a) h)
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.alter : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [Hashable α] →
        [LawfulBEq α] →
          Std.DHashMap.Internal.Raw₀ α β → (a : α) → (Option (β a) → Option (β a)) → Std.DHashMap.Internal.Raw₀ α β
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a b : α} {fallback : β}, (a == b) = true → m.getD a fallback = m.getD b fallback
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.sliceFrom_le_sliceFrom_iff : ∀ {s : String.Slice} {p₀ q r : s.Pos} {h₁ : p₀ ≤ q} {h₂ : p₀ ≤ r}, p₀.sliceFrom q h₁ ≤ p₀.sliceFrom r h₂ ↔ q ≤ r
-- Init.Data.String.Lemmas.Basic
String.singleton_append_inj : ∀ {c : Char} {s : String} {d : Char} {t : String}, String.singleton c ++ s = String.singleton d ++ t ↔ c = d ∧ s = t
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- We say that `R` satisfies the strong rank condition if `(Fin n → R) →ₗ[R] (Fin m → R)` injective
implies `n ≤ m`.  -/
StrongRankCondition : (R : Type u) → [Semiring R] → Prop
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_counitIso_inv_app_app_app : ∀ {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]
  (X : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (X_1 : D) (X_2 : C),
  ((CategoryTheory.Functor.flipping.counitIso.inv.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((X.obj X_1).obj X_2)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.WithCache.mk.sizeOf_spec : ∀ {α : Type u} {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} [inst : SizeOf α] (val : α)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig), sizeOf { val := val, cache := cache } = 1 + sizeOf val + sizeOf cache
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Complex.volume_sum_rpow_lt : ∀ (ι : Type u_1) [inst : Fintype ι] [Nonempty ι] {p : ℝ},
  1 ≤ p →
    ∀ (r : ℝ),
      MeasureTheory.volume {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} =
        ENNReal.ofReal r ^ (2 * Fintype.card ι) *
          ENNReal.ofReal
            ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Icc_subset : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a b : { x // p x }), Subtype.val '' Set.Icc a b ⊆ Set.Icc ↑a ↑b
-- Lean.Parser.Do
Lean.Parser.Term.doLetExpr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mk'_mem_incidenceSet_left_iff : ∀ {V : Type u} (G : SimpleGraph V) {a b : V}, s(a, b) ∈ G.incidenceSet a ↔ G.Adj a b
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq_succ : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α} (n : ℕ),
  MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i n.succ =
    MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s
      (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i k)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.comapDomain_add : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f)
  (x y : AddMonoidAlgebra R N),
  AddMonoidAlgebra.comapDomain f hf (x + y) = AddMonoidAlgebra.comapDomain f hf x + AddMonoidAlgebra.comapDomain f hf y
-- Init.Data.Fin.Lemmas
Fin.cast_castLT : ∀ {k m n : ℕ} (i : Fin k) (h : ↑i < m) (mn : m = n), Fin.cast mn (i.castLT h) = i.castLT ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instTop : {α : Type u_1} → [inst : MeasurableSpace α] → Top (Subtype MeasurableSet)
-- Mathlib.Algebra.Order.Module.Defs
PosSMulReflectLE.toPosSMulStrictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β] [inst_3 : Zero α]
  [PosSMulReflectLE α β], PosSMulStrictMono α β
-- Init.Data.SInt.Basic
/-- Converts a natural number to a 32-bit signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int32.ofNat 127 = 127`
* `Int32.ofNat 32770 = 32770`
* `Int32.ofNat 2_147_483_647 = 2_147_483_647`
* `Int32.ofNat 2_147_483_648 = -2_147_483_648`
 -/
Int32.ofNat : ℕ → Int32
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mkIso_hom_base : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right)
  (base : ψ.base ≅ ψ'.base)
  (left_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left.hom F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_1)
  (right_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right.hom G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_3),
  (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).hom.base = base.hom
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceBackward_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X)
  (g : CategoryTheory.Over f.left),
  f.iteratedSliceBackward.obj g = CategoryTheory.Over.mk (CategoryTheory.Over.homMk g.hom ⋯)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonLocationLink : Lean.ToJson Lean.Lsp.LocationLink
-- Init.Data.List.Lemmas
List.IsPrefix.eq_1 : ∀ {α : Type u} (l₁ l₂ : List α), (l₁ <+: l₂) = ∃ t, l₁ ++ t = l₂
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
groupHomology_induction_on : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {n : ℕ}
  {C : ↑(groupHomology A n) → Prop} (x : ↑(groupHomology A n)),
  (∀ (x : ↑(groupHomology.cycles A n)), C ((CategoryTheory.ConcreteCategory.hom (groupHomology.π A n)) x)) → C x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.inv_int_eq' : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (b : ℤ),
  (b != 0) = true → IntCast.intCast b * (Lean.Grind.CommRing.denoteInt b)⁻¹ = 1
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
MeasureTheory.VectorMeasure.withDensity_zero : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G}, μ.withDensity 0 B = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mk.sizeOf_spec : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : SizeOf A] [inst_7 : SizeOf B] [inst_8 : SizeOf C] [inst_9 : SizeOf A'] [inst_10 : SizeOf B']
  [inst_11 : SizeOf C'] (left : CategoryTheory.Functor A A') (base : CategoryTheory.Functor B B')
  (right : CategoryTheory.Functor C C')
  (squareLeft :
    autoParam (CategoryTheory.CatCommSq F left base F') CategoryTheory.Limits.CatCospanTransform.squareLeft._autoParam)
  (squareRight :
    autoParam (CategoryTheory.CatCommSq G right base G')
      CategoryTheory.Limits.CatCospanTransform.squareRight._autoParam),
  sizeOf { left := left, base := base, right := right, squareLeft := squareLeft, squareRight := squareRight } =
    1 + sizeOf left + sizeOf base + sizeOf right + sizeOf squareLeft + sizeOf squareRight
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instMulOneClass : {α : Type u} → [Mul α] → MulOneClass (WithOne α)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instZero : {α : Type u} → Zero (FreeAddGroup α)