mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.step_intermediateDropWhileWithPostcondition : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} {dropping : Bool},
  (Std.IterM.Intermediate.dropWhileWithPostcondition P dropping it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        if h' : dropping = true then do
          let __do_lift ← (P out).operation
          match __do_lift with
            | ⟨{ down := true }, h''⟩ =>
              pure
                (Std.Shrink.deflate
                  (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileWithPostcondition P true it') ⋯))
            | ⟨{ down := false }, h''⟩ =>
              pure
                (Std.Shrink.deflate
                  (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhileWithPostcondition P false it') out ⋯))
        else
          pure
            (Std.Shrink.deflate
              (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhileWithPostcondition P false it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure
          (Std.Shrink.deflate
            (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileWithPostcondition P dropping it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Init.SimpLemmas
Bool.or_assoc : ∀ (a b c : Bool), (a || b || c) = (a || (b || c))
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instProd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q] [CategoryTheory.Injective P] [CategoryTheory.Injective Q],
  CategoryTheory.Injective (P ⨯ Q)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The residual norm at `x` is minimal among all points of `E` if and only if
the adjoint of `A` sends the residual `y - A x` to zero.  -/
ContinuousLinearMap.forall_norm_sub_apply_le_iff_adjoint_apply_sub_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) (y : F) (x : E),
  (∀ (z : E), ‖y - A x‖ ≤ ‖y - A z‖) ↔ (ContinuousLinearMap.adjoint A) (y - A x) = 0
-- Mathlib.GroupTheory.Coset.Defs
/-- It can be useful to write `obtain ⟨h, H⟩ := mk_out_eq_mul ...`, and then `rw [H]` or
`simp_rw [H]` or `simp only [H]`. In order for `simp_rw` and `simp only` to work, this lemma is
stated in terms of an arbitrary `h : s`, rather than the specific `h = g⁻¹ * (mk g).out`.  -/
QuotientGroup.mk_out_eq_mul : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) (g : α), ∃ h, Quotient.out ↑g = g * ↑h
-- Init.Prelude
/-- Propositionally equal terms are also heterogeneously equal.  -/
heq_of_eq : ∀ {α : Sort u_1} {a a' : α}, a = a' → a ≍ a'
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_succ : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a : α}, Std.PRange.UpwardEnumerable.LT a (Std.PRange.succ a)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g)
  (e : Z ⟶ X) (he : CategoryTheory.CategoryStruct.comp e f = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift f e he)
      (CategoryTheory.Limits.kernelIsoOfEq h).hom =
    CategoryTheory.Limits.kernel.lift g e ⋯
-- Mathlib.FieldTheory.Finite.GaloisField
/-- A Galois field with exponent 1 is equivalent to `ZMod`  -/
GaloisField.equivZmodP : (p : ℕ) → [h_prime : Fact (Nat.Prime p)] → GaloisField p 1 ≃ₐ[ZMod p] ZMod p
-- Init.Omega.Constraint
/-- Shorthand for the second component of `positivize`.  -/
Lean.Omega.positivizeCoeffs : Lean.Omega.Constraint → Lean.Omega.Coeffs → Lean.Omega.Coeffs
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.lift_injective : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L),
  Function.Injective IntermediateField.lift
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instCategoryProfiniteAddGrp.eq_1 : instCategoryProfiniteAddGrp =
  { Hom := fun A B => A.Hom B, id := fun A => { hom' := ContinuousAddMonoidHom.id ↑A.toProfinite.toTop },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @instCategoryProfiniteAddGrp._proof_1,
    comp_id := @instCategoryProfiniteAddGrp._proof_2, assoc := @instCategoryProfiniteAddGrp._proof_3 }
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `FunLike.coe_add`. -/
MeasureTheory.VectorMeasure.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_integral_sub : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] ⦃f g : β × γ → E⦄,
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    MeasureTheory.Integrable g ((κ.compProd η) a) →
      ∫ (x : β), ∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x) ∂κ a =
        ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a - ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.insertMany!_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {l : List ((a : α) × β a)}, (↑(t₁.insertMany! l)).Equiv ↑(t₂.insertMany! l)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instIsStableUnderCobaseChangeInnerAnodyneExtensions : SSet.innerAnodyneExtensions.IsStableUnderCobaseChange
-- Lean.DocString.Markdown
/-- Renders a `Part` (a logical document section) at the given heading level. Headings use ATX-style
(`#`, `##`, …) with level `0` rendering as `#`.
 -/
Lean.Doc.partMarkdown : {i : Type u_1} →
  {b : Type u_2} →
    {p : Type u_3} →
      [Lean.Doc.MarkdownInline i] →
        [Lean.Doc.MarkdownBlock i b] → ℕ → Lean.Doc.Part i b p → Lean.Doc.MarkdownM (Array String)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.comp_inv_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (g : Y ⟶ X) [inst_1 : CategoryTheory.IsIso g]
  {f : Y ⟶ X}, CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g) = CategoryTheory.CategoryStruct.id Y ↔ f = g
-- Init.Data.List.Sort.Lemmas
List.MergeSort.Internal.splitInTwo_fst_append_splitInTwo_snd : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  ↑(List.MergeSort.Internal.splitInTwo l).1 ++ ↑(List.MergeSort.Internal.splitInTwo l).2 = ↑l
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsQuotientMap.isGeneratedBy : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] {f : Y → Z},
  Topology.IsQuotientMap f → ∀ [Topology.IsGeneratedBy X Y], Topology.IsGeneratedBy X Z
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.next?.eq_1 : ∀ {α : Type u_1}, RBTree.RBNode.Stream.nil.next? = none
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.sum_restrict_disjointed_spanningSets : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite ν],
  (MeasureTheory.Measure.sum fun n => μ.restrict (disjointed (MeasureTheory.spanningSets ν) n)) = μ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for reverse monotonicity of multiplication on the left,
