mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.module' : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {R₁ : Type u_5} →
        {s : ι → Type u_7} →
          [inst_1 : (i : ι) → AddCommMonoid (s i)] →
            [inst_2 : (i : ι) → Module R (s i)] →
              [inst_3 : Semiring R₁] →
                [inst_4 : Module R₁ R] → [SMulCommClass R₁ R R] → Module R₁ (PiTensorProduct R fun i => s i)
-- Mathlib.RingTheory.Etale.QuasiFinite
Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.FiniteType R S]
  (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal S) [inst_5 : q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q],
  ∃ R' x x_1,
    ∃ (_ : Algebra.Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ e,
            ∃ (_ : IsIdempotentElem e),
              ∃ e₀,
                ∃ (_ : IsIdempotentElem e₀) (_ :
                  (Algebra.TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e),
                  ∃ P',
                    ∃ (_ : P'.IsPrime) (_ : P'.LiesOver P),
                      Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = q ∧
                        e ∉ P' ∧
                          Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (Algebra.ofId R R') ⋯) ∧
                            (∀ (P'' : Ideal (TensorProduct R R' ↥(integralClosure R S))),
                                P''.IsPrime →
                                  P''.LiesOver P →
                                    e₀ ∉ P'' →
                                      P'' =
                                        Ideal.comap
                                          (Algebra.TensorProduct.map (AlgHom.id R' R')
                                              (integralClosure R S).val).toRingHom
                                          P') ∧
                              ∀ (P'' : Ideal (TensorProduct R R' S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.fst : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E × F} {g : α → G}, f =o[𝕜; l] g → (fun x => (f x).1) =o[𝕜; l] g
-- Mathlib.Order.SymmDiff
/-- Notation for symmDiff  -/
symmDiff.«term_∆_» : Lean.TrailingParserDescr
-- Mathlib.Data.Set.Lattice
Set.iUnion_iInter_ge_nat_add : ∀ {α : Type u_1} (f : ℕ → Set α) (k : ℕ), ⋃ n, ⋂ i, ⋂ (_ : i ≥ n), f (i + k) = ⋃ n, ⋂ i, ⋂ (_ : i ≥ n), f i
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.Forget₂.createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.Forget₂.createsLimit F =
    CategoryTheory.createsLimitOfReflectsIso fun c' t =>
      have this := ⋯;
      have this_1 := ⋯;
      {
        liftedCone :=
          {
            pt :=
              AddGrpCat.of (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddGrpCat))).pt,
            π :=
              {
                app := fun j =>
                  AddGrpCat.ofHom
                    (AddMonCat.limitπAddMonoidHom (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)) j),
                naturality := ⋯ } },
        validLift :=
          (AddMonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat))).uniqueUpToIso t,
        makesLimit :=
          CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget₂ AddGrpCat AddMonCat)
            (AddMonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)))
            (fun x =>
              {
                hom' :=
                  {
                    toFun := fun v =>
                      EquivLike.coe
                        (equivShrink
                          ↑((F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)).comp
                                (CategoryTheory.forget AddMonCat)).sections)
                        ⟨fun j =>
                          (CategoryTheory.ConcreteCategory.hom
                              (((CategoryTheory.forget AddMonCat).mapCone
                                      ((CategoryTheory.forget₂ AddGrpCat AddMonCat).mapCone x)).π.app
                                j))
                            v,
                          ⋯⟩,
                    map_zero' := ⋯, map_add' := ⋯ } })
            ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
/-- Equational lemma for `Pseudofunctor.isoMapOfCommSq` when
both vertical maps of the square are the same and horizontal maps are identities.  -/
CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {X₁ X₂ : B} (f : X₁ ⟶ X₂),
  F.isoMapOfCommSq ⋯ =
    CategoryTheory.Bicategory.whiskerRightIso (F.mapId X₁) (F.map f) ≪≫
      CategoryTheory.Bicategory.leftUnitor (F.map f) ≪≫
        (CategoryTheory.Bicategory.rightUnitor (F.map f)).symm ≪≫
          (CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId X₂)).symm
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_eq' : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ} (k : Fin n → ℕ) (x : Fin n → R),
  Function.Injective k → (∀ (i : Fin n), x i ≠ 0) → (∑ i, Polynomial.C (x i) * Polynomial.X ^ k i).support.card = n
