mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.HomotopyCategory.homToNerveMk_comp_assoc : ∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C] {D : Type u}
  [inst_1 : CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor X.HomotopyCategory C)
  (G : CategoryTheory.Functor C D) {Z : SSet.Truncated 2} (h : (SSet.truncation 2).obj (CategoryTheory.nerve D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homToNerveMk (F.comp G)) h =
    CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homToNerveMk F)
      (CategoryTheory.CategoryStruct.comp ((SSet.truncation 2).map (CategoryTheory.nerveMap G)) h)
-- Mathlib.ModelTheory.PartialEquiv
/-- Restriction of a partial equivalence to a substructure of the codomain.  -/
FirstOrder.Language.PartialEquiv.codRestrict : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] → (f : L.PartialEquiv M N) → {A : L.Substructure N} → A ≤ f.cod → L.PartialEquiv M N
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.get_insertMany_list.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (v : β) → none = some v → motive (some v))
  (h_2 : none = none → motive none),
  (match w : none with
    | some v => h_1 v w
    | none => h_2 w) =
    h_2 ⋯
-- Mathlib.CategoryTheory.Subobject.Comma
/-- Projecting and then lifting a subobject recovers the original subobject, because there is at
most one morphism making the projected subobject into a structured arrow.  -/
CategoryTheory.StructuredArrow.lift_projectSubobject : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} [inst_2 : CategoryTheory.Limits.HasFiniteLimits C]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteLimits T] {A : CategoryTheory.StructuredArrow S T}
  (P : CategoryTheory.Subobject A)
  {q : S ⟶ T.obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.StructuredArrow.projectSubobject P))}
  (hq : CategoryTheory.CategoryStruct.comp q (T.map (CategoryTheory.StructuredArrow.projectSubobject P).arrow) = A.hom),
  CategoryTheory.StructuredArrow.liftSubobject (CategoryTheory.StructuredArrow.projectSubobject P) hq = P
-- Mathlib.RingTheory.Polynomial.Tower
Polynomial.aeval_algebraMap_eq_zero_iff_of_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B] {x : A} {p : Polynomial R},
  Function.Injective ⇑(algebraMap A B) → ((Polynomial.aeval ((algebraMap A B) x)) p = 0 ↔ (Polynomial.aeval x) p = 0)
