mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Util.Trace
/-- Run the provided action `k`, and log its execution within a trace node.

The message is produced after the action completes, and has access to its return value.
If it is more convenient to produce the message as part of the computation,
then `Lean.withTraceNode'` can be used instead.
If profiling is enabled, this will also log the runtime of `k`.

The class `ExceptToTraceResult` is used to convert the result produced by `k` into a `TraceResult`
(success/failure/error), which is stored in `TraceData.result?`. The rendering layer uses
`TraceResult.toEmoji` to prepend the appropriate emoji (✅️/❌️/💥️) when displaying the trace.
A typical invocation might be:
```lean4
withTraceNode `isPosTrace
    (msg := fun _ => return m!"checking positivity") do
  return 0 < x
```

The `cls`, `collapsed`, and `tag` arguments are forwarded to the constructor of `TraceData`.
 -/
Lean.withTraceNode : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [Lean.MonadTrace m] →
        [Lean.MonadRef m] →
          [Lean.AddMessageContext m] →
            [Lean.MonadOptions m] →
              {ε : Type} →
                [always : Lean.MonadAlwaysExcept ε m] →
                  [MonadLiftT BaseIO m] →
                    [Lean.ExceptToTraceResult ε α] →
                      Lean.Name →
                        (Except ε α → m Lean.MessageData) → m α → optParam Bool true → optParam String "" → m α
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.addCommMonoid : {α : Type u_2} →
  [inst : AddCommMonoid α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → AddCommMonoid (NonemptyInterval α)
-- Std.Data.TreeMap.Basic
/-- Removes all mappings of the map for which the given function returns `false`.  -/
Std.TreeMap.filter : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (α → β → Bool) → Std.TreeMap α β cmp → Std.TreeMap α β cmp
-- Mathlib.Data.Set.Lattice
/-- `sUnion` is monotone under taking a subset of each set.  -/
Set.sUnion_mono_subsets : ∀ {α : Type u_1} {s : Set (Set α)} {f : Set α → Set α}, (∀ (t : Set α), t ⊆ f t) → ⋃₀ s ⊆ ⋃₀ (f '' s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {km : α}, t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_subset_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s₁ s₂ t₁ t₂ : Finset α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ + t₁ ⊆ s₂ + t₂
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.measurable_rnDerivAux : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ),
  Measurable fun p => κ.rnDerivAux η p.1 p.2
-- Init.Grind.Lemmas
Lean.Grind.eval_congr₁ : ∀ {α : Sort u} {β : Sort v} {f : α → β} {a a' : α} {b : β}, a = a' → f a' = b → f a = b
-- Mathlib.Order.Hom.Lattice
SupHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] (f : SupHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = f
-- Init.Data.Int.Linear
Int.Internal.Linear.emod_le_cert : ℤ → ℤ → Bool
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
/-- [Stacks Tag 00GX](https://stacks.math.columbia.edu/tag/00GX) (Part 2) -/
IsIntegral.isAlmostIntegral : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsFractionRing R S]
  {s : S}, IsIntegral R s → IsAlmostIntegral R s
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsInvariantBlock.eq_1 : ∀ (G : Type u_1) {X : Type u_2} [inst : VAdd G X] (B : Set X), AddAction.IsInvariantBlock G B = ∀ (g : G), g +ᵥ B ⊆ B
-- Init.Data.Rat.Lemmas
Rat.add_le_add_left : ∀ {a b c : ℚ}, c + a ≤ c + b ↔ a ≤ b
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.range_eq_top : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), f.range = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.Order.Interval.Finset.Basic
Finset.eq_of_mem_uIcc_of_mem_uIcc' : ∀ {α : Type u_2} [inst : DistribLattice α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
  b ∈ Finset.uIcc a c → c ∈ Finset.uIcc a b → b = c
-- Lean.ProjFns
/-- Constructor associated with the auxiliary projection function.  -/
Lean.ProjectionFunctionInfo.ctorName : Lean.ProjectionFunctionInfo → Lean.Name
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'AddMonoidHom_apply : ∀ {o : Type u_4} (m' : o → Type u_7) (n' : o → Type u_8) (α : Type u_12) [inst : AddZeroClass α]
  (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o), (Matrix.blockDiag'AddMonoidHom m' n' α) M k = M.blockDiag' k
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode.mk : Lean.Expr → Lean.Expr → Lean.MetavarContext → List Lean.Expr → ℕ → Lean.Meta.SynthInstance.ConsumerNode
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The `b`-th inclusion into the sigma object over `f` has the form `f b ⟶ ∐ f`.  -/
CategoryTheory.Limits.Sigma.ι : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f : β → C) → [inst_1 : CategoryTheory.Limits.HasCoproduct f] → (b : β) → f b ⟶ ∐ f
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.IsNatPowModT.bit0 : ∀ {a b m : ℕ} {c : ℕ}, Mathlib.Meta.NormNum.IsNatPowModT ((a.pow b).mod m = c) a (2 * b) m ((c.mul c).mod m)
-- Mathlib.Algebra.Order.Group.PartialSups
partialSups_const_add : ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeSup α] [inst_1 : AddGroup α] [inst_2 : Preorder ι]
  [inst_3 : LocallyFiniteOrderBot ι] [AddLeftMono α] (f : ι → α) (c : α) (i : ι),
  (partialSups fun x => c + f x) i = c + (partialSups f) i
-- Mathlib.Order.Filter.Pointwise
Filter.top_add_top : ∀ {α : Type u_2} [inst : AddMonoid α], ⊤ + ⊤ = ⊤
-- Mathlib.Order.Filter.Pointwise
Filter.eventually_inv : ∀ {α : Type u_2} [inst : Inv α] {f : Filter α} {p : α → Prop}, (∀ᶠ (x : α) in f⁻¹, p x) ↔ ∀ᶠ (x : α) in f, p x⁻¹
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  k ∉ m₂ → (m₁ ∩ m₂).getD k fallback = fallback
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.eq_append_of_dropSuffix?_bool_eq_some : ∀ {p : Char → Bool} {s : String} {res : String.Slice},
  s.dropSuffix? p = some res → ∃ c, s = res.copy ++ String.singleton c ∧ p c = true
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_trans_apply : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A]
  [inst_3 : Mul B] [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] [inst_8 : Add C]
  [inst_9 : Mul C] [inst_10 : SMul R C] [inst_11 : Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : C),
  (e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C}
  {n m : ℤ} (f : CategoryTheory.ShiftedHom X Y n) (g : CategoryTheory.ShiftedHom Y Z m) (q : ℤ) (hq : n + m = q),
  (CategoryTheory.ShiftedHom.opEquiv' n m q hq).symm
      (CategoryTheory.CategoryStruct.comp (Quiver.Hom.op g)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y))
          ((CategoryTheory.shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)))) =
    f.comp g ⋯
-- Init.System.IO
/-- Reads up to the given number of bytes from the stream.

If the returned array is empty, an end-of-file marker (EOF) has been reached. An EOF does not
actually close a stream, so further reads may block and return more data.
 -/
IO.FS.Stream.read : IO.FS.Stream → USize → IO ByteArray
-- Mathlib.Algebra.Torsor.Defs
smul_sdiv_eq_div_sdiv : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (g : G) (p q : P), g • p /ₛ q = g / (q /ₛ p)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- Construct a continuous function from a bare function, a continuous function, and a proof that
they are equal.  -/
OmegaCompletePartialOrder.ContinuousHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : OmegaCompletePartialOrder β] → (f : α → β) → (g : α →𝒄 β) → f = ⇑g → α →𝒄 β
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instVAddCommClassSubtypeMem : ∀ {S : Type u'} {T : Type u''} {R : Type u} {M : Type v} [inst : VAdd R M] [inst_1 : SetLike S M]
  [hS : VAddMemClass S R M] (s : S) [inst_2 : VAdd T M] [inst_3 : VAddMemClass S T M] [VAddCommClass T R M],
  VAddCommClass T R ↥s
-- Init.Data.String.Lemmas.FindPos
String.Slice.le_posLE_iff : ∀ {s : String.Slice} {p : s.Pos} {q : String.Pos.Raw}, p ≤ s.posLE q ↔ p.offset ≤ q
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.instCategory : {C : Type u} → [CategoryTheory.Category.{v, u} C] → CategoryTheory.Category.{v, u} (CategoryTheory.WithInitial C)
-- Mathlib.GroupTheory.Rank
Group.rank_range_le : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] [inst_2 : Group.FG G] {f : G →* H},
  Group.rank ↥f.range ≤ Group.rank G
-- Mathlib.Topology.Algebra.Ring.Basic
/-- If `R` is a ring which is a topological semiring, then it is automatically a topological
ring. This exists so that one can place a topological ring structure on `R` without explicitly
proving `continuous_neg`.  -/
IsTopologicalSemiring.toIsTopologicalRing : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonAssocRing R], IsTopologicalSemiring R → IsTopologicalRing R
-- Init.Data.Slice.Lemmas
Std.Slice.length_toList_eq_size : ∀ {γ : Type u} {α β : Type v} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  {s : Std.Slice γ} [inst_2 : Std.Slice.SliceSize γ] [Std.Slice.LawfulSliceSize γ] [Std.Iterators.Finite α Id],
  s.toList.length = s.size
-- Mathlib.Algebra.Group.Defs
AddCommMagma.toAdd : {G : Type u} → [self : AddCommMagma G] → Add G
-- Mathlib.Algebra.Polynomial.Basic
/-- See also `Polynomial.sum_add'`.  -/
Polynomial.sum_add : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (p : Polynomial R) (f g : ℕ → R → S),
  (p.sum fun n x => f n x + g n x) = p.sum f + p.sum g
