mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.ENNReal.Operations
ENNReal.toReal_iSup : ∀ {ι : Sort u_1} {f : ι → ENNReal}, (∀ (i : ι), f i ≠ ⊤) → (iSup f).toReal = ⨆ i, (f i).toReal
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.instZeroPoint : {R : Type u_1} → [inst : CommRing R] → {σ : Type u_5} → (F : FormalGroup R) → Zero (F.Point σ)
-- Mathlib.RepresentationTheory.FDRep
/-- The forgetful functor to `Rep k G` preserves hom-sets and their vector space structure.  -/
FDRep.forget₂HomLinearEquiv : {R : Type u} →
  {G : Type v} →
    [inst : CommRing R] →
      [inst_1 : Monoid G] →
        (X Y : FDRep R G) →
          ((CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).obj X ⟶
              (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).obj Y) ≃ₗ[R]
            X ⟶ Y
-- Init.Data.Option.Lemmas
Option.isSome_get_of_isSome_pbind : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} (h : (o.pbind f).isSome = true),
  (f (o.get ⋯) ⋯).isSome = true
-- Mathlib.Data.Set.Sups
Set.sups_nonempty : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α}, (s ⊻ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousAt_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {x : α} {z : β},
  UpperSemicontinuousAt (fun _x => z) x
-- Init.Data.SInt.Bitwise
Int8.xor_left_inj : ∀ {a b : Int8} (c : Int8), a ^^^ c = b ^^^ c ↔ a = b
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.presheafFiberMap_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P : CategoryTheory.Functor Dᵒᵖ A} {T : A}
  {f g : (Φ.map F K).presheafFiber.obj P ⟶ T},
  (∀ (X : C) (x : Φ.fiber.obj X),
      CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) f =
        CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) g) →
    f = g
-- Mathlib.Algebra.Group.Conj
ConjClasses.mem_carrier_iff_mk_eq : ∀ {α : Type u} [inst : Monoid α] {a : α} {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioc_orderDual_def : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (b a : αᵒᵈ),
  Finset.Ioc b a = Finset.map OrderDual.toDual.toEmbedding (Finset.Ico (OrderDual.ofDual a) (OrderDual.ofDual b))
-- Mathlib.RingTheory.PicardGroup
/-- The canonical isomorphism between a module and the result of tensoring it
from the left by two mutually dual invertible modules.  -/
Module.Invertible.leftCancelEquiv : {R : Type u} →
  {M : Type v} →
    {N : Type u_1} →
      (P : Type u_2) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      (TensorProduct R M N ≃ₗ[R] R) → TensorProduct R M (TensorProduct R N P) ≃ₗ[R] P
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition]
  [inst_3 : Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X_1 : P.Over Q X),
  ((CategoryTheory.MorphismProperty.Over.mapCongr Q hfg hf).hom.app X_1).left =
    CategoryTheory.CategoryStruct.id X_1.left
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.of : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} (x y : M), r x y → AddConGen.Rel r x y
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.limit_cone_comp_aux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (s : CategoryTheory.Limits.Cone (F.comp G)) (j : C),
  CategoryTheory.CategoryStruct.comp (s.π.app (CategoryTheory.Functor.Initial.lift F (F.obj j)))
      (G.map (CategoryTheory.Functor.Initial.homToLift F (F.obj j))) =
    s.π.app j
-- Init.Data.Fin.Lemmas
Fin.mul_assoc : ∀ {n : ℕ} (a b c : Fin n), a * b * c = a * (b * c)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrderInf.mk : {α : Type u_3} →
  [toPartialOrder : PartialOrder α] →
    [toInfSet : InfSet α] →
      (∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)) →
        ConditionallyCompletePartialOrderInf α
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.exists_mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} {p : G → Prop}, (∃ g ∈ AddSubgroup.zmultiples x, p g) ↔ ∃ m, p (m • x)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.r'.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M),
  Localization.r' S = { r := fun a b => ∃ c, ↑c * (↑b.2 * a.1) = ↑c * (↑a.2 * b.1), iseqv := ⋯, mul' := ⋯ }
-- Mathlib.Algebra.Algebra.Equiv
AlgEquivClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : EquivLike F A B]
  [toRingEquivClass : RingEquivClass F A B],
  (∀ (f : F) (r : R), f ((algebraMap R A) r) = (algebraMap R B) r) → AlgEquivClass F R A B
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- A variant of `app_invApp` that gives an `eqToHom` instead of `homOfLE`.  -/
AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens)
  (hU : U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f) {Z : CommRingCat}
  (h :
    Y.presheaf.obj
        (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.appIso f ((TopologicalSpace.Opens.map f.base).obj U)).inv h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) h
