mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.inl_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inl f g))
      (CategoryTheory.Limits.PreservesPushout.iso G f g).inv =
    CategoryTheory.Limits.pushout.inl (G.map f) (G.map g)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.hom_comp_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X},
  CategoryTheory.CategoryStruct.comp α.hom f = CategoryTheory.CategoryStruct.id X ↔ f = α.inv
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.ofLower_lt_ofLower : ∀ {α : Type u_1} [inst : Preorder α] {x y : Topology.WithLower α},
  Topology.WithLower.ofLower x < Topology.WithLower.ofLower y ↔ x < y
-- Init.Data.Rat.Lemmas
Rat.neg_divInt : ∀ (n d : ℤ), -Rat.divInt n d = Rat.divInt (-n) d
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_symm_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.isNClique_right : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → G.IsNClique (r + 1) (insert v t)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.liftK.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k k_1 : A ⟶ S.X₂) (e_k : k = k_1)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0), h.liftK k hk = h.liftK k_1 ⋯
-- Mathlib.Data.Ordmap.Ordnode
/-- O(m + n). Build a set on the disjoint union by combining sets on the factors.
`Or.inl a ∈ s.copair t` iff `a ∈ s`, and `Or.inr b ∈ s.copair t` iff `b ∈ t`.

```
copair {1, 2} {2, 3} = {inl 1, inl 2, inr 2, inr 3}
```  -/
Ordnode.copair : {α : Type u_1} → {β : Type u_2} → Ordnode α → Ordnode β → Ordnode (α ⊕ β)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.injOn_genWeightSpace : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M],
  Set.InjOn (fun χ => LieModule.genWeightSpace M χ) {χ | LieModule.genWeightSpace M χ ≠ ⊥}
-- Init.Data.String.Defs
String.Slice.mk.inj : ∀ {str : String} {startInclusive endExclusive : str.Pos}
  {startInclusive_le_endExclusive : startInclusive ≤ endExclusive} {str_1 : String}
  {startInclusive_1 endExclusive_1 : str_1.Pos} {startInclusive_le_endExclusive_1 : startInclusive_1 ≤ endExclusive_1},
  { str := str, startInclusive := startInclusive, endExclusive := endExclusive,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive } =
      { str := str_1, startInclusive := startInclusive_1, endExclusive := endExclusive_1,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive_1 } →
    str = str_1 ∧ startInclusive ≍ startInclusive_1 ∧ endExclusive ≍ endExclusive_1
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Countable.countable_functions : ∀ {L : FirstOrder.Language} [h : Countable L.Symbols], Countable ((l : ℕ) × L.Functions l)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombinationOn.eq_1 : ∀ (α : Type u_1) (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (v : α → M) (s : Set α),
  Finsupp.linearCombinationOn α M R v s =
    LinearMap.codRestrict (Submodule.span R (v '' s))
      (Finsupp.linearCombination R v ∘ₗ (Finsupp.supported R R s).subtype) ⋯
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.subset : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {t : Set E}, StrictConcaveOn 𝕜 t f → s ⊆ t → Convex 𝕜 s → StrictConcaveOn 𝕜 s f
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteBiproducts : ∀ (C : Type uC) [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C], CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.mapHomotopyCategory_homMk : ∀ {V W : SSet.Truncated 2} (f : V ⟶ W)
  {x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
  (e : SSet.Truncated.Edge x y),
  (SSet.Truncated.mapHomotopyCategory f).map (SSet.Truncated.HomotopyCategory.homMk e) =
    SSet.Truncated.HomotopyCategory.homMk (e.map f)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.nnnorm_toLp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : α → E) (hf : MeasureTheory.MemLp f p μ),
  ‖MeasureTheory.MemLp.toLp f hf‖₊ = (MeasureTheory.eLpNorm f p μ).toNNReal
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsMarkovKernel.prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.prodMkRight γ κ)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instSMul : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] →
                        [inst_7 : Module R₂ M₂] →
                          {S₂ : Type u_9} →
                            [inst_8 : DistribSMul S₂ M₂] →
                              [SMulCommClass R₂ S₂ M₂] → [ContinuousConstSMul S₂ M₂] → SMul S₂ (M₁ →SL[σ₁₂] M₂)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.coe_pi : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] (I : Set η) (H : (i : η) → Subgroup (f i)),
  ↑(Subgroup.pi I H) = I.pi fun i => ↑(H i)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.ofUniqueLift.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (X : Type u) (of : X → G)
  (h : ∀ {H : Type u} [inst_1 : AddGroup H] (f : X → H), ∃! F, ∀ (a : X), F (of a) = f a),
  FreeAddGroupBasis.ofUniqueLift X of h =
    FreeAddGroupBasis.ofLift X of
      (fun {H} [AddGroup H] =>
        { toFun := fun f => Classical.choose ⋯, invFun := fun F => ⇑F ∘ of, left_inv := ⋯, right_inv := ⋯ })
      ⋯