-- Init.Data.Nat.Lemmas
Nat.div_le_iff_le_mul_add_pred : ∀ {b a c : ℕ}, 0 < b → (a / b ≤ c ↔ a ≤ b * c + (b - 1))
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.toContinuousAffineMap_injective : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [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₂],
  Function.Injective AffineIsometry.toContinuousAffineMap
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.isCancelAdd : ∀ {α : Type u} [inst : Mul α] [IsCancelMul α], IsCancelAdd (Additive α)
-- Mathlib.Algebra.BigOperators.Associated
Prime.dvd_finsetProd_iff : ∀ {M₀ : Type u_3} {M : Type u_4} [inst : CommMonoidWithZero M] {S : Finset M₀} {p : M},
  Prime p → ∀ (g : M₀ → M), p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a
-- Mathlib.Analysis.Complex.Norm
Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub : ∀ {x : ℝ}, ‖x‖ ≤ 1 → Complex.normSq (↑x - Complex.I * ↑√(1 - x ^ 2)) = 1
-- Mathlib.Order.Filter.Curry
Filter.curry_le_prod : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β}, l.curry m ≤ l ×ˢ m
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopCat.Presheaf.presieveOfCovering.indexOfHom_spec : ∀ {X : TopCat} {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X)
  (f : (V : TopologicalSpace.Opens ↑X) × { f // TopCat.Presheaf.presieveOfCovering U f }),
  f.fst = U (TopCat.Presheaf.presieveOfCovering.indexOfHom U f)
-- Aesop.Stats.Extension
Aesop.StatsExtensionEntry.mk : Lean.Syntax → String → Option Lean.Position → Aesop.Stats → Aesop.StatsExtensionEntry
-- Aesop.RuleTac.Forward.Basic
Aesop.ForwardHypData.mk : Std.HashMap Lean.FVarId ℕ → Aesop.ForwardHypData
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.NormNums.mk.injEq : ∀ (tree : Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt) (erased : Lean.PHashSet Lean.Name)
  (tree_1 : Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt) (erased_1 : Lean.PHashSet Lean.Name),
  ({ tree := tree, erased := erased } = { tree := tree_1, erased := erased_1 }) = (tree = tree_1 ∧ erased = erased_1)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.mapTR.loop.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          ((bs : List β) → motive [] bs) →
            ((a : α) → (as : List α) → (bs : List β) → motive (a :: as) bs) → motive x x_1
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
/-- Etale morphisms are weakly étale.  -/
AlgebraicGeometry.WeaklyEtale.instOfEtale : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Etale f], AlgebraicGeometry.WeaklyEtale f
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
/-- The functor `N` for the equivalence is obtained by composing
`N' : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)` and the inverse
of the equivalence `ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ)`.  -/
CategoryTheory.Idempotents.DoldKan.N : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.IsIdempotentComplete C] →
        [CategoryTheory.Limits.HasFiniteCoproducts C] →
          CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (ChainComplex C ℕ)
