mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
addInvariantVectorField_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] (v w : AddGroupLieAlgebra I G),
  addInvariantVectorField (v + w) = addInvariantVectorField v + addInvariantVectorField w
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₁ → (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.Tactic.Push
/-- The configuration options for the `push` tactic.  -/
Mathlib.Tactic.Push.Config : Type
-- Mathlib.Logic.Relation
/-- **Alias** of `IsTrans.comap`. -/
Transitive.comap : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [IsTrans β r] (f : α → β), IsTrans α (Function.onFun r f)
-- Mathlib.Data.Finset.Preimage
/-- Reindexing and then restricting to a `Finset` is the same as first restricting to the preimage
of this `Finset` and then reindexing.  -/
Finset.restrict_comp_piCongrLeft : ∀ {α : Type u} {β : Type v} {π : β → Type u_1} (s : Finset β) (e : α ≃ β),
  s.restrict ∘ ⇑(Equiv.piCongrLeft π e) =
    ⇑(Equiv.piCongrLeft (fun b => π ↑b) (e.restrictPreimageFinset s)) ∘ (s.preimage ⇑e ⋯).restrict
-- Mathlib.Algebra.Lie.Sl2
/-- Given a representation of a Lie algebra with distinguished `sl₂` triple, a vector is said to be
primitive if it is a simultaneous eigenvector for the action of both `h` and `e`, and the eigenvalue
for `e` is zero.  -/
IsSl2Triple.HasPrimitiveVectorWith : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [Module R M] → [LieRingModule L M] → {h e f : L} → IsSl2Triple h e f → M → R → Prop
-- Mathlib.NumberTheory.Height.NumberField
NumberField.multisetInfinitePlace.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.multisetInfinitePlace K = NumberField.multisetInfinitePlace K
-- Std.Time.Time.HourMarker
/-- Converts a 12-hour clock time to a 24-hour clock time based on the `HourMarker`.
 -/
Std.Time.HourMarker.toAbsolute : Std.Time.HourMarker → Std.Time.Internal.Bounded.LE 1 12 → Std.Time.Hour.Ordinal
-- Init.Data.Fin.Lemmas
Fin.succ_lt_succ_iff : ∀ {n : ℕ} {a b : Fin n}, a.succ < b.succ ↔ a < b
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.union_unmixedEmbeddingsOver_mixedEmbeddingsOver : ∀ {K : Type u_3} (L : Type u_4) [inst : Field K] [inst_1 : Field L] (ψ : K →+* ℂ) [inst_2 : Algebra K L],
  NumberField.ComplexEmbedding.unmixedEmbeddingsOver L ψ ∪ NumberField.ComplexEmbedding.mixedEmbeddingsOver L ψ =
    {φ | NumberField.ComplexEmbedding.LiesOver φ ψ}
-- Mathlib.Data.String.Basic
_private.Mathlib.Data.String.Basic.0.String.compare.eq_1 : ∀ (s₁ s₂ : String), s₁.compare s₂ = compareOfLessAndEq s₁ s₂
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : CompleteLattice α] [inst_1 : SizeOf α] (toSublattice : Sublattice α)
  (sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier)
  (sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier),
  sizeOf { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' } =
    1 + sizeOf toSublattice
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.splitAtPred.match_3.congr_eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  x = [] →
    (match x with
      | [] => h_1 ()
      | a :: as => h_2 a as) ≍
      h_1 ()
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedGroup.toNNNorm : {E : Type u_5} → [SeminormedGroup E] → NNNorm E
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryGTD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : α × β}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGTD k fallback = t₂.getEntryGTD k fallback
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k k' : α},
  m.WF →
    m.getKey? k = some k' →
      Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.filterMap f m) k = (Std.DHashMap.Raw.Const.get? m k).bind (f k')
-- Init.Data.String.Basic
String.replaceStartEnd! : (s : String) → s.Pos → s.Pos → String.Slice
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.forIn'.loop.match_3.eq_1 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (x : 0 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Monotone convergence theorem** for a supremum over a directed family and indexed by a
countable type.  -/
MeasureTheory.lintegral_iSup_directed_of_measurable : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β]
  {f : β → α → ENNReal},
  (∀ (b : β), Measurable (f b)) →
    Directed (fun x1 x2 => x1 ≤ x2) f → ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_vadd : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {K : Type u_3} [inst_2 : VAdd K H]
  [inst_3 : VAddAssocClass K H H] (c : K) (f : AddConstMap G H a b), ⇑(c +ᵥ f) = c +ᵥ ⇑f
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.instFunLikeSubtypeForallProdVMemSubmoduleCocycles₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → {A : Rep.{u_1, u, u} k G} → FunLike (↥(groupCohomology.cocycles₂ A)) (G × G) ↑A
-- Mathlib.Data.Sum.Order
Sum.instLTSum : {α : Type u_1} → {β : Type u_2} → [LT α] → [LT β] → LT (α ⊕ β)
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.eq_add_neg_iff_add_eq : ∀ {α : Type u} [inst : AddMonoid α] (c : AddUnits α) {a b : α}, a = b + ↑(-c) ↔ a + ↑c = b
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instNonemptyCarrierObjPartOrdEmbIsCardinalFiltered : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ), Nonempty ↑J.obj
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Mon.mul.go.match_1.eq_2 : ∀ (motive : Nat.Internal.SOM.Mon → Nat.Internal.SOM.Mon → Sort u_1) (m₂ : Nat.Internal.SOM.Mon)
  (h_1 : (m₁ : Nat.Internal.SOM.Mon) → motive m₁ []) (h_2 : (m₂ : Nat.Internal.SOM.Mon) → motive [] m₂)
  (h_3 :
    (v₁ : Nat.Internal.Linear.Var) →
      (m₁ : List Nat.Internal.Linear.Var) →
        (v₂ : Nat.Internal.Linear.Var) → (m₂ : List Nat.Internal.Linear.Var) → motive (v₁ :: m₁) (v₂ :: m₂)),
  (m₂ = [] → False) →
    (match [], m₂ with
      | m₁, [] => h_1 m₁
      | [], m₂ => h_2 m₂
      | v₁ :: m₁, v₂ :: m₂ => h_3 v₁ m₁ v₂ m₂) =
      h_2 m₂
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassP_add_coe : ∀ (L : PeriodPair) (z : ℂ) (l : ↥L.lattice), L.weierstrassP (z + ↑l) = L.weierstrassP z
-- Mathlib.Data.Finset.Disjoint
Finset.empty_disjUnion : ∀ {α : Type u_2} (t : Finset α) (h : optParam (Disjoint ∅ t) ⋯), ∅.disjUnion t h = t
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.exists_pos_preimage_ball : ∀ {α : Type u_1} {δ : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoMetricSpace δ]
  (f : α → δ) (x : δ), μ ≠ 0 → ∃ n, 0 < μ (f ⁻¹' Metric.ball x ↑n)
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.centralizer_center : ∀ {G : Type u_1} [inst : Group G], Subgroup.centralizer ↑(Subgroup.center G) = ⊤
-- Lean.Elab.Tactic.Omega.Core
/-- Check if a problem has no constraints.  -/
Lean.Elab.Tactic.Omega.Problem.isEmpty : Lean.Elab.Tactic.Omega.Problem → Bool
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.one_sub_e_mem_of_false : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I)
  {x y : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)} {a : I},
  ↑y a = true →
    ↑x a = false →
      1 - Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) a ∈
        Profinite.NobelingProof.factors C s x
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
TopologicalSpace.PositiveCompacts.mk.congr_simp : ∀ {α : Type u_4} [inst : TopologicalSpace α] (toCompacts toCompacts_1 : TopologicalSpace.Compacts α)
  (e_toCompacts : toCompacts = toCompacts_1) (interior_nonempty' : (interior toCompacts.carrier).Nonempty),
  { toCompacts := toCompacts, interior_nonempty' := interior_nonempty' } =
    { toCompacts := toCompacts_1, interior_nonempty' := ⋯ }
-- Mathlib.GroupTheory.PGroup
IsPGroup.dvd_orderOf : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)], IsPGroup p G → ∀ {g : G}, g ≠ 1 → p ∣ orderOf g
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.one_def : ∀ {α : Type u_2} [inst : NonUnitalNonAssocSemiring α], 1 = NonUnitalRingHom.id α
-- Std.Tactic.Do.Syntax
/-- Like `intro`, but introducing stateful hypotheses into the stateful context of the `Std.Do.SPred`
proof mode.
That is, given a stateful goal `(hᵢ : Hᵢ)* ⊢ₛ P → T`, `mintro h` transforms
into `(hᵢ : Hᵢ)*, (h : P) ⊢ₛ T`.

