mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁.coe_mk : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : G → ↑A)
  (hf : f ∈ groupCohomology.cocycles₁ A), ⇑⟨f, hf⟩ = f
-- Mathlib.Tactic.Translate.Core
/-- Linter, mostly used by translate attributes, that checks that the source declaration doesn't
have certain attributes  -/
Mathlib.Tactic.Translate.linter.existingAttributeWarning : Lean.Option Bool
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Inclusion-exclusion principle** for the measure of a union of sets of finite measure.

The measure of the union of the `s i` over `i ∈ t` is the alternating sum of the measures of the
intersections of the `s i`.  -/
MeasureTheory.measureReal_biUnion_eq_sum_powerset : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {ι : Type u_5} {t : Finset ι} {s : ι → Set X},
  (∀ i ∈ t, MeasurableSet (s i)) →
    autoParam (∀ i ∈ t, μ (s i) ≠ ⊤) MeasureTheory.measureReal_biUnion_eq_sum_powerset._auto_1 →
      μ.real (⋃ i ∈ t, s i) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (u.card + 1) * μ.real (⋂ i ∈ u, s i)
-- Lean.DocString.Types
Lean.Doc.instInhabitedBlock : {a : Type u_1} → {a_1 : Type u_2} → Inhabited (Lean.Doc.Block a a_1)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.min he ∈ t
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.add_rat : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (r : ℚ), LiouvilleWith p (x + ↑r)
-- Mathlib.Order.Comparable
CompRel.rfl : ∀ {α : Type u_1} {a : α} {r : α → α → Prop} [Std.Refl r], CompRel r a a
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
prod_galRestrict_eq_norm : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : FiniteDimensional K L]
  [inst_14 : IsGalois K L] [inst_15 : IsIntegrallyClosed A] (x : B),
  ∏ σ, ((galRestrict A K L B) σ) x =
    (algebraMap A B) (IsIntegralClosure.mk' A ((Algebra.norm K) ((algebraMap B L) x)) ⋯)
-- Mathlib.Order.BoundedOrder.Basic
BoundedOrder.toOrderTop : {α : Type u} → {inst : LE α} → [self : BoundedOrder α] → OrderTop α
-- Mathlib.GroupTheory.Commutator.Basic
mem_commutatorSet_iff : ∀ {G : Type u_1} [inst : Group G] {g : G}, g ∈ commutatorSet G ↔ ∃ g₁ g₂, ⁅g₁, g₂⁆ = g
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_lt_one_of_nonneg_of_lt_one_right : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [MulPosMono M₀],
  a ≤ 1 → 0 ≤ b → b < 1 → a * b < 1
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.apply : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (h : f v = 0) (x : V), (LinearEquiv.transvection h) x = x + f x • v
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.range_map : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S),
  Set.range (AddMonoidAlgebra.map f) = {x | ∀ (i : M), x.coeff i ∈ Set.range ⇑f}
