mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Message
Lean.indentD : Lean.MessageData → Lean.MessageData
-- Mathlib.Order.Circular
/-- The order of the `↔` has been chosen so that `rw [btw_cyclic]` cycles to the right while
`rw [← btw_cyclic]` cycles to the left (thus following the prepended arrow).  -/
btw_cyclic : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c ↔ btw c a b
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.ofHom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj A] [inst_3 : CategoryTheory.GrpObj B] (f : A ⟶ B)
  [inst_4 : CategoryTheory.IsMonHom f], (CategoryTheory.Grp.ofHom f).hom.hom = f
-- Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
_private.Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing.0.ModularForm.E₄CubeSubE₆SqForm_qExpansion_coeff_one : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄CubeSubE₆SqForm✝) = 1728
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- The transvection associated with a linear form `f` and a vector `v`.

NB. In mathematics, these linear maps are only called “transvections” when `f v = 0`.
See also `Module.preReflection` for a similar definition, up to a sign.  -/
LinearMap.transvection : {R : Type u_1} →
  {V : Type u_2} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid V] → [inst_2 : Module R V] → Module.Dual R V → V → V →ₗ[R] V
-- Init.Data.String.Defs
String.toByteArray_singleton : ∀ {c : Char}, (String.singleton c).toByteArray = [c].utf8Encode
-- Lean.Meta.Hint
/-- The granularity at which the diff for this suggestion should be rendered in the Infoview. See
`DiffMode` for the possible granularities. This is `.auto` by default.
 -/
Lean.Meta.Hint.Suggestion.diffGranularity : Lean.Meta.Hint.Suggestion → Lean.Meta.Hint.DiffGranularity
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.leibnizAdjunction_adj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) (adj₂ : F ⊣₂ G)
  [inst_3 : CategoryTheory.Limits.HasPullbacks C₂] [inst_4 : CategoryTheory.Limits.HasPushouts C₃]
  (X₁ : CategoryTheory.Arrow C₁),
  (F.leibnizAdjunction G adj₂).adj X₁ = CategoryTheory.Functor.LeibnizAdjunction.adj F G adj₂ X₁
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.finsuppAntidiag_zero : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : DecidableEq μ] [inst_2 : AddCommMonoid μ]
  [inst_3 : PartialOrder μ] [CanonicallyOrderedAdd μ] [inst_5 : Finset.HasAntidiagonal μ] (s : Finset ι),
  s.finsuppAntidiag 0 = {0}
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.homOfElement_eq_iff : ∀ {X : Type u} (x y : X), CategoryTheory.homOfElement x = CategoryTheory.homOfElement y ↔ x = y
-- Mathlib.Analysis.Analytic.Composition
/-- The `0`-th coefficient of `q.comp p` is `q 0`. Since these maps are multilinear maps in zero
variables, but on different spaces, we cannot state this directly, so we state it when applied to
arbitrary vectors (which have to be the zero vector).  -/
FormalMultilinearSeries.comp_coeff_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G]
  (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 0 → E) (v' : Fin 0 → F),
  (q.comp p 0) v = (q 0) v'
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.toMonObj : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {M : C} → [self : CategoryTheory.BimonObj M] → CategoryTheory.MonObj M
-- Mathlib.Data.Finset.Lattice.Fold
map_finset_sup' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  [inst_2 : FunLike F α β] [SupHomClass F α β] (f : F) {s : Finset ι} (hs : s.Nonempty) (g : ι → α),
  f (s.sup' hs g) = s.sup' hs (⇑f ∘ g)
-- Mathlib.Topology.Category.TopCat.Opens
/-- A homeomorphism of spaces gives an equivalence of categories of open sets.  -/
TopologicalSpace.Opens.mapMapIso : {X Y : TopCat} → (X ≅ Y) → (TopologicalSpace.Opens ↑Y ≌ TopologicalSpace.Opens ↑X)
-- Mathlib.Analysis.Analytic.Order
/-- If two functions agree in a neighborhood of `z₀`, then their orders at `z₀` agree.  -/
analyticOrderAt_congr : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜}, f =ᶠ[nhds z₀] g → analyticOrderAt f z₀ = analyticOrderAt g z₀
-- Mathlib.Analysis.Normed.Module.Ray
sameRay_iff_norm_smul_eq : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F}, SameRay ℝ x y ↔ ‖x‖ • y = ‖y‖ • x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.findEntry?_some_mem_toList : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α} {y : α × β} {t : RBTree.RBMap α β cmp},
  t.findEntry? x = some y → y ∈ t.toList
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instCompl.eq_1 : ∀ {R : Type u} {M : Type v} [inst : AddGroup R] [inst_1 : AddAction R M],
  SubAddAction.instCompl = { compl := fun s => { carrier := (↑s)ᶜ, vadd_mem' := ⋯ } }
-- Aesop.RuleTac.Cases
Aesop.CasesTarget'.patterns.sizeOf_spec : ∀ (ps : Array (Lean.Expr × Lean.Meta.SavedState)), sizeOf (Aesop.CasesTarget'.patterns ps) = 1 + sizeOf ps
-- Mathlib.RingTheory.Etale.Field
Algebra.FormallyEtale.iff_formallyUnramified_of_field : ∀ {K : Type u_1} {A : Type u} [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A] [Algebra.EssFiniteType K A],
  Algebra.FormallyEtale K A ↔ Algebra.FormallyUnramified K A
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality - strict inequality condition**.
The condition is that not all elements of `z` with a nonzero weight are equal to each other;
see `geom_mean_lt_arith_mean_weighted_iff_of_nonneg'` for a version that compares the elements to
their center of mass `∑ i ∈ s, w i * z i` instead.  -/
Real.geom_mean_lt_arith_mean_weighted_iff_of_nonneg : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 →
      (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, ∃ k ∈ s, w j ≠ 0 ∧ w k ≠ 0 ∧ z j ≠ z k)
-- Mathlib.Order.Hom.Lattice
Pi.evalLatticeHom_apply : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → Lattice (α i)] (i : ι) (f : (i : ι) → α i),
  (Pi.evalLatticeHom i) f = f i
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.splitEpiEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [inst_2 : F.Full] [inst_3 : F.Faithful],
  F.splitEpiEquiv f =
    { toFun := fun f_1 => f_1.map F, invFun := fun s => { section_ := F.preimage s.section_, id := ⋯ }, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.apply_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B) (x : B), e (e.symm x) = x
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_inter_cancel_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, (s ∪ t) ∩ s = s
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_eq_of_L2 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
  (x y : PiLp 2 β), dist x y = √(∑ i, dist (x.ofLp i) (y.ofLp i) ^ 2)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.nat_add_aleph0 : ∀ (n : ℕ), ↑n + Cardinal.aleph0 = Cardinal.aleph0