namely `a * b₁ ≤ a * b₂ → b₁ ≤ b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedCancelMonoid`.  -/
MulLeftReflectLE : (M : Type u_1) → [Mul M] → [LE M] → Prop
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.generator.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor D Cᵒᵖ) [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C],
  CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.generator✝ F =
    ∐ fun X => ∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator✝ C
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
/-- Local generator data `q` is locally free data if all of the natural morphisms
`free (q.generators i).I ⟶ M.over (q.X i)` are isomorphisms.  -/
SheafOfModules.LocalGeneratorsData.IsLocallyFreeData : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → M.LocalGeneratorsData → Prop
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_restrictScalars : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] {𝕜' : Type u_1}
  [inst_6 : NontriviallyNormedField 𝕜'] [inst_7 : NormedAlgebra 𝕜' 𝕜] [inst_8 : NormedSpace 𝕜' G]
  [inst_9 : IsScalarTower 𝕜' 𝕜 G] [inst_10 : (i : ι) → NormedSpace 𝕜' (E i)]
  [inst_11 : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] (f : ContinuousMultilinearMap 𝕜 E G),
  ‖ContinuousMultilinearMap.restrictScalars 𝕜' f‖ = ‖f‖
-- Mathlib.Data.Set.Function
Set.SurjOn.iterate : ∀ {α : Type u_1} {f : α → α} {s : Set α}, Set.SurjOn f s s → ∀ (n : ℕ), Set.SurjOn f^[n] s s
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.HasSmallLocalizedHom.small : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [self : CategoryTheory.Localization.HasSmallLocalizedHom W X Y], Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y)
-- Mathlib.Algebra.Group.Action.End
AddAction.toPerm_zero : ∀ (G : Type u_1) (α : Type u_5) [inst : AddGroup G] [inst_1 : AddAction G α], AddAction.toPerm 0 = 1
-- Mathlib.CategoryTheory.Join.Basic
/-- Morphisms in `C ⋆ D` are those of `C` and `D`, plus a unique
morphism `(left c ⟶ right d)` for every `c : C` and `d : D`.  -/
CategoryTheory.Join.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Join C D → CategoryTheory.Join C D → Type (max v₁ v₂)
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_eq_filter_Ico_zero : ∀ (n : ℕ), n.primesBelow = Finset.filter Nat.Prime (Finset.Ico 0 n)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.partialTraj_compProd_traj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a b : ℕ},
  a ≤ b →
    ∀ (u : (i : ↥(Finset.Iic a)) → X ↑i),
      ((ProbabilityTheory.Kernel.partialTraj κ a b) u).compProd (ProbabilityTheory.Kernel.traj κ b) =
        MeasureTheory.Measure.map (fun x => (Preorder.frestrictLe b x, x)) ((ProbabilityTheory.Kernel.traj κ a) u)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.CotangentSpace.map_ofComp_surjective : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  Function.Surjective ⇑(Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Build an `addEquiv` from an isomorphism in the category `AddGrpCat`  -/
CategoryTheory.Iso.addGroupIsoToAddEquiv : {X Y : AddGrpCat} → (X ≅ Y) → ↑X ≃+ ↑Y
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.mk.sizeOf_spec : ∀ (matcherName : Lean.Name) (matchType : Lean.Expr) (discrInfos : Array Lean.Meta.Match.DiscrInfo)
  (lhss : List Lean.Meta.Match.AltLHS) (isSplitter : Option Lean.Meta.Match.Overlaps),
  sizeOf
      { matcherName := matcherName, matchType := matchType, discrInfos := discrInfos, lhss := lhss,
        isSplitter := isSplitter } =
    1 + sizeOf matcherName + sizeOf matchType + sizeOf discrInfos + sizeOf lhss + sizeOf isSplitter
-- Mathlib.RepresentationTheory.Equiv
/-- Every `f : α → V` can induce an intertwining map between `(α →₀ k[G])` and `V`.  -/
Representation.freeLift : {G : Type v} →
  [inst : Monoid G] →
    {V : Type v'} →
      [inst_1 : AddCommMonoid V] →
        {k : Type u} →
          [inst_2 : CommSemiring k] →
            [inst_3 : Module k V] →
              (σ : Representation k G V) → {α : Type w'} → (α → V) → (Representation.free k G α).IntertwiningMap σ
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMulAction.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [inst : Monoid M] [inst_1 : MulAction M β],
  Filter.Germ.instMulAction = { toSMul := Filter.Germ.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- If a graph is cliquefree, any graph that is contained in it is also cliquefree.  -/
SimpleGraph.CliqueFree.comap : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} {H : SimpleGraph β},
  H.IsContained G → G.CliqueFree n → H.CliqueFree n
-- Mathlib.Algebra.Field.Defs
/-- However `NNRat.cast` is defined, it must be equal to `a / b`.

Do not use this lemma directly. Use `NNRat.cast_def` instead.  -/
Field.nnratCast_def : ∀ {K : Type u} [self : Field K] (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.Limits.Fork.ext.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (i i_1 : s.pt ≅ t.pt) (e_i : i = i_1) (w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι),
  CategoryTheory.Limits.Fork.ext i w = CategoryTheory.Limits.Fork.ext i_1 ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_erase_le_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α}, (t.erase k).isEmpty = false → (cmp (t.erase k).maxKey! t.maxKey!).isLE = true
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.mk : Lean.Lsp.LeanImport → Array Lean.Lsp.Ipc.ModuleHierarchy → Lean.Lsp.Ipc.ModuleHierarchy
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.coe_tail : ∀ {α : Type u_1} {n : ℕ} (x : Fin (n + 1) ↪ α), ⇑(Fin.Embedding.tail x) = Fin.tail ⇑x
-- Mathlib.Algebra.Module.LocalizedModule.AtPrime
/-- Given a prime ideal `P` and `f : M →ₗ[R] M'`, `IsLocalizedModule.AtPrime P f` states that `M'`
is isomorphic to the localization of `M` at the complement of `P`.  -/
IsLocalizedModule.AtPrime : {R : Type u_1} →
  {M : Type u_2} →
    {M' : Type u_3} →
      [inst : CommSemiring R] →
        (P : Ideal R) →
          [P.IsPrime] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M'] → [inst_4 : Module R M] → [inst_5 : Module R M'] → (M →ₗ[R] M') → Prop
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sup : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], y \ (x ⊔ z) = y \ x ⊓ y \ z
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.repr_apply_coe : ∀ {ι : Type u_1} {G : Type u_3} [inst : AddGroup G] (b : FreeAddGroupBasis ι G) (i : ι),
  b.repr (b i) = FreeAddGroup.of i
-- Lean.Parser.Types
Lean.Parser.ParserCache.mk.sizeOf_spec : ∀ (tokenCache : Lean.Parser.TokenCacheEntry)
  (parserCache : Std.HashMap Lean.Parser.ParserCacheKey Lean.Parser.ParserCacheEntry),
  sizeOf { tokenCache := tokenCache, parserCache := parserCache } = 1 + sizeOf tokenCache + sizeOf parserCache
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.smul_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : Mul R] (r : R) (l : Mathlib.Tactic.Module.NF R M),
  r • l =
    List.map
      (fun x =>
        match x with
        | (a, x) => (r * a, x))
      l
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedExpr.default : Lean.IR.Expr
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.map_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  CochainComplex.mappingCone.map φ φ (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id L) ⋯ =
    CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone φ)
-- Mathlib.RingTheory.RingInvo
/-- Turn an element of a type `F` satisfying `RingInvoClass F R` into an actual
`RingInvo`. This is declared as the default coercion from `F` to `RingInvo R`.  -/
RingInvoClass.toRingInvo : {F : Type u_1} →
  {R : Type u_3} → [inst : Semiring R] → [inst_1 : EquivLike F R Rᵐᵒᵖ] → [RingInvoClass F R] → F → RingInvo R
-- Mathlib.Analysis.Calculus.TangentCone.DimOne
/-- In one dimension, a point is a point of unique differentiability of a set
iff it is an accumulation point of the set.  -/
uniqueDiffWithinAt_iff_accPt : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {s : Set 𝕜} {x : 𝕜},
  UniqueDiffWithinAt 𝕜 s x ↔ AccPt x (Filter.principal s)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_vsub_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ : P), midpoint R p₁ p₂ -ᵥ p₂ = ⅟2 • (p₁ -ᵥ p₂)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If `F : ι → X → α` is a family of functions equicontinuous at `x`,