-- Init.Data.UInt.Lemmas
UInt16.add_mul : ∀ {a b c : UInt16}, (a + b) * c = a * c + b * c
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfRoot.congr_simp : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb pb_1 : PowerBasis A S) (e_pb : pb = pb_1) (pb' pb'_1 : PowerBasis A S')
  (e_pb' : pb' = pb'_1) (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0)
  (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0), pb.equivOfRoot pb' h₁ h₂ = pb_1.equivOfRoot pb'_1 ⋯ ⋯
-- Mathlib.Logic.Equiv.Fin.Basic
finSumFinEquiv_symm_apply_castSucc : ∀ {m : ℕ} (x : Fin m), finSumFinEquiv.symm x.castSucc = Sum.inl x
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.instIsDominantToNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.IsDominant (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_inverse_obj_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) {X_1 Y : D}
  (g : X_1 ⟶ Y),
  ((CategoryTheory.Functor.currying.inverse.obj F).obj X).map g =
    F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)
-- Aesop.Tree.Data
Aesop.GoalState.unprovable : Aesop.GoalState
-- Mathlib.Topology.Separation.Basic
/-- A topological space is called an R₀ space, if `Specializes` relation is symmetric.

In other words, given two points `x y : X`,
if every neighborhood of `y` contains `x`, then every neighborhood of `x` contains `y`.  -/
R0Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.Order.Category.BddLat
/-- `latToBddLat` and `OrderDual` commute.  -/
latToBddLatCompDualIsoDualCompLatToBddLat : latToBddLat.comp BddLat.dual ≅ Lat.dual.comp latToBddLat
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation)
The covering of `D(i')` by the pullback of the diagonal components of `X ×ₛ X`.
See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D₀ : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] →
              [inst_2 : CategoryTheory.IsCofiltered I] →
                [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] →
                  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) → (D.obj A.i').OpenCover
-- Mathlib.Order.InitialSeg
/-- **Alias** of the reverse direction of `PrincipalSeg.isMin_apply_iff`. -/
PrincipalSeg.map_isMin : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} [inst_1 : PartialOrder α] (f : α <i β),
  IsMin a → IsMin (f.toRelEmbedding a)
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain_refl' : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M], Finsupp.equivMapDomain (Equiv.refl α) = id
-- Mathlib.Tactic.GCongr.Core
/-- Run the `intro` tactic `n` times on the given goal.  -/
_private.Mathlib.Tactic.GCongr.Core.0.Mathlib.Tactic.GCongr.introN : Lean.MVarId → ℕ → Mathlib.Tactic.GCongr.GCongrM (List Lean.MVarId)
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms], (P ⊓ Q).IsClosedUnderIsomorphisms
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceParams : Type
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ₀Iter_succ' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (h : autoParam (n + (i + 1) = m) CategoryTheory.SimplicialObject.δ₀Iter_succ'._auto_1),
  X.δ₀Iter (i + 1) h = CategoryTheory.CategoryStruct.comp (X.δ₀Iter i ⋯) (X.δ 0)
-- Mathlib.Order.PiLex
Pi.lex_lt_of_lt_of_preorder : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : (i : ι) → Preorder (β i)] {r : ι → ι → Prop},
  WellFounded r → ∀ {x y : (i : ι) → β i}, x < y → ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.unpackMantissa.eq_1 : ∀ {spec : Float.Model.Format} (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.unpackMantissa b =
    BitVec.cast ⋯ (BitVec.extractLsb (spec.mantissaBitsWithoutImplicit - 1) 0 b)
-- Mathlib.Topology.ContinuousMap.Bounded.Star
BoundedContinuousFunction.coe_toContinuousMapStarₐ : ∀ {α : Type u} {β : Type v} (𝕜 : Type u_2) [inst : NormedField 𝕜] [inst_1 : TopologicalSpace α] [inst_2 : NormedRing β]
  [inst_3 : NormedAlgebra 𝕜 β] [inst_4 : StarAddMonoid β] [inst_5 : NormedStarGroup β]
  (f : BoundedContinuousFunction α β), ⇑((BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) f) = ⇑f
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_neg : ∀ {R : Type u} {a : R} [inst : Ring R], Polynomial.C (-a) = -Polynomial.C a
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionUnitIso : ∀ (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.MonoidalLeftAction C D] (x : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso x =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso x
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.psumPart.eq_1 : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] {n : ℕ} (μ : n.Partition),
  MvPolynomial.psumPart σ R μ = (Multiset.map (MvPolynomial.psum σ R) μ.parts).prod
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.generators.δ : ∀ {n : ℕ} (i : Fin (n + 2)), SimplexCategoryGenRel.generators (SimplexCategoryGenRel.δ i)
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
normRingNorm_toFun : ∀ (R : Type u_2) [inst : NonUnitalNormedRing R] (a : R), (normRingNorm R).toFun a = ‖a‖
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of `one_lt_mul_of_le_of_lt`. -/
one_lt_mul : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [MulPosMono M₀],
  1 ≤ a → 1 < b → 1 < a * b
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctorCore.map_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) (X : B),
  self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
-- Std.Http.Data.Extensions
Std.Http.instInhabitedExtensions.default : Std.Http.Extensions
-- Init.Data.Order.Classes
/-- This typeclass states that the order structure on `α`, represented by an `LE α` instance,
is a linear order.
In other words, the less-or-equal relation is reflexive, transitive, antisymmetric and total.
 -/