-- Init.Data.UInt.Lemmas
USize.div_self : ∀ {a : USize}, a / a = if a = 0 then 0 else 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [Inhabited α] {k fallback : α} {f : β k → β k}, (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.adj_of_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v x y : V} (p : G.Walk u v), s(x, y) ∈ p.edges → G.Adj x y
-- Lean.Meta.Closure
Lean.Meta.Closure.ToProcessElement.mk : Lean.FVarId → Lean.FVarId → Lean.Meta.Closure.ToProcessElement
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_id' : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) _auto_248✝ → cfcₙ (fun x => x) a = a
-- Mathlib.Topology.Instances.PNat
PNat.instNoncompactSpace : NoncompactSpace ℕ+
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
/-- **Alias** of the reverse direction of `EuclideanGeometry.Sphere.dist_sq_eq_iff_mem_orthRadius`. -/
EuclideanGeometry.Sphere.dist_sq_eq_of_mem_orthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  q ∈ s.orthRadius p → dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyonedaType.eq_1 : CommGrpCat.coyonedaType =
  {
    obj := fun X =>
      { obj := fun G => CommGrpCat.of (Opposite.unop X → ↑G),
        map := fun {X_1 Y} f =>
          CommGrpCat.ofHom (MonoidHom.pi fun i => (CommGrpCat.Hom.hom f).comp (Pi.evalMonoidHom (fun a => ↑X_1) i)),
        map_id := ⋯, map_comp := ⋯ },
    map := fun {X Y} f =>
      {
        app := fun G =>
          CommGrpCat.ofHom
            (MonoidHom.pi fun i => Pi.evalMonoidHom (fun a => ↑G) ((CategoryTheory.ConcreteCategory.hom f.unop) i)),
        naturality := ⋯ },
    map_id := CommGrpCat.coyonedaType._proof_4, map_comp := @CommGrpCat.coyonedaType._proof_5 }
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
/-- The (limit) fork which expresses `(Subfunctor.equalizer f g).toFunctor` as
the equalizer of `f` and `g`.  -/
CategoryTheory.Subfunctor.equalizer.fork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F₁ F₂ : CategoryTheory.Functor C (Type w)} →
      {A : CategoryTheory.Subfunctor F₁} → (f g : A.toFunctor ⟶ F₂) → CategoryTheory.Limits.Fork f g
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_ne_top : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y},
  eHolderNorm r f ≠ ⊤ ↔ MemHolder r f
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_val : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R),
  EuclideanDomain.gcd a b = EuclideanDomain.gcd (b % a) a
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.isMarkovKernel_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f),
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.deterministic f hf)
-- Mathlib.Analysis.SpecificLimits.Normed
HasSummableGeomSeries.summable_geometric_of_norm_lt_one : ∀ {K : Type u_4} {inst : NormedRing K} [self : HasSummableGeomSeries K] (ξ : K), ‖ξ‖ < 1 → Summable fun n => ξ ^ n
-- Lean.Data.Lsp.Internal
Lean.Lsp.ImportInfo.mk.inj : ∀ {module : String} {isPrivate isAll isMeta : Bool} {module_1 : String} {isPrivate_1 isAll_1 isMeta_1 : Bool},
  { module := module, isPrivate := isPrivate, isAll := isAll, isMeta := isMeta } =
      { module := module_1, isPrivate := isPrivate_1, isAll := isAll_1, isMeta := isMeta_1 } →
    module = module_1 ∧ isPrivate = isPrivate_1 ∧ isAll = isAll_1 ∧ isMeta = isMeta_1
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (toModuleCat : ModuleCat R)
  (form : QuadraticForm R ↑toModuleCat),
  sizeOf { toModuleCat := toModuleCat, form := form } = 1 + sizeOf toModuleCat + sizeOf form
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- The second leg of a pullback cone is a normal monomorphism if the right component is too.

