mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ιOrZero_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄)
  (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j),
  HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
    HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.instLTColex : {ι : Type u_1} →
  {α : ι → Type u_2} → [inst : (i : ι) → Zero (α i)] → [LT ι] → [(i : ι) → LT (α i)] → LT (Colex (Π₀ (i : ι), α i))
-- Mathlib.Geometry.Manifold.HasGroupoid
OpenPartialHomeomorph.singletonChartedSpace_chartAt_source : ∀ {H : Type u} [inst : TopologicalSpace H] {α : Type u_5} [inst_1 : TopologicalSpace α] (e : OpenPartialHomeomorph α H)
  (h : e.source = Set.univ) {x : α}, (chartAt H x).source = Set.univ
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.pOpcycles_restrictionOpcyclesIso_inv_assoc : ∀ {ι : 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]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j : ι) (hi : c.prev j = i) {i' j' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hi'' : c'.prev j' = i') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j] {Z : C} (h : (K.restriction e).opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles j')
      (CategoryTheory.CategoryStruct.comp (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv h) =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').inv
      (CategoryTheory.CategoryStruct.comp ((K.restriction e).pOpcycles j) h)
-- Mathlib.Order.Filter.Extr
IsMaxFilter.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → ∀ {g : β → γ}, Antitone g → IsMinFilter (g ∘ f) l a
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_zero : CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.hom.app CategoryTheory.Limits.WalkingParallelPair.zero =
  CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WalkingParallelPair.zero
-- Init.Data.Nat.Log2
Nat.log2_def : ∀ (n : ℕ), n.log2 = if 2 ≤ n then (n / 2).log2 + 1 else 0
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.stalkToFiberRingHom_germ : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)) (x : ↑(ProjectiveSpectrum.top 𝒜))
  (hx : x ∈ U) (s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.stalkToFiberRingHom 𝒜 x))
      ((CategoryTheory.ConcreteCategory.hom
          ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ U x hx))
        s) =
    ↑s ⟨x, hx⟩
-- Init.Grind.Config
Lean.Grind.GrobnerConfig.toNoopConfig : Lean.Grind.GrobnerConfig → Lean.Grind.NoopConfig
-- Mathlib.Algebra.Colimit.Module
/-- The relation on the direct sum that generates the additive congruence that defines the
colimit as a quotient.  -/
Module.DirectLimit.Eqv : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        {G : ι → Type u_3} →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              ((i j : ι) → i ≤ j → G i →ₗ[R] G j) → [DecidableEq ι] → DirectSum ι G → DirectSum ι G → Prop
-- Mathlib.CategoryTheory.Subobject.Types
Types.monoOverEquivalenceSet_inverse_obj : ∀ (α : Type u) (s : Set α),
  (Types.monoOverEquivalenceSet α).inverse.obj s = CategoryTheory.MonoOver.mk (TypeCat.ofHom Subtype.val)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_comp_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [inst_1 : CategoryTheory.IsIso α]
  {f : X ⟶ Z} {g : Y ⟶ Z},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f = g ↔ f = CategoryTheory.CategoryStruct.comp α g
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.pow_eq_empty : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α} {n : ℕ}, s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.antilipschitz : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → AntilipschitzWith 1 f
-- Mathlib.Algebra.CharP.Invertible
CharP.isUnit_ofNat_iff : ∀ {R : Type u_1} [inst : Ring R] {p : ℕ} [CharP R p] {n : ℕ} [inst_2 : n.AtLeastTwo],
  Nat.Prime p → (IsUnit (OfNat.ofNat n) ↔ ¬p ∣ OfNat.ofNat n)
-- Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
CategoryTheory.InjectiveObject.instIsClosedUnderLimitsOfShapeIsInjectiveDiscrete : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (J : Type u_1),
  (CategoryTheory.isInjective C).IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J)
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- If `f` has a derivative at `x`, then `fderiv 𝕜 f x` is such a derivative. Otherwise, it is
set to `0`.  -/
fderiv : (𝕜 : Type u_4) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_5} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            {F : Type u_6} →
              [inst_4 : AddCommGroup F] →
                [inst_5 : Module 𝕜 F] → [inst_6 : TopologicalSpace F] → (E → F) → E → E →L[𝕜] F
-- Mathlib.Algebra.Homology.Embedding.TruncLE
ComplexShape.Embedding.truncLEFunctor.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e e_1 : c.Embedding c') (e_e : e = e_1)
  [inst : e.IsTruncLE] (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : CategoryTheory.CategoryWithHomology C], e.truncLEFunctor C = e_1.truncLEFunctor C
-- Init.Data.SInt.Bitwise
Int64.xor_left_inj : ∀ {a b : Int64} (c : Int64), a ^^^ c = b ^^^ c ↔ a = b
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOpEquiv_inverse_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {Y X : CategoryTheory.Limits.Cone F.op} (f : Y ⟶ X),
  CategoryTheory.Limits.coconeOpEquiv.inverse.map f = Opposite.op { hom := f.hom.unop, w := ⋯ }
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.algebraToUnder_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (A : (CategoryTheory.coprodMonad X).Algebra),
  (CategoryTheory.algebraToUnder X).obj A =
    CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl A.a)
-- Mathlib.Analysis.Normed.Operator.Banach
/-- An injective continuous linear map with a closed range defines a continuous linear equivalence
between its domain and its range.  -/
ContinuousLinearMap.equivRange : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] →
                      {σ' : 𝕜' →+* 𝕜} →
                        [inst_6 : RingHomInvPair σ σ'] →
                          [RingHomIsometric σ] →
                            [RingHomIsometric σ'] →
                              [CompleteSpace F] →
                                [CompleteSpace E] →
                                  [inst_11 : RingHomInvPair σ' σ] →
                                    {f : E →SL[σ] F} →
                                      Function.Injective ⇑f → IsClosed (Set.range ⇑f) → E ≃SL[σ] ↥(↑f).range
-- Mathlib.Algebra.Divisibility.Basic
/-- An element `a` in a semigroup is primal if whenever `a` is a divisor of `b * c`, it can be
factored as the product of a divisor of `b` and a divisor of `c`.  -/
IsPrimal : {α : Type u_1} → [Semigroup α] → α → Prop
-- Mathlib.Algebra.Lie.OfAssociative
AlgHom.toLieHom_id : ∀ {A : Type v} [inst : Ring A] {R : Type u} [inst_1 : CommRing R] [inst_2 : Algebra R A],
  (AlgHom.id R A).toLieHom = LieHom.id
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.postComp_b : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} {n : ℕ}
  {Z Z' : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z) (h : Z ⟶ Z') (i : Fin (n + 1)),
  (f.postComp h).b i = CategoryTheory.CategoryStruct.comp (f.b i) h
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.eval.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ), AdicCompletion.eval I M n = { toFun := fun f => ↑f n, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.dim_lt_of_nonDegenerate : ∀ (X : SSet) {n : ℕ} (x : ↑(X.nonDegenerate n)) (d : ℕ) [X.HasDimensionLT d], n < d
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, a ∈ m → m.getKey? a = some (m.getKey! a)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits, then `F.unop : C ⥤ D` preserves limits.  -/
CategoryTheory.Limits.preservesLimitsOfSize_unop : ∀ {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.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop
-- Mathlib.Geometry.Manifold.Algebra.Structures
/-- A `C^n` (semi)ring is a topological (semi)ring. This is not an instance for technical reasons,
see note [Design choices about smooth algebraic structures].  -/
topologicalSemiring_of_contMDiffRing : ∀ {𝕜 : Type u_1} {R : Type u_2} {E : Type u_3} {H : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace H]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : ChartedSpace H R] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) [inst_6 : Semiring R] [ContMDiffRing I n R],
  IsTopologicalSemiring R
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.inv_pair₁ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_1) [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p],
  RingHomInvPair (WittVector.FractionRing.frobeniusRingHom p k) ↑(WittVector.FractionRing.frobenius p k).symm
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_insertMany_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List (α × β)}, (Std.DTreeMap.Raw.Const.insertMany t l).size ≤ t.size + l.length
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
/-- `a ↦ a ^ p` is operator concave for `p ∈ [0,1]`.  -/
CFC.concaveOn_rpow : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {p : ℝ},
  p ∈ Set.Icc 0 1 → ConcaveOn ℝ (Set.Ici 0) fun a => a ^ p