-- Mathlib.Data.Sum.Lattice
Sum.Lex.instDistribLattice : {α : Type u_1} → {β : Type u_2} → [DistribLattice α] → [DistribLattice β] → DistribLattice (α ⊕ₗ β)
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.preadditiveNatLinear : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.Linear ℕ C
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryEquivClass.toSemilinearIsometryClass : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} (𝓕 : Type u_10) [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂]
  [inst_6 : Module R E] [inst_7 : Module R₂ E₂] [inst_8 : EquivLike 𝓕 E E₂]
  [s : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂], SemilinearIsometryClass 𝓕 σ₁₂ E E₂
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_le_right : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G) [h : H₂.Normal], ⁅H₁, H₂⁆ ≤ H₂
-- Mathlib.Algebra.Free
FreeSemigroup.traverse.eq_1 : ∀ {m : Type u → Type u} [inst : Applicative m] {α β : Type u} (F : α → m β) (x : FreeSemigroup α),
  FreeSemigroup.traverse F x =
    x.recOnPure (fun x => pure <$> F x) fun _x _y ihx ihy => (fun x1 x2 => x1 * x2) <$> ihx <*> ihy
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ico_right_eq_Ico_add_one_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {a b : α}, a ≤ b → ¬IsMax b → insert b (Finset.Ico a b) = Finset.Ico a (b + 1)
-- Init.Data.Rat.Lemmas
Rat.one_num : Rat.num 1 = 1
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.ιObj_πObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιObj I κ f) (CategoryTheory.SmallObject.πObj I κ f) = f
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffOn.sum_section : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {u : Set M} {ι : Type u_7} {t : ι → (x : M) → V x}
  {s : Finset ι},
  (∀ i ∈ s, ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t i x⟩) u) →
    ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, ∑ i ∈ s, t i x⟩) u
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.wp.eq_1 : ∀ {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type w'} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [self : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog)
  (post : Value → Pred) (epost : EPred),
  Std.Internal.Do.wp x post epost = (Std.Internal.Do.WP.wpTrans x).apply post epost
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.IsBasis.contract_sdiff_isBasis_sdiff`. -/
Matroid.IsBasis.contract_diff_isBasis_diff : ∀ {α : Type u_1} {M : Matroid α} {I J X Y : Set α},
  M.IsBasis I X → M.IsBasis J Y → I ⊆ J → (M.contract I).IsBasis (J \ I) (Y \ X)
-- Mathlib.Order.Defs.Unbundled
asymm_of_isTrans_of_irrefl : ∀ {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] [Std.Irrefl r], Std.Asymm r
-- Mathlib.Probability.Process.Stopping
/-- The stopped process of a strongly adapted process with continuous paths is strongly adapted.  -/
MeasureTheory.StronglyAdapted.stoppedProcess : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : Nonempty ι] [inst_3 : LinearOrder ι]
  [inst_4 : TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [inst_7 : MeasurableSpace ι]
  [BorelSpace ι] {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [TopologicalSpace.MetrizableSpace ι],
  MeasureTheory.StronglyAdapted f u →
    (∀ (ω : Ω), Continuous fun i => u i ω) →
      MeasureTheory.IsStoppingTime f τ → MeasureTheory.StronglyAdapted f (MeasureTheory.stoppedProcess u τ)
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.mkSizeOfMinors.loop : {α : Type} →
  Array Lean.Expr →
    Array Lean.Expr → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → ℕ → Array Lean.Expr → Lean.MetaM α
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.associatorNatIsoLeftCat_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a : B) {b c d : B} (g : b ⟶ c) (h : c ⟶ d)
  (X : ↑(CategoryTheory.Cat.of (a ⟶ b))),
  (CategoryTheory.Bicategory.associatorNatIsoLeftCat a g h).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator X g h).inv
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_ite : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {p : ι → Prop} [inst_1 : DecidablePred p]
  (f g : ι → M), (∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s with p x, f x + ∑ x ∈ s with ¬p x, g x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_neg' : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] {s : Finset α} {a : α}, a ∈ -s ↔ -a ∈ s
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_restrict : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {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) (s : Set X),
  (μ.restrict s).transpose B = (μ.transpose B).restrict s
-- Mathlib.Algebra.Group.Defs
add_neg_cancel : ∀ {G : Type u_1} [inst : AddGroup G] (a : G), a + -a = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log_pow : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (n : ℕ) (a : A),
  (∀ x ∈ spectrum ℝ a, x ≠ 0) → autoParam (IsSelfAdjoint a) CFC.log_pow._auto_1 → CFC.log (a ^ n) = n • CFC.log a
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesOnBall.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F],
  HasFPowerSeriesOnBall f p x r →
    ∀ {y : E}, ↑‖y‖₊ < r → HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.setLIntegral_toKernel_Iic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → StieltjesFunction ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) (x : ℝ) {s : Set β},
  MeasurableSet s →
    ∫⁻ (b : β) in s, ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) (Set.Iic x) ∂ν a =
      (κ a) (s ×ˢ Set.Iic x)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.isLeftQuasiInverse_iff_isRightQuasiInverse_swap : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃},
  u.IsLeftQuasiInverse v ↔ v.IsRightQuasiInverse u
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.absNorm_eq' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  {I : FractionalIdeal (nonZeroDivisors R) K} (a : ↥(nonZeroDivisors R)) (I₀ : Ideal R),
  a • ↑I = Submodule.map (Algebra.linearMap R K) I₀ →
    FractionalIdeal.absNorm I = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addFactStep.go : Lean.Expr → ℕ → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Unit
-- Init.Prelude
Lean.Syntax.brecOn_2.eq : ∀ {motive_1 : Lean.Syntax → Sort u} {motive_2 : Array Lean.Syntax → Sort u} {motive_3 : List Lean.Syntax → Sort u}
  (t : List Lean.Syntax) (F_1 : (t : Lean.Syntax) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t),
  Lean.Syntax.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.Syntax.brecOn_2.go t F_1 F_2 F_3).2
-- Init.Data.Array.Subarray
/-- Checks whether all of the elements in a subarray satisfy a monadic Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that does not satisfy the predicate is found.

Example:
```lean example
#eval #["red", "green", "blue", "orange"].toSubarray.popFront.allM fun x => do
  IO.println x
  pure (x.length == 5)
```
```output
green
blue
```
```output
false
```
 -/
Subarray.allM : {α : Type u} → {m : Type → Type w} → [Monad m] → (α → m Bool) → Subarray α → m Bool
-- Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
/-- A function `f` is summable in a uniform additive group `α` if and only if the net of its partial
sums is Cauchy and its sum in `Completion α` lies in the range of `toCompl : α →+ Completion α`.
(The condition that the net of partial sums is Cauchy can be checked using
`cauchySeq_finset_iff_sum_vanishing` or `cauchySeq_finset_iff_tsum_vanishing`.)  -/
summable_iff_cauchySeq_finset_and_tsum_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [inst_2 : IsUniformAddGroup α]
  (f : β → α),
  Summable f ↔
    (CauchySeq fun s => ∑ b ∈ s, f b) ∧
      ∑' (i : β), UniformSpace.Completion.toCompl (f i) ∈ Set.range ⇑UniformSpace.Completion.toCompl
-- Mathlib.Order.Defs.Unbundled
RelUpperSet.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (P a)] (carrier : Set α)
  (isRelUpperSet' : IsRelUpperSet carrier P), sizeOf { carrier := carrier, isRelUpperSet' := isRelUpperSet' } = 1
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- **Alias** of `TemperedDistribution.fourier_apply`. -/
TemperedDistribution.fourierTransform_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F] (f : TemperedDistribution E F) (g : SchwartzMap E ℂ),
  (FourierTransform.fourier f) g = f (FourierTransform.fourier g)
-- Init.Data.Array.Erase
Array.eraseP_ne_empty_iff : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, xs.eraseP p ≠ #[] ↔ xs ≠ #[] ∧ ∀ (x : α), p x = true → xs ≠ #[x]
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- An induction principle useful to prove statements about resultants.
Let `P` be a predicate on a polynomial.
If `R → S` injective implies `(∀ p : S[X], P p) → (∀ p : R[X], P p)`,
and if `R → S` surjective implies `(∀ p : R[X], P p) → (∀ p : S[X], P p)`,
then we may reduce to the case where `R` is a field and `p` splits.  -/
Polynomial.induction_of_Splits_of_injective_of_surjective : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R) (P : {R : Type u} → [inst : CommRing R] → Polynomial R → Prop),
  (∀ (R : Type u) [inst : Field R] (p : Polynomial R), p.Splits → P p) →
    (∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
        Function.Injective ⇑φ → ∀ (p : Polynomial R), P (Polynomial.map φ p) → P p) →
      (∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S),
          Function.Surjective ⇑φ → ∀ (p : Polynomial S), (∀ (q : Polynomial R), P q) → P p) →
        P p
-- Mathlib.Topology.Order.IntermediateValue
/-- **Intermediate Value Theorem** for continuous functions on closed intervals, case
`f a ≤ t ≤ f b`.  -/
intermediate_value_Icc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α}, a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b
-- Mathlib.ModelTheory.ElementaryMaps
/-- Composition of elementary embeddings is associative.  -/
FirstOrder.Language.ElementaryEmbedding.comp_assoc : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [inst : L.Structure M]
  [inst_1 : L.Structure N] [inst_2 : L.Structure P] [inst_3 : L.Structure Q] (f : L.ElementaryEmbedding M N)
  (g : L.ElementaryEmbedding N P) (h : L.ElementaryEmbedding P Q), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Mapping by the identity morphism is just the identity functor.  -/
CategoryTheory.Under.mapId : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (Y : T) →
      CategoryTheory.Under.map (CategoryTheory.CategoryStruct.id Y) ≅ CategoryTheory.Functor.id (CategoryTheory.Under Y)
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasStrictFDerivAt_sub_const_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasStrictFDerivAt (fun x => f x - c) f' x ↔ HasStrictFDerivAt f f' x
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An intersection of blocks is a block.  -/
AddAction.IsBlock.iInter : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {ι : Sort u_3} {B : ι → Set X},
  (∀ (i : ι), AddAction.IsBlock G (B i)) → AddAction.IsBlock G (⋂ i, B i)
-- Lean.Level
Lean.instHashableLevelMVarId : Hashable Lean.LevelMVarId
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_array_eq_insertManyIfNewUnit_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (a : Array α),
  Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m a =
    Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m a.toList
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map₂_coe_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : WithZero β),
  WithZero.map₂ f (↑a) b = WithZero.map (fun b => f a b) b
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorComm_apply : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Invertible 2]
  (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (x : TensorProduct R M₁ M₂),
  (Q₁.tensorComm Q₂) x = (TensorProduct.comm R M₁ M₂) x
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_alls : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}
  {v : α → M}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (f f_1 : Option (β a) → Option (β a)),
  f = f_1 →
    ∀ (a_1 a_2 : Std.DHashMap.Internal.AssocList α β),
      a_1 = a_2 → Std.DHashMap.Internal.AssocList.alter a f a_1 = Std.DHashMap.Internal.AssocList.alter a f_1 a_2
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G : C)
  {X Y : C} (f : X ⟶ Y) (j : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ C).obj G).map f).app j =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator j G X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G f))
        (CategoryTheory.MonoidalCategoryStruct.associator j G Y).inv)
-- Mathlib.Topology.DenseEmbedding
/-- If `i : α → β` is a dense embedding with dense complement of the range, then any compact set in
`α` has empty interior.  -/
IsDenseInducing.interior_compact_eq_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β} [T2Space β],
  IsDenseInducing i → Dense (Set.range i)ᶜ → ∀ {s : Set α}, IsCompact s → interior s = ∅
-- Mathlib.Analysis.Convex.StoneSeparation
/-- In a tetrahedron with vertices `x`, `y`, `p`, `q`, any segment `[u, v]` joining the opposite
edges `[x, p]` and `[y, q]` passes through any triangle of vertices `p`, `q`, `z` where
`z ∈ [x, y]`.  -/
not_disjoint_segment_convexHull_triple : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {p q u v x y z : E},
  z ∈ segment 𝕜 x y → u ∈ segment 𝕜 x p → v ∈ segment 𝕜 y q → ¬Disjoint (segment 𝕜 u v) ((convexHull 𝕜) {p, q, z})
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_toAddMonoidHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits.  -/
CategoryTheory.Limits.reflectsLimits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimits F], CategoryTheory.Limits.ReflectsLimits F.op
-- Mathlib.Algebra.Group.Pi.Basic
Pi.group.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Group (f i)],
  Pi.group = { toDivInvMonoid := Pi.divInvMonoid, inv_mul_cancel := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BinaryBiconeMorphism.wsnd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B),
  CategoryTheory.CategoryStruct.comp self.hom B.snd = A.snd
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.hasIntegral_const : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} (c : E),
  BoxIntegral.HasIntegral I l (fun x => c) vol ((vol I) c)
-- Init.Data.Nat.Basic
Nat.le_eq : ∀ {x y : ℕ}, x.le y = (x ≤ y)
-- Init.Data.SInt.Lemmas
UInt64.toInt64_ofNat' : ∀ {n : ℕ}, (UInt64.ofNat n).toInt64 = Int64.ofNat n
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.faceOpposite_point_eq_point_succAbove : ∀ {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 : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1))
  (j : Fin (n - 1 + 1)), (s.faceOpposite i).points j = s.points (i.succAbove (Fin.cast ⋯ j))
-- Mathlib.Algebra.Algebra.Operations
Submodule.one_mem_div : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {I J : Submodule R A}, 1 ∈ I / J ↔ J ≤ I
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multispan_map_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) (a : J.L),
  I.multispan.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd a) = I.snd a
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instRespectsIsoScheme : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.WeaklyEtale