mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Term
Lean.Parser.Term.unreachable.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.scale.injEq : ∀ (a : ℕ) (a_1 : Mathlib.Tactic.Linarith.CompSource) (a_2 : ℕ) (a_3 : Mathlib.Tactic.Linarith.CompSource),
  (Mathlib.Tactic.Linarith.CompSource.scale a a_1 = Mathlib.Tactic.Linarith.CompSource.scale a_2 a_3) =
    (a = a_2 ∧ a_1 = a_3)
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- Morphisms into `Spec ℤ[n]` are equivalent the choice of `n` global sections.
Use `homOverEquiv` instead.
 -/
AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv : (n : Type u) →
  {X : AlgebraicGeometry.Scheme} →
    (X ⟶ AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ)))) ≃
      (n → ↑(X.presheaf.obj (Opposite.op ⊤)))
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The explicit binary cofan of `X, Y` given by `X × Y`.  -/
TopCat.prodBinaryFan : (X Y : TopCat) → CategoryTheory.Limits.BinaryFan X Y
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.trim_trim : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m₁ m₂ : MeasurableSpace α} {hm₁₂ : m₁ ≤ m₂}
  {hm₂ : m₂ ≤ m0}, (μ.trim hm₂).trim hm₁₂ = μ.trim ⋯
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- If a vector space has a finite basis, then it is finite-dimensional.  -/
Module.Basis.finiteDimensional_of_finite : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type w}
  [Finite ι] (h : Module.Basis ι K V), FiniteDimensional K V
-- Mathlib.GroupTheory.Index
AddSubgroup.instFiniteIndexTop : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.FiniteIndex
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.relabelNat'_fst_eq_relabelNat : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {aig : Std.Sat.AIG α}, aig.relabelNat'.1 = aig.relabelNat
-- Mathlib.SetTheory.Cardinal.Finite
Nat.bijective_iff_surjective_and_card : ∀ {α : Type u_1} {β : Type u_2} [Finite α] (f : α → β),
  Function.Bijective f ↔ Function.Surjective f ∧ Nat.card α = Nat.card β
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.effectiveEpiFamily_of_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.ReflectsEffectiveEpiFamilies]
  {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B),
  (CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) →
    CategoryTheory.EffectiveEpiFamily X π
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyπ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  S.homologyπ = CategoryTheory.CategoryStruct.comp S.leftHomologyπ S.leftHomologyIso.hom
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_le_div_iff_le_mul' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, a⁻¹ ≤ b / c ↔ c ≤ a * b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- If `W` is the pullback of `f, g`, it is also the pullback of `f ≫ i, g ≫ i` for any mono `i`.  -/
CategoryTheory.Limits.PullbackCone.isLimitOfCompMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ W) →
        (g : Y ⟶ W) →
          (i : W ⟶ Z) →
            [CategoryTheory.Mono i] →
              (s : CategoryTheory.Limits.PullbackCone f g) →
                CategoryTheory.Limits.IsLimit s →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk s.fst s.snd ⋯)
-- Mathlib.Algebra.Quandle
_private.Mathlib.Algebra.Quandle.0.Rack.toEnvelGroup.mapAux.match_1.eq_3 : ∀ {R : Type u_1} (motive : Rack.PreEnvelGroup R → Sort u_2) (a b : Rack.PreEnvelGroup R)
  (h_1 : Unit → motive Rack.PreEnvelGroup.unit) (h_2 : (x : R) → motive (Rack.PreEnvelGroup.incl x))
  (h_3 : (a b : Rack.PreEnvelGroup R) → motive (a.mul b)) (h_4 : (a : Rack.PreEnvelGroup R) → motive a.inv),
  (match a.mul b with
    | Rack.PreEnvelGroup.unit => h_1 ()
    | Rack.PreEnvelGroup.incl x => h_2 x
    | a.mul b => h_3 a b
    | a.inv => h_4 a) =
    h_3 a b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.toList_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v}, Std.DHashMap.Const.toList ∅ = []
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.mk.sizeOf_spec : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  [inst_4 : SizeOf A] [inst_5 : SizeOf B] [inst_6 : SizeOf C] [inst_7 : SizeOf X] (fst : x.fst ⟶ y.fst)
  (snd : x.snd ⟶ y.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst F) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight snd G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w._autoParam),
  sizeOf { fst := fst, snd := snd, w := w } = 1 + sizeOf fst + sizeOf snd + sizeOf w