Furthermore, `mintro ∀s` is like `intro s`, but preserves the stateful goal.
That is, `mintro ∀s` brings the topmost state variable `s:σ` in scope and transforms
`(hᵢ : Hᵢ)* ⊢ₛ T` (where the entailment is in `Std.Do.SPred (σ::σs)`) into
`(hᵢ : Hᵢ s)* ⊢ₛ T s` (where the entailment is in `Std.Do.SPred σs`).

Beyond that, `mintro` supports the full syntax of `mcases` patterns
(`mintro pat = (mintro h; mcases h with pat`), and can perform multiple
introductions in sequence.
 -/
Lean.Parser.Tactic.mintroError : Lean.ParserDescr
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.add_lt_left_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommMonoid M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {a b : M} (c : M), a < b ↔ a + c < b + c
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegular], μ.InnerRegularCompactLTTop
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- If a sequence of functions is uniformly Cauchy on a set, then the values at each point form
a Cauchy sequence.  See `UniformCauchySeqOn.cauchy_map` for the non-`atTop` case.  -/
UniformCauchySeqOn.cauchySeq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {x : α} [Nonempty ι]
  [inst_2 : SemilatticeSup ι], UniformCauchySeqOn F Filter.atTop s → x ∈ s → CauchySeq fun i => F i x
