mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.Maps
TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.congr_simp : ∀ (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ)
  [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : AddCommMonoid P] [inst_15 : Module A P]
  [inst_16 : AddCommMonoid Q] [inst_17 : Module R Q] [inst_18 : Module R P] [inst_19 : IsScalarTower R A P]
  [inst_20 : Algebra A B] [inst_21 : IsScalarTower A B M] [inst_22 : CommSemiring S] [inst_23 : Algebra R S]
  [inst_24 : Algebra S B] [inst_25 : Module S M] [inst_26 : Module S N] [inst_27 : IsScalarTower R S M]
  [inst_28 : SMulCommClass A S M] [inst_29 : SMulCommClass S A M] [inst_30 : IsScalarTower S B M]
  [inst_31 : IsScalarTower R S N],
  TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B M N P Q =
    TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B M N P Q
-- Init.Data.List.Lemmas
List.exists_mem_of_length_pos : ∀ {α : Type u_1} {l : List α}, 0 < l.length → ∃ a, a ∈ l
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {a : α} {fallback : β} {c : ℕ},
  Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.emptyWithCapacity c) a fallback = fallback
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffOn.contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffOn I I' n f s → s ∈ nhds x → ContMDiffAt I I' n f x
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.balanceₘ k v l r =
    if l.size + r.size ≤ 1 then Std.DTreeMap.Internal.Impl.bin k v l r
    else
      if h : r.size > Std.DTreeMap.Internal.delta * l.size then
        match r, h with
        | Std.DTreeMap.Internal.Impl.leaf, h => ⋯.elim
        | Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h => Std.DTreeMap.Internal.Impl.rotateL k v l rk rv rl rr
      else
        if h_1 : l.size > Std.DTreeMap.Internal.delta * r.size then
          match l, h, h_1 with
          | Std.DTreeMap.Internal.Impl.leaf, h, h_2 => ⋯.elim
          | Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_2 =>
            Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll lr r
        else Std.DTreeMap.Internal.Impl.bin k v l r
-- Mathlib.Topology.Connected.PathConnected
Topology.IsInducing.joinedIn_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {F : Set X}
  {f : X → Y}, Topology.IsInducing f → x ∈ F → y ∈ F → (JoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
_private.Mathlib.Analysis.InnerProductSpace.LinearMap.0.«term⟪_,_⟫_2» : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.forMUncurried_eq_forM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Monad m] [LawfulMonad m] {f : α × β → m PUnit.{w + 1}},
  Std.DTreeMap.Const.forMUncurried f t = (Std.DTreeMap.Const.toList t).forM f
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCastD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (fallback : β a),
  Std.DHashMap.Internal.AssocList.getCastD a fallback Std.DHashMap.Internal.AssocList.nil = fallback
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFrameAndAndOfSimpAnd : ∀ {φ ψ : Prop} (σs : List (Type u_1)) (P P' Q Q' QQ : Std.Do.SPred σs) [Std.Do.SPred.Tactic.HasFrame P Q φ]
  [Std.Do.SPred.Tactic.HasFrame P' Q' ψ] [Std.Do.SPred.Tactic.SimpAnd Q Q' QQ],
  Std.Do.SPred.Tactic.HasFrame spred(P ∧ P') QQ (φ ∧ ψ)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom.ext_iff : ∀ {B : Type u_1} {C : Type u_2} {inst : CategoryTheory.Bicategory C} {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {x y : X.Hom Y}, x = y ↔ x.hom = y.hom
-- Lean.Server.References
/-- Range where this reference occurs.  -/
Lean.Server.Reference.range : Lean.Server.Reference → Lean.Lsp.Range
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial
/-- Two polynomials in `MvPolynomial (m × m) k` over an infinite field `k` are equal if their
evaluations agree at every invertible matrix.

The proof considers `(p - q) * det(X)`, where `det(X) := Matrix.det (Matrix.mvPolynomialX m m k)`
is the generic determinant polynomial. Evaluated at any `s : m × m → k`, this product vanishes:
if `det (Matrix.of fun i j => s (i, j)) = 0` the determinant factor kills it; otherwise the
matrix is invertible and the hypothesis applies. By `MvPolynomial.funext` the product is zero,
and since `det(X) ≠ 0` and `MvPolynomial _ k` is an integral domain, `p = q`.  -/
MvPolynomial.eq_of_eval_eq_on_gl : ∀ {m : Type u_1} {k : Type u_2} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Field k] [Infinite k]
  {p q : MvPolynomial (m × m) k},
  (∀ (g : GL m k), (MvPolynomial.eval fun ij => ↑g ij.1 ij.2) p = (MvPolynomial.eval fun ij => ↑g ij.1 ij.2) q) → p = q
-- Mathlib.Data.Set.Card
Set.ncard_univ : ∀ (α : Type u_3), Set.univ.ncard = Nat.card α
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Every Schwartz function is smooth.  -/
SchwartzMap.smooth : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) (n : ℕ∞), ContDiff ℝ ↑n ⇑f
-- Mathlib.RingTheory.Flat.Basic
/-- If an `R`-module `M` is linearly equivalent to another `R`-module `N`, then `M` is flat
if and only if `N` is flat.  -/
Module.Flat.equiv_iff : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), Module.Flat R M ↔ Module.Flat R N
-- Mathlib.RepresentationTheory.Subrepresentation
/-- A subrepresentation is a submodule.  -/
Subrepresentation.toSubmodule : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] → {ρ : Representation A G W} → Subrepresentation ρ → Submodule A W
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis'.eRk_eq_eRk_insert : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → ∀ (e : α), M.eRk (insert e I) = M.eRk (insert e X)
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] (a a_1 : ↥b.support),
  a = a_1 → ∀ (a_2 a_3 : ↥b.support), a_2 = a_3 → b.cartanMatrix a a_2 = b.cartanMatrix a_1 a_3