it tends to `f y` along a filter `l` for any `y ∈ s`,
the limit function `f` tends to `z` along `𝓝[s] x`, and `x ∈ closure s`,
then `(F · x)` tends to `z` along `l`.

In some sense, this is a converse of `EquicontinuousAt.closure`.  -/
EquicontinuousAt.tendsto_of_mem_closure : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι}
  {F : ι → X → α} {f : X → α} {s : Set X} {x : X} {z : α},
  EquicontinuousAt F x →
    Filter.Tendsto f (nhdsWithin x s) (nhds z) →
      (∀ y ∈ s, Filter.Tendsto (fun x => F x y) l (nhds (f y))) →
        x ∈ closure s → Filter.Tendsto (fun x_1 => F x_1 x) l (nhds z)
-- Mathlib.Order.Sublocale
Sublocale.restrict.eq_1 : ∀ {X : Type u_1} [inst : Order.Frame X] (S : Sublocale X),
  S.restrict = { toFun := fun x => sInf {s | x ≤ ↑s}, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_comp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : Type u_4} [inst_5 : AddCommGroup P]
  [inst_6 : Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P),
  AdicCompletion.map I g ∘ₗ AdicCompletion.map I f = AdicCompletion.map I (g ∘ₗ f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_le_maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β} {km kmi : α}, t.maxKey? = some km → (t.insert k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Init.Grind.AC
Lean.Grind.AC.eq_erase_dup : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} {x : Std.IdempotentOp ctx.op}
  (lhs rhs lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_erase_dup_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' = Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R),
  I.IsRadical → (IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.IsPrime)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.coe_val_add_coe_neg_val : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x : AddUnits ↥S}, ↑↑x + ↑↑(-x) = 0
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.
 -/