-- Lean.Meta.Tactic.Cases
Lean.Meta.GeneralizeIndicesSubgoal.numEqs : Lean.Meta.GeneralizeIndicesSubgoal → ℕ
-- Lean.Meta.Sym.AlphaShareCommon
/-- Incremental variant of `shareCommonAlpha` for expressions constructed from already-shared subterms.

Use this when an expression `e` was produced by a Lean API (e.g., `inferType`, `mkApp4`) that
does not preserve maximal sharing, but the inputs to that API were already maximally shared.
In this case, only the newly constructed nodes need processing—the shared subterms can be
looked up directly in the `AlphaShareCommonM` state without building a temporary hashmap.

Unlike `shareCommonAlpha`, this function does not use a local `Std.HashMap ExprPtr Expr` to
track visited nodes. This is more efficient when the number of new (unshared) nodes is small,
which is the common case when wrapping API calls that build a few constructor nodes around
shared inputs.

Example:
```
-- `a` and `b` are already maximally shared
let result := mkApp2 f a b  -- result is not maximally shared
let result ← shareCommonAlphaInc result -- efficiently restore sharing
```
 -/
Lean.Meta.Sym.shareCommonAlphaInc : Lean.Expr → Lean.Meta.Sym.AlphaShareCommonM Lean.Expr
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The functor `LeftExtension L F ⥤ LeftExtension (G ⋙ L) (G ⋙ F)`
obtained by precomposition.  -/
CategoryTheory.Functor.LeftExtension.precomp : {C : Type u_1} →
  {C' : Type u_2} →
    {H : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (L : CategoryTheory.Functor C D) →
                  (F : CategoryTheory.Functor C H) →
                    (G : CategoryTheory.Functor C' C) →
                      CategoryTheory.Functor (L.LeftExtension F) ((G.comp L).LeftExtension (G.comp F))
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.EStateM.run_bind.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (x : α) (s : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.ok x s with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error e s => h_2 e s) =
    h_1 x s
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_le_ker_coord : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n}, k ≤ l.castSucc → b.flag k ≤ (b.coord l).ker
-- Init.Prelude
/-- The less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. -/
LT.lt : {α : Type u} → [self : LT α] → α → α → Prop
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.image_lipschitz : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {f : X → Y} {s N : Set X}
  {ε K₂ : NNReal}, Metric.IsCover ε s N → LipschitzWith K₂ f → Metric.IsCover (K₂ * ε) (f '' s) (f '' N)
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- Given an integrable function `f` with values in `ℝ≥0` in a sigma-finite space, there exists a
lower semicontinuous function `g > f` with integral arbitrarily close to that of `f`.
Formulation in terms of `integral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.  -/
MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnreal : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] {μ : MeasureTheory.Measure α}
  [μ.WeaklyRegular] [MeasureTheory.SigmaFinite μ] (f : α → NNReal),
  MeasureTheory.Integrable (fun x => ↑(f x)) μ →
    ∀ {ε : ℝ},
      0 < ε →
        ∃ g,
          (∀ (x : α), ↑(f x) < g x) ∧
            LowerSemicontinuous g ∧
              (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
                MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧
                  ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ε
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
/-- Extend all the  bits in the input BitVec w `x` to have width `w`,
then construct the parallel-prefix-sum circuit.  -/
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Init.Data.Array.Lemmas
Array.ne_empty_of_mem : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs → xs ≠ #[]
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.comp_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] (f : CocompactMap γ δ) (g : CocompactMap β γ)
  (h : CocompactMap α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsRegular.not_isSingular : ∀ {c : Cardinal.{u_1}}, c.IsRegular → ¬c.IsSingular
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderivFun_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {i : σ} (r : R), MvPowerSeries.pderivFun i (MvPowerSeries.C r) = 0
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instMulOneClass.eq_1 : ∀ {α : Type u_1} [inst : MulOneClass α],
  MulOpposite.instMulOneClass = { toMulOne := MulOpposite.instMulOne, one_mul := ⋯, mul_one := ⋯ }
-- Lean.MetavarContext
/-- Similar to `LocalContext.mkBinding`, but handles metavariables correctly.
This function trusts that `xs` has all forward dependencies that appear in `e` and that the variables are in order.
It will panic when any of the `xs` is neither a free variable nor a metavariable.

- If `usedOnly := true` then `forall` and `lambda` expressions are created only for used variables.
- If `usedLetOnly := true` then `let` expressions are created only for used (let-) variables.
- If `generalizeNondepLet := true` then nondependent let variables become `forall` or `lambda` expressions
  according to the value of `usedOnly`.
  Generally, `generalizeNondepLet` should be `true`
  *unless* all nondep entries in `xs` have known provenance,
  e.g. when leaving a telescope combinator like `Meta.lambdaLetTelescope`.
  See also `LocalDecl.ldecl`.
  - This needs to be `true` when making terms that should remain type correct with respect to the same `lctx`;
    for example, if `e' ← mkBinding true lctx xs e (generalizeNondepLet := true)`
    and `xs' ← xs.filterM (FVarId.isLetVar · false)`,
    then one has that `mkAppN e' xs'` is definitionally equal to `e` with respect to `lctx`.
  - **Note:** `generalizeNondepLet := true` is the common case, so `mkBinding` API uses it as the default.
 -/
Lean.MetavarContext.MkBinding.mkBinding : Bool →
  Lean.LocalContext →
    Array Lean.Expr → Lean.Expr → Bool → Bool → Bool → Bool → Lean.MetavarContext.MkBinding.M Lean.Expr
-- Mathlib.Data.Nat.Nth
Nat.nth_comp_of_strictMono : ∀ {p : ℕ → Prop} {n : ℕ} {f : ℕ → ℕ},
  StrictMono f →
    (∀ (k : ℕ), p k → k ∈ Set.range f) →
      (∀ (hfi : (Set.ofPred p).Finite), n < hfi.toFinset.card) → f (Nat.nth (fun i => p (f i)) n) = Nat.nth p n
-- Init.Data.String.Basic
String.Internal.toArray_empty : String.Internal.toArray "" = #[]
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.extend_apply' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] [inst_3 : DiscreteTopology δ] {f : α ↪ δ} {x : δ},
  x ∉ Set.range ⇑f →
    ∀ (g : BoundedContinuousFunction α β) (h : BoundedContinuousFunction δ β),
      (BoundedContinuousFunction.extend f g h) x = h x
-- Init.Data.Char.Lemmas
Char.lt_iff_val_lt_val : ∀ {a b : Char}, a < b ↔ a.val < b.val
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.maxEntry?.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β),
  x.maxEntry? =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => some ⟨k, v⟩
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      r.maxEntry?
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.instTopologicalSpaceInfiniteAdeleRing : (K : Type u_1) → [inst : Field K] → TopologicalSpace (NumberField.InfiniteAdeleRing K)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.aestronglyMeasurable_condExpInd : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasurableSet s →
    μ s ≠ ⊤ → ∀ (x : G), MeasureTheory.AEStronglyMeasurable (↑↑((MeasureTheory.condExpInd G hm μ s) x)) μ
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extended_coeIdeal_eq_map : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  (I₀ : Ideal A), FractionalIdeal.extended L hf ↑I₀ = ↑(Ideal.map f I₀)
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Sheaf.image_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F'),
  (CategoryTheory.Sheaf.image f).obj =
    (CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.range f.hom)).toFunctor
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_insert_one : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ} {a : α} [inst : DecidableEq α],
  a ∉ s → f a = 1 → Nat.multinomial (insert a s) f = (s.sum f).succ * Nat.multinomial s f
