mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- If there is a `y` in `f`'s domain with `c = ArchimedeanClass (y - x)`, but there
is no closer `z` to `x` where the difference is of a higher `ArchimedeanClass`, then
`f.eval x` is simply `f.val y` truncated at `c`.

This doesn't mean every `x` can be evaluated this way: it is possible that one can find
an infinite chain of `y` that keeps getting closer to `x` in terms of Archimedean classes,
yet `x` is still isolated within a very high Archimedean class. In fact, in the next theorem,
we will show that there is always such chain for `x` not in `f`'s domain.  -/
HahnEmbedding.Partial.eval_eq_truncLT : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} {c : FiniteArchimedeanClass M} {y : ↥(↑f).domain},
  ArchimedeanClass.mk (↑y - x) = ↑c →
    (∀ (z : ↥(↑f).domain), ↑z - x ∉ FiniteArchimedeanClass.ball K c) →
      f.eval x = toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑↑f y)))
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_C : ∀ {F : Type u} [inst : Field F] (x : F), (Polynomial.C x).natSepDegree = 0
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_zero_left`.  -/
hammingDist_zero_left : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)], hammingDist 0 = hammingNorm
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- Auxiliary definition for `IsEventuallyConstantFrom.cocone`.  -/
CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} → F.IsEventuallyConstantFrom i₀ → [CategoryTheory.IsFiltered J] → (j : J) → F.obj j ⟶ F.obj i₀
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The product of elements in a complete lattice is the infimum.  -/
Preorder.isLimitIInf : {C : Type u} →
  [inst : CompleteLattice C] →
    {ι : Type u_1} →
      (X : ι → C) →
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (⨅ i, X i) fun i => CategoryTheory.homOfLE ⋯)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_fst'_eq_p₁_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] {Z : C} (h : A₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃))
      (CategoryTheory.CategoryStruct.comp (hf₁.fst' f₃) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃) h
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_real_smul : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {𝕜' : Type u_10} [inst_4 : RCLike 𝕜'] [inst_5 : NormedSpace 𝕜' F] {g : E → 𝕜'},
  Function.HasTemperateGrowth g → ∀ (c : ℝ), SchwartzMap.smulLeftCLM F (c • g) = c • SchwartzMap.smulLeftCLM F g
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.isSplittingField_sub : ∀ (K : Type u_1) (F : Type u_2) [inst : Field K] [inst_1 : Fintype K] [inst_2 : Field F] [inst_3 : Algebra F K],
  Polynomial.IsSplittingField F K (Polynomial.X ^ Fintype.card K - Polynomial.X)
-- Mathlib.Algebra.Module.Submodule.Lattice
/-- The universal set is the top element of the lattice of submodules.  -/
Submodule.instTop : {R : Type u_1} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Top (Submodule R M)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.DTreeMap.Raw.Const.unitOfList l cmp).isEmpty = l.isEmpty
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) {Z : C} (h : X.obj { len := n + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.σ j) h) =
    CategoryTheory.CategoryStruct.comp (X.σ (j.castLT ⋯)) (CategoryTheory.CategoryStruct.comp (X.δ (i.pred ⋯)) h)
-- Mathlib.Data.Finite.Prod
Equiv.finite_left : ∀ {α : Sort u_3} {β : Sort u_4} [Finite α], Finite (α ≃ β)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A function or predicate over `X` and `S` can be lifted to the localization if it
is invariant under expansion on the left.  -/
AddOreLocalization.liftExpand : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_3} →
          [inst_2 : AddAction R X] →
            {C : Sort u_2} →
              (P : X → ↥S → C) →
                (∀ (r : X) (t : R) (s : ↥S) (ht : t + ↑s ∈ S), P r s = P (t +ᵥ r) ⟨t + ↑s, ht⟩) →
                  AddOreLocalization S X → C
-- Init.Grind.PP
Lean.Grind.NodeDef : Type
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.Walk.length.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (v_3 : V) (h : G.Adj u v_3) (q : G.Walk v_3 v),
  (SimpleGraph.Walk.cons h q).length = q.length.succ
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.locality : ∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H) {e : OpenPartialHomeomorph H H},
  (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ G) → e ∈ G
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
CStarAlgebra.convexOn_ringInverse_algebraMap_add : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {t : ℝ},
  0 < t → ConvexOn ℝ (Set.Ici 0) fun x => Ring.inverse ((algebraMap ℝ A) t + x)
-- Init.Data.String.Slice
String.Slice.SplitIterator.operating.injEq : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  [inst : String.Slice.Pattern.ToForwardSearcher pat σ] (currPos : s.Pos)
  (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (currPos_1 : s.Pos)
  (searcher_1 : Std.Iter (String.Slice.Pattern.SearchStep s)),
  (String.Slice.SplitIterator.operating currPos searcher = String.Slice.SplitIterator.operating currPos_1 searcher_1) =
    (currPos = currPos_1 ∧ searcher = searcher_1)
-- Init.WF
measure : {α : Sort u} → (α → ℕ) → WellFoundedRelation α
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map sending `x : H × H → A` to `(g₁, g₂ : G × G) ↦ φ (x (f g₁, f g₂))`.  -/
groupCohomology.cochainsMap₂ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u_1, u, u} k H} →
          {B : Rep.{u_1, u, u} k G} →
            (f : G →* H) → (Rep.res f A ⟶ B) → (ModuleCat.of k (H × H → ↑A) ⟶ ModuleCat.of k (G × G → ↑B))
-- Std.Time.Time.Unit.Basic
/-- Converts a `Millisecond.Offset` to a `Nanosecond.Offset`.
 -/
Std.Time.Nanosecond.Offset.ofMilliseconds : Std.Time.Millisecond.Offset → Std.Time.Nanosecond.Offset
-- Mathlib.Tactic.FieldSimp.Attr
/-- Initialize the attribute `field` grouping the simprocs associated to the `field_simp` tactic.  -/
fieldSimpExt : Lean.Meta.Simp.SimprocExtension
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
/-- If `X : SSet`, this is the functor `X.N ⥤ SSet` which sends a
nondegenerate simplex of `X` to the subcomplex of `X` that it generates.  -/
SSet.functorN : (X : SSet) → CategoryTheory.Functor X.N SSet
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.continuous_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G}, IsBoundedBilinearMap 𝕜 f → ∀ {e₂ : F}, Continuous fun e₁ => f (e₁, e₂)
-- Mathlib.RepresentationTheory.Coinvariants
Representation.coinvariantsToFinsupp_mk_single : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] {ρ : Representation k G V} {α : Type u_9} (x : α) (a : V),
  (ρ.coinvariantsToFinsupp α) ((Representation.Coinvariants.mk (ρ.finsupp α)) fun₀ | x => a) =
    fun₀ | x => (Representation.Coinvariants.mk ρ) a
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates colimits, then `F.leftOp : Cᵒᵖ ⥤ D` creates limits.  -/
CategoryTheory.Limits.createsLimitsLeftOp : {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.CreatesColimits F] → CategoryTheory.CreatesLimits F.leftOp
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.orderTop_add_eq_left : ∀ {R : Type u_3} [inst : AddMonoid R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R},
  x.orderTop < y.orderTop → (x + y).orderTop = x.orderTop
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.elabSetOption : Lean.Elab.Tactic.Tactic
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.visitLevel : Lean.Level → Lean.CollectLevelParams.Visitor
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The Fubini theorem for a functor `F : J ⥤ K ⥤ C`,
showing that the colimit of `uncurry.obj F` can be computed as
the colimit of the colimits of the functors `F.obj j`.
 -/
CategoryTheory.Limits.colimitUncurryIsoColimitCompColim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C] →
                [inst_4 : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)] →
                  [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] →
                    CategoryTheory.Limits.colimit (CategoryTheory.Functor.uncurry.obj F) ≅
                      CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim)
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.mk''_rightQuotientEquiv : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : AddSubgroup.IsComplement (↑H) T)
  (q : Quotient (QuotientAddGroup.rightRel H)), Quotient.mk'' ↑(hT.rightQuotientEquiv q) = q
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- A vector with coprime entries, left-multiplied by a matrix in `SL(2, R)`, has
coprime entries.  -/
IsCoprime.mulVecSL : ∀ {R : Type u_1} [inst : CommRing R] {v : Fin 2 → R},
  IsCoprime (v 0) (v 1) → ∀ (A : Matrix.SpecialLinearGroup (Fin 2) R), IsCoprime ((↑A).mulVec v 0) ((↑A).mulVec v 1)
-- Mathlib.LinearAlgebra.Prod
/-- The first projection of a product is a linear map.  -/
LinearMap.fst : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → M × M₂ →ₗ[R] M
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.isTheta_congr_right : ∀ {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [inst : Norm G] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α},
  f' =Θ[l] g' → (k =Θ[l] f' ↔ k =Θ[l] g')
-- Mathlib.Order.Interval.Set.OrdConnected
Set.OrdConnected.preimage_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : β → α},
  s.OrdConnected → Monotone f → (f ⁻¹' s).OrdConnected
-- Mathlib.Data.FunLike.Equiv
EquivLike.toFunLike : {E : Sort u_1} → {α : Sort u_3} → {β : Sort u_4} → [EquivLike E α β] → FunLike E α β
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.divides_sq_eq_zero_z : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] {x y : ℤ}, x * x = ↑d * y * y → x = 0 ∧ y = 0
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The equiv between continuous representations are symmetric.  -/
ContRepresentation.Equiv.symm : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {ρ : ContRepresentation R G V} → {σ : ContRepresentation R G W} → ρ.Equiv σ → σ.Equiv ρ
-- Mathlib.Order.Bounds.Image
/-- The image under a monotone function of a set which is bounded below is bounded below.
See also `BddBelow.image2`.  -/
Monotone.map_bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {s : Set α}, BddBelow s → BddBelow (f '' s)
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_val : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), (s₁ \ s₂).val = s₁.val - s₂.val
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstr.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u}
  {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u}
  {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u}
  {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u}
  {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u}
  {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} (t : Lean.Meta.Grind.Arith.Linear.IneqCnstr)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t)
  (F_3 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t)
  (F_4 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t)
  (F_5 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t)
  (F_6 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t)
  (F_7 : (t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_3 t (Lean.Meta.Grind.Arith.Linear.IneqCnstr.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Init.Data.List.Lemmas
List.getLast_reverse : ∀ {α : Type u_1} {l : List α} (h : l.reverse ≠ []), l.reverse.getLast h = l.head ⋯
-- Mathlib.GroupTheory.NoncommPiCoprod
/-- The canonical homomorphism from a family of additive monoids. See also
`LinearMap.lsum` for a linear version without the commutativity assumption.  -/
AddMonoidHom.noncommPiCoprod : {M : Type u_1} →
  [inst : AddMonoid M] →
    {ι : Type u_2} →
      [Fintype ι] →
        {N : ι → Type u_3} →
          [inst_2 : (i : ι) → AddMonoid (N i)] →
            (ϕ : (i : ι) → N i →+ M) →
              (Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)) → ((i : ι) → N i) →+ M
-- Mathlib.LinearAlgebra.Basis.Bilinear
LinearMap.BilinForm.ext_iff_basis : ∀ {ι₁ : Type u_1} {Rₗ : Type u_10} {Mₗ : Type u_11} [inst : CommSemiring Rₗ] [inst_1 : AddCommMonoid Mₗ]
  [inst_2 : Module Rₗ Mₗ] (b₁' : Module.Basis ι₁ Rₗ Mₗ) {B B' : LinearMap.BilinForm Rₗ Mₗ},
  B = B' ↔ ∀ (i j : ι₁), (B (b₁' i)) (b₁' j) = (B' (b₁' i)) (b₁' j)
-- Mathlib.GroupTheory.Solvable
Group.isSolvable_def : ∀ (G : Type u_1) [inst : Group G], Group.IsSolvable G ↔ ∃ n, derivedSeries G n = ⊥
-- Mathlib.Algebra.BigOperators.Finprod
finprod_apply_ne_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (a : α), ∏ᶠ (_ : f a ≠ 1), f a = f a
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.hasDerivAt_log_log : ∀ {x : ℝ}, x ≠ 0 → x ≠ 1 → x ≠ -1 → HasDerivAt (fun x => Real.log (Real.log x)) (x⁻¹ / Real.log x) x
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_3.eq_4 : ∀ (motive : (X Y : CategoryTheory.Limits.WalkingReflexivePair) → (X ⟶ Y) → Sort u_1)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingReflexivePair) → motive x x (CategoryTheory.Limits.WalkingReflexivePair.Hom.id x))
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
  (h_3 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
  (h_4 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
  (h_5 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion)
  (h_6 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion),
  (match CategoryTheory.Limits.WalkingReflexivePair.zero, CategoryTheory.Limits.WalkingReflexivePair.one,
      CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion with
    | x, .(x), CategoryTheory.Limits.WalkingReflexivePair.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.left => h_2 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.right => h_3 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.zero), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion => h_4 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion => h_5 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion => h_6 ()) =
    h_4 ()
-- Init.Data.BitVec.Lemmas
BitVec.toInt_intMin_of_pos : ∀ {v : ℕ}, 0 < v → (BitVec.intMin v).toInt = -2 ^ (v - 1)
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.root_apply_eq_zero_of_notMem_rootSet : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [CharZero K]
  [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L) {h : ↥H},
  ↑h ∈ I → ∀ {β : ↥LieSubalgebra.root}, β ∉ I.rootSet → ↑β h = 0
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_iff_smul_mem : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s : Set E},
  Balanced 𝕜 s ↔ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
-- Init.Data.Vector.Lemmas
Vector.push_inj_right : ∀ {α : Type u_1} {n : ℕ} {a b : α} {xs : Vector α n}, xs.push a = xs.push b ↔ a = b
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosed_singleton_iff_isMaximal : ∀ {R : Type u} [inst : CommSemiring R] (x : PrimeSpectrum R), IsClosed {x} ↔ x.asIdeal.IsMaximal
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
_private.Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification.0.NumberField.InfinitePlace.embeddingConjugateIte.eq_1 : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L),
  NumberField.InfinitePlace.embeddingConjugateIte✝ v w =
    if NumberField.ComplexEmbedding.LiesOver w.embedding v.embedding then w.embedding
    else NumberField.ComplexEmbedding.conjugate w.embedding
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
DifferentiableWithinAt.mlieBracketWithin_congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s t : Set M} {x : M}
  {V W V₁ W₁ : (x : M) → TangentSpace I x} [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  MDiffAt[s] (T% V) x →
    Set.EqOn V₁ V t →
      V₁ x = V x →
        MDiffAt[s] (T% W) x →
          Set.EqOn W₁ W t →
            W₁ x = W x →
              UniqueMDiffAt[t] x →
                t ⊆ s → VectorField.mlieBracketWithin I V₁ W₁ t x = VectorField.mlieBracketWithin I V W s x
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = true ↔ ∀ (a : α), m.contains a = false
-- Mathlib.Analysis.Normed.Group.Basic
ne_zero_of_mem_sphere : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {r : ℝ}, r ≠ 0 → ∀ (x : ↑(Metric.sphere 0 r)), ↑x ≠ 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- The map of a binary fan is a limit iff the fork consisting of the mapped morphisms is a limit. This
essentially lets us commute `BinaryFan.mk` with `Functor.mapCone`.
 -/
CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {P X Y : C} →
            (f : P ⟶ X) →
              (g : P ⟶ Y) →
                CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.BinaryFan.mk f g)) ≃
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (G.map f) (G.map g))
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- `EqOnSource` is an equivalence relation.  -/
OpenPartialHomeomorph.eqOnSourceSetoid : {X : Type u_1} →
  {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → Setoid (OpenPartialHomeomorph X Y)
-- Mathlib.Data.Finset.Sups
Finset.subset_sups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {u : Finset α} {s t : Set α},
  ↑u ⊆ s ⊻ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊻ t'
-- Init.Data.List.MapIdx
List.mapIdx_reverse : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β},
  List.mapIdx f l.reverse = (List.mapIdx (fun i => f (l.length - 1 - i)) l).reverse
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombinationLineMapWeights_self : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] (i : ι) (c : k),
  Finset.affineCombinationLineMapWeights i i c = Pi.single i 1
-- Mathlib.Data.ENNReal.Basic
ENNReal.instAdd : Add ENNReal