mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- All functors `F : J ⥤ C` from `J` have limits  -/
CategoryTheory.Limits.HasLimitsOfShape.has_limit : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  [self : CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasLimit F
-- Mathlib.Data.Finsupp.Basic
/-- **Alias** of `Finsupp.curryEquiv`.

---

The equivalence between `α × β →₀ M` and `α →₀ β →₀ M` given by currying/uncurrying.  -/
Finsupp.finsuppProdEquiv : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : Zero M] → (α × β →₀ M) ≃ (α →₀ β →₀ M)
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- Each neighborhood filter has a basis of path-connected neighborhoods.  -/
LocallyPathConnectedSpace.path_connected_basis : ∀ {X : Type u_4} {inst : TopologicalSpace X} [self : LocallyPathConnectedSpace X] (x : X),
  (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsPathConnected s) id
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- The typeclass associated with the structure `EffectiveEquivalenceRelation`.  -/
CategoryTheory.IsEffectiveEquivalenceRelation : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R A : C} → (R ⟶ A) → (R ⟶ A) → Prop
-- Init.Data.Option.Monadic
_private.Init.Data.Option.Monadic.0.Option.instDecidableEq.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (val : α) → motive (some val)),
  (match none with
    | none => h_1 ()
    | some val => h_2 val) =
    h_1 ()
