mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalState.mk.inj : ∀ {nextDeclIdx : ℕ} {enodeMap : Lean.Meta.Grind.ENodeMap} {exprs : Lean.PArray Lean.Expr}
  {parents : Lean.Meta.Grind.ParentMap} {congrTable : Lean.Meta.Grind.CongrTable enodeMap}
  {appMap : Lean.PHashMap Lean.HeadIndex (List Lean.Expr)} {indicesFound : Lean.PHashSet Lean.HeadIndex}
  {newFacts : Array Lean.Meta.Grind.NewFact} {inconsistent : Bool} {nextIdx : ℕ}
  {newRawFacts : Std.Queue Lean.Meta.Grind.NewRawFact} {facts : Lean.PArray Lean.Expr}
  {extThms : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Array Lean.Meta.Ext.ExtTheorem)}
  {ematch : Lean.Meta.Grind.EMatch.State} {inj : Lean.Meta.Grind.Injective.State} {split : Lean.Meta.Grind.Split.State}
  {clean : Lean.Meta.Grind.Clean.State} {sstates : Array Lean.Meta.Grind.SolverExtensionState} {nextDeclIdx_1 : ℕ}
  {enodeMap_1 : Lean.Meta.Grind.ENodeMap} {exprs_1 : Lean.PArray Lean.Expr} {parents_1 : Lean.Meta.Grind.ParentMap}
  {congrTable_1 : Lean.Meta.Grind.CongrTable enodeMap_1} {appMap_1 : Lean.PHashMap Lean.HeadIndex (List Lean.Expr)}
  {indicesFound_1 : Lean.PHashSet Lean.HeadIndex} {newFacts_1 : Array Lean.Meta.Grind.NewFact} {inconsistent_1 : Bool}
  {nextIdx_1 : ℕ} {newRawFacts_1 : Std.Queue Lean.Meta.Grind.NewRawFact} {facts_1 : Lean.PArray Lean.Expr}
  {extThms_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Array Lean.Meta.Ext.ExtTheorem)}
  {ematch_1 : Lean.Meta.Grind.EMatch.State} {inj_1 : Lean.Meta.Grind.Injective.State}
  {split_1 : Lean.Meta.Grind.Split.State} {clean_1 : Lean.Meta.Grind.Clean.State}
  {sstates_1 : Array Lean.Meta.Grind.SolverExtensionState},
  { nextDeclIdx := nextDeclIdx, enodeMap := enodeMap, exprs := exprs, parents := parents, congrTable := congrTable,
        appMap := appMap, indicesFound := indicesFound, newFacts := newFacts, inconsistent := inconsistent,
        nextIdx := nextIdx, newRawFacts := newRawFacts, facts := facts, extThms := extThms, ematch := ematch,
        inj := inj, split := split, clean := clean, sstates := sstates } =
      { nextDeclIdx := nextDeclIdx_1, enodeMap := enodeMap_1, exprs := exprs_1, parents := parents_1,
        congrTable := congrTable_1, appMap := appMap_1, indicesFound := indicesFound_1, newFacts := newFacts_1,
        inconsistent := inconsistent_1, nextIdx := nextIdx_1, newRawFacts := newRawFacts_1, facts := facts_1,
        extThms := extThms_1, ematch := ematch_1, inj := inj_1, split := split_1, clean := clean_1,
        sstates := sstates_1 } →
    nextDeclIdx = nextDeclIdx_1 ∧
      enodeMap = enodeMap_1 ∧
        exprs = exprs_1 ∧
          parents = parents_1 ∧
            congrTable ≍ congrTable_1 ∧
              appMap = appMap_1 ∧
                indicesFound = indicesFound_1 ∧
                  newFacts = newFacts_1 ∧
                    inconsistent = inconsistent_1 ∧
                      nextIdx = nextIdx_1 ∧
                        newRawFacts = newRawFacts_1 ∧
                          facts = facts_1 ∧
                            extThms = extThms_1 ∧
                              ematch = ematch_1 ∧ inj = inj_1 ∧ split = split_1 ∧ clean = clean_1 ∧ sstates = sstates_1
