mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.instMonoidalForallEval : {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) → (CategoryTheory.Pi.eval C i).Monoidal
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The underlying monoid homomorphism of a continuous representation.  -/
ContRepresentation.toMonoidHom : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] → [inst_5 : Module R V] → ContRepresentation R G V → G →* V →L[R] V
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.isIso_iff_mk_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.IsIso f ↔ CategoryTheory.Subobject.mk f = ⊤
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
Equiv.pointReflection_midpoint_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), (Equiv.pointReflection (midpoint R x y)) x = y
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_le_rpow_iff : ∀ {x y : ENNReal} {z : ℝ}, 0 < z → (x ^ z ≤ y ^ z ↔ x ≤ y)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.mod_smul : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I) (a : A)
  (f : PowerSeries A) [inst_1 : IsAdicComplete I A], H.mod (a • f) = a • H.mod f
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.map_eq_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Ideal R) [inst_1 : p.IsPrime] (Rₚ : Type u_4) [inst_2 : CommSemiring Rₚ]
  [inst_3 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ],
  Ideal.map (algebraMap R Rₚ) p = IsLocalRing.maximalIdeal Rₚ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} [inst_3 : Inhabited (γ k)],
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filterMap f m).get! k = ((m.get? k).bind (f k)).get!
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_1.eq_1 : ∀ (motive : Option (List Lean.MVarId) → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : (l : List Lean.MVarId) → motive (some l)),
  (match none with
    | none => h_1 ()
    | some l => h_2 l) =
    h_1 ()
-- Mathlib.Data.Nat.Init
Eq.ndrec.congr_simp : ∀ {α : Sort u2} {a : α} {motive : α → Sort u1} (m m_1 : motive a), m = m_1 → ∀ {b : α} (h : a = b), h ▸ m = h ▸ m_1
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A variant of `Finset.add_sum_erase` with the addition swapped.  -/
Finset.sum_erase_add : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι},
  a ∈ s → ∑ x ∈ s.erase a, f x + f a = ∑ x ∈ s, f x
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.InClosure.recOn : ∀ {R : Type u_1} [inst : Ring R] {s : Set R} {C : R → Prop} {x : R},
  x ∈ Subring.closure s →
    C 1 → C (-1) → (∀ z ∈ s, ∀ (n : R), C n → C (z * n)) → (∀ {x y : R}, C x → C y → C (x + y)) → C x
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cyclesMap_id : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ),
  X.cyclesMap f g f g (CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.mk₂ f g)) n =
    CategoryTheory.CategoryStruct.id (X.cycles f g n)
-- Lean.Parser.Command
Lean.Parser.Command.theorem.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {fallback : α},
      Std.Internal.List.minKeyD (Std.Internal.List.insertEntry k v l) fallback =
        (Std.Internal.List.minKey? l).elim k fun k' => if (compare k k').isLE = true then k else k'
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.antitone_i₀ : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r r' : ℤ) (pq : κ)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_24)
  (hrr' : autoParam (r ≤ r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_26),
  self.i₀ r' pq ⋯ ≤ self.i₀ r pq ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_erase_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], (m.erase k).get! k = default
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.mk : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  [to_isSeparable : Algebra.IsSeparable F E] [to_normal : Normal F E], IsGalois F E
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- The heterobasic version of `tensorTensorTensorComm` coincides with the regular version.  -/
TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq : ∀ (R : Type uR) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : AddCommMonoid Q] [inst_7 : Module R Q] [inst_8 : Module R P],
  TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R M N P Q =
    TensorProduct.tensorTensorTensorComm R M N P Q
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.obj_carrier : ∀ {R : Type u} [inst : Ring R] (M : FGModuleCat R), ↑M.obj = ↑M
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.revPositions.eq_1 : ∀ (s : String.Slice), s.revPositions = s.revPositionsFrom s.endPos
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_lt_coe : ∀ {x y : ℝ}, ↑x < ↑y ↔ x < y
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.unop_ofNat : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], MulOpposite.unop (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Topology.Closure
closure.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), closure s = ⋂₀ {t | IsClosed t ∧ s ⊆ t}
-- Mathlib.NumberTheory.ModularForms.Basic
instCoeTCModularFormOfModularFormClass : {F : Type u_1} →
  {Γ : Subgroup (GL (Fin 2) ℝ)} →
    {k : ℤ} → [inst : FunLike F UpperHalfPlane ℂ] → [ModularFormClass F Γ k] → CoeTC F (ModularForm Γ k)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.Data.PNat.Defs