See also `pullback.sndOfMono` for the basic monomorphism version, and
`normalOfIsPullbackFstOfNormal` for the flipped version.
 -/
CategoryTheory.normalOfIsPullbackSndOfNormal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q R S : C} →
        {f : P ⟶ Q} →
          {g : P ⟶ R} →
            {h : Q ⟶ S} →
              {k : R ⟶ S} →
                [hn : CategoryTheory.NormalMono h] →
                  (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm) →
                      CategoryTheory.NormalMono g
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback a `CompletelyDistribLattice.MinimalAxioms` along an injection.  -/
Function.Injective.completelyDistribLatticeMinimalAxioms : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  CompletelyDistribLattice.MinimalAxioms β →
    ∀ (f : α → β),
      Function.Injective f →
        (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
          (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) → CompletelyDistribLattice.MinimalAxioms α
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.existsUnique_mem_range : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), ∃! n, n < p ∧ x - ↑n ∈ IsLocalRing.maximalIdeal ℤ_[p]
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_toEquiv_symm : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  e.toEquiv.symm = ↑e.symm
-- Mathlib.Algebra.Group.Action.Pi
Pi.mulAction : {ι : Type u_1} →
  {α : ι → Type u_4} → (M : Type u_7) → {m : Monoid M} → [(i : ι) → MulAction M (α i)] → MulAction M ((i : ι) → α i)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.val_himp : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : ↥L), ↑(a ⇨ b) = ↑a ⇨ ↑b
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.intCast : {α : Type u} → [inst : Lean.Grind.Semiring α] → ℤ → Lean.Grind.Ring.OfSemiring.Q α
-- Mathlib.Logic.Relation
Relation.EqvGen.below.rel : ∀ {α : Type u_1} {r : α → α → Prop} {motive : (a a_1 : α) → Relation.EqvGen r a a_1 → Prop} (x y : α) (a : r x y),
  Relation.EqvGen.below ⋯
-- Mathlib.Data.List.Rotate
List.IsRotated.dropLast_tail : ∀ {α : Type u_1} {L : List α} (hL : L ≠ []), L.head hL = L.getLast hL → L.dropLast ~r L.tail
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul : ∀ {R : Type u_1} [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Ideal R}
  [inst_3 : P.IsPrime] [IsDomain R] [IsDomain S] [FaithfulSMul R S],
  IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
-- Aesop.Script.StructureDynamic
_private.Aesop.Script.StructureDynamic.0.Aesop.Script.structureDynamicCore.applyStepAndSolveRemaining : Lean.MVarId →
  Lean.Meta.SavedState →
    Array Lean.MVarId →
      Lean.MVarId → ℕ → Aesop.Script.Step → Aesop.Script.DynStructureM (Option Aesop.Script.DynStructureResult)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α] {f : (a : α) → β a → γ a}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    ∀ {h : Std.Internal.List.containsKey k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = true},
      Std.Internal.List.getKey k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) h = Std.Internal.List.getKey k l ⋯
-- Init.Data.UInt.Basic
instShiftRightUInt64 : ShiftRight UInt64
-- Lean.Compiler.LCNF.Types
Lean.Expr.isAny : Lean.Expr → Bool
-- Mathlib.RingTheory.DividedPowers.Basic
/-- If an element of a divided power ideal is killed by multiplication
by some nonzero integer `n`, then its `n`th power is zero.

Proposition 1.2.7 of [Berthelot-1974], part (i).  -/
DividedPowers.nilpotent_of_mem_dpIdeal : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {a : A} {n : ℕ},
  n ≠ 0 → (∀ {y : A}, y ∈ I → n • y = 0) → ∀ (hI : DividedPowers I), a ∈ I → a ^ n = 0
