mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addCommMonoid : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : AddCommMonoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffAdd I' n G] → AddCommMonoid (ContMDiffMap I I' N G n)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- If a wideCoequalizer of `f` exists, we can access the corresponding projection by
saying `wideCoequalizer.π f`.  -/
CategoryTheory.Limits.wideCoequalizer.π : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        (f : J → (X ⟶ Y)) →
          [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] → Y ⟶ CategoryTheory.Limits.wideCoequalizer f
-- Mathlib.Algebra.IsPrimePow
IsPrimePow.not_isUnit : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → ¬IsUnit n
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1_sub : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f g : α → β) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ),
  MeasureTheory.Integrable.toL1 (f - g) ⋯ = MeasureTheory.Integrable.toL1 f hf - MeasureTheory.Integrable.toL1 g hg
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.instIsLeftDerivabilityStructureOppositeOpOpOfIsRightDerivabilityStructure : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  [Φ.IsRightDerivabilityStructure], Φ.op.IsLeftDerivabilityStructure
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_neg_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  (-μ).transpose B = -μ.transpose B
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Returns a term that is equal to `e`, but containing constructor applications
and literal values. `e` is the left-hand side of the equations in a `match`-expression
condition.
Remark: we could use the right-hand side to interrupt the recursion. For example,
suppose the equation is `x = ?head :: ?tail`. We only need to show that `x` is equal to
some term of the form `a :: as` to satisfy it. This function may return `a₁ :: b :: bs`,
which still allows us to satisfy the equation, but may have a bigger proof (e.g.,
a proof that `as` is equal to `b::bs`)
 -/
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.tryToProveFalse.go : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair_map_right : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y),
  (CategoryTheory.Limits.parallelPair f g).map CategoryTheory.Limits.WalkingParallelPairHom.right = g
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.defEq.injEq : ∀ (lhs : ℕ) (rhs : Lean.Meta.Grind.CnstrRHS) (lhs_1 : ℕ) (rhs_1 : Lean.Meta.Grind.CnstrRHS),
  (Lean.Meta.Grind.EMatchTheoremConstraint.defEq lhs rhs = Lean.Meta.Grind.EMatchTheoremConstraint.defEq lhs_1 rhs_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.RingTheory.Localization.Integer
IsLocalization.integerMultiple_injective : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {ι : Type u_4} (s : Finset ι) (f : ι → S),
  Function.Injective f → Function.Injective (IsLocalization.integerMultiple M s f)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHom : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' : Cᵒᵖ} {d d' : Dᵒᵖ} (f : d ⟶ d')
  (g : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f.unop g.unop).op
-- Mathlib.RingTheory.Congruence.Defs
RingCon.mk : {R : Type u_1} →
  [inst : Add R] →
    [inst_1 : Mul R] →
      (toCon : Con R) →
        (∀ {w x y z : R}, toCon.toSetoid w x → toCon.toSetoid y z → toCon.toSetoid (w + y) (x + z)) → RingCon R
-- Mathlib.RingTheory.Localization.Algebra
/-- An algebra map `A →ₐ[R] B` induces an algebra map on localizations `Aₚ →ₐ[Rₚ] Bₚ`.  -/
IsLocalization.mapₐ : {R : Type u_5} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {A : Type u_6} →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            {B : Type u_7} →
              [inst_3 : CommSemiring B] →
                [inst_4 : Algebra R B] →
                  (Rₚ : Type u_8) →
                    [inst_5 : CommSemiring Rₚ] →
                      [inst_6 : Algebra R Rₚ] →
                        [IsLocalization M Rₚ] →
                          (Aₚ : Type u_9) →
                            [inst_8 : CommSemiring Aₚ] →
                              [inst_9 : Algebra R Aₚ] →
                                [inst_10 : Algebra A Aₚ] →
                                  [IsScalarTower R A Aₚ] →
                                    [IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ] →
                                      (Bₚ : Type u_10) →
                                        [inst_13 : CommSemiring Bₚ] →
                                          [inst_14 : Algebra R Bₚ] →
                                            [inst_15 : Algebra B Bₚ] →
                                              [IsScalarTower R B Bₚ] →
                                                [IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ] →
                                                  [inst_18 : Algebra Rₚ Aₚ] →
                                                    [inst_19 : Algebra Rₚ Bₚ] →
                                                      [IsScalarTower R Rₚ Aₚ] →
                                                        [IsScalarTower R Rₚ Bₚ] → (A →ₐ[R] B) → Aₚ →ₐ[Rₚ] Bₚ
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v)))
  (X : CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{w, v, u} F),
  (CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence F).inverse.obj X =
    Opposite.op (F.elementsMk (Opposite.op X.left) (CategoryTheory.uliftYonedaEquiv X.hom))
