mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  (CategoryTheory.Limits.kernelBiproductToSubtypeIso f p).inv =
    CategoryTheory.Limits.limit.lift
      (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0)
      (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯)
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsInertiaField.algebraMap_ringEquiv_symm_apply : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (E : Type u_6) [inst_4 : Field E] [inst_5 : Algebra E L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (E' : Type u_9) [inst_7 : Field E'] [inst_8 : Algebra E' L]
  [inst_9 : IsInertiaField K L P E] [inst_10 : IsInertiaField K L P E'] (x : E'),
  (algebraMap E L) ((IsInertiaField.ringEquiv K L P E E').symm x) = (algebraMap E' L) x
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.support_countable : ∀ {α : Type u_1} (p : PMF α), p.support.Countable
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.instHasBinaryProducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C],
  CategoryTheory.Limits.HasBinaryProducts C
-- Mathlib.RingTheory.ChainOfDivisors
/-- The order isomorphism between the factors of `mk m` and the factors of `mk n` induced by a
bijection between the factors of `m` and the factors of `n` that preserves `∣`.  -/
mkFactorOrderIsoOfFactorDvdEquiv : {M : Type u_1} →
  [inst : CommMonoidWithZero M] →
    {N : Type u_2} →
      [inst_1 : CommMonoidWithZero N] →
        [Subsingleton Mˣ] →
          [Subsingleton Nˣ] →
            {m : M} →
              {n : N} →
                {d : { l // l ∣ m } ≃ { l // l ∣ n }} →
                  (∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') →
                    ↑(Set.Iic (Associates.mk m)) ≃o ↑(Set.Iic (Associates.mk n))
-- Mathlib.Algebra.Group.Units.Defs
Units.inv_mul_cancel_left : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) (b : α), ↑a⁻¹ * (↑a * b) = b
-- Mathlib.LinearAlgebra.Ray
SameRay.congr_simp : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (v₁ v₁_1 : M),
  v₁ = v₁_1 → ∀ (v₂ v₂_1 : M), v₂ = v₂_1 → SameRay R v₁ v₂ = SameRay R v₁_1 v₂_1
-- Mathlib.Data.Fin.Basic
Fin.neZero : ∀ {n : ℕ} (i : Fin n), NeZero n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {km kmi : α}, t.maxKey? = some km → (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- An auxiliary construction for `mkHom`.

Here we build by induction a family of commutative squares,
but don't require at the type level that these successive commutative squares actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map)
in `mkHom`.
 -/
ChainComplex.mkHomAux : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (P Q : ChainComplex V ℕ) →
        (zero : P.X 0 ⟶ Q.X 0) →
          (one : P.X 1 ⟶ Q.X 1) →
            CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero →
              ((n : ℕ) →
                  (p :
                      (f : P.X n ⟶ Q.X n) ×'
                        (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
                          CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) =
                            CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) →
                    (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
                      CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) =
                        CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst) →
                (n : ℕ) →
                  (f : P.X n ⟶ Q.X n) ×'
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
                      CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) =
                        CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f
-- Mathlib.ModelTheory.Complexity
/-- Indicates that a bounded formula is in prenex normal form - that is, it consists of quantifiers
applied to a quantifier-free formula.  -/
FirstOrder.Language.BoundedFormula.IsPrenex : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → Prop
-- Mathlib.Data.PFunctor.Univariate.M
/-- return all the subtrees of the root of a tree `x : M F`  -/
PFunctor.M.children : {F : PFunctor.{uA, uB}} → (x : F.M) → F.B x.head → F.M
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.eta : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M}
  (h : ∀ (c : R) {x : M}, x ∈ p.carrier → c • x ∈ p.carrier), { toAddSubmonoid := p.toAddSubmonoid, smul_mem' := h } = p
-- Mathlib.Data.Set.Image
Set.image_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α → β) (a : Set α), f ∘ g '' a = f '' g '' a
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.range_zero : ∀ {α : Type u_5} {β : Type u_6} [inst : Zero β] [Nonempty α], Set.range 0 = {0}
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.str : (self : AddMonCat) → AddMonoid ↑self
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.ExtensionMap : Type
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Ico : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (a b : α i), Function.update f i '' Set.Ico a b = Set.Ico (Function.update f i a) (Function.update f i b)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_modify_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ [Inhabited α] {k : α} {f : β k → β k} (hc : (m.modify k f).contains k = true), (m.modify k f).getKey k hc = k
-- Mathlib.Algebra.Lie.Killing
LieAlgebra.IsKilling.killingForm_nondegenerate : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsKilling R L], (killingForm R L).Nondegenerate
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.dotProduct_cons : ∀ {α : Type u} {n : ℕ} [inst : AddCommMonoid α] [inst_1 : Mul α] (v : Fin n.succ → α) (x : α) (w : Fin n → α),
  v ⬝ᵥ Matrix.vecCons x w = Matrix.vecHead v * x + Matrix.vecTail v ⬝ᵥ w
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.MapSubtype.orderIso.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G),
  Subgroup.MapSubtype.orderIso H =
    { toFun := fun H' => ⟨Subgroup.map H.subtype H', ⋯⟩, invFun := fun sH' => (↑sH').subgroupOf H, left_inv := ⋯,
      right_inv := ⋯, map_rel_iff' := ⋯ }
-- Std.Time.Internal.UnitVal
/-- Creates a `UnitVal` from an `Int`.
 -/
Std.Time.Internal.UnitVal.ofInt : {α : ℚ} → ℤ → Std.Time.Internal.UnitVal α
-- Lean.MetavarContext
/-- Normal unification behaviour  -/
Lean.MetavarKind.natural : Lean.MetavarKind
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.methods : Lean.Elab.Tactic.Grind.Context → Lean.Meta.Grind.Methods
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.IntegrableOn.biUnion_finset : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {s : Finset ι} {t : ι → Set X},
  (∀ i ∈ s, MeasurableSet (t i)) → (∀ i ∈ s, μ.IntegrableOn f (t i)) → μ.IntegrableOn f (⋃ i ∈ s, t i)
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.toIsTopologicalAddGroup : ∀ {α : Type u} [inst : AddGroup α] (self : AddGroupTopology α), IsTopologicalAddGroup α
-- Lean.Util.ParamMinimizer
/-- Has not found a solution.  -/
Lean.Util.ParamMinimizer.Status.missing : Lean.Util.ParamMinimizer.Status
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_sInf : ∀ {M : Type u_2} [inst : MulOneClass M] (S : Set (Submonoid M)), (sInf S).op = sInf (Submonoid.unop ⁻¹' S)
-- Mathlib.Computability.Partrec
Partrec.rfindOpt : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → ℕ → Option σ},
  Computable₂ f → Partrec fun a => Nat.rfindOpt (f a)
-- Mathlib.Data.Sym.Sym2
/-- `fromRel` induces an order embedding from symmetric relations to `Sym2` sets.  -/
Sym2.fromRelOrderEmbedding : {α : Type u_1} → { r // Std.Symm r } ↪o Set (Sym2 α)
-- Mathlib.Algebra.Torsor.Defs
Equiv.vaddConst.eq_1 : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [inst_1 : AddTorsor G P] (p : P),
  Equiv.vaddConst p = { toFun := fun v => v +ᵥ p, invFun := fun p' => p' -ᵥ p, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.SetTheory.Cardinal.Order
IsWellOrder.subtype_nonempty : ∀ {α : Type u}, Nonempty { r // IsWellOrder α r }
-- Mathlib.Data.Part
Function.comp.congr_simp : ∀ {α : Sort u} {β : Sort v} {δ : Sort w} (f f_1 : β → δ),
  f = f_1 → ∀ (g g_1 : α → β), g = g_1 → ∀ (a a_1 : α), a = a_1 → (f ∘ g) a = (f_1 ∘ g_1) a_1
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_eq_blsub_iff_succ : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}),
  o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, Order.succ a < o.blsub f
-- Init.Data.UInt.Bitwise
UInt16.toNat_shiftRight : ∀ (a b : UInt16), (a >>> b).toNat = a.toNat >>> (b.toNat % 16)
-- Mathlib.Algebra.Order.Monoid.NatCast
zero_le_three : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : Preorder α] [ZeroLEOneClass α] [AddLeftMono α], 0 ≤ 3
-- Mathlib.Analysis.Normed.Field.Krasner
IsKrasner.krasner' : ∀ {K : Type u_1} {L : Type u_2} {inst : NormedField L} {inst_1 : Field K} {inst_2 : Algebra K L} [self : IsKrasner K L]
  {x y : L},
  IsSeparable K x →
    (Polynomial.map (algebraMap K L) (minpoly K x)).Splits →
      IsIntegral K y → (∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖) → x ∈ K⟮y⟯
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.IterM.step_flatMapAfterM.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₁', h⟩ with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => h_1 it₁' b h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it₁' h
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.apply_coe_mem_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (S : AddSubsemigroup M) (x : ↥S),
  f ↑x ∈ AddSubsemigroup.map f S
-- Lean.Meta.Tactic.Ext
/-- Erases a name marked as a `ext` attribute.
Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem`
found somewhere in the state's tree, and is not erased.
 -/
Lean.Meta.Ext.ExtTheorems.erase : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Lean.Meta.Ext.ExtTheorems → Lean.Name → m Lean.Meta.Ext.ExtTheorems
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tanh_zero : Complex.tanh 0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- If `G` has more than `extremalNumber (card V) H` edges, then `G` contains a copy of `H`.  -/
SimpleGraph.IsContained.of_extremalNumber_lt_card_edgeFinset : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V]
  [inst_1 : DecidableRel G.Adj], SimpleGraph.extremalNumber (Fintype.card V) H < G.edgeFinset.card → H.IsContained G
-- Mathlib.Topology.Compactness.LocallyFinite
/-- If `X` is a compact space, then a locally finite family of nonempty sets of `X` can have only
finitely many elements, `Fintype` version.  -/
LocallyFinite.fintypeOfCompact : {X : Type u_1} →
  {ι : Type u_2} →
    [inst : TopologicalSpace X] →
      [CompactSpace X] → {f : ι → Set X} → LocallyFinite f → (∀ (i : ι), (f i).Nonempty) → Fintype ι
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.map.eq_1 : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] [inst_7 : ContinuousAdd N] [inst_8 : ContinuousConstSMul R N] (f : M →L[R] N)
  (s : ClosedSubmodule R M), ClosedSubmodule.map f s = (Submodule.map ↑f ↑s).closure
-- Init.Data.Array.Basic
/-- Returns the last element of the array for which the monadic predicate `p` returns `true`, or `none`
if no such element is found. Elements of the array are checked in reverse, from right to left..

The monad `m` is restricted to `Type → Type` to avoid needing to use `ULift Bool` in `p`'s type.

Example:
```lean example
#eval #[7, 5, 8, 1, 2, 6, 5, 8].findRevM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 5
Almost! 6
```
```output
some 2
```
 -/
Array.findRevM? : {α : Type} → {m : Type → Type w} → [Monad m] → (α → m Bool) → Array α → m (Option α)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- If `A`, `B` and `C` have the module topology, and if furthermore `B` is a finite `R`-module,
then any bilinear map `A × B → C` is automatically continuous
 -/
IsModuleTopology.continuous_bilinear_of_finite_right : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] [IsTopologicalRing R] {A : Type u_2}
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3}
  [inst_6 : AddCommGroup B] [inst_7 : Module R B] [aB : TopologicalSpace B] [IsModuleTopology R B] {C : Type u_4}
  [inst_9 : AddCommGroup C] [inst_10 : Module R C] [aC : TopologicalSpace C] [IsModuleTopology R C] [Module.Finite R B]
  (bil : A →ₗ[R] B →ₗ[R] C), Continuous fun ab => (bil ab.1) ab.2
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_def : ∀ (x : ℝ), x.sigmoid = (1 + Real.exp (-x))⁻¹
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_mul : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x y : ℤ_[p]), (x * y).zmodRepr = x.zmodRepr * y.zmodRepr % p
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_congr_enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} {ε' : Type u_8}
  [inst : TopologicalSpace ε] [inst_1 : TopologicalSpace ε'] [inst_2 : ContinuousENorm ε] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) → (MeasureTheory.MemLp f p μ ↔ MeasureTheory.MemLp g p μ)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- Given a morphism `φ : S₁ ⟶ S₂` of short complexes and left homology data `h₁` and `h₂`
for `S₁` and `S₂` respectively, this is the induced left homology map `h₁.H ⟶ h₁.H`.  -/
CategoryTheory.ShortComplex.leftHomologyMap' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ⟶ S₂) → (h₁ : S₁.LeftHomologyData) → (h₂ : S₂.LeftHomologyData) → h₁.H ⟶ h₂.H
-- Init.Data.Range.Polymorphic.Fin
Fin.least?_eq_of_zero : Std.PRange.least? = none
-- Mathlib.Algebra.Order.SuccPred
Order.add_one_le_iff_of_not_isMax : ∀ {α : Type u_1} {x y : α} [inst : Preorder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α],
  ¬IsMax x → (x + 1 ≤ y ↔ x < y)
-- Mathlib.Algebra.Ring.Parity
even_sub_one : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Even (a - 1) ↔ Odd a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Functor.essImage.of_overPost : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F : CategoryTheory.Functor T D} {Y : CategoryTheory.Over (F.obj X)},
  (CategoryTheory.Over.post F).essImage Y → F.essImage Y.left
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.remainder_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), (WittVector.remainder p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Lean.Parser.Term
Lean.Parser.Term.local.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.ULift
ULift.up_inf : ∀ {α : Type u} [inst : Min α] (a b : α), { down := a ⊓ b } = { down := a } ⊓ { down := b }
-- Std.Data.Internal.List.Associative
/-- This is a strange dependent version of `Option.map` in which the mapping function is allowed to
"know" about the option that is being mapped. This happens to be useful in this file (see
`getValueCast_eq_getEntry?`), but we do not want it to leak out of the file.  -/
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap : {α : Type u} → {β : Type v} → (o : Option α) → ((a : α) → o = some a → β) → Option β
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The functor which sends `S : SnakeInput C` to its second line `S.L₂`.  -/
CategoryTheory.ShortComplex.SnakeInput.functorL₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)
-- Init.Prelude
HShiftLeft.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HShiftLeft α β γ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getKeyD k fallback = t₂.getKeyD k fallback
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard_le_coverMincard : ∀ {X : Type u_1} {U : SetRel X X} (T : X → X) (F : Set X) (n : ℕ),
  Dynamics.netMaxcard T F U n ≤ Dynamics.coverMincard T F U n
-- Std.Data.DTreeMap.Iterator
Std.DTreeMap.toList_iter : ∀ {α : Type u_1} {β : α → Type u_2} {cmp : α → α → Ordering} (m : Std.DTreeMap α β cmp), m.iter.toList = m.toList
-- Lean.Elab.SyntheticMVars
/-- Try to process pending synthetic metavariables.

If `postpone == .no`,then `pendingMVars` is `[]` after executing this method.
If `postpone == .partial`, then `pendingMVars` contains only `.tc` and `.coe` kinds.

It keeps executing `synthesizeSyntheticMVarsStep` while progress is being made.
If `postpone != .yes`, then it applies default instances to `SyntheticMVarKind.typeClass` (if available)
metavariables that are still unresolved, and then tries to resolve metavariables
with `postponeOnError == false`. That is, we force them to produce error messages and/or commit to
a "best option". If, after that, we still haven't made progress, we report "stuck" errors If `postpone == .no`.

Remark: we set `ignoreStuckTC := true` when elaborating `simp` arguments. Then,
pending TC problems become implicit parameters for the simp theorem.
 -/
Lean.Elab.Term.synthesizeSyntheticMVars : optParam Lean.Elab.Term.PostponeBehavior Lean.Elab.Term.PostponeBehavior.yes →
  optParam Bool false → Lean.Elab.TermElabM Unit
-- Lean.Meta.Basic
Lean.Meta.instInhabitedDiagnostics : Inhabited Lean.Meta.Diagnostics
-- Mathlib.Algebra.Group.Subgroup.Ker
AddEquiv.range_eq_top : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (e : G ≃+ G'), (↑e).range = ⊤
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLineRange.fromJson : Lean.Json → Except String Lean.Lsp.LineRange
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.unop_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : Opposite.op P ⟶ Opposite.op X)
  (π₂ : Opposite.op P ⟶ Opposite.op Y),
  (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).unop = CategoryTheory.Limits.BinaryCofan.mk π₁.unop π₂.unop
-- Init.Data.UInt.Lemmas
USize.ofNat_uInt8ToNat : ∀ (n : UInt8), USize.ofNat n.toNat = n.toUSize
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P]
  (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (d.pullbackGluedIso i).inv.left
      (CategoryTheory.Limits.pullback.snd d.glued.hom (𝒰.f i)) =
    (d.cocone i).pt.hom
-- Mathlib.ModelTheory.Definability
Set.definable_biUnion_finset : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {ι : Type u_2}
  {f : ι → Set (α → M)}, (∀ (i : ι), A.Definable L (f i)) → ∀ (s : Finset ι), A.Definable L (⋃ i ∈ s, f i)
-- Mathlib.Algebra.Group.Units.Basic
eq_zero_of_add_left : ∀ {α : Type u} [inst : AddCommMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 → b = 0
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_restrictScalars : ∀ (R : Type u_11) {S : Type u_12} {M : Type u_13} {N : Type u_14} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : SMul R S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M]
  [inst_6 : IsScalarTower R S M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : Module S N]
  [inst_10 : IsScalarTower R S N] (f : M →ₗ[S] N), (↑R f).ker = Submodule.restrictScalars R f.ker
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- This is a more convenient formulation to show that a `PushoutCocone` constructed using
`PushoutCocone.mk` is a colimit cocone.
 -/
CategoryTheory.Limits.PushoutCocone.IsColimit.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {W : C} →
            {inl : Y ⟶ W} →
              {inr : Z ⟶ W} →
                (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr) →
                  (desc : (s : CategoryTheory.Limits.PushoutCocone f g) → W ⟶ s.pt) →
                    (∀ (s : CategoryTheory.Limits.PushoutCocone f g),
                        CategoryTheory.CategoryStruct.comp inl (desc s) = s.inl) →
                      (∀ (s : CategoryTheory.Limits.PushoutCocone f g),
                          CategoryTheory.CategoryStruct.comp inr (desc s) = s.inr) →
                        (∀ (s : CategoryTheory.Limits.PushoutCocone f g) (m : W ⟶ s.pt),
                            CategoryTheory.CategoryStruct.comp inl m = s.inl →
                              CategoryTheory.CategoryStruct.comp inr m = s.inr → m = desc s) →
                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr eq)