Std.DTreeMap.Internal.Impl.mergeWith! : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] →
        ((a : α) → β a → β a → β a) →
          Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Lean.Elab.DefView
/-- Resulting elaboration state, including any environment additions.  -/
Lean.Elab.HeaderProcessedSnapshot.state : Lean.Elab.HeaderProcessedSnapshot → Lean.Elab.Term.SavedState
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendCyclesIso_inv_iCycles : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').inv ((K.extend e).iCycles j') =
    CategoryTheory.CategoryStruct.comp (K.iCycles j) (K.extendXIso e hj').inv
-- Init.Data.Nat.Bitwise.Lemmas
Nat.two_pow_sub_one_mod_two : ∀ {n : ℕ}, (2 ^ n - 1) % 2 = 1 % 2 ^ n
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.RewriteInterface.mk : Bool →
  String →
    Lean.Expr →
      String →
        Array Lean.Widget.CodeWithInfos →
          Lean.Widget.CodeWithInfos → Lean.Expr → Bool → Mathlib.Tactic.LibraryRewrite.RewriteInterface
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_nsmul : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddMonoid (f i)] (i : I) (x : f i) (n : ℕ),
  Pi.single i (n • x) = n • Pi.single i x
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (l : Std.Sat.Literal α),
  sizeOf (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l) = 1 + sizeOf l
-- Mathlib.Analysis.Convolution
MeasureTheory.smul_convolution : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  {L : E →L[𝕜] E' →L[𝕜] F} [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G] [SMulCommClass ℝ 𝕜 F] {y : 𝕜},
  MeasureTheory.convolution (y • f) g L μ = y • MeasureTheory.convolution f g L μ