mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- If `F` creates finite colimits in any universe, then it creates finite colimits.  -/
CategoryTheory.Limits.createsFiniteColimitsOfCreatesFiniteColimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          ((J : Type w) →
              {x : CategoryTheory.SmallCategory J} →
                CategoryTheory.FinCategory J → CategoryTheory.CreatesColimitsOfShape J F) →
            CategoryTheory.Limits.CreatesFiniteColimits F
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.lowerBound?_greatest_lb : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} {lb : Option α} {x y : α}
  [Std.TransCmp cmp] [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.Ordered cmp t →
    (∀ {x : α}, lb = some x → RBTree.RBNode.All (fun x_1 => RBTree.RBNode.cmpLT cmp x x_1) t) →
      RBTree.RBNode.lowerBound? cut t lb = some x →
        y ∈ t → cut x = Ordering.gt → cmp x y = Ordering.lt → cut y = Ordering.lt
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_forall : ∀ {σs : List (Type u)} {α : Sort u_1} {φ : α → Prop}, (∀ x, ⌜φ x⌝) ⊣⊢ₛ ⌜∀ (x : α), φ x⌝
-- Lean.Meta.Basic
Lean.Meta.FunInfo.mk : Array Lean.Meta.ParamInfo → Array ℕ → Lean.Meta.FunInfo
-- Std.Do.SPred.SVal
/-- A projection from the types `σs` of type `σ`.  -/
Std.Do.SVal.GetTy.get : {σ : Type u} → {σs : List (Type u)} → [self : Std.Do.SVal.GetTy σ σs] → Std.Do.SVal σs σ
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.coe_aevalAeval_eq_evalEval : ∀ {A : Type u_2} [inst : CommSemiring A] (x y : A), ⇑(Polynomial.aevalAeval x y) = Polynomial.evalEval x y
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
/-- The Sigmoid function as an `OrderEmbedding` from `ℝ` to `I`.  -/
OrderEmbedding.sigmoid : ℝ ↪o ↑unitInterval
-- Mathlib.CategoryTheory.Sites.Continuous
/-- `Functor.IsContinuous` is preserved under enlarging the universe if the starting
universe is large enough. SGA 4 III 1.5.  -/
_private.Mathlib.CategoryTheory.Sites.Continuous.0.CategoryTheory.Functor.isSheaf_of_isContinuous_aux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (G : CategoryTheory.Functor Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))),
  CategoryTheory.Presieve.IsSheaf K G → CategoryTheory.Presieve.IsSheaf J (F.op.comp G)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.leadingNode.parenthesizer : Lean.SyntaxNodeKind → ℕ → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoX₂_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hf : S.f = 0),
  CategoryTheory.CategoryStruct.comp (S.opcyclesIsoX₂ hf).hom S.pOpcycles = CategoryTheory.CategoryStruct.id S.opcycles
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_zero_eq_sum : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R] (n : ℕ), arithGeom a b 0 n = b * ∑ k ∈ Finset.range n, a ^ k
-- Init.Data.Slice.List.Lemmas
ListSlice.size_mkSlice_rci : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.size (Std.Rci.Sliceable.mkSlice xs lo...*) = Std.Slice.size xs - lo
-- Lean.Message
Lean.instToJsonBaseMessage : {α : Type u_1} → [Lean.ToJson α] → Lean.ToJson (Lean.BaseMessage α)
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_source'' : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  (e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coe_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (f g : MonoidAlgebra R M), ⇑(f + g).coeff = ⇑f.coeff + ⇑g.coeff
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.ext : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {f g : X →ₑ[φ] Y}, (∀ (x : X), f x = g x) → f = g
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyLift_unique : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q)
  (γ : CategoryTheory.sheafify J P ⟶ Q),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) γ = η → γ = CategoryTheory.sheafifyLift J η hQ
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mem_support_coeff_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {m : Fin n →₀ ℕ},
  m ∈ (((MvPolynomial.finSuccEquiv R n) f).coeff i).support ↔ Finsupp.cons i m ∈ f.support
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instSMulℝ : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} → {α : Type u_1} → [inst : SMul α ℝ] → [inst_1 : SMul α ℂ] → [IsScalarTower α ℝ ℂ] → SMul α (ModularForm Γ k)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.dischargeDepth : Lean.Meta.Simp.Context → UInt32
-- Mathlib.Algebra.Ring.Nat
Nat.instSemiring : Semiring ℕ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqResolvableCompletionItem : BEq Lean.Lsp.ResolvableCompletionItem
-- Init.Data.String.Lemmas.Iterate
String.forIn_eq_forIn_chars : ∀ {β : Type u} {m : Type u → Type v} [inst : Monad m] {s : String} {b : β} {f : Char → β → m (ForInStep β)},
  forIn s b f = forIn s.chars b f