-- Mathlib.Data.EReal.Inv
EReal.div_lt_iff : ∀ {a b c : EReal}, 0 < c → c ≠ ⊤ → (b / c < a ↔ b < a * c)
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.PositivityExt.mk.injEq : ∀
  (eval eval_1 :
    {u : Lean.Level} →
      {α : Q(Type u)} →
        (zα : Q(Zero «$α»)) →
          (pα? : Option Q(PartialOrder «$α»)) →
            (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)),
  ({ eval := eval } = { eval := eval_1 }) = (eval = eval_1)
-- Mathlib.Order.Filter.NAry
/-- Symmetric statement to `Filter.map_map₂_distrib_right`.  -/
Filter.map_map₂_right_comm : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : Filter α} {g : Filter β}
  {m : α → β' → γ} {n : β → β'} {m' : α → β → δ} {n' : δ → γ},
  (∀ (a : α) (b : β), m a (n b) = n' (m' a b)) → Filter.map₂ m f (Filter.map n g) = Filter.map n' (Filter.map₂ m' f g)
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.norm_eq_one_of_mem_rootsOfUnity : ∀ {ζ : ℂˣ} {n : ℕ} [NeZero n], ζ ∈ rootsOfUnity n ℂ → ‖↑ζ‖ = 1
-- Mathlib.Combinatorics.Colex
Finset.toFinset_bitIndices_sum_two_pow : ∀ (s : Finset ℕ), (∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).counitIso.hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.ι_jointly_surjective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes},
  c.IsColimit → ∀ (y : c.pt), ∃ j x, c.ι j x = y
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_refl : ∀ (R : Type u_7) [inst : Mul R] [inst_1 : Add R], ⇑(RingEquiv.refl R) = id
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_one : CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.hom.app
    (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one) =
  CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one)