-- Mathlib.Order.Disjoint
codisjoint_top_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, Codisjoint a ⊤
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- (implementation) tensor product of R-modules  -/
SemimoduleCat.MonoidalCategory.tensorObj : {R : Type u} → [inst : CommSemiring R] → SemimoduleCat R → SemimoduleCat R → SemimoduleCat R
-- Mathlib.Algebra.Homology.Embedding.TruncLE
ComplexShape.Embedding.truncLE'Functor_map : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncLE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.CategoryWithHomology C] {X Y : HomologicalComplex C c'} (φ : X ⟶ Y),
  (e.truncLE'Functor C).map φ = HomologicalComplex.truncLE'Map φ e
-- Mathlib.Algebra.CubicDiscriminant
Cubic.monic_of_c_eq_one : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 1 → P.toPoly.Monic
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} [inst_1 : SizeOf C]
  (toPreZeroHypercover : CategoryTheory.PreZeroHypercover S) (mem₀ : toPreZeroHypercover.presieve₀ ∈ J.coverings S),
  sizeOf { toPreZeroHypercover := toPreZeroHypercover, mem₀ := mem₀ } = 1 + sizeOf toPreZeroHypercover + sizeOf mem₀
-- Mathlib.Algebra.MonoidAlgebra.Lift
MonoidAlgebra.liftNC_single : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : NonUnitalNonAssocSemiring R] (f : k →+ R)
  (g : G → R) (a : G) (b : k), (MonoidAlgebra.liftNC f g) (MonoidAlgebra.single a b) = f b * g a
-- Mathlib.CategoryTheory.Limits.Opposites
/-- The limit of `F.rightOp` is the opposite of `colimit F`.  -/
CategoryTheory.Limits.limitRightOpIsoOpColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.Limits.limit F.rightOp ≅ Opposite.op (CategoryTheory.Limits.colimit F)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.HasBasis.nhds_of_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {ι : Sort u_1} {p : ι → Prop}
  {s : ι → Set G}, (nhds 1).HasBasis p s → ∀ (x : G), (nhds x).HasBasis p fun i => {y | y / x ∈ s i}
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : FrameHom α β) (f' : α → β)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one : ∀ (R : Type u_1) [inst : CommRing R] (p k : ℕ) [hn : Fact (Nat.Prime p)],
  Polynomial.cyclotomic (p ^ (k + 1)) R * (Polynomial.X ^ p ^ k - 1) = Polynomial.X ^ p ^ (k + 1) - 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryLED_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : α × β}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLED k fallback = t₂.getEntryLED k fallback
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.mulI_orthogonal_eq_symplComp : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H),
  Sᗮ.mulI = S.symplComp
-- Mathlib.Order.CompleteBooleanAlgebra
codisjoint_iInf₂_iff : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : Order.Coframe α] {a : α} {f : (i : ι) → κ i → α},
  Codisjoint a (⨅ i, ⨅ j, f i j) ↔ ∀ (i : ι) (j : κ i), Codisjoint a (f i j)
-- Init.Data.Order.PackageFactories
/-- Use this factory to conveniently define a linear order on a type `α` and all the associated
operations and instances given an `Ord α` instance.

Creates a `LinearOrderPackage α` instance. Such an instance entails `LE α`, `LT α`, `BEq α`,
`Ord α`, `Min α` and `Max α` instances as well as an `IsLinearOrder α` instance and `LawfulOrder*`
instances proving the compatibility of the operations with the linear order.

In the presence of `Ord α`, `TransOrd α` and `LawfulEqOrd α` instances, no arguments are required
and the factory can be used as in this
example:

```lean
public instance : LinearOrderPackage X := .ofLE X
```

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly
provide some arguments:

```lean
public instance : LinearOrderPackage X := .ofLE X {
  transOrd := sorry
  eq_of_compare := sorry }
```

It is also possible to do all of this by hand, without resorting to `LinearOrderPackage`. This
can be useful if, say, one wants to avoid specifying an `LT α` instance, which is not possible with
`LinearOrderPackage`.

**How the arguments are filled**

Lean tries to fill all of the fields of the `args : Packages.LinearOrderOfLEArgs α` parameter
automatically. If it fails, it is necessary to provide some of the fields manually.

* For the data-carrying typeclasses `LE`, `LT`, `BEq`, `Ord`, `Min` and `Max`, existing instances
  are always preferred. If no existing instances can be synthesized, it is attempted to derive an
  instance from the `Ord` instance.
* Some proof obligations can be filled automatically if the data-carrying typeclasses have been
  derived from the `Ord` instance. For example: If the `beq` field is omitted and no `BEq α` instance
  can be synthesized, it is derived from the `LE α` instance. In this case, `beq_iff`
  can be omitted because Lean can infer that `BEq α` and `Ord α` are compatible.
* Other proof obligations, such as `transOrd`, can be omitted if matching instances can be
  synthesized.
 -/
Std.LinearOrderPackage.ofOrd : (α : Type u) →
  autoParam (Std.Packages.LinearOrderOfOrdArgs α) Std.LinearOrderPackage.ofOrd._auto_1 → Std.LinearOrderPackage α
-- Init.Data.SInt.Bitwise
Int32.neg_one_xor : ∀ {a : Int32}, -1 ^^^ a = ~~~a
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₁_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C},
  CategoryTheory.OverPresheafAux.YonedaCollection.map₁ (CategoryTheory.CategoryStruct.id F) = id
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Multiplicative inverse of a rational function.  -/
RatFunc.inv : {K : Type u_1} → [inst : CommRing K] → [IsDomain K] → RatFunc K → RatFunc K
-- Mathlib.Tactic.Widget.Calc
/-- Is this the first calc step?  -/
CalcParams.isFirst : CalcParams → Bool
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.shearMulRight.eq_1 : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G],
  Homeomorph.shearMulRight G =
    { toEquiv := (Equiv.refl G).prodShear Equiv.mulLeft, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Algebra.Category.Grp.Basic
/-- Universe lift functor for commutative groups.  -/
CommGrpCat.uliftFunctor : CategoryTheory.Functor CommGrpCat CommGrpCat
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
measurable_lineDeriv_uncurry : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  [SecondCountableTopology E] [inst_10 : MeasurableSpace F] [BorelSpace F],
  Continuous f → Measurable fun p => lineDeriv 𝕜 f p.1 p.2
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] {inst_1 : DecidableLE β} [inst_2 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (xs xs_1 : List α), xs = xs_1 → List.maxIdxOn? f xs = List.maxIdxOn? f_1 xs_1
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mem_comap : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : AddGroup N]
  [inst_3 : TopologicalSpace N] {H : OpenAddSubgroup N} {f : G →+ N} {hf : Continuous ⇑f} {x : G},
  x ∈ OpenAddSubgroup.comap f hf H ↔ f x ∈ H
-- Init.Data.SInt.Bitwise
ISize.not_eq_neg_sub : ∀ (a : ISize), ~~~a = -a - 1
-- Mathlib.Algebra.Group.Units.Defs
/-- See `isAddUnit_iff_exists` for a similar lemma with one existential.  -/
isAddUnit_iff_exists_and_exists : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M}, IsAddUnit a ↔ (∃ b, a + b = 0) ∧ ∃ c, c + a = 0
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_balance! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size →
        (Std.DTreeMap.Internal.Impl.balance! k v l r).size = l.size + 1 + r.size
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPtInd_succ : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α) (N : ℕ) (x : α),
  (MeasureTheory.SimpleFunc.nearestPtInd e (N + 1)) x =
    if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (MeasureTheory.SimpleFunc.nearestPtInd e N) x
