mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_3.splitter : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (x y : (CategoryTheory.WithTerminal C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3) →
      (x y : (CategoryTheory.WithTerminal C)ᵒᵖ) →
        (f : Opposite.unop y ⟶ Opposite.unop x) →
          (x_1 : x ⟶ y) →
            ((x y : C) →
                (f :
                    Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of y)) ⟶
                      Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of x))) →
                  (x_2 :
                      Opposite.op (CategoryTheory.WithTerminal.of x) ⟶ Opposite.op (CategoryTheory.WithTerminal.of y)) →
                    motive (Opposite.op (CategoryTheory.WithTerminal.of x))
                      (Opposite.op (CategoryTheory.WithTerminal.of y)) f x_2) →
              ((a : C) →
                  (x :
                      Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of a)) ⟶
                        Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star)) →
                    (x_2 :
                        Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op (CategoryTheory.WithTerminal.of a)) →
                      motive (Opposite.op CategoryTheory.WithTerminal.star)
                        (Opposite.op (CategoryTheory.WithTerminal.of a)) x x_2) →
                ((x :
                      Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star) ⟶
                        Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star)) →
                    (x_2 :
                        Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op CategoryTheory.WithTerminal.star) →
                      motive (Opposite.op CategoryTheory.WithTerminal.star)
                        (Opposite.op CategoryTheory.WithTerminal.star) x x_2) →
                  motive x y f x_1
-- Init.Data.Order.Ord
Std.TransCmp.gt_of_gt_of_gt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.gt → cmp b c = Ordering.gt → cmp a c = Ordering.gt
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.homMk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (τ₁ τ₁_1 : S₁.X₁ ⟶ S₂.X₁) (e_τ₁ : τ₁ = τ₁_1) (τ₂ τ₂_1 : S₁.X₂ ⟶ S₂.X₂)
  (e_τ₂ : τ₂ = τ₂_1) (τ₃ τ₃_1 : S₁.X₃ ⟶ S₂.X₃) (e_τ₃ : τ₃ = τ₃_1)
  (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
  (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃),
  CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃ = CategoryTheory.ShortComplex.homMk τ₁_1 τ₂_1 τ₃_1 ⋯ ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : Inhabited α] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.DTreeMap.Const.ofList l cmp).getKey! k' = k