/-- Write a successor as an element of `ℕ+`.  -/
Nat.succPNat : ℕ → ℕ+
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instNontrivialCarrierStalkCommRingCatPresheafSmoothSheafCommRing : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  [Nontrivial R] (x : M), Nontrivial ↑((smoothSheafCommRing IM I M R).presheaf.stalk x)
-- Mathlib.Geometry.Euclidean.Incenter
/-- The unique weights of the vertices in an affine combination equal to the given touchpoint.  -/
Affine.Simplex.touchpointWeights : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Finset (Fin (n + 1)) → Fin (n + 1) → Fin (n + 1) → ℝ
-- Std.Http.Protocol.H1
/-- Handles `Reader.State.complete` by deciding whether to stay open for the next
message or transition to `.closed`.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processReaderCompleteState : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Topology.Algebra.Module.Complement
/-- If `h : IsTopCompl p q`, `h.projectionOnto` is the continuous linear projection `M →L[R] p`
along `q`. This is the continuous version of `Submodule.linearProjOfIsCompl`.

See also `Submodule.IsTopCompl.projection` for the same projection as an element of `M →L[R] M`.  -/
Submodule.projectionOntoL : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] → (p q : Submodule R M) → Submodule.IsTopCompl p q → M →L[R] ↥p
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule : {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] → LieSubmodule R L M → Submodule R M
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
NNRealRMK.integralLinearMap_rieszMeasure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X]
  [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal),
  CompactlySupportedContinuousMap.integralLinearMap (NNRealRMK.rieszMeasure Λ) = Λ
-- Mathlib.RingTheory.WittVector.Defs
WittVector.constantCoeff_wittNSMul : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (m n : ℕ), MvPolynomial.constantCoeff (WittVector.wittNSMul p m n) = 0
-- Init.Data.Array.Lemmas
Array.beq_empty_eq : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α}, (xs == #[]) = xs.isEmpty
-- Mathlib.Analysis.Normed.Group.Defs
/-- A type `E` equipped with a continuous map `‖·‖ₑ : E → ℝ≥0∞`

NB. We do not demand that the topology is somehow defined by the enorm:
for `ℝ≥0∞` (the motivating example behind this definition), this is not true.  -/
ContinuousENorm : (E : Type u_8) → [TopologicalSpace E] → Type u_8
-- Mathlib.CategoryTheory.Yoneda
/-- The data which expresses that a functor `F : Cᵒᵖ ⥤ Type v` is representable by `Y : C`.

In the situation where `F` factors through a concrete category, it may be more convenient to use
the API in the file `Mathlib/CategoryTheory/ConcreteCategory/Representable.lean`.  -/
CategoryTheory.Functor.RepresentableBy : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor Cᵒᵖ (Type v) → C → Type (max (max u₁ v) v₁)
-- Mathlib.RingTheory.Ideal.Defs
Ideal.add_mem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) {a b : α}, a ∈ I → b ∈ I → a + b ∈ I
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.algebra : {X Y : AlgebraicGeometry.Scheme} → {f : X ⟶ Y} → (self : AlgebraicGeometry.ValuativeCommSq f) → Algebra self.R self.K
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- The skew monoid algebra of `G` over `k` is the type of finite formal `k`-linear
combinations of terms of `G`, endowed with a skewed convolution product.  -/
SkewMonoidAlgebra : (k : Type u_1) → Type u_2 → [Zero k] → Type (max u_1 u_2)
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_iff_exists_mem_nhds_image_subset_compact : ∀ {M₁ : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] (f : M₁ → M₂), IsCompactOperator f ↔ ∃ V ∈ nhds 0, ∃ K, IsCompact K ∧ f '' V ⊆ K
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.instAddCommGroup.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddCommGroup N],
  ZeroHom.instAddCommGroup = { toAddGroup := ZeroHom.instAddGroup, add_comm := ⋯ }
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A subsemigroup of a magma `M` is a subset closed under multiplication.  -/
Subsemigroup : (M : Type u_3) → [Mul M] → Type u_3
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The underlying family of 2-morphisms.  -/
CategoryTheory.Oplax.LaxTrans.Modification.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Oplax.LaxTrans.Modification η θ → (a : B) → η.app a ⟶ θ.app a
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp.inj : ∀ {e : Lean.Expr} {f₁ g₁ f₂ g₂ : Mathlib.Tactic.BicategoryLike.Mor₁} {η θ : Mathlib.Tactic.BicategoryLike.Mor₂Iso}
  {e_1 : Lean.Expr} {f₁_1 g₁_1 f₂_1 g₂_1 : Mathlib.Tactic.BicategoryLike.Mor₁}
  {η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso},
  Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp e f₁ g₁ f₂ g₂ η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp e_1 f₁_1 g₁_1 f₂_1 g₂_1 η_1 θ_1 →
    e = e_1 ∧ f₁ = f₁_1 ∧ g₁ = g₁_1 ∧ f₂ = f₂_1 ∧ g₂ = g₂_1 ∧ η = η_1 ∧ θ = θ_1
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.max : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α},
  IsLocalMax f a → IsLocalMax g a → IsLocalMax (fun x => max (f x) (g x)) a
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_lt_prod' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {f g : ι → M}
  {s : Finset ι} [MulLeftStrictMono M], (∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → ∏ i ∈ s, f i < ∏ i ∈ s, g i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorμ_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ W X Y Z)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj W Y)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.SemiCartesianMonoidalCategory.snd W X)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z)