-- Mathlib.Order.Lattice
/-- Transfer `SemilatticeSup` across an `Equiv`.  -/
Equiv.semilatticeSup : {α : Type u} → {β : Type v} → α ≃ β → [SemilatticeSup β] → SemilatticeSup α
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.instIsStableUnderRetractsFibrations : (HomotopicalAlgebra.fibrations SSet).IsStableUnderRetracts
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.I.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (K K_1 : CochainComplex C ℤ),
  K = K_1 → CochainComplex.cm5b.I K = CochainComplex.cm5b.I K_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexFuel.eq_5 : ∀ (fuel_2 : ℕ) (pw₁ : Lean.Grind.CommRing.Power) (m₁_2 : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power)
  (m₂_2 : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.revlexFuel fuel_2.succ (Lean.Grind.CommRing.Mon.mult pw₁ m₁_2)
      (Lean.Grind.CommRing.Mon.mult pw₂ m₂_2) =
    bif pw₁.x == pw₂.x then
      (Lean.Grind.CommRing.Mon.revlexFuel fuel_2 m₁_2 m₂_2).then (Lean.Grind.CommRing.powerRevlex pw₁.k pw₂.k)
    else
      bif Nat.blt pw₁.x pw₂.x then
        (Lean.Grind.CommRing.Mon.revlexFuel fuel_2 m₁_2 (Lean.Grind.CommRing.Mon.mult pw₂ m₂_2)).then Ordering.lt
      else (Lean.Grind.CommRing.Mon.revlexFuel fuel_2 (Lean.Grind.CommRing.Mon.mult pw₁ m₁_2) m₂_2).then Ordering.gt
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Given a pushout square assembled from a pushout square on the left and
a commuting square on the right, the right square is a pushout square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
|            |            |
v₁₁          v₁₂          v₁₃
↓            ↓            ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
```
 -/
CategoryTheory.IsPushout.of_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
  CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
      (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂) →
    CategoryTheory.CategoryStruct.comp h₁₂ v₁₃ = CategoryTheory.CategoryStruct.comp v₁₂ h₂₂ →
      CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ → CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂
-- Lean.MonadEnv
Lean.getConstVal : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Lean.ConstantVal
-- Std.Http.Data.URI.Basic
/-- The encoded username.
 -/
Std.Http.URI.UserInfo.username : Std.Http.URI.UserInfo → Std.Http.URI.EncodedUserInfo
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Restrict the codomain of a continuous multilinear map to a submodule.  -/
ContinuousMultilinearMap.codRestrict : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] →
                      (f : ContinuousMultilinearMap R M₁ M₂) →
                        (p : Submodule R M₂) → (∀ (v : (i : ι) → M₁ i), f v ∈ p) → ContinuousMultilinearMap R M₁ ↥p
-- Mathlib.ModelTheory.Equivalence
/-- Two (bounded) formulas are semantically equivalent over a theory `T` when they have the same
interpretation in every model of `T`. (This is also known as logical equivalence, which also has a
proof-theoretic definition.)  -/
FirstOrder.Language.Theory.Iff : {L : FirstOrder.Language} → {α : Type w} → {n : ℕ} → L.Theory → L.BoundedFormula α n → L.BoundedFormula α n → Prop
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.instDecidableEqHom : {d : ℕ} → {n m : SimplexCategory.Truncated d} → DecidableEq (n ⟶ m)
-- Mathlib.Algebra.Group.AddChar
AddChar.toMonoidHom_apply : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M) (a : Multiplicative A),
  ψ.toMonoidHom a = ψ (Multiplicative.toAdd a)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedStructuralAtom.default : Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.TypeToCharPResult.failure : {u : Lean.Level} → {α : Q(Type u)} → Tactic.ReduceModChar.TypeToCharPResult α
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNNRat_add : ∀ {α : Type u_1} [inst : Semiring α] {f : α → α → α} {a b : α} {na nb nc da db dc k : ℕ},
  f = HAdd.hAdd →
    Mathlib.Meta.NormNum.IsNNRat a na da →
      Mathlib.Meta.NormNum.IsNNRat b nb db →
        (na.mul db).add (nb.mul da) = k.mul nc → da.mul db = k.mul dc → Mathlib.Meta.NormNum.IsNNRat (f a b) nc dc
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFacAux.eq_1 : ∀ (n x : ℕ), n.minFacAux x = if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2)
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closure of a set equals the intersection of its closed thickenings of positive radii.  -/
Metric.closure_eq_iInter_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α), closure E = ⋂ δ, ⋂ (_ : 0 < δ), Metric.cthickening δ E
-- Mathlib.RingTheory.Ideal.Over
Ideal.under_def : ∀ (A : Type u_2) [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B),
  Ideal.under A P = Ideal.comap (algebraMap A B) P
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_le : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : Associates α},
  a.factors ≤ b.factors ↔ a ≤ b
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.mono_δ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j), CategoryTheory.Limits.IsZero (S.X₂.homology i) → CategoryTheory.Mono (hS.δ i j hij)
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- A `Pseudoelement` of `P` is just an equivalence class of arrows ending in `P` by being
pseudo-equal.  -/
CategoryTheory.Abelian.Pseudoelement : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → C → Type (max u v)
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- The topology of compact convergence on `E →L[𝕜] F`.  -/
CompactConvergenceCLM.«term_→L_c[_]_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instCoeCommMonCat : Coe CommGrpCat CommMonCat
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A),
  (Φ.presheafFiberMapCocone F K P).pt = (Φ.map F K).presheafFiber.obj P
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.peek.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (a a_1 : σ → Option (Γ k) → σ),
  (Turing.TM2to1.StAct.peek a = Turing.TM2to1.StAct.peek a_1) = (a = a_1)
-- Mathlib.Computability.EpsilonNFA
/-- **Alias** of the reverse direction of `εNFA.isPath_singleton`. -/
εNFA.IsPath.singleton : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {s t : σ} {a : Option α}, t ∈ M.step s a → M.IsPath s t [a]
-- Mathlib.Algebra.FreeAlgebra
/-- Coercion from `X` to `Pre R X`. Note: Used for notation only.  -/
FreeAlgebra.Pre.hasCoeGenerator : (R : Type u_1) → (X : Type u_2) → Coe X (FreeAlgebra.Pre R X)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage_of_eq : ∀ {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] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y : C} (f : G.obj X ⟶ G.obj Y) (g : X ⟶ Y),
  G.map g = f → CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F f = F.obj.map g.op
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPullbacksAlong.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y},
  (∀ {W : C} (g : W ⟶ Y), P g → CategoryTheory.Limits.HasPullback g f) → P.HasPullbacksAlong f
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.instLawfulOperatorBinaryInputMkBEqCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkBEqCached
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The inverse of an isomorphism has a functorial choice of pullbacks.  -/
CategoryTheory.ChosenPullbacksAlong.isoInv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {Y X : C} → (f : Y ≅ X) → CategoryTheory.ChosenPullbacksAlong f.inv
-- Mathlib.GroupTheory.Index
AddSubgroup.disjoint_of_coprime_natCard : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, (Nat.card ↥H).Coprime (Nat.card ↥K) → Disjoint H K
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.comp_one : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : One β] (g : C(β, γ)), g.comp 1 = ContinuousMap.const α (g 1)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.mod_def : ∀ {R : Type u} [inst : Field R] {p q : Polynomial R}, p % q = p %ₘ (q * Polynomial.C q.leadingCoeff⁻¹)
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q) →
    AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) =
      @AlgebraicGeometry.IsAffineHom ⊓ AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => Q
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.mkIso_inv_hom_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (e : ρ.Equiv σ) (y : Y), (Rep.Hom.hom (Rep.mkIso e).inv) y = e.symm y
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.not_isPrincipal_iff_of_monotone : ∀ {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  (∀ (a : Ordinal.{u}), Monotone (op a)) →
    (∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) → (¬Ordinal.IsPrincipal op o ↔ ∃ a < o, o ≤ op a a)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.AndKind.iff : Mathlib.Tactic.ITauto.AndKind
-- Mathlib.Algebra.Opposites
MulOpposite.op_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] (a : α) (b : β), MulOpposite.op (a • b) = a • MulOpposite.op b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.map.eq_2 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → γ a) (size : ℕ) (k' : α)
  (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.map f (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    Std.DTreeMap.Internal.Impl.inner size k' (f k' v') (Std.DTreeMap.Internal.Impl.map f l')
      (Std.DTreeMap.Internal.Impl.map f r')
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.upperBounds_subset : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsUpperSet s → s.Nonempty → upperBounds s ⊆ s
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_iff_lt_mul : ∀ {a b c : ℤ}, 0 < c → (a / c < b ↔ a < b * c)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.comp_p_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (f : P.Hom Q) {Z : C} (h : Q.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.f (CategoryTheory.CategoryStruct.comp Q.p h) =
    CategoryTheory.CategoryStruct.comp f.f h
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape : ∀ {J : Type w} {inst : LinearOrder J} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  [self : CategoryTheory.Limits.HasIterationOfShape J C], CategoryTheory.Limits.HasColimitsOfShape J C
-- Init.Data.String.Slice
/-- Removes the specified number of characters \(Unicode code points\) from the start of the slice.

If `n` is greater than the amount of characters in `s`, returns an empty slice.

Examples:

* `"red green blue".toSlice.drop 4 == "green blue".toSlice`

* `"red green blue".toSlice.drop 10 == "blue".toSlice`

* `"red green blue".toSlice.drop 50 == "".toSlice`
 -/
String.Slice.drop : String.Slice → ℕ → String.Slice
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ.eq_1 : ∀ {F : Type u_2} [inst : Field F] (j : F) [inst_1 : DecidableEq F],
  WeierstrassCurve.ofJ j =
    if j = 0 then if 3 = 0 then WeierstrassCurve.ofJ1728 F else WeierstrassCurve.ofJ0 F
    else if j = 1728 then WeierstrassCurve.ofJ1728 F else WeierstrassCurve.ofJNe0Or1728 j
-- Mathlib.Topology.Order.AtTopBotIxx
tendsto_Ioo_atTop : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a b : X} {α : Type u_2}
  {l : Filter α} {f : α → ↑(Set.Ioo a b)},
  autoParam (Order.IsSuccPrelimit b) tendsto_Ioo_atTop._auto_1 →
    (Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun x => ↑(f x)) l (nhdsWithin b (Set.Iio b)))
-- Mathlib.Tactic.NormNum.Core
/-- A simp plugin which calls `NormNum.eval`.  -/
Mathlib.Meta.NormNum.tryNormNum : optParam Bool false → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Data.Nat.ChineseRemainder
Nat.modEq_list_prod_iff : ∀ {a b : ℕ} {l : List ℕ}, List.Pairwise Nat.Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.as_ideal_le_as_ideal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x y : ProjectiveSpectrum 𝒜), x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ x ≤ y
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
_private.Mathlib.CategoryTheory.Triangulated.SpectralObject.0.CategoryTheory.ComposableArrows.Precomp.obj.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin (n + 1 + 1) → Sort u_1) (isLt : 0 < n + 1 + 1) (h_1 : (isLt : 0 < n + 1 + 1) → motive ⟨0, isLt⟩)
  (h_2 : (i : ℕ) → (hi : i + 1 < n + 1 + 1) → motive ⟨i.succ, hi⟩),
  (match ⟨0, isLt⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨i.succ, hi⟩ => h_2 i hi) =
    h_1 isLt
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get? k = none
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.id_mapMon_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X X.X))
      CategoryTheory.MonObj.mul
-- Mathlib.Topology.UniformSpace.Defs
tendsto_left_nhds_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {a : α}, Filter.Tendsto (fun a' => (a, a')) (nhds a) (uniformity α)
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_of_mem_nhds_one_of_inv_mul_right_subset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {s s' t : Set G},
  s' ∈ nhds 1 → (∀ x ∈ s', x⁻¹ ∈ s') → s * s' ⊆ t → closure s ⊆ t
-- Batteries.Tactic.Trans
Batteries.Tactic.TransRelation.app.sizeOf_spec : ∀ (rel : Lean.Expr), sizeOf (Batteries.Tactic.TransRelation.app rel) = 1 + sizeOf rel
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.instCharacteristicUpperCentralSeries : ∀ (G : Type u_1) [inst : AddGroup G] (n : ℕ), (AddSubgroup.upperCentralSeries G n).Characteristic
-- Mathlib.CategoryTheory.Category.Pairwise
/-- An inductive type representing either a single term of a type `ι`, or a pair of terms.
We use this as the objects of a category to describe the sheaf condition.
 -/
CategoryTheory.Pairwise : Type v → Type v
-- Mathlib.CategoryTheory.Localization.HasLocalization
/-- The data of a localized category with a given universe
for the morphisms.  -/
CategoryTheory.MorphismProperty.HasLocalization : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Type (max (max (u + 1) v) (w + 1))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k a : α} {fallback : β},
  Std.DHashMap.Const.getD (m.erase k) a fallback =
    if (k == a) = true then fallback else Std.DHashMap.Const.getD m a fallback
-- Mathlib.Topology.ContinuousMap.Bounded.Star
BoundedContinuousFunction.instStarModule : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : NormedField 𝕜] [inst_1 : StarRing 𝕜] [inst_2 : TopologicalSpace α]
  [inst_3 : SeminormedAddCommGroup β] [inst_4 : StarAddMonoid β] [inst_5 : NormedStarGroup β] [inst_6 : NormedSpace 𝕜 β]
  [StarModule 𝕜 β], StarModule 𝕜 (BoundedContinuousFunction α β)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMul_one_group_smul : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (g : ↥A) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.unitsSMul φ 1 (↑g • w) = ↑(φ g) • HNNExtension.NormalWord.unitsSMul φ 1 w
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_ofNat : ∀ (n : ℕ), { toBitVec := BitVec.ofNat 64 n } = OfNat.ofNat n
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A cofork on `f` and `g` is just a `Cocone (parallelPair f g)`.  -/
CategoryTheory.Limits.Cofork : {C : Type u} → {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → (X ⟶ Y) → (X ⟶ Y) → Type (max (max 0 u) v)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_ofSnowflaking_ball : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  {r : ℝ},
  0 ≤ r →
    ⇑Metric.Snowflaking.ofSnowflaking '' Metric.ball x r = Metric.ball (Metric.Snowflaking.ofSnowflaking x) (r ^ α⁻¹)
-- Mathlib.Order.WithBot
IsMin.withTop : ∀ {α : Type u_1} {a : α} [inst : LE α], IsMin a → IsMin ↑a
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `not_isSolvable_of_mem_derivedSeries`. -/
not_solvable_of_mem_derivedSeries : ∀ {G : Type u_1} [inst : Group G] {g : G}, g ≠ 1 → (∀ (n : ℕ), g ∈ derivedSeries G n) → ¬Group.IsSolvable G
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_symm_neg : ∀ {A : Type u_3} {E : Type u_4} (x' : E) [inst : AddCommGroup E],
  (WithCStarModule.equiv A E).symm (-x') = -(WithCStarModule.equiv A E).symm x'
-- Mathlib.Algebra.Module.Injective
Module.injective_iff_ulift_injective : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Small.{v, u} R],
  Module.Injective R M ↔ Module.Injective R (ULift.{v', v} M)
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.get! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → Std.DTreeMap.Raw α β cmp → (a : α) → [Inhabited (β a)] → β a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {k a : α} [inst_3 : Inhabited (β a)] {v : β k},
      (m.insert k v).get! a = if h : (k == a) = true then cast ⋯ v else m.get! a
-- Mathlib.GroupTheory.Complement
/-- A right transversal is in bijection with right cosets.  -/
AddSubgroup.IsComplement.rightQuotientEquiv : {G : Type u_1} →
  [inst : AddGroup G] →
    {H : AddSubgroup G} → {T : Set G} → AddSubgroup.IsComplement (↑H) T → Quotient (QuotientAddGroup.rightRel H) ≃ ↑T
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.codRestrict : ∀ {R₂ : Type u_1} [inst : Semiring R₂] {M₁ : Type u_2} {M₂ : Type u_3} [inst_1 : TopologicalSpace M₁]
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  {f : M₁ → M₂},
  IsCompactOperator f →
    ∀ {V : Submodule R₂ M₂} (hV : ∀ (x : M₁), f x ∈ V), IsClosed ↑V → IsCompactOperator (Set.codRestrict f (↑V) hV)
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.insertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.insertIfNew a b = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m, h⟩ a b) else m
-- Mathlib.Algebra.Category.ModuleCat.Colimits
/-- The cocone for `F` constructed from the colimit of
`(F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)`.  -/
ModuleCat.HasColimit.colimitCocone : {R : Type w} →
  [inst : Ring R] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] →
            CategoryTheory.Limits.Cocone F
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Expect.mk : Std.Http.Header.Expect