-- Mathlib.CategoryTheory.Pi.Basic
/-- When `i = j`, projections `Pi.eval C i` and `Pi.eval C j` are related by the equivalence
`Pi.eqToEquivalence C h : C i ≌ C j`.  -/
CategoryTheory.Pi.evalCompEqToEquivalenceFunctor : {I : Type w₀} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {i j : I} →
        (h : i = j) →
          (CategoryTheory.Pi.eval C i).comp (CategoryTheory.Pi.eqToEquivalence C h).functor ≅ CategoryTheory.Pi.eval C j
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg : {α : Type} →
  {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → ℕ → m α → m α
-- Mathlib.Analysis.Normed.Group.Basic
/-- The norm of a seminormed group as an additive group seminorm.  -/
normAddGroupSeminorm : (E : Type u_5) → [inst : SeminormedAddGroup E] → AddGroupSeminorm E
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.inner_lid_lid : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : TensorProduct 𝕜 𝕜 E), inner 𝕜 ((TensorProduct.lid 𝕜 E) x) ((TensorProduct.lid 𝕜 E) y) = inner 𝕜 x y
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comapEquiv_coe : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R),
  ⇑(MvPolynomial.comapEquiv f) = MvPolynomial.comap ↑f
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.get.congr_simp : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C C_1 : G.EdgeLabeling K),
  C = C_1 → ∀ (x x_1 : V) (e_x : x = x_1) (y y_1 : V) (e_y : y = y_1) (h : G.Adj x y), C.get x y h = C_1.get x_1 y_1 ⋯
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.coe_mem_inertia : ∀ {M : Type u_6} [inst : AddGroup M] {I : AddSubgroup M} {G : Type u_7} [inst_1 : Group G] [inst_2 : MulAction G M]
  {H : Subgroup G} {σ : ↥H}, ↑σ ∈ I.inertia G ↔ σ ∈ I.inertia ↥H
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject.Augmented C}
  {f g : X ⟶ Y}, f = g ↔ f.left = g.left ∧ f.right = g.right
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instSetLike : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → SetLike hI.SubDPIdeal A
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedProofInstInfo : Inhabited Lean.Meta.Sym.ProofInstInfo
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.bot_of_map_eq_bot : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L},
  Function.Injective ⇑f → LieIdeal.map f I = ⊥ → I = ⊥