-- Mathlib.Algebra.Order.Interval.Basic
Interval.length_pure : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] (a : α), (Interval.pure a).length = 0
-- Mathlib.Topology.UniformSpace.Cauchy
/-- **Alias** of the reverse direction of `totallyBounded_insert`. -/
TotallyBounded.insert : ∀ {α : Type u} [uniformSpace : UniformSpace α] (a : α) {s : Set α}, TotallyBounded s → TotallyBounded (insert a s)
-- Mathlib.CategoryTheory.Sites.CoverPreserving
/-- A functor `G : (C, J) ⥤ (D, K)` between sites is *cover-preserving*
if for all covering sieves `R` in `C`, `R.functorPushforward G` is a covering sieve in `D`.
 -/
CategoryTheory.CoverPreserving : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.GrothendieckTopology C →
          CategoryTheory.GrothendieckTopology D → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_sSup_of_directedOn : ∀ {G : Type u_1} [inst : AddGroup G] {K : Set (AddSubgroup G)},
  K.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) K → ∀ {x : G}, x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℕ)
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj Y).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n }))
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n)
      (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) h)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The functor `Karoubi (HomologicalComplex C c) ⥤ HomologicalComplex (Karoubi C) c`.  -/
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c))
            (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c)
-- Mathlib.Data.Finsupp.Basic
/-- The equivalence between `α × β →₀ M` and `α →₀ β →₀ M` given by currying/uncurrying.  -/
Finsupp.curryEquiv : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : Zero M] → (α × β →₀ M) ≃ (α →₀ β →₀ M)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg_of_Z_eq_zero' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  P 2 = 0 → W'.neg P = ![P 0, -P 1, 0]
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- **Alias** of the reverse direction of `ContinuousLinearMap.isPositive_toLinearMap_iff`. -/
ContinuousLinearMap.IsPositive.toLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E), T.IsPositive → (↑T).IsPositive
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.postcomp_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f g : X ⟶ Y} (h : P.LeftHomotopy f g) {Z : C} (p : Y ⟶ Z),
  (h.postcomp p).h = CategoryTheory.CategoryStruct.comp h.h p