-- Mathlib.NumberTheory.Bernoulli
bernoulliPowerSeries_mul_exp_sub_one : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : Algebra ℚ A],
  bernoulliPowerSeries A * (PowerSeries.exp A - 1) = PowerSeries.X
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.IsConnected.is_nonempty : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} [self : CategoryTheory.IsConnected J], Nonempty J
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- **Church-Rosser theorem** for word reduction: If `w1 w2 w3` are words such that `w1` reduces
to `w2` and `w3` respectively, then there is a word `w4` such that `w2` and `w3` reduce to `w4`
respectively. This is also known as Newman's diamond lemma.  -/
FreeGroup.Red.church_rosser : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)},
  FreeGroup.Red L₁ L₂ → FreeGroup.Red L₁ L₃ → Relation.Join FreeGroup.Red L₂ L₃
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.mk_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β)
  (h1 : (↑f).toFun 1 = 1) (hmul : ∀ (x y : α), (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y),
  { toZeroHom := ↑f, map_one' := h1, map_mul' := hmul } = f
-- Mathlib.Data.Sym.Basic
SymOptionSuccEquiv.decode_inr : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n.succ),
  SymOptionSuccEquiv.decode (Sum.inr s) = Sym.map (⇑Function.Embedding.some) s
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear maps on the left preserves `C^n` functions in a domain
at a point.  -/
ContDiffWithinAt.continuousLinearMap_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞}
  (g : F →L[𝕜] G), ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n (⇑g ∘ f) s x
-- Init.Data.Array.Find
Array.find?_map : ∀ {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {xs : Array β},
  Array.find? p (Array.map f xs) = Option.map f (Array.find? (p ∘ f) xs)
-- Lean.Widget.Diff
/-- If true, the expression before and the expression after are identical.  -/
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.isEmpty : Lean.Widget.ExprDiff✝ → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- The map of a fork is a limit iff the fork consisting of the mapped morphisms is a limit. This
essentially lets us commute `Fork.ofι` with `Functor.mapCone`.
 -/
CategoryTheory.Limits.isLimitMapConeForkEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            {f g : X ⟶ Y} →
              {h : Z ⟶ X} →
                (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) →
                  CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.Fork.ofι h w)) ≃
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (G.map h) ⋯)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.eq_of_not_indep_subset : ∀ {α : Type u_1} {M : Matroid α} {C X : Set α}, M.IsCircuit C → ¬M.Indep X → X ⊆ C → X = C
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.classifier_Ω₀ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.Presheaf.classifier C).Ω₀ = (CategoryTheory.Functor.const Cᵒᵖ).obj PUnit.{max (u + 1) (v + 1)}
-- Mathlib.Algebra.Order.UpperLower
LowerSet.Iic_one : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α], LowerSet.Iic 1 = 1
-- Lean.PrivateName
Lean.privatePrefix? : Lean.Name → Option Lean.Name
-- Mathlib.Algebra.Order.Field.Basic
le_one_div_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (a ≤ 1 / b ↔ b ≤ 1 / a)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE_eq_getEntryLE : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β} {k : α}
  {hto : t.Ordered} {he : ∃ a ∈ t, (compare a k).isLE = true},
  Std.DTreeMap.Internal.Impl.getKeyLE k t hto he = (Std.DTreeMap.Internal.Impl.getEntryLE k t hto he).fst