-- Std.Data.TreeMap.Slice
Std.TreeMap.instSliceableRciSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.instSliceableRciSlice._auto_1) →
      Std.Rci.Sliceable (Std.TreeMap α β cmp) α (Std.DTreeMap.Internal.Const.RciSlice α β)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- Bird's Theorem 1  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.birdDetSpec_eq_det : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R), A.det = BirdDet.Spec.birdDet A
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : a ≤ b)
  (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))
      ((t.eTruncGEIsoGEGE a b hab).inv.app X) =
    CategoryTheory.CategoryStruct.id ((t.eTruncGE.obj b).obj ((CategoryTheory.Functor.id C).obj X))
-- Lean.Environment
/-- The final, complete constant info, potentially filled asynchronously.  -/
Lean.AsyncConstantInfo.constInfo : Lean.AsyncConstantInfo → Task Lean.ConstantInfo
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.interLift_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S}
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (f : G.Hom E) (g : G.Hom F)
  (i : G.I₀), (CategoryTheory.PreZeroHypercover.interLift f g).s₀ i = (f.s₀ i, g.s₀ i)
-- Mathlib.Data.Fin.SuccPred
Fin.lt_succAbove_iff_lt_castSucc : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p < p.succAbove i ↔ p < i.succ
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
InnerProductSpace.volume_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [Nontrivial E] (x : E) (r : ℝ),
  MeasureTheory.volume (Metric.closedBall x r) =
    ENNReal.ofReal r ^ Module.finrank ℝ E *
      ENNReal.ofReal (√Real.pi ^ Module.finrank ℝ E / Real.Gamma (↑(Module.finrank ℝ E) / 2 + 1))
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf_inj : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ K : Subgroup G}, H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_apply : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (f : PowerSeries R),
  (PowerSeries.expand p hp) f = PowerSeries.subst (PowerSeries.X ^ p) f
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match Lean.Grind.CommRing.Expr.num k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.intCast k => h_2 k
    | Lean.Grind.CommRing.Expr.natCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_1 k
-- Mathlib.Order.Filter.Map
Filter.range_mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β}, Set.range m ∈ Filter.map m f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.CommSq.cone_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z} (s : CategoryTheory.CommSq f g h i), s.cone.snd = g
-- Mathlib.LinearAlgebra.BilinearForm.Basic
/-- The restriction of a bilinear form on a submodule.  -/
LinearMap.BilinForm.restrict : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → LinearMap.BilinForm R M → (W : Submodule R M) → LinearMap.BilinForm R ↥W
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      AddMonoidAlgebra.Monic D q →
        p ≠ 0 → AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- `ofTensorProduct` is functorial in `M`.  -/
AdicCompletion.ofTensorProduct_naturality : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  AdicCompletion.map I f ∘ₗ AdicCompletion.ofTensorProduct I M =
    AdicCompletion.ofTensorProduct I N ∘ₗ TensorProduct.AlgebraTensorModule.map LinearMap.id f
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.SemiringExpr : Type
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.symm_mapsTo : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y},
  e.IsImage s t → Set.MapsTo (↑e.symm) (e.target ∩ t) (e.source ∩ s)
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.instCoeSortType : {R : Type u} → [inst : CommRing R] → CoeSort (BialgCat R) (Type v)
-- Mathlib.Topology.MetricSpace.Thickening
/-- **Alias** of `Metric.infEDist_le_infEDist_thickening_add`.