-- Mathlib.Data.Fin.Tuple.Basic
/-- Updating a tuple and adding an element at the beginning commute.  -/
Fin.cons_update : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin n) (y : α i.succ),
  Fin.cons x (Function.update p i y) = Function.update (Fin.cons x p) i.succ y
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isomorphisms_le_isoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass],
  CategoryTheory.MorphismProperty.isomorphisms C ≤ P.isoModSerre
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- If we take `J = I.comap f` then `quotientMap` is injective automatically.  -/
Ideal.quotientMap_injective : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] {I : Ideal S} {f : R →+* S} [inst_2 : I.IsTwoSided],
  Function.Injective ⇑(Ideal.quotientMap I f ⋯)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instBEqCnstrRHS : BEq Lean.Meta.Grind.CnstrRHS
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_iff_isLittleO_one : ∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) {F'' : Type u_10} [inst : Norm E] [inst_1 : Norm F]
  [inst_2 : NormedAddCommGroup F''] {f : α → E} {l : Filter α} [inst_3 : One F] [NormOneClass F] {c : F''},
  c ≠ 0 → ((f =o[l] fun _x => c) ↔ f =o[l] fun _x => 1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKeyD_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.alter t k f ≠ ∅ →
    ∀ {fallback : α},
      (Std.ExtDTreeMap.Const.alter t k f).maxKeyD fallback = k ↔
        (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Lean.Meta.Match.SimpH
/-- Apply the given substitution to `fvarIds`.
This is an auxiliary method for `substRHS`.
 -/
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.applySubst : Lean.Meta.FVarSubst → List Lean.FVarId → List Lean.FVarId
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.single_blocks : ∀ {n : ℕ} (h : 0 < n), (Composition.single n h).blocks = [n]
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : SecondCountableTopology E]
  [inst_7 : FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [inst_8 : μ.IsAddHaarMeasure] (f : SchwartzMap E F)
  (m : E),
  LineDeriv.lineDerivOp m ((SchwartzMap.toTemperedDistributionCLM E F μ) f) =
    (SchwartzMap.toTemperedDistributionCLM E F μ) (LineDeriv.lineDerivOp m f)
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
/-- The linear equivalence of multilinear maps on free modules over `R` indexed by `fun i => κ i` on
the domain and `ι'` on the codomain and the dependent, finitely supported maps from
`(Π i, κ i) × ι'` into `R`.
 -/
MultilinearMap.freeDFinsuppEquiv : {ι : Type uι} →
  {κ : ι → Type uκ} →
    {R : Type uR} →
      {ι' : Type u_1} →
        [DecidableEq ι] →
          [Fintype ι] →
            [inst : CommSemiring R] →
              [(i : ι) → Fintype (κ i)] →
                [(i : ι) → DecidableEq (κ i)] →
                  (Π₀ (x : ((i : ι) → κ i) × ι'), R) ≃ₗ[R] MultilinearMap R (fun i => Π₀ (x : κ i), R) (Π₀ (x : ι'), R)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedAdd.toIsOrderedAddMonoid : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α], IsOrderedAddMonoid α
-- Mathlib.Data.Seq.Defs
Stream'.Seq.val_cons : ∀ {α : Type u} (s : Stream'.Seq α) (x : α), ↑(Stream'.Seq.cons x s) = Stream'.cons (some x) ↑s
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.isLUB_of_l_image : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : Preorder β]
  (gi : GaloisCoinsertion l u) {s : Set β} {a : α}, IsLUB (l '' s) a → IsLUB s (u a)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M}, LinearIndependent R v ↔ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.inverse_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N) (g : N → M)
  (h₁ : Function.LeftInverse g ⇑f) (a : N), (f.inverse g h₁) a = g a
-- Mathlib.Order.Fin.Basic
Fin.monotone_castPred_comp : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : α → Fin (n + 1)} (hf : ∀ (a : α), f a ≠ Fin.last n),
  Monotone f → Monotone fun a => (f a).castPred ⋯
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- `toIocMod` is continuous on the right at every point.  -/
continuousWithinAt_toIocMod_Iic : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  ContinuousWithinAt (toIocMod hp a) (Set.Iic x) x
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_ne_zero_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {a : R},
  Int.fract a ≠ 0 ↔ a ∉ Set.range Int.cast
-- Mathlib.CategoryTheory.Sites.Hypercover.One
_private.Mathlib.CategoryTheory.Sites.Hypercover.One.0.CategoryTheory.PreOneHypercover.Hom.mapMulticospan.match_3.eq_1 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  (motive : (X Y : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) → (X ⟶ Y) → Sort u_4)
  (x : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) →
      motive x x (CategoryTheory.Limits.WalkingMulticospan.Hom.id x))
  (h_2 :
    (i : E.multicospanShape.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i))
        (CategoryTheory.Limits.WalkingMulticospan.right i) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i))
  (h_3 :
    (i : E.multicospanShape.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i))
        (CategoryTheory.Limits.WalkingMulticospan.right i) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)),
  (match x, x, CategoryTheory.Limits.WalkingMulticospan.Hom.id x with
    | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i)),
      .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.fst i => h_2 i
    | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i)),
      .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.snd i =>
      h_3 i) =
    h_1 x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_le_size_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, m.size ≤ (m.erase k).size + 1
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixingSubgroup_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], ⊥.fixingSubgroup = ⊤
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.ker_le_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H : Subgroup N),
  f.ker ≤ Subgroup.comap f H
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.lt_digits_length_iff : ∀ {b k : ℕ}, 1 < b → ∀ (n : ℕ), k < (b.digits n).length ↔ b ^ k ≤ n
-- Init.Data.String.Basic
String.ext_iff : ∀ {s₁ s₂ : String}, s₁ = s₂ ↔ s₁.toList = s₂.toList
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Lift an element of a tensor product and a scalar  -/
PolynomialLaw.exists_lift' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type v}
  [inst_3 : CommSemiring S] [inst_4 : Algebra R S] (t : TensorProduct R S M) (s : S),
  ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.mk.inj : ∀ {carrier : Type u} {str : CommMonoid carrier} {carrier_1 : Type u} {str_1 : CommMonoid carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.append_right : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)}, FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.Red.Step (L₁ ++ L₃) (L₂ ++ L₃)
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instIntCast : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → IntCast (TruncatedWittVector p n R)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
ofDegLex_injective : ∀ {α : Type u_1}, Function.Injective ⇑ofDegLex
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
/-- `f` is not true under any assignment.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable : (α : Type u) → {σ : Type v} → [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] → σ → Prop
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instLTOrdinal : LT Std.Time.Millisecond.Ordinal
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.map_left : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn)
  (g : N₁ ⋊[φ₁] G₁), ((SemidirectProduct.map fn fg h) g).left = fn g.left
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β)
  {s : Set α}, MeasurableSet s → ∀ {r : β}, r ≠ 0 → ⇑(f.restrict s) ⁻¹' {r} = s ∩ ⇑f ⁻¹' {r}