-- Mathlib.CategoryTheory.Limits.Cones
/-- Extending a cone by a composition is the same as extending the cone twice.  -/
CategoryTheory.Limits.Cone.extendComp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cone F) →
            {X Y : C} →
              (f : X ⟶ Y) → (g : Y ⟶ s.pt) → s.extend (CategoryTheory.CategoryStruct.comp f g) ≅ (s.extend g).extend f
-- Init.Grind.Module.Basic
/-- Scalar multiplication by natural numbers.  -/
Lean.Grind.IntModule.nsmul : {M : Type u} → [self : Lean.Grind.IntModule M] → SMul ℕ M
-- Mathlib.Data.Sign.Basic
sign_mul_abs : ∀ {α : Type u} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (x : α), ↑(SignType.sign x) * |x| = x
-- Mathlib.Algebra.GroupWithZero.ULift
ULift.monoidWithZero : {α : Type u} → [MonoidWithZero α] → MonoidWithZero (ULift.{u_1, u} α)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g)
        (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.instInhabited : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → Inhabited (L.Equiv M M)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- If there is a divided power structure on `I⬝(A/J)` such that the quotient map is
a dp-morphism, then `J ⊓ I` is a sub-dp-ideal of `I`.  -/
DividedPowers.subDPIdeal_inf_of_quot : {A : Type u_2} →
  [inst : CommRing A] →
    {I : Ideal A} →
      {hI : DividedPowers I} →
        {J : Ideal A} →
          {hJ : DividedPowers (Ideal.map (Ideal.Quotient.mk J) I)} →
            {φ : hI.DPMorphism hJ} → φ.toRingHom = Ideal.Quotient.mk J → hI.SubDPIdeal
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates K a =
    ⟦NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet a⟧
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_rpow_self : ∀ {y : ℝ}, y ≠ 0 → ∀ (x : NNReal), (x ^ y) ^ (1 / y) = x
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.gciMapComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f),
  Subsemigroup.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯
-- Mathlib.Data.Nat.Dist
Nat.dist_eq_zero : ∀ {n m : ℕ}, n = m → n.dist m = 0
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.Method.static : Aesop.ScriptGenerated.Method
-- Std.Time.DateTime.PlainDateTime
Std.Time.instReprPlainDateTime.repr : Std.Time.PlainDateTime → ℕ → Std.Format
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isProbabilityMeasure_comap : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsProbabilityMeasure μ] {f : β → α},
  Function.Injective f →
    (∀ᵐ (a : α) ∂μ, a ∈ Set.range f) →
      (∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)) →
        MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap f μ)
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.instMul : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Mul ↑(Set.Ioc 0 1)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- Given `R[X] → S` and `S[Y] → T`, the cotangent space of `R[X][Y] → T` is isomorphic
to the direct product of the cotangent space of `S[Y] → T` and `R[X] → S` (base changed to `T`).  -/
Algebra.Generators.CotangentSpace.compEquiv : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {T : Type u₃} →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [inst_6 : IsScalarTower R S T] →
                    {ι : Type w₁} →
                      {σ : Type w₂} →
                        (Q : Algebra.Generators S T ι) →
                          (P : Algebra.Generators R S σ) →
                            (Q.comp P).toExtension.CotangentSpace ≃ₗ[T]
                              Q.toExtension.CotangentSpace × TensorProduct S T P.toExtension.CotangentSpace
-- Mathlib.CategoryTheory.Action.Limits
/-- `F.mapAction : Action V G ⥤ Action W G` preserves the colimit of some `K : J ⥤ Action V G` if
`K ⋙ forget V G` has a colimit and `F` preserves the colimit of `K ⋙ forget V G`.  -/
Action.Functor.mapActionPreservesColimit_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  {J : Type u_5} [inst_3 : CategoryTheory.Category.{v_3, u_5} J] (K : CategoryTheory.Functor J (Action V G))
  [CategoryTheory.Limits.HasColimit (K.comp (Action.forget V G))]
  [CategoryTheory.Limits.PreservesColimit (K.comp (Action.forget V G)) F],
  CategoryTheory.Limits.PreservesColimit K (F.mapAction G)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A bicone over a pair is a bilimit bicone if and only if the corresponding binary bicone is a