-- Init.Data.Fin.Lemmas
Fin.rev_succ : ∀ {n : ℕ} (k : Fin n), k.succ.rev = k.rev.castSucc
-- Init.Grind.Ring.Basic
/-- Multiplication is commutative.  -/
Lean.Grind.CommSemiring.mul_comm : ∀ {α : Type u} [self : Lean.Grind.CommSemiring α] (a b : α), a * b = b * a
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Mk₁.map.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (isLt isLt_1 : 0 < 2)
  (x_3 : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩),
  CategoryTheory.ComposableArrows.Mk₁.map f ⟨0, isLt⟩ ⟨0, isLt_1⟩ x_3 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨0, isLt⟩)
-- Mathlib.Data.Fintype.Quotient
_private.Mathlib.Data.Fintype.Quotient.0.Quotient.listChoice.match_1.splitter : {ι : Type u_1} → (motive : (a : ι) → a ∈ [] → Sort u_2) → (a : ι) → (a_1 : a ∈ []) → motive a a_1
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_nnratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ≥0), (↑q).imJ = 0
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R) {e : R}, Nat.rawCast 1 = e → a ^ 0 = e + 0
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
CategoryTheory.JointlyReflectIsomorphisms.shortComplexQuasiIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [inst_2 : CategoryTheory.Abelian C] [inst_3 : (i : I) → CategoryTheory.Abelian (D i)]
      [inst_4 : CategoryTheory.CategoryWithHomology C]
      [inst_5 : ∀ (i : I), CategoryTheory.Limits.PreservesFiniteLimits (F i)]
      [inst_6 : ∀ (i : I), CategoryTheory.Limits.PreservesFiniteColimits (F i)] {S₁ S₂ : CategoryTheory.ShortComplex C}
      (f : S₁ ⟶ S₂),
      CategoryTheory.ShortComplex.QuasiIso f ↔
        ∀ (i : I), CategoryTheory.ShortComplex.QuasiIso ((F i).mapShortComplex.map f)
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedHGFunCoeff_eq_zero_right : ∀ (a b : Multiset ℂ) (n m : ℕ),
  autoParam (-↑n - ↑m ∈ b) Complex.regularizedHGFunCoeff_eq_zero_right._auto_1 → Complex.regularizedHGFunCoeff a b n = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.ext_iff : ∀ {X : SSet} {n : ℕ} {f g : X.Path n}, f = g ↔ f.vertex = g.vertex ∧ f.arrow = g.arrow
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittMul_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittMul p 0 = MvPolynomial.X (0, 0) * MvPolynomial.X (1, 0)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.preservesEpimorphisms_π₁ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C],
  CategoryTheory.ShortComplex.π₁.PreservesEpimorphisms
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_addConst : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.Poly.denote ctx (p.addConst k) = Int.Internal.Linear.Poly.denote ctx p + k
-- Batteries.Data.List.Lemmas
List.isSuffixOf?_eq_some_iff_append_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs ys zs : List α}, xs.isSuffixOf? ys = some zs ↔ zs ++ xs = ys
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- If `γ` is a nonzero element of a linearly ordered group with zero element adjoined, then `{γ}`
is a neighbourhood of `γ`.  -/
WithZeroTopology.singleton_mem_nhds_of_ne_zero : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀}, γ ≠ 0 → {γ} ∈ nhds γ
-- Mathlib.Tactic.Peel
/-- If `f` is a lambda then use its binding name to generate a new hygienic name,
and otherwise choose a new hygienic name.  -/
Mathlib.Tactic.Peel.mkFreshBinderName : Lean.Expr → Lean.MetaM Lean.Name
-- Mathlib.ModelTheory.Definability
/-- A coordinate projection is a definable function.  -/
FirstOrder.Language.definableFun_var : ∀ {M : Type u_1} (L : FirstOrder.Language) [inst : L.Structure M] {α : Type u_2} (i : α),
  Set.DefinableFun L ∅ fun v => v i
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
/-- Elliptic elements have no fixed points in `OnePoint K`.  -/
Matrix.GeneralLinearGroup.IsElliptic.smul_ne_self : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] [inst_2 : LinearOrder K] [IsStrictOrderedRing K]
  {g : GL (Fin 2) K}, g.IsElliptic → ∀ (c : OnePoint K), g • c ≠ c
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_sdiff_singleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} [T1Space E] (y : E),
  HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_3.eq_2 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l'))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l' => h_3 l'
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_2 ()
-- Mathlib.Data.Set.Function
Set.MapsTo.comp_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} (g : β → γ),
  Set.MapsTo f s t → Set.MapsTo (g ∘ f) s (g '' t)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.toList_eq_fold : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toList = Std.Iter.fold (fun l out => l ++ [out]) [] it
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_eq_mk_iff_associated : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, Associates.mk a = Associates.mk b ↔ Associated a b
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.continuousOn_logb : ∀ {b : ℝ}, ContinuousOn (Real.logb b) {0}ᶜ
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMapClass.mk : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} [inst : TopologicalSpace α] [inst_1 : Zero β]
  [inst_2 : TopologicalSpace β] [inst_3 : FunLike F α β] [toContinuousMapClass : ContinuousMapClass F α β],
  (∀ (f : F), HasCompactSupport ⇑f) → CompactlySupportedContinuousMapClass F α β
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseSigned : Std.Internal.Parsec.String.Parser ℕ → Std.Internal.Parsec.String.Parser ℤ
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
tateComplexFunctor_obj : ∀ (R G : Type u) [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G),
  (tateComplexFunctor R G).obj M = tateComplex M