-- Mathlib.Algebra.Group.InjSurj
/-- A type has cancellative multiplication, if it admits an injective map that
preserves `*` to another type with cancellative multiplication.  -/
Function.Injective.isCancelMul : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : Mul M₂] [IsCancelMul M₂] (f : M₁ → M₂),
  Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → IsCancelMul M₁
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If ∠ABC = π, then (dist A C) = (dist A B) + (dist B C).  -/
EuclideanGeometry.dist_eq_add_dist_of_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi → dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂
-- Std.Data.DTreeMap.Raw.Basic
/-- Folds the given monadic function over the mappings in the map in descending order.  -/
Std.DTreeMap.Raw.foldrM : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → ((a : α) → β a → δ → m δ) → δ → Std.DTreeMap.Raw α β cmp → m δ
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.coe_toAddSubgroup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R), ↑s.toAddSubgroup = ↑s
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.symm_image_eq_source_inter_preimage : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  {s : Set Y}, s ⊆ e.target → ↑e.symm '' s = e.source ∩ ↑e ⁻¹' s
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Two factorisations through monomorphisms satisfying the universal property
must factor through isomorphic objects.  -/
CategoryTheory.Limits.IsImage.isoExt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {F F' : CategoryTheory.Limits.MonoFactorisation f} →
          CategoryTheory.Limits.IsImage F → CategoryTheory.Limits.IsImage F' → (F.I ≅ F'.I)
-- Mathlib.Order.Filter.Finite
Finset.eventuallyEq_iInter : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f g : ι → Set α},
  (∀ i ∈ s, f i =ᶠ[l] g i) → ⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i
-- Mathlib.Data.Rat.Lemmas
Rat.sub_natCast_den : ∀ (q : ℚ) (n : ℕ), (q - ↑n).den = q.den
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.π_symm : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₂ c₁ c₁₂]
  [TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂), c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)
-- Mathlib.Order.Hom.Lattice
/-- A `SupHomClass` morphism preserves suprema.  -/
SupHomClass.map_sup : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Max α} {inst_1 : Max β} {inst_2 : FunLike F α β}
  [self : SupHomClass F α β] (f : F) (a b : α), f (a ⊔ b) = f a ⊔ f b
-- Lean.KeyedDeclsAttribute
/-- Attribute name (e.g., `term_elab)  -/
Lean.KeyedDeclsAttribute.Def.name : {γ : Type} → Lean.KeyedDeclsAttribute.Def γ → Lean.Name
-- Mathlib.Order.Iterate
Function.Commute.iterate_pos_lt_iff_map_lt' : ∀ {α : Type u_1} [inst : LinearOrder α] {f g : α → α},
  Function.Commute f g → StrictMono f → Monotone g → ∀ {x : α} {n : ℕ}, 0 < n → (f^[n] x < g^[n] x ↔ f x < g x)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_eq_top : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂}, f.ker = ⊤ ↔ f = 0
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveExprProps.mk.sizeOf_spec : ∀ (expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx), sizeOf { expr := expr } = 1 + sizeOf expr
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_map_eq_toList_filterMapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {it : Std.IterM m β},
  (Std.IterM.map f it).toList = (Std.IterM.filterMapM (fun b => pure (some (f b))) it).toList
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- When `α` has a star operation, square matrices `Matrix n n α` have a star
operation equal to `Matrix.conjTranspose`.  -/
Matrix.instStar : {n : Type u_3} → {α : Type v} → [Star α] → Star (Matrix n n α)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_surjective_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Injective ⇑f → Function.Surjective (AddSubsemigroup.comap f)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_eq_stoppedValue : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι],
  MeasureTheory.stoppedProcess u τ = fun i => MeasureTheory.stoppedValue u fun ω => min (↑i) (τ ω)
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHSubOffset_4 : HSub Std.Time.PlainTime Std.Time.Hour.Offset Std.Time.PlainTime
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
nonneg_of_le_add_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddLeftReflectLE α] {a b : α}, a ≤ a + b → 0 ≤ b
-- Mathlib.Topology.Sheaves.Presheaf
/-- Pulling back along the inverse of a homeomorphism is the same as pushing forward along it.  -/
TopCat.Presheaf.pullbackInvIsoPushforwardHom : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} → (H : X ≅ Y) → TopCat.Presheaf.pullback C H.inv ≅ TopCat.Presheaf.pushforward C H.hom
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.sub_mem_orthogonal_of_inner_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} {x y : E}, (∀ (v : ↥K), inner 𝕜 (↑v) x = inner 𝕜 (↑v) y) → x - y ∈ Kᗮ
-- Mathlib.CategoryTheory.Limits.Sifted
/-- Sifted colimits commute with binary products  -/
CategoryTheory.IsSifted.colim_preservesBinaryProducts_of_isSifted : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
    CategoryTheory.Limits.colim