Std.IsLinearOrder : (α : Type u) → [LE α] → Prop
-- Mathlib.Data.Set.Sups
Set.sups_infs_subset_left : ∀ {α : Type u_2} [inst : DistribLattice α] (s t u : Set α), s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.map.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f f_1 : α → β)
  (e_f : f = f_1) (hf : Continuous f) (K K_1 : TopologicalSpace.NonemptyCompacts α),
  K = K_1 → TopologicalSpace.NonemptyCompacts.map f hf K = TopologicalSpace.NonemptyCompacts.map f_1 ⋯ K_1
-- Mathlib.Algebra.Opposites
AddOpposite.unop_inj : ∀ {α : Type u_1} {x y : αᵃᵒᵖ}, AddOpposite.unop x = AddOpposite.unop y ↔ x = y
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.toIterator : ∀ {l m r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → String.Legacy.Iterator.ValidFor l.reverse (m ++ r) s.toLegacyIterator
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.coeff_divX : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.divX.coeff n = p.coeff (n + 1)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProd.mul.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  [inst : (a : Q(«$α»)) → SizeOf (BaseType a)] {x : Q(«$α»)} {e : Q(ℕ)} {b : Q(«$α»)}
  (a : Mathlib.Tactic.Ring.Common.ExBase BaseType sα x) (a_1 : Mathlib.Tactic.Ring.Common.ExProdNat e)
  (a_2 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα b),
  sizeOf (Mathlib.Tactic.Ring.Common.ExProd.mul a a_1 a_2) =
    1 + sizeOf x + sizeOf e + sizeOf b + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- A Scheme is affine if the canonical map `X ⟶ Spec Γ(X)` is an isomorphism.  -/
AlgebraicGeometry.IsAffine : AlgebraicGeometry.Scheme → Prop
-- Lean.Data.NameMap.Basic
Lean.NameMap.contains : {α : Type} → Lean.NameMap α → Lean.Name → Bool
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_lt_max_of_ne : ∀ {x y : NNReal}, x ≠ y → x.agm y < max x y
-- Mathlib.Order.Interval.Finset.Defs
instLocallyFiniteOrderBotSubtypeLtOfDecidableLTOfLocallyFiniteOrder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {y : α} [inst_1 : DecidableLT α] [inst_2 : LocallyFiniteOrder α],
  instLocallyFiniteOrderBotSubtypeLtOfDecidableLTOfLocallyFiniteOrder =
    { finsetIio := fun a => Finset.subtype (fun x => y < x) (Finset.Ioo y ↑a),
      finsetIic := fun a => Finset.subtype (fun x => y < x) (Finset.Ioc y ↑a), finset_mem_Iic := ⋯,
      finset_mem_Iio := ⋯ }
-- Lean.Elab.DefView
Lean.Elab.DefKind.def : Lean.Elab.DefKind
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_p : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)),
  ((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).obj P).p = P.p.f
-- Lean.Elab.Do.Basic
Lean.Elab.Do.CodeLiveness.deadSemantically.sizeOf_spec : sizeOf Lean.Elab.Do.CodeLiveness.deadSemantically = 1
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getKey!ₘ : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → [Inhabited α] → Std.DHashMap.Internal.Raw₀ α β → α → α
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.mk_eq_zero_iff : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] {p : E}, SeparationQuotient.mk p = 0 ↔ ‖p‖ = 0
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ_natDegree_eq_φ_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → (RatFunc.Luroth.Φ✝ E).natDegree = (RatFunc.Luroth.φ✝ E).natDegree
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.lintegral_swapLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : β × α) (g : γ → ENNReal),
  ∫⁻ (c : γ), g c ∂κ.swapLeft a = ∫⁻ (c : γ), g c ∂κ a.swap
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex k P n} {w : Fin (n + 1) → k},
  ∑ i, w i = 1 →
    ∀ {i : Fin (n + 1)},
      (Finset.affineCombination k Finset.univ s.points) w ∈ affineSpan k (Set.range (s.faceOpposite i).points) ↔ w i = 0
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Decl.atom.inj : ∀ {α : Type} {idx idx_1 : α}, Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.atom idx_1 → idx = idx_1
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.basisAt.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {M : Type u_4} [inst_1 : TopologicalSpace M] {F : Type u_5}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_5 : (x : M) → AddCommGroup (V x)]
  [inst_6 : (x : M) → Module 𝕜 (V x)] [inst_7 : (x : M) → TopologicalSpace (V x)] [inst_8 : FiberBundle F V]
  [inst_9 : VectorBundle 𝕜 F V] {ι : Type u_7} {x : M} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_10 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F) (hx : x ∈ e.baseSet),
  e.basisAt b hx = b.map (Bundle.Trivialization.linearEquivAt 𝕜 e x hx).symm