-- Lean.Compiler.Specialize
Lean.Compiler.hasWeakSpecializeAttribute : Lean.Environment → Lean.Name → Bool
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instSubringClass : ∀ {K : Type u} [inst : Field K], SubringClass (ValuationSubring K) K
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.forM_eq_forM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m]
  {f : α → m PUnit.{w + 1}}, forM t f = t.toList.forM f
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.groupSeminorm.eq_1 : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M},
  QuotientGroup.groupSeminorm =
    { toFun := fun x => Metric.infDist 1 {m | ↑m = x}, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.bitraverse_comp : ∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t] {F G : Type u → Type u}
  [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β'),
  bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') =
    Functor.Comp.mk ∘ Functor.map (bitraverse f f') ∘ bitraverse g g'
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `Rat.den a`.  -/
Mathlib.Meta.Positivity.evalRatDen : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.instInhabitedContext : Inhabited Mathlib.Tactic.AtomM.Context
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonneg_iff : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R]
  [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R], 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.seq_destruct_cons : ∀ {α : Type u} (a : α) (s : Stream'.WSeq α), Stream'.Seq.destruct (Stream'.WSeq.cons a s) = some (some a, s)
-- Init.Data.Iterators.Lemmas.Combinators.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Append.0.Std.IterM.step_append.match_1.splitter : {α₁ β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α₁ m β] →
      {it₁ : Std.IterM m β} →
        (motive : it₁.Step → Sort u_3) →
          (x : it₁.Step) →
            ((it₁' : Std.IterM m β) →
                (out : β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩) →
              ((it₁' : Std.IterM m β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩) →
                ((h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves colimits, then `F.leftOp : Cᵒᵖ ⥤ D` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimits F],
  CategoryTheory.Limits.PreservesLimits F.leftOp
-- Mathlib.RingTheory.LocalRing.Module
_private.Mathlib.RingTheory.LocalRing.Module.0.term𝔪 : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Group.Torsor
/-- The map `p' ↦ p -ᵥ p'` as a homeomorphism: `Equiv.constVSub` as a homeomorphism  -/
Homeomorph.constVSub : {V : Type u_1} →
  {P : Type u_2} →
    [inst : AddGroup V] →
      [inst_1 : TopologicalSpace V] →
        [inst_2 : AddTorsor V P] → [inst_3 : TopologicalSpace P] → [IsTopologicalAddTorsor P] → P → P ≃ₜ V
-- Mathlib.Order.Lattice
Subtype.coe_inf : ∀ {α : Type u} [inst : SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) (x y : Subtype P),
  ↑(x ⊓ y) = ↑x ⊓ ↑y
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.coe_add : ∀ {α : Type u} [inst : Add α] (a b : α), ↑(a + b) = ↑a + ↑b
-- Mathlib.Analysis.LocallyConvex.AbsConvex
/-- **Alias** of the reverse direction of `absConvexHull_eq_self`. -/
AbsConvex.absConvexHull_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E}, AbsConvex 𝕜 s → (absConvexHull 𝕜) s = s
-- Mathlib.Topology.Bases
/-- In a first-countable space, a cluster point `x` of a sequence
is the limit of some subsequence.  -/
MapClusterPt.tendsto_subseq : ∀ {α : Type u} [t : TopologicalSpace α] [FirstCountableTopology α] {x : α} {u : ℕ → α},
  MapClusterPt x Filter.atTop u → ∃ ψ, StrictMono ψ ∧ Filter.Tendsto (u ∘ ψ) Filter.atTop (nhds x)
-- Lean.Declaration
Lean.ConstantInfo.axiomInfo : Lean.AxiomVal → Lean.ConstantInfo
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k fallback : α},
      (m₁.inter m₂ ⋯).getKeyD k fallback =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then m₁.getKeyD k fallback else fallback
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_surjective : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A],
  Function.Surjective ⇑imaginaryPart
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier : ∀ {R : CommRingCat} [IsJacobsonRing ↑R], JacobsonSpace ↥(AlgebraicGeometry.Spec R)
-- Mathlib.Order.IsNormal
Order.IsNormal.le_iff_le_sSup : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLinearOrder β],
  Order.IsNormal f →
    ∀ {x : α} {y : β}, (f ⁻¹' Set.Iic y).Nonempty → BddAbove (f ⁻¹' Set.Iic y) → (f x ≤ y ↔ x ≤ sSup (f ⁻¹' Set.Iic y))
-- Mathlib.SetTheory.Cardinal.Arithmetic
/-- Infinite types permit a relation where fewer elements than its cardinality
are missed along all verticals and fewer elements than its cardinality are hit
along all horizontals.  -/
Cardinal.exists_rel_mk_fibers_lt : ∀ (α : Type u_1) [Infinite α],
  ∃ r, (∀ (x : α), Cardinal.mk { y // ¬r x y } < Cardinal.mk α) ∧ ∀ (y : α), Cardinal.mk { x // r x y } < Cardinal.mk α
-- Mathlib.NumberTheory.Height.Projectivization
Projectivization.logHeight_eq_log_mulHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [inst_2 : Finite ι]
  (x : Projectivization K (ι → K)), x.logHeight = Real.log x.mulHeight
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_nonpos_iff_of_le : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : LinearOrder k] [IsStrictOrderedRing k] [inst_5 : PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E]
  {f : k → E} {x y : k}, x ≤ y → (slope f x y ≤ 0 ↔ f y ≤ f x)
-- Init.Data.SInt.Lemmas
Int16.toInt32_mod : ∀ (a b : Int16), (a % b).toInt32 = a.toInt32 % b.toInt32
-- Mathlib.CategoryTheory.ComposableArrows.Four
/-- The morphism `mk₃ f₁ f₂ f₃₄ ⟶ mk₃ f₁ f₂₃ f₄` when `f₂ ≫ f₂ = f₂₃` and `f₃ ≫ f₃ = f₃₄`.  -/
CategoryTheory.ComposableArrows.fourδ₃Toδ₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {i₀ i₁ i₂ i₃ i₄ : C} →
      (f₁ : i₀ ⟶ i₁) →
        (f₂ : i₁ ⟶ i₂) →
          (f₃ : i₂ ⟶ i₃) →
            (f₄ : i₃ ⟶ i₄) →
              (f₂₃ : i₁ ⟶ i₃) →
                (f₃₄ : i₂ ⟶ i₄) →
                  autoParam (CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃)
                      CategoryTheory.ComposableArrows.fourδ₃Toδ₂._auto_1 →
                    autoParam (CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄)
                        CategoryTheory.ComposableArrows.fourδ₃Toδ₂._auto_3 →
                      (CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃₄ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁ f₂₃ f₄)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono'_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.HomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h).left =
    CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h.left
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : Y ⟶ Z) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Y) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id X)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) h
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.whiskering_linearYoneda : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C],
  (CategoryTheory.linearYoneda R C).comp
      ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (ModuleCat R) (Type v)).obj (CategoryTheory.forget (ModuleCat R))) =
    CategoryTheory.yoneda
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.mk.inj : ∀ {α : Type u} {β : Type v} {inst : TopologicalSpace α} {inst_1 : TopologicalSpace β} {toContinuousMap : C(α, β)}
  {cocompact_tendsto' : Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (Filter.cocompact β)}
  {toContinuousMap_1 : C(α, β)}
  {cocompact_tendsto'_1 : Filter.Tendsto toContinuousMap_1.toFun (Filter.cocompact α) (Filter.cocompact β)},
  { toContinuousMap := toContinuousMap, cocompact_tendsto' := cocompact_tendsto' } =
      { toContinuousMap := toContinuousMap_1, cocompact_tendsto' := cocompact_tendsto'_1 } →
    toContinuousMap = toContinuousMap_1
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_add_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {g : α → ENNReal},
  Measurable g → μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g
-- Mathlib.Order.CompleteLattice.Lemmas
disjoint_of_sSup_disjoint : ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : Set α}, Disjoint (sSup a) (sSup b) → ⊥ ∉ a ∨ ⊥ ∉ b → Disjoint a b
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' : Φ.RightResolution X₂} (self : R.Hom R') {Z : C₂} (h : Φ.functor.obj R'.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp R.w (CategoryTheory.CategoryStruct.comp (Φ.functor.map self.f) h) =
    CategoryTheory.CategoryStruct.comp R'.w h
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.Over.mapComp.eq_1 : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Over.mapComp f g =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Over.isoMk
          (CategoryTheory.Iso.refl ((CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g)).obj x).left) ⋯)
      ⋯