-- Init.Omega.Coeffs
/-- Type synonym for `IntList := List Int`.  -/
Lean.Omega.Coeffs : Type
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
/-- Interpret `n`-th roots of unity in `ℂ` as elements of the circle  -/
rootsOfUnitytoCircle : (n : ℕ) → [NeZero n] → ↥(rootsOfUnity n ℂ) →* Circle
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
CategoryTheory.Limits.pointwiseBinaryBicone_fst_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  (F G : CategoryTheory.Functor D C) (X : D),
  (CategoryTheory.Limits.pointwiseBinaryBicone F G).fst.app X = CategoryTheory.Limits.biprod.fst
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalBool_qq : Lean.Meta.ReduceEval Bool
-- Batteries.Data.UnionFind.Basic
/-- Link two union-find nodes, uniting their respective classes.
Panics if either index is out of bounds.  -/
Batteries.UnionFind.union! : Batteries.UnionFind → ℕ → ℕ → Batteries.UnionFind
-- Mathlib.Algebra.Module.Defs
/-- Pushforward a `Module` structure along a surjective additive monoid homomorphism.
See note [reducible non-instances].  -/
Function.Surjective.module : (R : Type u_1) →
  {M : Type u_3} →
    {M₂ : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid M₂] →
              [inst_4 : SMul R M₂] →
                (f : M →+ M₂) → Function.Surjective ⇑f → (∀ (c : R) (x : M), f (c • x) = c • f x) → Module R M₂
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
volume_regionBetween_eq_lintegral' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {s : Set α},
  Measurable f →
    Measurable g →
      MeasurableSet s →
        (μ.prod MeasureTheory.volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ENNReal.ofReal ((g - f) y) ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.whiskerRight_id_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  {Z : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (h : ψ'.comp (CategoryTheory.Limits.CatCospanTransform.id F' G') ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η
        (CategoryTheory.Limits.CatCospanTransform.id F' G'))
      h =
    CategoryTheory.CategoryStruct.comp ψ.rightUnitor.hom
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp ψ'.rightUnitor.inv h))
-- Aesop.Forward.State
Aesop.ClusterState.AddM.Context.mk.injEq : ∀ (premiseMVars : Array Lean.MVarId) (premiseLMVars : Array Lean.LMVarId) (premiseMVars_1 : Array Lean.MVarId)
  (premiseLMVars_1 : Array Lean.LMVarId),
  ({ premiseMVars := premiseMVars, premiseLMVars := premiseLMVars } =
      { premiseMVars := premiseMVars_1, premiseLMVars := premiseLMVars_1 }) =
    (premiseMVars = premiseMVars_1 ∧ premiseLMVars = premiseLMVars_1)
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.comp_apply : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {P : Type u_3} [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P} {R : Type u_10} [inst_3 : Semiring R] [inst_4 : MulSemiringAction M R] {S : Type u_12}
  [inst_5 : Semiring S] [inst_6 : MulSemiringAction N S] {T : Type u_14} [inst_7 : Semiring T]
  [inst_8 : MulSemiringAction P T] (g : S →ₑ+*[ψ] T) (f : R →ₑ+*[φ] S) [inst_9 : φ.CompTriple ψ χ] (x : R),
  (g.comp f) x = g (f x)
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession.mk : Lean.Server.RpcObjectStore → ℕ → Lean.Server.FileWorker.RpcSession
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orInL.sizeOf_spec : ∀ (p : Mathlib.Tactic.ITauto.Proof), sizeOf p.orInL = 1 + sizeOf p
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.memLp_finsetSum : ∀ {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] {p : ENNReal} {μ : MeasureTheory.Measure α} [ContinuousAdd ε'] {ι : Type u_5}
  (s : Finset ι) {f : ι → α → ε'},
  (∀ i ∈ s, MeasureTheory.MemLp (f i) p μ) → MeasureTheory.MemLp (fun a => ∑ i ∈ s, f i a) p μ
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.terminal.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] {P : C}
  {f g : P ⟶ ⊤_ C}, f = g ↔ True
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.twoPowShift_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget aig w) (lhs : BitVec w)
  (rhs : BitVec target.n) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < target.n), ⟦assign, { aig := aig, ref := target.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.twoPowShift aig target).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.twoPowShift aig target).vec.get idx hidx }⟧ =
          (lhs <<< (rhs &&& BitVec.twoPow target.n target.pow)).getLsbD idx
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The type `(shrinkCoyoneda.obj X).obj Y` is equivalent to `X.unop ⟶ Y`.  -/
CategoryTheory.shrinkCoyonedaObjObjEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      {X : Cᵒᵖ} → {Y : C} → (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y ≃ (Opposite.unop X ⟶ Y)
-- Mathlib.Computability.Partrec
Computable.decode : ∀ {α : Type u_1} [inst : Primcodable α], Computable Encodable.decode
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.le_order_prod : ∀ {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} (φ : ι → PowerSeries R) (s : Finset ι),
  ∑ i ∈ s, (φ i).order ≤ (∏ i ∈ s, φ i).order
-- Aesop.Forward.State
/-- A map from hypotheses to the rules and premises that they matched against
when they were initially added to the rule state. Invariant: the rule states
in which a hypothesis `h` appear are exactly those identified by the rule
names in `hyps[h]`. Furthermore, `h` only appears in slots with premise
indices greater than or equal to those in `hyps[h]`.  -/
Aesop.ForwardState.hyps : Aesop.ForwardState → Lean.PHashMap Lean.FVarId (Lean.PArray (Aesop.RuleName × Aesop.PremiseIndex))
-- Mathlib.Computability.StateTransition
StateTransition.tr_eval : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop},
  StateTransition.Respects f₁ f₂ tr →
    ∀ {a₁ b₁ : σ₁} {a₂ : σ₂},
      tr a₁ a₂ → b₁ ∈ StateTransition.eval f₁ a₁ → ∃ b₂, tr b₁ b₂ ∧ b₂ ∈ StateTransition.eval f₂ a₂