-- Mathlib.Order.Hom.Lattice
InfHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Min β] [inst_2 : Min γ] (f : InfHom β γ)
  (g : InfHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.coeff_rename_mapDomain : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ),
  Function.Injective f →
    ∀ (φ : MvPolynomial σ R) (d : σ →₀ ℕ),
      MvPolynomial.coeff (Finsupp.mapDomain f d) ((MvPolynomial.rename f) φ) = MvPolynomial.coeff d φ
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapDomainAlgHom.eq_1 : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (f : M →* N),
  MonoidAlgebra.mapDomainAlgHom R A f = { toRingHom := MonoidAlgebra.mapDomainRingHom A f, commutes' := ⋯ }
-- Mathlib.Data.Vector.Basic
List.Vector.inductionOn_cons : ∀ {α : Type u_1} {C : {n : ℕ} → List.Vector α n → Sort u_6} {n : ℕ} (x : α) (v : List.Vector α n)
  (nil : C List.Vector.nil) (cons : {n : ℕ} → {x : α} → {w : List.Vector α n} → C w → C (x ::ᵥ w)),
  ((x ::ᵥ v).inductionOn nil fun {n} {x} {w} => cons) = cons (v.inductionOn nil fun {n} {x} {w} => cons)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- If `f : ⦋m⦌ ⟶ ⦋n+1⦌` is a morphism and `j` is not in the range of `f`,
then `factor_δ f j` is a morphism `⦋m⦌ ⟶ ⦋n⦌` such that
`factor_δ f j ≫ δ j = f` (as witnessed by `factor_δ_spec`).
 -/
SimplexCategory.factor_δ : {m n : ℕ} → ({ len := m } ⟶ { len := n + 1 }) → Fin (n + 2) → ({ len := m } ⟶ { len := n })
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.mk.injEq : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (toHom : A →g B)
  (injective' : Function.Injective ⇑toHom) (toHom_1 : A →g B) (injective'_1 : Function.Injective ⇑toHom_1),
  ({ toHom := toHom, injective' := injective' } = { toHom := toHom_1, injective' := injective'_1 }) = (toHom = toHom_1)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.mkTypeMismatchError : Option Lean.MessageData → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.lintegral_laverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  (f : α → ENNReal), ∫⁻ (_x : α), ⨍⁻ (a : α), f a ∂μ ∂μ = ∫⁻ (x : α), f x ∂μ
-- Init.Data.UInt.Lemmas
USize.toUInt64_ofFin : ∀ {n : Fin USize.size}, (USize.ofFin n).toUInt64 = UInt64.ofNatLT ↑n ⋯
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial.eq_def : ∀ (n x : ℕ),
  n.descFactorial x =
    match x with
    | 0 => 1
    | k.succ => (n - k) * n.descFactorial k
-- Mathlib.Data.List.NodupEquivFin
OrderEmbedding.ofMapLEIff.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : PartialOrder α] [inst_1 : Preorder β] (f f_1 : α → β) (e_f : f = f_1)
  (hf : ∀ (a b : α), f a ≤ f b ↔ a ≤ b), OrderEmbedding.ofMapLEIff f hf = OrderEmbedding.ofMapLEIff f_1 ⋯