-- Mathlib.Order.Bounds.Defs
/-- `a` is a greatest element of a set `s`; for a partial order, it is unique if exists.  -/
IsGreatest : {α : Type u_1} → [LE α] → Set α → α → Prop
-- Mathlib.Algebra.Category.MonCat.Basic
MulEquiv.toCommMonCatIso.eq_1 : ∀ {X Y : Type u} [inst : CommMonoid X] [inst_1 : CommMonoid Y] (e : X ≃* Y),
  e.toCommMonCatIso =
    { hom := CommMonCat.ofHom e.toMonoidHom, inv := CommMonCat.ofHom e.symm.toMonoidHom, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edgeFinset_replaceVertex_of_adj : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : DecidableEq V] [inst_1 : Fintype V]
  [inst_2 : DecidableRel G.Adj],
  G.Adj s t →
    (G.replaceVertex s t).edgeFinset =
      (G.edgeFinset \ G.incidenceFinset t ∪ Finset.image (fun x => s(x, t)) (G.neighborFinset s)) \ {s(t, t)}
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- For a manifold `N` and a `C^n` homomorphism `φ` between additive Lie groups `G'`,
`G''`, the 'left-composition-by-`φ`' group homomorphism from `C^n⟮I, N; I', G'⟯` to
`C^n⟮I, N; I'', G''⟯`.  -/
ContMDiffMap.compLeftAddMonoidHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    (I : ModelWithCorners 𝕜 E H) →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            (N : Type u_6) →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {E'' : Type u_7} →
                                    [inst_9 : NormedAddCommGroup E''] →
                                      [inst_10 : NormedSpace 𝕜 E''] →
                                        {H'' : Type u_8} →
                                          [inst_11 : TopologicalSpace H''] →
                                            {I'' : ModelWithCorners 𝕜 E'' H''} →
                                              {n : WithTop ℕ∞} →
                                                {G' : Type u_10} →
                                                  [inst_12 : AddMonoid G'] →
                                                    [inst_13 : TopologicalSpace G'] →
                                                      [inst_14 : ChartedSpace H' G'] →
                                                        [inst_15 : ContMDiffAdd I' n G'] →
                                                          {G'' : Type u_11} →
                                                            [inst_16 : AddMonoid G''] →
                                                              [inst_17 : TopologicalSpace G''] →
                                                                [inst_18 : ChartedSpace H'' G''] →
                                                                  [inst_19 : ContMDiffAdd I'' n G''] →
                                                                    (φ : G' →+ G'') →
                                                                      ContMDiff I' I'' n ⇑φ →
                                                                        ContMDiffMap I I' N G' n →+
                                                                          ContMDiffMap I I'' N G'' n
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lt_blsub : ∀ {o : Ordinal.{u_3}} (f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}) (i : Ordinal.{u_3}) (h : i < o),
  f i h < o.blsub f
-- Lean.Meta.Transform
/-- Continue transformation with the given expression (defaults to current expression).
For `pre`, this means visiting the children of the expression.
For `post`, this is equivalent to returning `done`.  -/
Lean.TransformStep.continue : optParam (Option Lean.Expr) none → Lean.TransformStep
-- Lean.Meta.Tactic.Assert
Lean.Meta.AssertAfterResult.mk : Lean.FVarId → Lean.MVarId → Lean.Meta.FVarSubst → Lean.Meta.AssertAfterResult
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.le_one_iff_subsingleton : ∀ {α : Type u}, Cardinal.mk α ≤ 1 ↔ Subsingleton α
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPt.congr_simp : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e e_1 : ℕ → α),
  e = e_1 → ∀ (N N_1 : ℕ), N = N_1 → MeasureTheory.SimpleFunc.nearestPt e N = MeasureTheory.SimpleFunc.nearestPt e_1 N_1
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- Define `stirlingSeq n` as $\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}$.
Stirling's formula states that this sequence has limit $\sqrt(π)$.
 -/
Stirling.stirlingSeq : ℕ → ℝ
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The distance to a set is controlled by the Hausdorff distance.  -/
Metric.infEDist_le_hausdorffEDist_of_mem : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
  x ∈ s → Metric.infEDist x t ≤ Metric.hausdorffEDist s t
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
exists_finite_card_le_of_finite_of_linearIndependent_of_span : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V}
  (ht : t.Finite),
  LinearIndepOn K id s → s ⊆ ↑(Submodule.span K t) → ∃ (h : s.Finite), h.toFinset.card ≤ ht.toFinset.card