-- Mathlib.Lean.Json
Lean.instFromJsonSubtypeOfDecidablePred_mathlib : {α : Type u} → [Lean.FromJson α] → (p : α → Prop) → [DecidablePred p] → Lean.FromJson (Subtype p)
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.comp_assoc : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P]
  [inst_3 : Add Q] (f : M →ₙ+ N) (g : N →ₙ+ P) (h : P →ₙ+ Q), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.notMem_of_notMem_closure : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {P : M}, P ∉ AddSubsemigroup.closure s → P ∉ s
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Hom.instModule : {R : Type u} →
  [inst : Semiring R] →
    {M N : SemimoduleCat R} →
      {S : Type u_1} → [inst_1 : Semiring S] → [inst_2 : Module S ↑N] → [SMulCommClass R S ↑N] → Module S (M ⟶ N)
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.curry_apply_cons : ∀ {n : ℕ} {α : Type u} {p : Fin n → Type u} {τ : Type u} (f : ((i : Fin (n + 1)) → Matrix.vecCons α p i) → τ) (a : α),
  Function.FromTypes.curry f a = Function.FromTypes.curry ((fun {x} => f) ∘' Fin.cons a)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} {x' y' : C} (f : x ⟶ y) (g : x' ⟶ y')
  [CategoryTheory.IsIso f] [CategoryTheory.IsIso g],
  CategoryTheory.IsIso (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g)
-- Mathlib.Control.Traversable.Lemmas
Traversable.map_traverse : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] {α β γ : Type u} (g : α → F β) (f : β → γ) (x : t α),
  Functor.map f <$> traverse g x = traverse (Functor.map f ∘ g) x
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.map_smulₑ : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B] (f : A →ₑ+[φ] B)
  (m : M) (x : A), f (m • x) = φ m • f x
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalDbgTrace : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The right whiskering of a 2-isomorphism is a 2-isomorphism.  -/
CategoryTheory.Bicategory.whiskerRightIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f g : a ⟶ b} →
        (f ≅ g) → (h : b ⟶ c) → CategoryTheory.CategoryStruct.comp f h ≅ CategoryTheory.CategoryStruct.comp g h
-- Init.Data.UInt.Lemmas
UInt16.ofFin_toFin : ∀ (n : UInt16), UInt16.ofFin n.toFin = n
-- Mathlib.Order.Interval.Basic
/-- The injection that induces the order on intervals.  -/
NonemptyInterval.toDualProd : {α : Type u_1} → [inst : LE α] → NonemptyInterval α → αᵒᵈ × α
-- Mathlib.Algebra.Torsor.Basic
/-- The same point subtracted from two points produces equal results
if and only if those points are equal.  -/
vsub_left_cancel_iff : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ p : P}, p₁ -ᵥ p = p₂ -ᵥ p ↔ p₁ = p₂
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_inter : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (S R : CategoryTheory.Sieve (F.obj X)),
  CategoryTheory.Sieve.functorPullback F (S ⊓ R) =
    CategoryTheory.Sieve.functorPullback F S ⊓ CategoryTheory.Sieve.functorPullback F R
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCancelCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CancelCommMonoid α],
  Colex.instCancelCommMonoid = { toCommMonoid := Colex.instCommMonoid, toIsLeftCancelMul := ⋯ }
-- Init.RCases
/-- `-` is a pattern which removes the value from the context  -/
Lean.Parser.Tactic.rcasesPat.clear : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.MonoFactorisation.kernel_ι_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] (F : CategoryTheory.Limits.MonoFactorisation f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) F.e = 0
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.prodMulEquiv_symm_apply : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (A : Subgroup G) (B : Subgroup H) [inst_2 : A.Normal]
  [inst_3 : B.Normal] (q : (G ⧸ A) × H ⧸ B),
  (QuotientGroup.prodMulEquiv A B).symm q = Quotient.liftOn₂' q.1 q.2 (fun g h => ↑(g, h)) ⋯