-- Lean.Message
/-- Convert a `TraceResult` to its emoji representation.  -/
Lean.TraceResult.toEmoji : Lean.TraceResult → String
-- Mathlib.Combinatorics.Enumerative.DyckWord
instAddDyckWord : Add DyckWord
-- Mathlib.Data.PNat.Defs
/-- Strong induction on `ℕ+`.  -/
PNat.strongInductionOn : {p : ℕ+ → Sort u_1} → (n : ℕ+) → ((k : ℕ+) → ((m : ℕ+) → m < k → p m) → p k) → p n
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.maximalIdeal_eq_bot : ∀ {R : Type u_4} [inst : Field R], IsLocalRing.maximalIdeal R = ⊥
-- Init.Tactics
/-- Similar to `let`, but using `refine'`  -/
Lean.Parser.Tactic.tacticLet'__ : Lean.ParserDescr
-- Mathlib.Algebra.Homology.CommSq
/-- The cokernel cofork attached to a commutative square in a preadditive category.  -/
CategoryTheory.CommSq.cokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X₁ X₂ X₃ X₄ : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] →
          {f : X₁ ⟶ X₂} →
            {g : X₁ ⟶ X₃} →
              {inl : X₂ ⟶ X₄} →
                {inr : X₃ ⟶ X₄} →
                  CategoryTheory.CommSq f g inl inr →
                    CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.biprod.lift f (-g))
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.toPartialEquiv : {X : Type u_1} → {G : Type u_2} → [inst : SMul G X] → Equidecomp X G → PartialEquiv X X
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.IsSFiniteKernel.compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ),
  ProbabilityTheory.IsSFiniteKernel (κ.compProd η)
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.res_zero : ∀ {α : Type u_2} (x : ℕ → α), PiNat.res x 0 = []
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.toNonUnitalSubsemiring_toSubsemiring : ∀ {R : Type u} [inst : NonAssocSemiring R] (S : Subsemiring R), S.toNonUnitalSubsemiring.toSubsemiring ⋯ = S
-- Mathlib.RingTheory.Perfection
PreTilt.valAux_add : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O →
    ∀ {p : ℕ} [inst_3 : Fact (Nat.Prime p)] [inst_4 : Fact ¬IsUnit ↑p] (f g : PreTilt O p),
      PreTilt.valAux K v O p (f + g) ≤ max (PreTilt.valAux K v O p f) (PreTilt.valAux K v O p g)