-- Mathlib.CategoryTheory.Sites.Precoverage
_private.Mathlib.CategoryTheory.Sites.Precoverage.0.CategoryTheory.Precoverage.comp_mem_coverings.match_1_1.splitter : (ι' α : Type (max u_1 u_2)) →
  (fib : ι' ⊕ α → Type (max u_1 u_2)) →
    (motive : (i : ι' ⊕ α) → fib i → Sort u_3) →
      (i : ι' ⊕ α) →
        (j : fib i) →
          ((i : ι') → (j : fib (Sum.inl i)) → motive (Sum.inl i) j) →
            ((i : α) → (j : fib (Sum.inr i)) → motive (Sum.inr i) j) → motive i j
-- Mathlib.Data.Seq.Defs
Stream'.Seq.corec_nil : ∀ {α : Type u} {β : Type v} (f : β → Option (α × β)) (b : β), f b = none → Stream'.Seq.corec f b = Stream'.Seq.nil
-- Mathlib.Topology.Sheaves.Skyscraper
/-- If `f : 𝓕 ⟶ skyscraperPresheaf p₀ c` is a natural transformation, then there is a morphism
`𝓕.stalk p₀ ⟶ c` defined as the morphism from colimit to cocone at `c`.
 -/
StalkSkyscraperPresheafAdjunctionAuxs.fromStalk : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [inst_3 : CategoryTheory.Limits.HasColimits C] →
              {𝓕 : TopCat.Presheaf C X} → {c : C} → (𝓕 ⟶ skyscraperPresheaf p₀ c) → (𝓕.stalk p₀ ⟶ c)
-- Init.Data.Vector.Lemmas
Vector.foldrM_push : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] {f : α → β → m β} {init : β}
  {xs : Vector α n} {a : α},
  Vector.foldrM f init (xs.push a) = do
    let b ← f a init
    Vector.foldrM f b xs
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.exists_eq_one : ∀ {R : Type u_1} {V : Type u_2} [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace V] [IsTopologicalRing R] [inst_5 : Module R V] [SeparatingDual R V] {x : V},
  x ≠ 0 → ∃ f, f x = 1
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_ne_zero : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] {p : ℚ}, ↑p ≠ 0 ↔ p ≠ 0
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.toKer_bracket : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] (E : LieAlgebra.Extension R M L)
  (x : ↥E.proj.ker) (y : L), E.toKer ⁅y, E.toKer.symm x⁆ = ⁅Exists.choose ⋯ y, x⁆
-- Mathlib.LinearAlgebra.Projection
Submodule.prodEquivOfIsCompl.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q), p.prodEquivOfIsCompl q h = p.prodEquivOfIsCompl q h
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univUnitBall_symm_apply_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  ↑OpenPartialHomeomorph.univUnitBall.symm 0 = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toList_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → β → Bool},
  t.WF → (Std.TreeMap.Raw.filter f t).toList = List.filter (fun p => f p.1 p.2) t.toList
-- Batteries.Data.Fin.Coding
/-- Get representative for the equivalence class of `x`.  -/
Fin.getRepr : {n : ℕ} → (s : Setoid (Fin n)) → [DecidableRel ⇑s] → Fin n → Fin n
-- Batteries.Logic
Eq.congr_left : ∀ {α : Sort u_1} {x y z : α}, x = y → (x = z ↔ y = z)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.map_srange : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (g : N →ₙ* P)
  (f : M →ₙ* N), Subsemigroup.map g f.srange = (g.comp f).srange
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Unsat : {α : Type u_1} → Std.Sat.CNF α → Prop
-- Init.Data.SInt.Lemmas
Int8.zero_mul : ∀ {a : Int8}, 0 * a = 0
-- Mathlib.RingTheory.Extension.Generators
/-- Given a commuting square
R --→ P = R[X] ---→ S
|                   |
↓                   ↓
R' -→ P' = R'[X'] → S
A hom between `P` and `P'` is an assignment `I → P'` such that the arrows commute.
Also see `Algebra.Generators.Hom.equivAlgHom`.
 -/
Algebra.Generators.Hom : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            Algebra.Generators R S ι →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst : CommRing R'] →
                      [inst_3 : CommRing S'] →
                        [inst_4 : Algebra R' S'] →
                          Algebra.Generators R' S' ι' → [Algebra S S'] → Type (max (max u_1 u_3) w)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasFDerivAt.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) • f') x