-- Mathlib.Order.Birkhoff
OrderEmbedding.birkhoffFinset_inf : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Fintype α] [inst_2 : DecidablePred SupIrred]
  [inst_3 : DecidableEq α] (a b : α),
  OrderEmbedding.birkhoffFinset (a ⊓ b) = OrderEmbedding.birkhoffFinset a ∩ OrderEmbedding.birkhoffFinset b
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.coe_comp : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {V₃ : Type u_6} {P : Type u_10} {P₂ : Type u_11} {P₃ : Type u_12}
  [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] [inst_9 : SeminormedAddCommGroup V₃]
  [inst_10 : NormedSpace 𝕜 V₃] [inst_11 : PseudoMetricSpace P₃] [inst_12 : NormedAddTorsor V₃ P₃] (g : P₂ →ᵃⁱ[𝕜] P₃)
  (f : P →ᵃⁱ[𝕜] P₂), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.natDegree_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.Monic → q.Monic → (p * q).natDegree = p.natDegree + q.natDegree
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.unop_normalizer : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup Gᵐᵒᵖ), (Subgroup.normalizer ↑H).unop = Subgroup.normalizer ↑H.unop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.hp₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  (h : CategoryTheory.Limits.ChosenPullback f₁ f₂) {Z : C} (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₂ (CategoryTheory.CategoryStruct.comp f₂ h_1) =
    CategoryTheory.CategoryStruct.comp h.p h_1
-- Mathlib.ModelTheory.Order
FirstOrder.Language.orderLHom_leSymb : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered],
  L.orderLHom.onRelation FirstOrder.Language.leSymb = FirstOrder.Language.leSymb
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddHaarMeasure.domSMul : ∀ {G : Type u_3} {A : Type u_4} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : MeasurableSpace A] [inst_4 : TopologicalSpace A] [inst_5 : BorelSpace A] [IsTopologicalAddGroup A]
  [inst_7 : ContinuousConstSMul G A] {μ : MeasureTheory.Measure A} [μ.IsAddHaarMeasure] (g : Gᵈᵐᵃ),
  (g • μ).IsAddHaarMeasure
-- Mathlib.SetTheory.Cardinal.Regular
/-- **Alias** of `Cardinal.IsRegular.cof_ord`. -/
Cardinal.IsRegular.cof_eq : ∀ {c : Cardinal.{u_1}}, c.IsRegular → c.ord.cof = c
-- Batteries.Data.Char.AsciiCasing
Char.toLower_eq_of_isUpper : ∀ {c : Char}, c.isUpper = true → c.toLower = Char.ofNat (c.toNat + 32)
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Ioc_update_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : DecidableEq ι] {x y : (i : ι) → α i}
  {i₀ : ι} {m : α i₀},
  m ≤ y i₀ →
    (Set.univ.pi fun i => Set.Ioc (x i) (Function.update y i₀ m i)) =
      {z | z i₀ ≤ m} ∩ Set.univ.pi fun i => Set.Ioc (x i) (y i)