-- Mathlib.Data.Set.Lattice
Set.iUnion_le_nat : ⋃ n, {i | i ≤ n} = Set.univ
-- Std.Data.DTreeMap.Internal.Operations
/-- The value.  -/
Std.DTreeMap.Internal.Impl.View.v : {α : Type u} → {β : α → Type v} → {size : ℕ} → (self : Std.DTreeMap.Internal.Impl.View α β size) → β self.k
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {he : t.isEmpty = false}, (cmp k (t.minKey he)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realMixedSpace K)
  {w : NumberField.InfinitePlace K} (hw : w.IsReal),
  (NumberField.mixedEmbedding.normAtPlace w) (↑(NumberField.mixedEmbedding.polarCoord K).symm x) = ‖x.1 ⟨w, hw⟩‖
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.getKey? k =
    (t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).isSome
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteLimits C]
  [CategoryTheory.Limits.PreservesFiniteLimits F], CategoryTheory.Limits.ReflectsFiniteLimits F
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `neg_add_lt_iff_lt_add`. -/
lt_add_of_neg_add_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, -b + a < c → a < b + c
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.ofIso_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X : C} [inst_2 : CategoryTheory.GrpObj G] (e : G ≅ X),
  CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom
-- Mathlib.Order.RelClasses
instIsWellFoundedTransGen : ∀ {α : Type u} (r : α → α → Prop) [i : IsWellFounded α r], IsWellFounded α (Relation.TransGen r)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a left homology data `h` is preserved by a functor `F`, this functor
preserves the cokernel of `h.f' : S.X₁ ⟶ h.K`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [h.IsPreservedBy F],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair h.f' 0) F
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_finsetSum : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_3} (s : Finset ι) (x y : R) (f : ι → Polynomial (Polynomial R)),
  Polynomial.evalEval x y (∑ i ∈ s, f i) = ∑ i ∈ s, Polynomial.evalEval x y (f i)
-- Lean.Elab.App
Lean.Elab.Term.hasElabWithoutExpectedType : Lean.Environment → Lean.Name → Bool
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.DTreeMap.Raw.Const.minEntryD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α × β → α × β
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
/-- `toDegLex` is the identity function to the `DegLex` of a type.  -/
toDegLex : {α : Type u_1} → α ≃ DegLex α
-- Mathlib.Data.ENNReal.Operations
ENNReal.toNNReal_sSup : ∀ (s : Set ENNReal), (∀ r ∈ s, r ≠ ⊤) → (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)
-- Init.Data.Array.MinMax
Array.min?_singleton_append' : ∀ {α : Type u_1} {x : α} [inst : Min α] {xs : Array α}, (#[x] ++ xs).min? = some (Array.foldl min x xs)
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasCondDistrib.comp_right : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {𝓩 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} {P : MeasureTheory.Measure Ω} {Y : Ω → 𝓨}
  {κ : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.SFinite P] [ProbabilityTheory.IsSFiniteKernel κ] {f : 𝓩 → 𝓧}
  {hf : Measurable f} {Z : Ω → 𝓩},
  ProbabilityTheory.HasCondDistrib Y Z (κ.comap f hf) P → ProbabilityTheory.HasCondDistrib Y (f ∘ Z) κ P
-- Init.Data.Vector.Attach
/-- If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.