-- Mathlib.Algebra.Order.Group.PosPart
posPart_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddGroup α] {a b : α}, a⁺ < b ↔ a < b ∧ 0 < b
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_le_of_le_comap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (S : L.Substructure M) {T : L.Substructure N} {f : L.Hom M N},
  S ≤ FirstOrder.Language.Substructure.comap f T → FirstOrder.Language.Substructure.map f S ≤ T
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.delabHtmlElement' : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `proofWidgetsJsxElement)
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacticM.sizeOf_spec : ∀ (decl : Lean.Name), sizeOf (Aesop.RuleTacDescr.tacticM decl) = 1 + sizeOf decl
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.map_embed_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_4)
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f : M →ₗ[R] N) [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S N] {m : M},
  (DividedPowerAlgebra.map S f) ((DividedPowerAlgebra.embed R M) m) = (DividedPowerAlgebra.embed S N) (f m)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : LeftCancelSemigroup α],
  OrderDual.instLeftCancelSemigroup = { toSemigroup := OrderDual.instSemigroup, toIsLeftCancelMul := ⋯ }
-- Init.Data.Order.LemmasExtra
/-- This lemma derives a `LawfulOrderInf α` instance from a property involving an `Ord α` instance.
 -/
Std.LawfulOrderInf.of_ord : ∀ (α : Type u) [inst : Ord α] [inst_1 : Min α] [inst_2 : LE α] [Std.LawfulOrderOrd α],
  (∀ (a b c : α), (compare a (b ⊓ c)).isLE = true ↔ (compare a b).isLE = true ∧ (compare a c).isLE = true) →
    Std.LawfulOrderInf α