-- Lean.Server.References
/-- Direct imports of the module of this ILean.  -/
Lean.Server.LoadedILean.directImports : Lean.Server.LoadedILean → Lean.Server.DirectImports
-- Init.Data.UInt.Bitwise
UInt8.toFin_xor : ∀ (a b : UInt8), (a ^^^ b).toFin = a.toFin ^^^ b.toFin
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.reverse_eq_id : CliffordAlgebra.reverse = LinearMap.id
-- Mathlib.Algebra.Group.Prod
MonoidHom.prod_comp_prodMap : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Type u_6}
  {N' : Type u_7} [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] [inst_4 : MulOneClass P] (f : P →* M) (g : P →* N)
  (f' : M →* M') (g' : N →* N'), (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
-- Init.Data.UInt.Bitwise
USize.xor_neg_one : ∀ {a : USize}, a ^^^ -1 = ~~~a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.instDecidableNil : {V : Type u} → {G : SimpleGraph V} → {v w : V} → (p : G.Walk v w) → Decidable p.Nil
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The comultiplication 2-morphism of the comonad.  -/
CategoryTheory.Bicategory.termΔ : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (C : G.ConnectedComponent),
  C.toSimpleGraph.spanningCoe.Adj v w ↔ v ∈ C.supp ∧ G.Adj v w
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceLE : Lean.Meta.Simp.Simproc
-- Lean.Elab.Command
Lean.Elab.Command.ModuleLinter.mk : (Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit) →
  autoParam Lean.Name Lean.Elab.Command.ModuleLinter.name._autoParam → Lean.Elab.Command.ModuleLinter
-- Mathlib.Algebra.Category.Grp.Limits
/-- The projection from `Functor.sections` to a factor as an `AddMonoidHom`.  -/
AddGrpCat.sectionsπAddMonoidHom : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddGrpCat) →
      (j : J) → ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections →+ ↑(F.obj j)
-- Mathlib.Algebra.Group.Prod
/-- `Prod.map` as an `AddMonoidHom`.  -/
AddMonoidHom.prodMap : {M : Type u_3} →
  {N : Type u_4} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {M' : Type u_6} →
          {N' : Type u_7} →
            [inst_2 : AddZeroClass M'] → [inst_3 : AddZeroClass N'] → (M →+ M') → (N →+ N') → M × N →+ M' × N'
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_finsupp_nat : ∀ (α : Type u) [Nonempty α], Cardinal.mk (α →₀ ℕ) = max (Cardinal.mk α) Cardinal.aleph0
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- The `i`-th horn `Λ[n, i]` of the standard `n`-simplex  -/
Simplicial.«termΛ[_,_]» : Lean.ParserDescr
-- Mathlib.Order.SymmDiff
symmDiff_bot : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a : α), symmDiff a ⊥ = a
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_mapId : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory B]
  [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] [inst_2 : CategoryTheory.Bicategory C] (obj : B → C)
  (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h))
              (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) =
          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h))
              (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom))
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁))
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_5)
  (b : B),
  (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).mapId
      b =
    mapId b
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_pos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}, 0 < a⁻¹ ↔ 0 < a
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- The ordered finpartition of `Fin n` into singletons.  -/
OrderedFinpartition.atomic : (n : ℕ) → OrderedFinpartition n
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.brecOn.go : {R : Type u} →
  [inst : Rack R] →
    {motive : (a a_1 : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R a a_1 → Sort u_1} →
      {a a_1 : Rack.PreEnvelGroup R} →
        (t : Rack.PreEnvelGroupRel' R a a_1) →
          ((a a_2 : Rack.PreEnvelGroup R) →
              (t : Rack.PreEnvelGroupRel' R a a_2) → Rack.PreEnvelGroupRel'.below t → motive a a_2 t) →
            motive a a_1 t ×' Rack.PreEnvelGroupRel'.below t
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.mk : ∀ {G : Type u_1} {α : Type u_2} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : autoParam (MeasureTheory.Measure α) MeasureTheory.IsAddFundamentalDomain._auto_1},
  MeasureTheory.NullMeasurableSet s μ →
    (∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s) →
      Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => g +ᵥ s) →
        MeasureTheory.IsAddFundamentalDomain G s μ
-- Mathlib.Probability.Kernel.Basic
/-- The restriction of a constant kernel to a measurable set is equal
to the constant kernel of the restricted measure.  -/
ProbabilityTheory.Kernel.restrict_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β}
  {μ : MeasureTheory.Measure β} (hs : MeasurableSet s),
  (ProbabilityTheory.Kernel.const α μ).restrict hs = ProbabilityTheory.Kernel.const α (μ.restrict s)
-- Mathlib.Data.Setoid.Partition
IndexedPartition.index_some : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (i : ι), hs.index (hs.some i) = i
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The preimage of a subfield along a ring homomorphism is a subfield.  -/
Subfield.comap : {K : Type u} → {L : Type v} → [inst : DivisionRing K] → [inst_1 : DivisionRing L] → (K →+* L) → Subfield L → Subfield K
-- Mathlib.Control.Fold
Traversable.foldlm : {α β : Type u} →
  {t : Type u → Type u} → [Traversable t] → {m : Type u → Type u} → [Monad m] → (α → β → m α) → α → t β → m α