-- Init.Data.SInt.Lemmas
Int32.toUInt32_ofNat : ∀ {n : ℕ}, Int32.toUInt32 (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.ext'_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} {f g : M ⟶ N}, f = g ↔ f.hom = g.hom
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_insert_self : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, k ∈ m.insert k
-- Lean.Data.Json.Basic
Lean.Json.getNat? : Lean.Json → Except String ℕ
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv'_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (f : (n → R) →ₗ[R] n → R) (i j : n), LinearMap.toMatrixAlgEquiv' f i j = f (Pi.single j 1) i
-- Mathlib.Geometry.Manifold.PoincareConjecture
_private.Mathlib.Geometry.Manifold.PoincareConjecture.0.exists_open_nonempty_homeomorph_isEmpty_diffeomorph_euclideanSpace_four : ProofWanted
  (∃ M,
    Nonempty (↥M ≃ₜ EuclideanSpace ℝ (Fin 4)) ∧
      IsEmpty
        (Diffeomorph (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4)))
          (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 4))) (↥M) (EuclideanSpace ℝ (Fin 4)) ↑⊤))
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- The modification between the corresponding strong transformation of the underlying oplax
functors.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Modification.toOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} →
            CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ →
              (CategoryTheory.Pseudofunctor.StrongTrans.toOplax η).Modification
                (CategoryTheory.Pseudofunctor.StrongTrans.toOplax θ)
-- Std.Http.Data.Method
Std.Http.Method.mkcalendar.sizeOf_spec : sizeOf Std.Http.Method.mkcalendar = 1
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_le_size_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  m.size ≤ (m.insert k).size
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀.congr_simp : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self self_1 : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀),
  self = self_1 →
    ∀ (r r_1 : ℤ) (e_r : r = r_1) (pq pq_1 : κ), pq = pq_1 → ∀ (hr : r₀ ≤ r), self.i₀ r pq hr = self_1.i₀ r_1 pq_1 ⋯