-- Mathlib.Order.Category.CompleteLat
CompleteLat.instCoeSortType : CoeSort CompleteLat (Type u_1)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instInhabited.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ContinuousMonoidHom.instInhabited A B = { default := 1 }
-- Mathlib.Probability.StrongLaw
/-- The truncation of `Xᵢ` up to `i` satisfies the strong law of large numbers (with respect to
the truncated expectation) along the sequence `c^n`, for any `c > 1`, up to a given `ε > 0`.
This follows from a variance control.  -/
ProbabilityTheory.strong_law_aux1 : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) MeasureTheory.volume →
    Pairwise (Function.onFun (fun f g => ProbabilityTheory.IndepFun f g MeasureTheory.volume) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) →
        (∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) →
          ∀ {c : ℝ},
            1 < c →
              ∀ {ε : ℝ},
                0 < ε →
                  ∀ᵐ (ω : Ω),
                    ∀ᶠ (n : ℕ) in Filter.atTop,
                      |∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) (↑i) ω -
                            ∫ (a : Ω), (∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) ↑i) a| <
                        ε * ↑⌊c ^ n⌋₊
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSigma.match_1.eq_1 : ∀ (n : ℕ) (f : Fin (n + 1) → ℕ) (motive : (i : Fin n) × Fin (f i.succ) → Sort u_1) (i : ℕ) (hi : i < n)
  (y : Fin (f ⟨i, hi⟩.succ)) (h_1 : (i : ℕ) → (hi : i < n) → (y : Fin (f ⟨i, hi⟩.succ)) → motive ⟨⟨i, hi⟩, y⟩),
  (match ⟨⟨i, hi⟩, y⟩ with
    | ⟨⟨i, hi⟩, y⟩ => h_1 i hi y) =
    h_1 i hi y
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.findCompletionCmdDataAtPos : Lean.Server.FileWorker.EditableDocument →
  String.Pos.Raw → Lean.Server.ServerTask (Option (Lean.Syntax × Lean.Elab.InfoTree))
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The functor which sends `S : SnakeInput C` to the auxiliary object `S.P`,
which is `pullback S.L₁.g S.v₀₁.τ₃`.  -/
CategoryTheory.ShortComplex.SnakeInput.functorP : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) C
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.single_mul_right_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MulZeroClass (α i)] [inst_1 : DecidableEq ι] (i j : ι)
  (f : (i : ι) → α i) (a : α i), Pi.single i (f i * a) j = f j * Pi.single i a j
-- Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
/-- If `f : α →+* β` is bounded with respect to a ring seminorm `nα` on `α` and a
power-multiplicative function `nβ : β → ℝ`, then `∀ x : α, nβ (f x) ≤ nα x`.  -/
contraction_of_isPowMul_of_boundedWrt : ∀ {F : Type u_1} {α : outParam (Type u_2)} [inst : Ring α] [inst_1 : FunLike F α ℝ] [RingSeminormClass F α ℝ]
  {β : Type u_3} [inst_3 : Ring β] (nα : F) {nβ : β → ℝ},
  IsPowMul nβ → ∀ {f : α →+* β}, RingHom.IsBoundedWrt (⇑nα) nβ f → ∀ (x : α), nβ (f x) ≤ nα x
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.FormallyUnramified.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.FormallyUnramified
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Mon.size : Lean.Grind.CommRing.Mon → ℕ
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IsIndObject.isFiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)},
  CategoryTheory.Limits.IsIndObject A →
    CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.coe_iInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Sort u_1}
  {S : ι → Subalgebra R A}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- A non-empty set with no doubling is the right translate of its stabilizer.  -/
Finset.op_vadd_stabilizer_of_no_doubling : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A : Finset G} {a : G},
  (A + A).card ≤ A.card → a ∈ A → AddOpposite.op a +ᵥ ↑(AddAction.stabilizer G A) = ↑A
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_le_induce_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.toSubgraph ≤ ⊤.induce {v_1 | v_1 ∈ p.support}
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.map_units : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (y : ↥S), IsUnit (f ↑y)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
uniqueMDiffOn_univ : ∀ {𝕜 : 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], UniqueMDiff[Set.univ]
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_addEquiv_lpBCF : ∀ {α : Type u_1} {E : Type u_2} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NormedAddCommGroup E] (f : ↥(lp (fun x => E) ⊤)), ⇑(AddEquiv.lpBCF f) = ↑f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            h)
  (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β) (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
      false),
  x = Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1 →
    x_1 ≍ h →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
        | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
          h_3 => h_2 size k v l size_2 k_2 v_2 l_1 r h r_2 h_3) ≍
        h_2 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 h
-- Mathlib.Algebra.Algebra.Rat
NNRat.instSMulCommClass : ∀ {R : Type u_2} {S : Type u_3} [inst : DivisionSemiring S] [inst_1 : CharZero S] [inst_2 : SMul R S]
  [SMulCommClass R S S], SMulCommClass ℚ≥0 R S
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.inv_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Inv β] (f : MeasureTheory.SimpleFunc α β) (x : α),
  f⁻¹ x = (f x)⁻¹
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.smul_index : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} (g : G) (pt : DiscreteTiling.PlacedTile ps), (g • pt).index = pt.index