-- Lean.Environment
Lean.EnvExtension.AsyncMode.async.sizeOf_spec : ∀ (branch : Lean.AsyncBranch), sizeOf (Lean.EnvExtension.AsyncMode.async branch) = 1 + sizeOf branch
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.isLongestMatch_sliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (self : String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos),
  String.Slice.Pattern.Model.IsLongestMatch pat (startPos.sliceFrom endPos ⋯)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Transversal.mk.inj : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {inst : (i : ι) → Group (G i)} {inst_1 : Group H}
  {φ : (i : ι) → H →* G i} {injective : ∀ (i : ι), Function.Injective ⇑(φ i)} {set : (i : ι) → Set (G i)}
  {one_mem : ∀ (i : ι), 1 ∈ set i} {compl : ∀ (i : ι), Subgroup.IsComplement (↑(φ i).range) (set i)}
  {injective_1 : ∀ (i : ι), Function.Injective ⇑(φ i)} {set_1 : (i : ι) → Set (G i)}
  {one_mem_1 : ∀ (i : ι), 1 ∈ set_1 i} {compl_1 : ∀ (i : ι), Subgroup.IsComplement (↑(φ i).range) (set_1 i)},
  { injective := injective, set := set, one_mem := one_mem, compl := compl } =
      { injective := injective_1, set := set_1, one_mem := one_mem_1, compl := compl_1 } →
    set = set_1
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- The translation number of a `CircleDeg1Lift`, $τ(f)=\lim_{n→∞}\frac{f^n(x)-x}{n}$. We use
an auxiliary sequence `\frac{f^{2^n}(0)}{2^n}` to define `τ(f)` because some proofs are simpler
this way.  -/
CircleDeg1Lift.translationNumber : CircleDeg1Lift → ℝ
-- Lean.Elab.Tactic.Simp
Lean.Meta.DSimp.ConfigWithOptions.config : Lean.Meta.DSimp.ConfigWithOptions → Lean.Meta.DSimp.Config
-- Mathlib.Order.Hom.Bounded
BotHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Bot α] [inst_1 : Bot β] [inst_2 : Bot γ] (f : BotHom β γ)
  (g : BotHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.scalar_eq_coe_self_center : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : ↥(Subgroup.center (Matrix.SpecialLinearGroup n R))) (i : n), (Matrix.scalar n) (↑↑A i i) = ↑↑A
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.mk : {α : Type u_1} →
  [inst : CompleteLattice α] →
    (toSublattice : Sublattice α) →
      (∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier) →
        (∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier) → CompleteSublattice α
-- Mathlib.Order.RelSeries
RelSeries.length_toList : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r), x.toList.length = x.length + 1
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β)
  {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β},
  MeasureTheory.MeasurePreserving (⇑e) μa μb → MeasureTheory.MeasurePreserving (⇑e.symm) μb μa
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_zero : Nat.fermatNumber 0 = 3
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_finsupp_of_infinite' : ∀ (α β : Type u) [Nonempty α] [inst : Zero β] [Infinite β], Cardinal.mk (α →₀ β) = max (Cardinal.mk α) (Cardinal.mk β)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (P out).Property → Sort u_3) (h'' : (P out).Property { down := true })
  (h_1 : (h'' : (P out).Property { down := true }) → motive ⟨{ down := true }, h''⟩)
  (h_2 : (h'' : (P out).Property { down := false }) → motive ⟨{ down := false }, h''⟩),
  (match ⟨{ down := true }, h''⟩ with
    | ⟨{ down := true }, h''⟩ => h_1 h''
    | ⟨{ down := false }, h''⟩ => h_2 h'') =
    h_1 h''
-- Mathlib.Data.Set.Card
Set.encard_sdiff_singleton_add_one : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → (s \ {a}).encard + 1 = s.encard
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.grind.ematch.diagnostics : Lean.Option Bool