-- Init.Data.Option.Lemmas
Option.filter_some_eq_some : ∀ {α : Type u_1} {p : α → Bool} {a : α}, Option.filter p (some a) = some a ↔ p a = true
-- Mathlib.MeasureTheory.MeasurableSpace.NCard
measurable_encard : ∀ {α : Type u_1} [Countable α], Measurable Set.encard
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.mkContinuousMultilinear.congr_simp : ∀ {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [inst : Fintype ι']
  [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
  [inst_6 : Fintype ι] [inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)] [inst_8 : (i : ι') → NormedSpace 𝕜 (E' i)]
  (f f_1 : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (e_f : f = f_1) (C C_1 : ℝ) (e_C : C = C_1)
  (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖),
  f.mkContinuousMultilinear C H = f_1.mkContinuousMultilinear C_1 ⋯
-- Mathlib.RingTheory.TensorProduct.Maps
/-- If the R- and S- action on S and A satisfy `CompatibleSMul` both ways,
then `S ⊗[R] A` is canonically isomorphic to `A`.  -/
Algebra.TensorProduct.lidOfCompatibleSMul : (R : Type u_3) →
  (S : Type u_4) →
    (A : Type u_6) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra S A] →
                [inst_5 : Algebra R S] →
                  [TensorProduct.CompatibleSMul R S S A] →
                    [TensorProduct.CompatibleSMul S R S A] → TensorProduct R S A ≃ₐ[S] A
-- Mathlib.Order.CompleteSublattice
/-- Copy of a complete sublattice with a new `carrier` equal to the old one. Useful to fix
definitional equalities.  -/
CompleteSublattice.copy : {α : Type u_1} → [inst : CompleteLattice α] → (L : CompleteSublattice α) → (s : Set α) → s = ↑L → CompleteSublattice α
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_iff_eq_mul_left : ∀ {a b c : ℤ}, b ≠ 0 → b ∣ a → (a / b = c ↔ a = c * b)
-- Mathlib.GroupTheory.Finiteness
AddMonoid.fg_of_addGroup_fg : ∀ {G : Type u_3} [inst : AddGroup G] [AddGroup.FG G], AddMonoid.FG G
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instVAddCommClass : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)]
  [inst_1 : (i : ι) → VAdd N (α i)] [∀ (i : ι), VAddCommClass M N (α i)], VAddCommClass M N ((i : ι) × α i)
-- Mathlib.Data.List.Basic
List.getLast_append_of_right_ne_nil : ∀ {α : Type u} (l₁ l₂ : List α) (h : l₂ ≠ []), (l₁ ++ l₂).getLast ⋯ = l₂.getLast h
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.union_indep_iff_forall_notMem_closure_right : ∀ {α : Type u_2} {M : Matroid α} {I J : Set α},
  M.Indep I → M.Indep J → (M.Indep (I ∪ J) ↔ ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e}))
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair F] (X : adj.toComonad.Coalgebra),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (G.map X.a) (adj.unit.app (G.obj X.A))) F
-- Std.Internal.Do.Triple.SpecLemmas
_private.Std.Internal.Do.Triple.SpecLemmas.0.Std.Internal.Do.Except.wpInst.match_1.eq_1 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (el : ε) → motive (Except.error el)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error el => h_2 el) =
    h_1 a
-- Mathlib.SetTheory.Ordinal.Basic
/-- `o.ToType` is an `OrderBot` whenever `o ≠ 0`.  -/
Ordinal.toTypeOrderBot : {o : Ordinal.{u_1}} → o ≠ 0 → OrderBot o.ToType
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.val_unitsEquivUnitsType_apply_coe : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (x : ↥S.units), ↑↑(S.unitsEquivUnitsType x) = (Units.coeHom M) ↑x
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundOptionTExceptPUnitPureOfLawfulMonad.match_5.eq_1 : ∀ {α : Type u_1} {P : α → Prop}
  (motive :
    (r : Option α) →
      (match r with
        | some a => P a
        | none => True) →
        Sort u_2)
  (a : α)
  (hp :
    match some a with
    | some a => P a
    | none => True)
  (h_1 :
    (a : α) →
      (hp :
          match some a with
          | some a => P a
          | none => True) →
        motive (some a) hp)
  (h_2 :
    (x :
        match none with
        | some a => P a
        | none => True) →
      motive none x),
  (match some a, hp with
    | some a, hp => h_1 a hp
    | none, x => h_2 x) =
    h_1 a hp