This is useful when we need to use `attach` to show termination.

Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldl_subtype` below.
 -/
Vector.foldl_attach : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : β → α → β} {b : β},
  Vector.foldl (fun acc t => f acc ↑t) b xs.attach = Vector.foldl f b xs
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.lift_def : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0)
  (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r)
  (x : TrivSqZeroExt R M), (TrivSqZeroExt.lift f g hg hfg hgf) x = f x.fst + g x.snd
-- Mathlib.Order.Lattice.Congruence
LatticeCon.ker_r : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : FunLike F α β]
  [inst_3 : LatticeHomClass F α β] (f : F) (a a_1 : α),
  (LatticeCon.ker f).toSetoid a a_1 = Function.onFun (fun x1 x2 => x1 = x2) (⇑f) a a_1
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.coeff_invUnitsSub : ∀ {R : Type u_1} [inst : Ring R] (u : Rˣ) (n : ℕ), (PowerSeries.coeff n) (PowerSeries.invUnitsSub u) = 1 /ₚ u ^ (n + 1)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.covariantSequence_exact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n₀ n₁ : ℕ)
  (h : n₀ + 1 = n₁), (CategoryTheory.Abelian.Ext.covariantSequence X hS n₀ n₁ h).Exact
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.hasHomology : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'},
  e.f j = j' → ∀ [K.HasHomology j], (K.extend e).HasHomology j'
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- A contravariant linear map on coweight space.  -/
RootPairing.Hom.coweightMap : {ι : 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] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                {P : RootPairing ι R M N} → {Q : RootPairing ι₂ R M₂ N₂} → P.Hom Q → N₂ →ₗ[R] N
-- Aesop.Tree.ExtractProof
Aesop.extractProof : Aesop.TreeM Unit
-- Init.Data.List.Find
List.findSome?_replicate : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : ℕ} {a : α},
  List.findSome? f (List.replicate n a) = if n = 0 then none else f a
-- Lean.Data.Lsp.Window
Lean.Lsp.instFromJsonShowMessageParams : Lean.FromJson Lean.Lsp.ShowMessageParams
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.commute_noncommPiCoprod : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → Monoid (N i)] (ϕ : (i : ι) → N i →* M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)} {m : M},
  (∀ (i : ι) (x : N i), Commute m ((ϕ i) x)) → ∀ (h : (i : ι) → N i), Commute m ((MonoidHom.noncommPiCoprod ϕ hcomm) h)
-- Init.Data.List.Find
List.lookup_replicate_ne : ∀ {α : Type u_2} [inst : BEq α] {a : α} {n : ℕ} {α_1 : Type u_1} {b : α_1} {k : α},
  (!k == a) = true → List.lookup k (List.replicate n (a, b)) = none
-- Mathlib.Geometry.Euclidean.Congruence
/-- **Side–Angle–Side (SAS) congruence**
If two triangles have two sides and the included angle equal, then the triangles are congruent.
This holds even if the triangles are degenerate.  -/
EuclideanGeometry.side_angle_side : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {a b c : P₁} {a' b' c' : P₂},
  EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' →
    dist a b = dist a' b' → dist b c = dist b' c' → Congruent ![a, b, c] ![a', b', c']
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.submoduleOf_span_singleton_of_mem : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Submodule R M)
  {x : M} (hx : x ∈ N), (R ∙ x).submoduleOf N = R ∙ ⟨x, hx⟩
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.mk_surjective : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T),
  ∃ X Y g, f = CategoryTheory.Arrow.mk g
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.card_eq_iff_eq_top : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Finite ↥H], Nat.card ↥H = Nat.card G ↔ H = ⊤
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_lt_arsinh : ∀ {x y : ℝ}, Real.arsinh x < Real.arsinh y ↔ x < y
-- Init.Data.Iterators.Basic
/-- Converts elements of `α` into elements of `Shrink α`.  -/
Std.Shrink.deflate : {α : Type u_1} → α → Std.Shrink α
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.inv_hom_iso_homₚ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat),
  CategoryTheory.CategoryStruct.comp ((HP.iso i).inv.app X)
      (CategoryTheory.CategoryStruct.comp ((f.hom i).app X) ((HP'.iso i).hom.app X)) =
    (f.homₚ i).app (TopPair.ofTopCat X)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.functorExt.congr_simp : ∀ {J : CategoryTheory.Limits.MulticospanShape} {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan J) C}
  (left left_1 :
    (i : J.L) →
      F.obj (CategoryTheory.Limits.WalkingMulticospan.left i) ≅ G.obj (CategoryTheory.Limits.WalkingMulticospan.left i))
  (e_left : left = left_1)
  (right right_1 :
    (i : J.R) →
      F.obj (CategoryTheory.Limits.WalkingMulticospan.right i) ≅
        G.obj (CategoryTheory.Limits.WalkingMulticospan.right i))
  (e_right : right = right_1)
  (wl :
    ∀ (i : J.R),
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i)) (right i).hom =
        CategoryTheory.CategoryStruct.comp (left (J.fst i)).hom
          (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i)))
  (wr :
    ∀ (i : J.R),
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)) (right i).hom =
        CategoryTheory.CategoryStruct.comp (left (J.snd i)).hom
          (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i))),
  CategoryTheory.Limits.WalkingMulticospan.functorExt left right wl wr =
    CategoryTheory.Limits.WalkingMulticospan.functorExt left_1 right_1 ⋯ ⋯
-- Mathlib.Algebra.Group.Graph
MonoidHom.coe_mgraph : ∀ {G : Type u_1} {H : Type u_2} [inst : Monoid G] [inst_1 : Monoid H] (f : G →* H), ↑f.mgraph = {x | f x.1 = x.2}
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
IicProdIoc_le : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] {a b : ι} (hba : b ≤ a), IicProdIoc a b = Preorder.frestrictLe₂ hba ∘ Prod.fst
-- Mathlib.RingTheory.GradedAlgebra.Radical
Ideal.IsHomogeneous.radical_eq : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : CommRing A] [inst_1 : AddCommMonoid ι] [inst_2 : LinearOrder ι]
  [IsOrderedCancelAddMonoid ι] [inst_4 : SetLike σ A] [inst_5 : AddSubmonoidClass σ A] {𝒜 : ι → σ}
  [inst_6 : GradedRing 𝒜] {I : Ideal A},
  Ideal.IsHomogeneous 𝒜 I → I.radical = sInf {J | Ideal.IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.comap_map_eq : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [inst_3 : Ring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R A),
  Subalgebra.comap f (Subalgebra.map f S) = S ⊔ Algebra.adjoin R (⇑f ⁻¹' {0})
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Ioc_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a - b ∈ Set.Ioc c d ↔ b ∈ Set.Ico (a - d) (a - c)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.insert_toList : ∀ {α : Type u_1} {t : RBTree.RBNode α} {v : α} {p : RBTree.RBNode.Path α},
  (p.insert t v).toList = p.withList (RBTree.RBNode.setRoot v t).toList
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.mk_fst : ∀ {Δ Δ' : SimplexCategory} (f : Δ ⟶ Δ') [inst : CategoryTheory.Epi f],
  (CategoryTheory.SimplicialObject.Splitting.IndexSet.mk f).fst = Opposite.op Δ'
-- Init.Data.Int.Gcd
Int.gcd_eq_natAbs_left : ∀ {a b : ℤ}, a ∣ b → a.gcd b = a.natAbs
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
at a point, and all functions in the series are differentiable with a summable bound on the
derivatives, then the series is differentiable on the set and its derivative is the sum of the
derivatives.  -/
hasFDerivAt_tsum_of_isPreconnected : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  {u : α → ℝ} [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {f' : α → E → E →L[𝕜] F} {s : Set E} {x₀ x : E},
  Summable u →
    IsOpen s →
      IsPreconnected s →
        (∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) →
          (∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n) →
            x₀ ∈ s →
              (Summable fun n => f n x₀) → x ∈ s → HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isOpen_setOfPred_disjoint_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], IsOpen {p | Disjoint ↑p.1 ↑p.2}
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip_eps : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) [inst_1 : NormedSpace ℂ E],
  ∀ ε > 0,
    ∀ (z : ℂ),
      BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
        DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1) →
          z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1 →
            ‖f z‖ ≤
              ‖(↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 0)) ^ (1 - z) *
                  (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 1)) ^ z‖
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.uniformContinuous : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), UniformContinuous ⇑h
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.instEssSurjArrowQuotient : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V],
  (CategoryTheory.Preadditive.RightFreyd.quotient V).EssSurj
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_eq_prod_of_nonempty' : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  {eX eX' : OpenPartialHomeomorph X X'} {eY eY' : OpenPartialHomeomorph Y Y'},
  (eX'.prod eY').source.Nonempty → (eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY')
-- Init.Data.Array.GetLit
_private.Init.Data.Array.GetLit.0.Array.toListLitAux.match_1.eq_2 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → List α → Sort u_2) (i : ℕ) (hi : i + 1 ≤ xs.size)
  (acc : List α) (h_1 : (x : 0 ≤ xs.size) → (acc : List α) → motive 0 x acc)
  (h_2 : (i : ℕ) → (hi : i + 1 ≤ xs.size) → (acc : List α) → motive i.succ hi acc),
  (match i.succ, hi, acc with
    | 0, x, acc => h_1 x acc
    | i.succ, hi, acc => h_2 i hi acc) =
    h_2 i hi acc
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R], PowerSeries.X ≠ 0