-- Mathlib.FieldTheory.FinTrdeg
/-- **Alias** of the reverse direction of `finTrdeg_iff_trdeg`. -/
FinTrdeg.of_trdeg : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  Algebra.trdeg K L < Cardinal.aleph0 → FinTrdeg K L
-- Mathlib.Tactic.Linarith.Verification
/-- `proveEqZeroUsing tac e` tries to use `tac` to construct a proof of `e = 0`.
 -/
Mathlib.Tactic.Linarith.proveEqZeroUsing : Lean.Elab.Tactic.TacticM Unit → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Vector.DecidableEq
Vector.isEqv_iff_rel : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n} {r : α → α → Bool},
  xs.isEqv ys r = true ↔ ∀ (i : ℕ) (h' : i < n), r xs[i] ys[i] = true
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.beq : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.beq m₂ = true
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- This is only `inferInstance` because of the `@[local instance]` on `HasAffineProperty` above.  -/
AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q], AlgebraicGeometry.IsZariskiLocalAtTarget P
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.cofilteredClosure.brecOn : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsCofiltered.cofilteredClosure f a → Prop} {a : C}
  (t : CategoryTheory.IsCofiltered.cofilteredClosure f a),
  (∀ (a : C) (t : CategoryTheory.IsCofiltered.cofilteredClosure f a),
      CategoryTheory.IsCofiltered.cofilteredClosure.below t → motive a t) →
    motive a t
-- Init.Data.UInt.Lemmas
UInt64.ofFin_lt_iff_lt : ∀ {a b : Fin UInt64.size}, UInt64.ofFin a < UInt64.ofFin b ↔ a < b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : AffineSubspace k P},
  s₁.Parallel s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_image2_eq_csSup_csSup : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
  {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
    (∀ (a : α), GaloisConnection (l a) (u₂ a)) →
      s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sSup (Set.image2 l s t) = l (sSup s) (sSup t)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_le_rpow : ∀ {x y : ENNReal} {z : ℝ}, x ≤ y → 0 ≤ z → x ^ z ≤ y ^ z
-- Aesop.Script.StructureStatic
Aesop.Script.UScript.toSScriptStatic : Aesop.Script.TacticState → Aesop.Script.UScript → Lean.CoreM (Aesop.Script.SScript × Bool)
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.PenroseVar.mk.injEq : ∀ (ident : String) (indices : List ℕ) (e : Lean.Expr) (ident_1 : String) (indices_1 : List ℕ) (e_1 : Lean.Expr),
  ({ ident := ident, indices := indices, e := e } = { ident := ident_1, indices := indices_1, e := e_1 }) =
    (ident = ident_1 ∧ indices = indices_1 ∧ e = e_1)
-- Mathlib.Topology.Order
induced_mono : ∀ {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {g : β → α},
  t₁ ≤ t₂ → TopologicalSpace.induced g t₁ ≤ TopologicalSpace.induced g t₂
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.enlarge.eq_1 : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) (δ : ℝ) (δpos : 0 < δ),
  v.enlarge δ δpos =
    { setsAt := fun x => v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ Metric.closedBall x δ},
      measurableSet := ⋯, nonempty_interior := ⋯, nontrivial := ⋯, covering := ⋯ }
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.val_ofNSMulEqZero : ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (n : ℕ) (ha : n • a = 0) (hn : n ≠ 0),
  ↑(AddUnits.ofNSMulEqZero a n ha hn) = a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edges_injective : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, Function.Injective SimpleGraph.Walk.edges
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.instInfinite : ∀ (α : Type u_1) (n : ℕ) [NeZero n] [Infinite α], Infinite ↑(Set.powersetCard α n)
-- Mathlib.Algebra.Polynomial.Splits
IsUnit.splits : ∀ {R : Type u_1} [inst : Semiring R] [NoZeroDivisors R] {f : Polynomial R}, IsUnit f → f.Splits
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.alternatizeUncurryFin_curryLeft : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E [⋀^Fin (n + 1)]→L[𝕜] F), ContinuousAlternatingMap.alternatizeUncurryFin f.curryLeft = (n + 1) • f
-- Aesop.RuleTac.Descr
Aesop.instInhabitedRuleTacDescr : Inhabited Aesop.RuleTacDescr