-- Mathlib.ModelTheory.DirectLimit
/-- The canonical map from a component to the direct limit.  -/
FirstOrder.Language.DirectLimit.of : (L : FirstOrder.Language) →
  (ι : Type v) →
    [inst : Preorder ι] →
      (G : ι → Type w) →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) →
            [inst_2 : IsDirectedOrder ι] →
              [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] →
                [inst_4 : Nonempty ι] → (i : ι) → L.Embedding (G i) (FirstOrder.Language.DirectLimit G f)
-- Mathlib.Algebra.AlgebraicCard
Algebraic.cardinalMk_lift_le_mul : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing A] [IsDomain A] [inst_4 : Algebra R A]
  [Module.IsTorsionFree R A],
  Cardinal.lift.{u, v} (Cardinal.mk { x // IsAlgebraic R x }) ≤
    Cardinal.lift.{v, u} (Cardinal.mk (Polynomial R)) * Cardinal.aleph0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightComp_inv_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ R₃ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (hr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r'.app X.right)))
  (hrr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom ((CategoryTheory.CategoryStruct.comp r r').app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightComp L r r' hr hr' hrr').inv.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equation_iff : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R),
  W'.Equation P ↔
    P 1 ^ 2 * P 2 + W'.a₁ * P 0 * P 1 * P 2 + W'.a₃ * P 1 * P 2 ^ 2 -
        (P 0 ^ 3 + W'.a₂ * P 0 ^ 2 * P 2 + W'.a₄ * P 0 * P 2 ^ 2 + W'.a₆ * P 2 ^ 3) =
      0
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.instInhabitedMethods : Inhabited Lean.Meta.Sym.DSimp.Methods
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.h1Cotangentι_ext_iff : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {x y : P.H1Cotangent}, x = y ↔ ↑x = ↑y
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.inv : ∀ {G : Type u_3} [inst : DivisionCommMonoid G] {k : ℕ} {ζ : G}, IsPrimitiveRoot ζ k → IsPrimitiveRoot ζ⁻¹ k
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₂ → (m₁ \ m₂).get! k = m₁.get! k
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f g : X ⟶ Y} (self : P.RightHomotopy f g) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.h (CategoryTheory.CategoryStruct.comp P.p₀ h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_le_enum' : ∀ (a : Ordinal.{u_1}) {o₁ o₂ : ↑(Set.Iio (Ordinal.type fun x1 x2 => x1 < x2))},
  (Ordinal.enum fun x1 x2 => x1 < x2) o₁ ≤ (Ordinal.enum fun x1 x2 => x1 < x2) o₂ ↔ o₁ ≤ o₂
-- Mathlib.Data.Seq.Defs
/-- Sets the value of sequence `s` at index `n` to `a`. If the `n`th element does not exist
(`s` terminates earlier), the sequence is left unchanged.  -/
Stream'.Seq.set : {α : Type u} → Stream'.Seq α → ℕ → α → Stream'.Seq α
-- Init.Data.BitVec.Lemmas
BitVec.reverse.eq_2 : ∀ (w : ℕ) (x_2 : BitVec (w + 1)), x_2.reverse = (BitVec.truncate w x_2).reverse.concat x_2.msb
-- Mathlib.CategoryTheory.Action.Continuous
CategoryTheory.Functor.mapContActionComp_hom : ∀ {V : Type u_5} {W : Type u_6} [inst : CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7}
  {CV : V → Type u_8} [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
  [inst_2 : CategoryTheory.ConcreteCategory V FV] [inst_3 : CategoryTheory.HasForget₂ V TopCat]
  [inst_4 : CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10}
  [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [inst_6 : CategoryTheory.ConcreteCategory W FW]
  [inst_7 : CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [inst_8 : Monoid G] [inst_9 : TopologicalSpace G]
  {T : Type u_12} [inst_10 : CategoryTheory.Category.{v_4, u_12} T] {FT : T → T → Type u_13} {CT : T → Type u_14}
  [inst_11 : (X Y : T) → FunLike (FT X Y) (CT X) (CT Y)] [inst_12 : CategoryTheory.ConcreteCategory T FT]
  [inst_13 : CategoryTheory.HasForget₂ T TopCat] (F : CategoryTheory.Functor V W)
  (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (F' : CategoryTheory.Functor W T)
  (H' : ∀ (X : ContAction W G), ((F'.mapAction G).obj X.obj).IsContinuous),
  (CategoryTheory.Functor.mapContActionComp G F H F' H').hom =
    { app := fun X => CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mapContAction G (F.comp F') ⋯).obj X),
      naturality := ⋯ }
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f : Option (β k) → Option (β k)),
  Std.DTreeMap.Internal.Impl.alter! k f Std.DTreeMap.Internal.Impl.leaf =
    match f none with
    | none => Std.DTreeMap.Internal.Impl.leaf
    | some v => Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.Algebra.Group.Basic
div_div_div_eq : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c d : α), a / b / (c / d) = a * d / (b * c)
-- Lean.Meta.Tactic.Simp.Simproc
/-- This global reference is populated using the command `builtin_simproc_pattern%`.

This reference is then used to process the attributes `builtin_simproc` and `builtin_sevalproc`.
Both attributes need the keys and the actual procedure registered using the command `builtin_simproc_pattern%`.
 -/
Lean.Meta.Simp.builtinSimprocDeclsRef : IO.Ref Lean.Meta.Simp.BuiltinSimprocs
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_def_zero : ∀ (x : ZMod 0), x.valMinAbs = x
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.instMonoidalExtendScalars : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (f : R →+* S) → (ModuleCat.extendScalars f).Monoidal
-- Init.Data.BEq
BEq.neq_of_neq_of_beq : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {a b c : α}, (a == b) = false → (b == c) = true → (a == c) = false
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.succ_mod_two : ∀ {x : ℕ}, x.succ % 2 = 1 - x % 2
-- Mathlib.RingTheory.Valuation.Basic
/-- The type of `Γ₀`-valued additive valuations on `R`.  -/
AddValuation : (R : Type u_3) → [Ring R] → (Γ₀ : Type u_4) → [LinearOrderedAddCommMonoidWithTop Γ₀] → Type (max u_3 u_4)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.himp_mono : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P P' Q Q' : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel Q P →
    Lean.Order.PartialOrder.rel P' Q' → Lean.Order.PartialOrder.rel (Lean.Order.himp P P') (Lean.Order.himp Q Q')
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Real.measureSpace : MeasureTheory.MeasureSpace ℝ
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMul.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Mul (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)],
  DirectLimit.instMul = { mul := DirectLimit.map₂ f f f (fun x x1 x2 => x1 * x2) ⋯ }
-- Mathlib.Algebra.Star.Conjneg
sum_conjneg : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] [inst_3 : Fintype G]
  (f : G → R), ∑ a, conjneg f a = ∑ a, (starRingEnd R) (f a)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded, subadditive function, then
`seminormFromBounded' f` is subadditive.  -/
seminormFromBounded_add : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f →
    (∀ (x y : R), f (x * y) ≤ c * f x * f y) →
      (∀ (a b : R), f (a + b) ≤ f a + f b) →
        ∀ (x y : R), seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGT_iff_getElem_gt_getElem_of_lt`. -/
List.sortedGT_of_getElem_gt_getElem_of_lt : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  (∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j < i → l[i] < l[j]) → l.SortedGT
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.brecOn_1.eq : ∀ {motive_1 : Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u}
  {motive_2 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u}
  {motive_3 : List (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u}
  {motive_4 : String × Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u}
  (t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝))
  (F_1 : (t : Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below✝ t → motive_1 t)
  (F_2 :
    (t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)) → Lean.Elab.ConfigEval.HandlerTrie.below_1✝ t → motive_2 t)
  (F_3 :
    (t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝)) → Lean.Elab.ConfigEval.HandlerTrie.below_2✝ t → motive_3 t)
  (F_4 : (t : String × Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below_3✝ t → motive_4 t),
  Lean.Elab.ConfigEval.HandlerTrie.brecOn_1✝ t F_1 F_2 F_3 F_4 =
    F_2 t (Lean.Elab.ConfigEval.HandlerTrie.brecOn_1.go✝ t F_1 F_2 F_3 F_4).2
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.isLower_orderDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α], Topology.IsLower αᵒᵈ ↔ Topology.IsUpper α
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_doubleL : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rk : α) (rv : β rk) (rlk : α)
  (rlv : β rlk) (rll rlr rr : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.doubleL k v l rk rv rlk rlv rll rlr rr).size =
    (Std.DTreeMap.Internal.Impl.bin k v l
        (Std.DTreeMap.Internal.Impl.bin rk rv (Std.DTreeMap.Internal.Impl.bin rlk rlv rll rlr) rr)).size
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.elabSimpConfigAux.evalConfigItem : (Lean.Term → Lean.Elab.TermElabM Lean.Meta.Simp.Config) →
  Lean.Elab.ConfigEval.EvalConfigItem Lean.Meta.Simp.ConfigWithOptions
-- Lean.Declaration
Lean.InductiveVal.isNested : Lean.InductiveVal → Bool
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousWithinAt.nnnorm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α}
  {a : α}, ContinuousWithinAt f s a → ContinuousWithinAt (fun x => ‖f x‖₊) s a