-- Init.Omega.IntList
Lean.Omega.IntList.dot_set_left : ∀ (xs ys : Lean.Omega.IntList) (i : ℕ) (z : ℤ), (xs.set i z).dot ys = xs.dot ys + (z - xs.get i) * ys.get i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1ToTensorOfIsTrivial.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  groupHomology.H1ToTensorOfIsTrivial A =
    ((QuotientAddGroup.lift (groupHomology.shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
            ((Finsupp.liftAddHom fun g =>
                  ↑((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A) (Additive.ofMul (Abelianization.of g)))).comp
              (groupHomology.cycles₁ A).toAddSubgroup.subtype)
            ⋯).comp
        ↑(ModuleCat.Hom.hom (groupHomology.H1Iso A).hom)).toIntLinearMap
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_pow_apply_eq_card_walk : ∀ {α : Type u_1} {V : Type u_2} {G : SimpleGraph V} [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : DecidableEq V] [inst_3 : Semiring α] (n : ℕ) (u v : V),
  (SimpleGraph.adjMatrix α G ^ n) u v = ↑(Fintype.card ↑{p | p.length = n})
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.mk.inj : ∀ {R : Type u_5} {inst : CommSemiring R} {A : Type u_6} {B : Type u_7} {inst_1 : AddCommMonoid A}
  {inst_2 : AddCommMonoid B} {inst_3 : Module R A} {inst_4 : Module R B} {inst_5 : CoalgebraStruct R A}
  {inst_6 : CoalgebraStruct R B} {toCoalgHom : A →ₗc[R] B} {invFun : B → A}
  {left_inv : autoParam (Function.LeftInverse invFun toCoalgHom.toFun) Equiv.left_inv._autoParam}
  {right_inv : autoParam (Function.RightInverse invFun toCoalgHom.toFun) Equiv.right_inv._autoParam}
  {toCoalgHom_1 : A →ₗc[R] B} {invFun_1 : B → A}
  {left_inv_1 : autoParam (Function.LeftInverse invFun_1 toCoalgHom_1.toFun) Equiv.left_inv._autoParam}
  {right_inv_1 : autoParam (Function.RightInverse invFun_1 toCoalgHom_1.toFun) Equiv.right_inv._autoParam},
  { toCoalgHom := toCoalgHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toCoalgHom := toCoalgHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 } →
    toCoalgHom = toCoalgHom_1 ∧ invFun = invFun_1
-- Mathlib.Algebra.Order.Sub.Basic
add_tsub_eq_max : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, a + (b - a) = max a b
-- Lean.Elab.App
/-- Return `some namedArg` if `namedArgs` contains an entry for `binderName`.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.findNamedArg? : List Lean.Elab.Term.NamedArg → Lean.Name → Option Lean.Elab.Term.NamedArg
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.not_revMatchesAt_startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice},
  ¬String.Slice.Pattern.Model.RevMatchesAt pat s.startPos
-- Mathlib.Order.Filter.Map
Filter.kernMap_principal : ∀ {α : Type u_1} {β : Type u_2} {m : α → β} {s : Set α},
  Filter.kernMap m (Filter.principal s) = Filter.principal (Set.kernImage m s)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeff_single : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ) (m : M),
  (PolynomialModule.single R n m).coeff = fun₀ | n => m
-- Mathlib.Tactic.Linarith.Parsing
/-- `toCompFold red e_map exprs monom_map` folds `toComp` over `exprs`,
updating `e_map` and `monom_map` as it goes.
 -/