---

For the equality, see `infEDist_thickening`.  -/
Metric.infEdist_le_infEdist_thickening_add : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
  Metric.infEDist x s ≤ Metric.infEDist x (Metric.thickening δ s) + ENNReal.ofReal δ
-- Mathlib.Topology.Algebra.Group.Basic
map_mul_left_nhds_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (x : G),
  Filter.map (fun x_1 => x * x_1) (nhds 1) = nhds x
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- The regularized hypergeometric function.  -/
Complex.regularizedHGFun : Multiset ℂ → Multiset ℂ → ℂ → ℂ
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Module.DirectLimit.congr.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {G' : ι → Type u_5} [inst_5 : (i : ι) → AddCommMonoid (G' i)]
  [inst_6 : (i : ι) → Module R (G' i)] {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} (e e_1 : (i : ι) → G i ≃ₗ[R] G' i)
  (e_e : e = e_1) (he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)),
  Module.DirectLimit.congr e he = Module.DirectLimit.congr e_1 ⋯
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Coloring.toPartition_parts : ∀ {V : Type u} {G : SimpleGraph V} {α : Type v} (C : G.Coloring α), C.toPartition.parts = C.colorClasses
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.GetElem?.match_1.eq_1 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (e : elem) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match some e with
    | some e => h_1 e
    | none => h_2 ()) =
    h_1 e
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_inter_mul_prod_sdiff : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s t : Finset ι) (f : ι → M),
  (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x
-- Mathlib.Tactic.Check
/-- `#check t` elaborates the term `t` and then pretty prints it with its type as `e : ty`.

If `t` is an identifier, then it pretty prints a type declaration form
for the global constant `t` instead.
Use `#check (t)` to pretty print it as an elaborated expression.

Like the `#check` command, the `#check` tactic allows stuck typeclass instance problems.
These become metavariables in the output.

To display only explicit arguments in the type signature, see `#check'`.
 -/
Mathlib.Tactic.«tactic#check__» : Lean.ParserDescr
-- Mathlib.Topology.Category.UniformSpace
/-- Construct a bundled `UniformSpace` from the underlying type and the typeclass.  -/
UniformSpaceCat.of : (carrier : Type u) → [str : UniformSpace carrier] → UniformSpaceCat
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.GrpObj.inv = -CategoryTheory.CategoryStruct.id X
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural embedding `M →* M ∗ N`.  -/
Monoid.Coprod.inl : {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M →* Monoid.Coprod M N
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- Since `minpolyX` of our `generator` annihilates `X`, the minimal polynomial `φ`
must divide it.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.φ_dvd_generator_minpolyX : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  RatFunc.Luroth.φ✝ E ∣
    Polynomial.map (algebraMap ↥K⟮RatFunc.Luroth.generator E⟯ ↥E)
      ((RatFunc.Luroth.generator E).minpolyX ↥K⟮RatFunc.Luroth.generator E⟯)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- When `f : ℂ → E` is differentiable, the `cauchyPowerSeries f z R` represents `f` as a power
series centered at `z` in the entirety of `ℂ`, regardless of `R : ℝ≥0`, with `0 < R`.  -/
Differentiable.hasFPowerSeriesOnBall : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E},
  Differentiable ℂ f → ∀ (z : ℂ) {R : NNReal}, 0 < R → HasFPowerSeriesOnBall f (cauchyPowerSeries f z ↑R) z ⊤
-- Init.Data.List.Lemmas
List.getLast.eq_3 : ∀ {α : Type u} (head b : α) (as : List α) (x_2 : head :: b :: as ≠ []),
  (head :: b :: as).getLast x_2 = (b :: as).getLast ⋯