-- Mathlib.Order.SuccPred.Limit
Order.isSuccLimitRecOn_succ : ∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α]
  (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) [inst_2 : NoMaxOrder α] (b : α),
  Order.isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b ⋯
-- Mathlib.Order.SuccPred.Tree
RootedTree.subtreeOf.eq_1 : ∀ (t : RootedTree) [inst : DecidableEq ↑t] (v : ↑t), t.subtreeOf v = t.subtree (IsPredArchimedean.findAtom v)
-- Mathlib.RingTheory.MvPolynomial.Groebner
/-- Division by a multivariate polynomial
whose leading coefficient is invertible with respect to a monomial order  -/
MonomialOrder.div_single : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {b : MvPolynomial σ R},
  IsUnit (m.leadingCoeff b) →
    ∀ (f : MvPolynomial σ R),
      ∃ g r, f = g * b + r ∧ m.toSyn (m.degree (b * g)) ≤ m.toSyn (m.degree f) ∧ ∀ c ∈ r.support, ¬m.degree b ≤ c
-- Mathlib.Analysis.InnerProductSpace.Subspace
_private.Mathlib.Analysis.InnerProductSpace.Subspace.0.«term⟪_,_⟫_2» : Lean.ParserDescr
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_mul : ∀ (a b : ℤ) (n : ℕ), a <<< n * b = (a * b) <<< n
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitStatus.ready.sizeOf_spec : ∀ (numCases : ℕ) (isRec tryPostpone : optParam Bool false),
  sizeOf (Lean.Meta.Grind.SplitStatus.ready numCases isRec tryPostpone) =
    1 + sizeOf numCases + sizeOf isRec + sizeOf tryPostpone
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_eq_some_iff : ∀ {w n : ℕ} {a : Bool} {l : BitVec w}, l[n]? = some a ↔ ∃ (h : n < w), l[n] = a
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.step_intermediateZip.match_1.splitter : {α₁ β₁ : Type u_1} →
  [inst : Std.Iterator α₁ Id β₁] →
    {it₁ : Std.Iter β₁} →
      (motive : it₁.Step → Sort u_2) →
        (x : it₁.Step) →
          ((it₁' : Std.Iter β₁) →
              (out : β₁) →
                (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩) →
            ((it₁' : Std.Iter β₁) →
                (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩) →
              ((hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩) → motive x
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ChooseArg.mk.inj : ∀ {ref : Lean.Syntax} {name : Lean.Name} {expectedType? : Option Lean.Term} {ref_1 : Lean.Syntax} {name_1 : Lean.Name}
  {expectedType?_1 : Option Lean.Term},
  { ref := ref, name := name, expectedType? := expectedType? } =
      { ref := ref_1, name := name_1, expectedType? := expectedType?_1 } →
    ref = ref_1 ∧ name = name_1 ∧ expectedType? = expectedType?_1
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.center.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G], AddSubgroup.center G = { toAddSubmonoid := AddSubmonoid.center G, neg_mem' := ⋯ }