bilimit.  -/
CategoryTheory.Limits.Bicone.toBinaryBiconeIsBilimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)) →
          b.toBinaryBicone.IsBilimit ≃ b.IsBilimit
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_5.splitter : {n : ℕ} →
  (motive :
      Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
          Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool →
        Sort u_1) →
    (x :
        Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
          Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool) →
      ((assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
          (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
            (derivedEmpty encounteredError : Bool) →
              motive (assignments, derivedLits, derivedEmpty, encounteredError)) →
        motive x
-- Mathlib.Analysis.InnerProductSpace.Orientation
Orientation.finOrthonormalBasis.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ} (hn : 0 < n)
  (h : Module.finrank ℝ E = n) (x x_1 : Orientation ℝ E (Fin n)),
  x = x_1 → Orientation.finOrthonormalBasis hn h x = Orientation.finOrthonormalBasis hn h x_1
-- Batteries.Data.List.Basic
List.dropSliceTR.eq_1 : ∀ {α : Type u_1} (n : ℕ) (l : List α), List.dropSliceTR n 0 l = l
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.expect_ne_zero_iff_eq_zero : ∀ {G : Type u_1} {R : Type u_3} [inst : AddGroup G] [inst_1 : Fintype G] [inst_2 : Semifield R] [inst_3 : CharZero R]
  {ψ : AddChar G R}, (Finset.univ.expect fun x => ψ x) ≠ 0 ↔ ψ = 0
-- Mathlib.Tactic.FunProp.Types
/-- `fun_prop` state  -/
Mathlib.Meta.FunProp.State : Type
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_zero_left' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a : α), Associated (gcd 0 a) a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.unop_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.LeftHomologyData), h.unop.H = Opposite.unop h.H
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.map_add : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (a b : M), f (a + b) = f a + f b
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.isIrreducible_transpose_iff : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R},
  A.transpose.IsIrreducible ↔ A.IsIrreducible
-- Aesop.Builder.Default
_private.Aesop.Builder.Default.0.Aesop.RuleBuilder.default.err : String → Aesop.RuleBuilderInput → Aesop.ElabM Aesop.LocalRuleSetMember
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.instBEqSparseCasesOnKey.beq : Lean.Meta.SparseCasesOnKey✝ → Lean.Meta.SparseCasesOnKey✝ → Bool
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z} (f : P.complex ⟶ Q.complex)
  (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne f comm)
      (Q.complex.d 2 1) =
    f.f 1 -
      CategoryTheory.CategoryStruct.comp (P.complex.d 1 0)
        (CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero f comm)
-- Mathlib.RingTheory.Coalgebra.Basic
/-- Every commutative (semi)ring is a coalgebra over itself, with `Δ r = 1 ⊗ₜ r`.  -/
CommSemiring.toCoalgebra : (R : Type u) → [inst : CommSemiring R] → Coalgebra R R
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.padicNormE.mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ_[p]), ‖q * r‖ = ‖q‖ * ‖r‖
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.code.closer : ℕ → Lean.Parser.ParserFn
-- Mathlib.Order.Filter.Extr
IsMinFilter.neg : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α}
  {l : Filter α}, IsMinFilter f l a → IsMaxFilter (fun x => -f x) l a
-- Mathlib.Order.Filter.CountablyGenerated
/-- The set of `i` that satisfy the predicate `p` is countable.  -/
Filter.HasCountableBasis.countable : ∀ {α : Type u_1} {ι : Type u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasCountableBasis p s → (Set.ofPred p).Countable
-- Mathlib.Data.Multiset.Fintype
/-- Construct a finset whose elements enumerate the elements of the multiset `m`.
The `ℕ` component is used to differentiate between equal elements: if `x` appears `n` times
then `(x, 0)`, ..., and `(x, n-1)` appear in the `Finset`.  -/
Multiset.toEnumFinset : {α : Type u_1} → [DecidableEq α] → Multiset α → Finset (α × ℕ)
-- Mathlib.Geometry.Manifold.Submersion
/-- `f : M → N` is a `C^n` submersion if around each point `x ∈ M`,
there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
such that in these charts, `f` looks like `(u, v) ↦ u`.

Implicit in this definition is an abstract choice `F` of a complement of `E` in `E'`:
being a submersion includes a choice of linear isomorphism between `E` and `E'' × F`, which is where
the choice of `F` enters. If you need stronger control over the complement `F`,
use `IsSubmersionOfComplement` instead.

Note that our global choice of complement is a bit stronger than asking `f` to be a submersion at
each `x ∈ M` w.r.t. to potentially varying complements: see `isSubmersionAt` for details.
 -/
Manifold.IsSubmersion : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 E'' G →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst : TopologicalSpace M] →
                                  [ChartedSpace H M] →
                                    [inst : TopologicalSpace N] → [ChartedSpace G N] → WithTop ℕ∞ → (M → N) → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is analytic on a set `s`, so are its successive Fréchet derivative. See also