-- Mathlib.Algebra.Category.ModuleCat.Projective
ModuleCat.projective_of_categoryTheory_projective : ∀ {R : Type u} [inst : Ring R] (P : ModuleCat R) [Module.Projective R ↑P], CategoryTheory.Projective P
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flippingEquiv_apply_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.Functor.flippingEquiv F).obj k).map f = (F.map f).app k
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- Inversion on a group is a `MulEquiv` to the opposite group. When `G` is commutative, there is
`MulEquiv.inv`.  -/
MulEquiv.inv' : (G : Type u_3) → [inst : DivisionMonoid G] → G ≃* Gᵐᵒᵖ
-- Mathlib.Data.List.Palindrome
List.Palindrome.below.singleton : ∀ {α : Type u_1} {motive : (a : List α) → a.Palindrome → Prop} (x : α), List.Palindrome.below ⋯
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.homeomorphAddCircle_apply_mk : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p q : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [inst_4 : OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜),
  (AddCircle.homeomorphAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.associator_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H I : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B),
  (CategoryTheory.Lax.LaxTrans.associator η θ ι).inv.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.ext.injEq : ∀ (ext₁? : Option Lean.Meta.SimpExtension) (ext₂? : Option Lean.Meta.Simp.SimprocExtension)
  (h : (ext₁?.isSome || ext₂?.isSome) = true) (ext₁?_1 : Option Lean.Meta.SimpExtension)
  (ext₂?_1 : Option Lean.Meta.Simp.SimprocExtension) (h_1 : (ext₁?_1.isSome || ext₂?_1.isSome) = true),
  (Lean.Elab.Tactic.ResolveSimpIdResult.ext ext₁? ext₂? h =
      Lean.Elab.Tactic.ResolveSimpIdResult.ext ext₁?_1 ext₂?_1 h_1) =
    (ext₁? = ext₁?_1 ∧ ext₂? = ext₂?_1)
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.LawfulZipOperator.mk : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α]
  {f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α}
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f],
  (∀ (aig : Std.Sat.AIG α) (input1 input2 : aig.BinaryInput) (h : aig.decls.size ≤ (f aig input1).aig.decls.size)
      (assign : α → Bool), ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧) →
    Std.Sat.AIG.RefVec.LawfulZipOperator α f
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.comm_comp_map : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : Semiring D] [inst_8 : Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D),
  (↑(Algebra.TensorProduct.comm R C D)).comp (Algebra.TensorProduct.map f g) =
    (Algebra.TensorProduct.map g f).comp ↑(Algebra.TensorProduct.comm R A B)
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.derivWithin_eq_of_nhds : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  f₁ =ᶠ[nhds x] f → derivWithin f₁ s x = derivWithin f s x
-- Mathlib.Data.Nat.Init
/-- **Alias** of `Nat.pow_two_sub_pow_two`. -/
Nat.sq_sub_sq : ∀ (a b : ℕ), a ^ 2 - b ^ 2 = (a + b) * (a - b)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumAddHom_comm : ∀ {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁ → Type u_1} {β₂ : ι₂ → Type u_2} {γ : Type u_3} [inst : DecidableEq ι₁]
  [inst_1 : DecidableEq ι₂] [inst_2 : (i : ι₁) → AddZeroClass (β₁ i)] [inst_3 : (i : ι₂) → AddZeroClass (β₂ i)]
  [inst_4 : AddCommMonoid γ] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i)
  (h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ),
  (DFinsupp.sumAddHom fun i₂ => (DFinsupp.sumAddHom fun i₁ => h i₁ i₂) f₁) f₂ =
    (DFinsupp.sumAddHom fun i₁ => (DFinsupp.sumAddHom fun i₂ => (h i₁ i₂).flip) f₂) f₁
-- Mathlib.Topology.Algebra.Algebra
/-- The inclusion of the base ring in a topological algebra as a continuous linear map.  -/
algebraMapCLM : (R : Type u_1) →
  (A : Type u) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          [inst_3 : TopologicalSpace R] → [inst_4 : TopologicalSpace A] → [ContinuousSMul R A] → R →L[R] A
-- Std.Http.Transport
/-- Sends a single ByteArray.
 -/
Std.Http.Internal.Mock.Client.send : Std.Http.Internal.Mock.Client → ByteArray → Std.Async.Async Unit
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.smul_left : ∀ {α : Type u_2} {M : Type u_7} {R : Type u_8} [inst : TopologicalSpace α] [inst_1 : Zero M]
  [inst_2 : SMulZeroClass R M] {f : α → R} {f' : α → M}, HasCompactSupport f' → HasCompactSupport (f • f')
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_coeff_cert : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → ℕ → Bool
-- Mathlib.GroupTheory.Congruence.Defs
/-- The division induced on the quotient by a congruence relation on a type with a
division.  -/
Con.hasDiv : {M : Type u_1} → [inst : Group M] → (c : Con M) → Div c.Quotient
-- Mathlib.Order.Interval.Set.Defs
Set.OrdConnected.mk : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α},
  (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s) → s.OrdConnected
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.punitCoprod_apply : ∀ (M : Type u_1) [inst : Monoid M], ⇑(MulEquiv.punitCoprod M) = ⇑Monoid.Coprod.snd
-- Lean.CoreM
/-- Number of heartbeats passed inside `withRestoreOrSaveFull`, not used otherwise.  -/
Lean.Core.SavedState.passedHeartbeats : Lean.Core.SavedState → ℕ
-- Std.Data.ExtHashSet.Basic
/-- Computes the union of the given hash sets.

This function always merges the smaller set into the larger set, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.ExtHashSet.union : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → Std.ExtHashSet α → Std.ExtHashSet α