-- Mathlib.Topology.Compactification.StoneCech
/-- The natural map from α to its Stone-Čech compactification.  -/
stoneCechUnit : {α : Type u} → [inst : TopologicalSpace α] → α → StoneCech α
-- Init.Data.Nat.Coprime
Nat.coprime_comm : ∀ {n m : ℕ}, n.Coprime m ↔ m.Coprime n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).isEmpty = false →
        ∀ {fallback : α},
          (t.alter k f).maxKeyD fallback = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
mem_span_insert_exchange : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  {x y : V}, x ∈ Submodule.span K (insert y s) → x ∉ Submodule.span K s → y ∈ Submodule.span K (insert x s)
-- Std.Time.Format.Basic
/-- Infer an `HourMarker` from an `ExtendedDayPeriod` parsed by `B`.  -/
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.markerOfExtendedDayPeriod : Std.Time.ExtendedDayPeriod → Std.Time.HourMarker
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
/-- If the comparison morphism `G.obj (limit F) ⟶ limit (F ⋙ G)` is an isomorphism, then `G`
preserves limits of `F`.  -/
CategoryTheory.preservesLimit_of_isIso_post : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.HasLimit F]
  [inst_4 : CategoryTheory.Limits.HasLimit (F.comp G)] [CategoryTheory.IsIso (CategoryTheory.Limits.limit.post F G)],
  CategoryTheory.Limits.PreservesLimit F G
-- Init.Data.Vector.Count
Vector.count_reverse : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} {a : α} {xs : Vector α n}, Vector.count a xs.reverse = Vector.count a xs
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.mk.injEq : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (op : Lean.Expr) (neutral? : Option Lean.Expr) (assocInst : Lean.Expr)
  (idempotentInst? commInst? neutralInst? : Option Lean.Expr) (nextId : ℕ) (vars : Lean.PArray Lean.Expr)
  (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Var)
  (denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Expr)
  (denoteEntries : Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)) (queue : Lean.Meta.Grind.AC.Queue)
  (basis : List Lean.Meta.Grind.AC.EqCnstr) (diseqs : Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr) (recheck : Bool)
  (id_1 : ℕ) (type_1 : Lean.Expr) (u_1 : Lean.Level) (op_1 : Lean.Expr) (neutral?_1 : Option Lean.Expr)
  (assocInst_1 : Lean.Expr) (idempotentInst?_1 commInst?_1 neutralInst?_1 : Option Lean.Expr) (nextId_1 : ℕ)
  (vars_1 : Lean.PArray Lean.Expr) (varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Var)
  (denote_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Expr)
  (denoteEntries_1 : Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)) (queue_1 : Lean.Meta.Grind.AC.Queue)
  (basis_1 : List Lean.Meta.Grind.AC.EqCnstr) (diseqs_1 : Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr) (recheck_1 : Bool),
  ({ id := id, type := type, u := u, op := op, neutral? := neutral?, assocInst := assocInst,
        idempotentInst? := idempotentInst?, commInst? := commInst?, neutralInst? := neutralInst?, nextId := nextId,
        vars := vars, varMap := varMap, denote := denote, denoteEntries := denoteEntries, queue := queue,
        basis := basis, diseqs := diseqs, recheck := recheck } =
      { id := id_1, type := type_1, u := u_1, op := op_1, neutral? := neutral?_1, assocInst := assocInst_1,
        idempotentInst? := idempotentInst?_1, commInst? := commInst?_1, neutralInst? := neutralInst?_1,
        nextId := nextId_1, vars := vars_1, varMap := varMap_1, denote := denote_1, denoteEntries := denoteEntries_1,
        queue := queue_1, basis := basis_1, diseqs := diseqs_1, recheck := recheck_1 }) =
    (id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          op = op_1 ∧
            neutral? = neutral?_1 ∧
              assocInst = assocInst_1 ∧
                idempotentInst? = idempotentInst?_1 ∧
                  commInst? = commInst?_1 ∧
                    neutralInst? = neutralInst?_1 ∧
                      nextId = nextId_1 ∧
                        vars = vars_1 ∧
                          varMap = varMap_1 ∧
                            denote = denote_1 ∧
                              denoteEntries = denoteEntries_1 ∧
                                queue = queue_1 ∧ basis = basis_1 ∧ diseqs = diseqs_1 ∧ recheck = recheck_1)