`AnalyticOnNhd.iteratedFDeriv_of_isOpen`, removing the completeness assumption but requiring the set
to be open.  -/
AnalyticOnNhd.iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} [CompleteSpace F], AnalyticOnNhd 𝕜 f s → ∀ (n : ℕ), AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_eq_iff' : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {b : Module.Basis ι R M} {f : M ≃ₗ[R] ι →₀ R}, b.repr = f ↔ ∀ (i : ι), f (b i) = fun₀ | i => 1
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.close : {α : Type} → Std.CloseableChannel.Unbounded✝ α → EIO Std.CloseableChannel.Error Unit
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.instStrictPatternModelForallCharProp : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.Model.StrictPatternModel p
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.mk_smul : ∀ {M' : Type u_1} {α : Type u_2} [inst : MulOneClass M'] [inst_1 : SMul M' α] {S : Submonoid M'} (g : M') (hg : g ∈ S)
  (a : α), ⟨g, hg⟩ • a = g • a
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.mapMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} [inst_1 : MulOneClass Y]
  [inst_2 : MulOneClass Z] (f : Y →* Z),
  LocallyConstant.mapMonoidHom f = { toFun := LocallyConstant.map ⇑f, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₁ i₂ i₃ i₄ i₅ : ι}
  (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ),
  CategoryTheory.Limits.IsZero ((X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₂)) →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero._auto_1)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero._auto_3),
      CategoryTheory.IsIso
        (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.nonsingular_add : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Nonsingular x₁ y₁ →
    W.Nonsingular x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
-- Init.Data.String.Basic
ByteArray.utf8Decode?_utf8Encode_singleton_append : ∀ {l : ByteArray} {c : Char}, ([c].utf8Encode ++ l).utf8Decode? = Option.map (fun x => #[c] ++ x) l.utf8Decode?
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_lt_natDegree : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {p : Polynomial R} {q : Polynomial S},
  p ≠ 0 → p.degree < q.degree → p.natDegree < q.natDegree
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.mapValueGroupWithZero_mk : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [inst_5 : ValuativeExtension A B] (r : A)
  (s : ↥(ValuativeRel.posSubmonoid A)),
  (ValuativeExtension.mapValueGroupWithZero A B) (ValuativeRel.ValueGroupWithZero.mk r s) =
    ValuativeRel.ValueGroupWithZero.mk ((algebraMap A B) r) ((ValuativeExtension.mapPosSubmonoid A B) s)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_eq_self_iff_mem : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  ↑⌈a⌉ = a ↔ a ∈ Set.range Int.cast
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The range of an algebra homomorphism, as an intermediate field.  -/
AlgHom.fieldRange : {K : Type u_1} →
  {L : Type u_2} →
    {L' : Type u_3} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Field L'] → [inst_3 : Algebra K L] → [inst_4 : Algebra K L'] → (L →ₐ[K] L') → IntermediateField K L'
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Destructor for M-types  -/
MvPFunctor.M.dest : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → {α : TypeVec.{u} n} → P.M α → ↑P (α ::: P.M α)
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.cast.sizeOf_spec : ∀ (declName unfold refold unfold' refold' : Lean.Name),
  sizeOf (Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.cast declName unfold refold unfold' refold') =
    1 + sizeOf declName + sizeOf unfold + sizeOf refold + sizeOf unfold' + sizeOf refold'
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGTD_eq_getD_getEntryGT? : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α} {fallback : α × β},
  Std.DTreeMap.Internal.Impl.Const.getEntryGTD k t fallback =
    (Std.DTreeMap.Internal.Impl.Const.getEntryGT? k t).getD fallback
-- Mathlib.Algebra.Module.Equiv.Opposite
LinearMap.ext_ring_op_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module S M] {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M}, f = g ↔ f 1 = g 1