Mathlib.Tactic.Linarith.toCompFold : Lean.Meta.TransparencyMode →
  Mathlib.Tactic.Linarith.ExprMap →
    List Lean.Expr →
      Std.TreeMap Mathlib.Tactic.Linarith.Monom ℕ compare →
        Lean.MetaM
          (List Mathlib.Tactic.Linarith.Comp ×
            Mathlib.Tactic.Linarith.ExprMap × Std.TreeMap Mathlib.Tactic.Linarith.Monom ℕ compare)
-- Init.Data.Array.QSort.Basic
_private.Init.Data.Array.QSort.Basic.0.Array.qpartition.loop : {α : Type u_1} →
  {n : ℕ} →
    (α → α → Bool) →
      (lo hi : ℕ) →
        hi < n →
          α →
            Vector α n →
              (i k : ℕ) →
                autoParam (lo ≤ i) Array.qpartition._auto_2✝ →
                  autoParam (i ≤ k) Array.qpartition._auto_4✝ →
                    autoParam (k ≤ hi) Array.qpartition._auto_6✝ → { m // lo ≤ m ∧ m ≤ hi } × Vector α n
-- Mathlib.Topology.UnitInterval
unitInterval.symm_le_symm : ∀ {i j : ↑unitInterval}, unitInterval.symm i ≤ unitInterval.symm j ↔ j ≤ i
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover),
  P f ↔ ∀ (i : 𝒰.toPreZeroHypercover.1), P (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i)
-- Init.Data.Vector.Basic
/-- Maps elements of a vector using the function `f`,
which also receives the index of the element, and the fact that the index is less than the size of the vector.  -/
Vector.mapFinIdx : {α : Type u_1} → {n : ℕ} → {β : Type u_2} → Vector α n → ((i : ℕ) → α → i < n → β) → Vector β n
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
/-- An auxiliary definition used to define topology on `ContinuousMultilinearMap 𝕜 E F`.  -/
ContinuousMultilinearMap.toUniformOnFun : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    {E : ι → Type u_3} →
      {F : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : (i : ι) → TopologicalSpace (E i)] →
            [inst_2 : (i : ι) → AddCommGroup (E i)] →
              [inst_3 : (i : ι) → Module 𝕜 (E i)] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      ContinuousMultilinearMap 𝕜 E F → UniformOnFun ((i : ι) → E i) F {s | Bornology.IsVonNBounded 𝕜 s}
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- Morphisms in the `SimplexCategory`.  -/
SimplexCategory.Hom : SimplexCategory → SimplexCategory → Type
-- Mathlib.CategoryTheory.Localization.Equivalence
/-- Basic constructor of an equivalence between localized categories  -/
CategoryTheory.Localization.isEquivalence : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁)
  (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  (W₂ : CategoryTheory.MorphismProperty C₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor C₁ D₂)
  (G' : CategoryTheory.Functor D₁ D₂) [CategoryTheory.Localization.Lifting L₁ W₁ G G']
  (F : CategoryTheory.Functor C₂ D₁) (F' : CategoryTheory.Functor D₂ D₁)
  [CategoryTheory.Localization.Lifting L₂ W₂ F F'] (α : G.comp F' ≅ L₁) (β : F.comp G' ≅ L₂), G'.IsEquivalence
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- A colimit can be realised as a quotient of a coproduct.  -/
CategoryTheory.Limits.colimitQuotientCoproduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] →
          (F : CategoryTheory.Functor J C) → (∐ fun j => F.obj j) ⟶ CategoryTheory.Limits.colimit F
-- Mathlib.FieldTheory.Fixed
FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [Finite G],
  FiniteDimensional (↥(FixedPoints.subfield G F)) F
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α},
  m.contains a = false → m.get? a = none
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_empty : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {s : Set Ω}, (ProbabilityTheory.uniformOn s) ∅ = 0
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.mono : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCancelCommMonoid β] {A : Set α} {B : Set β}
  {f : α → β} {m n : ℕ}, m ≤ n → IsAddFreimanHom n A B f → IsAddFreimanHom m A B f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toList_roc_eq : ∀ {m n i : ℕ}, ((m<...=n).toList[i]?.isNone = true) = (n ≤ i + m)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Construct a cone for the empty diagram given an object.  -/
CategoryTheory.Limits.asEmptyCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → C → CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)
-- Mathlib.Geometry.Euclidean.Basic
/-- The condition for two points on a line to be equidistant from
another point.  -/
EuclideanGeometry.dist_smul_vadd_eq_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {v : V} (p₁ p₂ : P),
  v ≠ 0 → ∀ (r : ℝ), dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * inner ℝ v (p₁ -ᵥ p₂) / inner ℝ v v