mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.inv_prodComparison_map_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B))
      (F.map CategoryTheory.Limits.prod.fst) =
    CategoryTheory.Limits.prod.fst
-- Mathlib.Topology.Homotopy.Basic
/-- Continuously extending a curried homotopy to a function from `ℝ` to `C(X, Y)`.
 -/
ContinuousMap.Homotopy.extend : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → {f₀ f₁ : C(X, Y)} → f₀.Homotopy f₁ → C(ℝ, C(X, Y))
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Vector.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.splitter : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) →
      (x : Std.IterStep (Std.IterM m α) α) →
        ((it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out)) →
          ((it : Std.IterM m α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.GroupTheory.Finiteness
Monoid.closure_finset_fg : ∀ {M : Type u_1} [inst : Monoid M] (s : Finset M), Monoid.FG ↥(Submonoid.closure ↑s)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.ext : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f g : S.LocalizationMap N}, (∀ (x : M), f x = g x) → f = g
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified : CategoryTheory.MorphismProperty.HasOfPostcompProperty (@AlgebraicGeometry.Etale)
  (@AlgebraicGeometry.LocallyOfFiniteType ⊓ @AlgebraicGeometry.FormallyUnramified)
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev?_eq_none_iff : ∀ {s : String.Slice} {p : s.Pos}, p.prev? = none ↔ p = s.startPos
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.quotientToQuotientRangePowQuotSucc_surjective : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [hfp : NeZero (p.ramificationIdx' P)] [IsDedekindDomain S],
  P ≠ ⊥ →
    ∀ [hP : P.IsPrime] {i : ℕ},
      i < p.ramificationIdx' P →
        ∀ {a : S} (a_mem : a ∈ P ^ i),
          a ∉ P ^ (i + 1) → Function.Surjective ⇑(p.quotientToQuotientRangePowQuotSucc P a_mem)
-- Mathlib.ModelTheory.Satisfiability
/-- A theory is complete when it is satisfiable and models each sentence or its negation.  -/
FirstOrder.Language.Theory.IsComplete : {L : FirstOrder.Language} → L.Theory → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multispanIndexCoend_snd : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : (CategoryTheory.Limits.multispanShapeCoend J).L),
  (CategoryTheory.Limits.multispanIndexCoend F).snd f =
    (F.obj (Opposite.op (CategoryTheory.Arrow.right f))).map (CategoryTheory.Arrow.hom f)
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiffAt_piLp_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_3 : Fintype ι]
  (p : ENNReal) [inst_4 : Fact (1 ≤ p)] {n : WithTop ℕ∞} {i : ι} {y : PiLp p E}, ContDiffAt 𝕜 n (fun f => f.ofLp i) y
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instAdd : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Add (FractionalIdeal S P)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.natTrailingDegree_reverse : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.reverse.natTrailingDegree = 0
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressProcessingInfo.mk.injEq : ∀ (range : Lean.Lsp.Range) (kind : Lean.Lsp.LeanFileProgressKind) (range_1 : Lean.Lsp.Range)
  (kind_1 : Lean.Lsp.LeanFileProgressKind),
  ({ range := range, kind := kind } = { range := range_1, kind := kind_1 }) = (range = range_1 ∧ kind = kind_1)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_of_div_tendsto_nhds : ∀ {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f g : α → 𝕜},
  (∀ᶠ (x : α) in l, g x = 0 → f x = 0) → ∀ (c : 𝕜), Filter.Tendsto (f / g) l (nhds c) → f =O[l] g
-- Mathlib.Analysis.Normed.Operator.CompleteCodomain
/-- If a space of multilinear maps from `Π i, E i` to `F` is complete, and each `E i` has a nonzero
element, then `F` is complete.  -/
SeparatingDual.completeSpace_of_completeSpace_continuousMultilinearMap : ∀ (𝕜 : Type u_1) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_4} [Finite ι] {M : ι → Type u_5} [inst_4 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_5 : (i : ι) → NormedSpace 𝕜 (M i)] [∀ (i : ι), SeparatingDual 𝕜 (M i)]
  [CompleteSpace (ContinuousMultilinearMap 𝕜 M F)] {m : (i : ι) → M i}, (∀ (i : ι), m i ≠ 0) → CompleteSpace F
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_10 : HAdd Std.Time.Millisecond.Offset Std.Time.Day.Offset Std.Time.Millisecond.Offset
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.pow_le_iff_le_log : ∀ {x y : ℝ} {n : ℕ}, 0 < x → 0 < y → (x ^ n ≤ y ↔ ↑n * Real.log x ≤ Real.log y)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_le_ediam : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], G.radius ≤ G.ediam
-- Mathlib.Data.Finite.Prod
Set.finite_image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β},
  (∀ b ∈ t, Set.InjOn (fun x => f x b) s) →
    (∀ a ∈ s, Set.InjOn (f a) t) → ((Set.image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.SeparatingLeft.eq_1 : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M), B.SeparatingLeft = ∀ (x : M₁), (∀ (y : M₂), (B x) y = 0) → x = 0
-- Mathlib.Condensed.Module
/-- The category of condensed `R`-modules, defined as sheaves of `R`-modules over
`CompHaus` with respect to the coherent Grothendieck topology.
 -/
CondensedMod : (R : Type (u + 1)) → [Ring R] → Type (u + 2)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → (m.isEmpty = false ↔ ∃ a, m.contains a = true)
-- Mathlib.Algebra.Algebra.Pi
/-- Use `AlgHom.pi_apply` instead.  -/
Pi.algHom_apply : ∀ {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {B : Type u_4} [inst_3 : Semiring B] [inst_4 : Algebra R B]
  (g : (i : ι) → B →ₐ[R] A i) (x : B) (i : ι), (Pi.algHom R A g) x i = (g i) x
-- Aesop.RuleTac.Forward.Basic
/-- Name of the `implDetail` hyp corresponding to the forward `hyp` with name
`fwdHypName` and depth `depth`.  -/
Aesop.forwardImplDetailHypName : Lean.Name → ℕ → Lean.Name
-- Mathlib.GroupTheory.Finiteness
AddGroup.closure_finset_fg : ∀ {G : Type u_3} [inst : AddGroup G] (s : Finset G), AddGroup.FG ↥(AddSubgroup.closure ↑s)
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.bijective : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), Function.Bijective ⇑h
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  {X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).functor.map f).f = f.f
-- Init.Data.Array.MapIdx
Array.mapFinIdxM.map.eq_2 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : (i : ℕ) → α → i < as.size → m β)
  (j : ℕ) (bs : Array β) (i_2 : ℕ) (inv_2 : i_2 + 1 + j = as.size),
  Array.mapFinIdxM.map as f i_2.succ j inv_2 bs = do
    let __do_lift ← f j as[j] ⋯
    Array.mapFinIdxM.map as f i_2 (j + 1) ⋯ (bs.push __do_lift)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The epimorphism in `SimplexCategory` associated to `A : Splitting.IndexSet Δ`  -/
CategoryTheory.SimplicialObject.Splitting.IndexSet.e : {Δ : SimplexCategoryᵒᵖ} →
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) → Opposite.unop Δ ⟶ Opposite.unop A.fst
-- Init.Data.BEq
/-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`.  -/
PartialEquivBEq.trans : ∀ {α : Type u_1} {inst : BEq α} [self : PartialEquivBEq α] {a b c : α},
  (a == b) = true → (b == c) = true → (a == c) = true
-- Mathlib.Data.Multiset.AddSub
Multiset.coe_sub : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : List α), ↑s - ↑t = ↑(s.diff t)
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_one : ∀ {ι : Type u_1} (u : Set ι), ProbabilityTheory.setBernoulli u 1 = MeasureTheory.Measure.dirac u
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A relative CW complex with an empty base is an absolute CW complex.  -/
Topology.RelCWComplex.toCWComplex : {X : Type u_1} → [inst : TopologicalSpace X] → (C : Set X) → [Topology.RelCWComplex C ∅] → Topology.CWComplex C
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Submonoid.subsemiringClosure_toNonUnitalSubsemiring : ∀ {R : Type u} [inst : NonAssocSemiring R] (M : Submonoid R),
  M.subsemiringClosure.toNonUnitalSubsemiring = NonUnitalSubsemiring.closure ↑M
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
ModularForm.levelOne_weight_six_rank_one : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 6) = 1
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Finset.product_self_eq_disjiUnion_perm_aux : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Finset α},
  f.IsCycleOn ↑s →
    (↑(Finset.range s.card)).PairwiseDisjoint fun k => Finset.map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s
-- Mathlib.Data.Set.Operations
Set.mem_image_of_mem : ∀ {α : Type u} {β : Type v} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
-- Mathlib.Logic.Pairwise
/-- **Alias** of the forward direction of `Function.injective_iff_pairwise_ne`. -/
Function.Injective.pairwise_ne : ∀ {α : Type u_1} {ι : Type u_3} {f : ι → α}, Function.Injective f → Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) f)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instZeroHom : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → Zero (M ⟶ N)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedParentSet : Inhabited Lean.Meta.Grind.ParentSet
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_eq_of_range_eq : ∀ {ι : Sort u_3} {ι' : Sort u_4} {f : ι → Ordinal.{u_5}} {g : ι' → Ordinal.{u_5}},
  Set.range f = Set.range g → iSup f = iSup g
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.instSemigroupWithZero : {α : Type u₁} → {β : Type u₂} → [inst : SemigroupWithZero β] → SemigroupWithZero (α →₀ β)
-- Mathlib.Order.Hom.Bounded
BotHom.instDistribLattice : {α : Type u_2} →
  {β : Type u_3} → [inst : Bot α] → [inst_1 : DistribLattice β] → [inst_2 : OrderBot β] → DistribLattice (BotHom α β)
-- Mathlib.Topology.MetricSpace.Basic
instMetricSpaceNNReal : MetricSpace NNReal
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.opcyclesMap'_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.opcyclesMap' (φ + φ') h₁ h₂ =
    CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂ + CategoryTheory.ShortComplex.opcyclesMap' φ' h₁ h₂
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.Corec.f.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : α ⊕ β → Sort u_3) →
      (x : α ⊕ β) → ((a : α) → motive (Sum.inl a)) → ((val : β) → motive (Sum.inr val)) → motive x
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sUnion_lem : ∀ {α β : Type u} (A : α → PSet.{u}) (B : β → PSet.{u}),
  (∀ (a : α), ∃ b, (A a).Equiv (B b)) →
    ∀ (a : (⋃₀ PSet.mk α A).Type), ∃ b, ((⋃₀ PSet.mk α A).Func a).Equiv ((⋃₀ PSet.mk β B).Func b)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.copyCount_pos : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V],
  0 < G.copyCount H ↔ H.IsContained G
-- Mathlib.RingTheory.Unramified.LocalStructure
_private.Mathlib.RingTheory.Unramified.LocalStructure.0.Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top_aux₂ : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Ideal R}
  [inst_3 : P.IsPrime] {Q : Ideal S} [inst_4 : Q.IsPrime] [inst_5 : Q.LiesOver P] [Algebra.IsUnramifiedAt R Q] (x : S)
  (p : Polynomial R) [inst_7 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)]
  [inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q],
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (Polynomial.aeval (1 ⊗ₜ[R] x)).toRingHom →
    R[x] = ⊤ →
      ¬minpoly P.ResidueField ((algebraMap S Q.ResidueField) x) ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
-- Mathlib.Data.Vector.Defs
/-- `toList` of `cons` of a vector and an element is
the `cons` of the list obtained by `toList` and the element  -/
List.Vector.toList_cons : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), (a ::ᵥ v).toList = a :: v.toList
-- Init.Grind.Order
Lean.Grind.Order.of_natCast_eq : ∀ {α : Type u} [inst : NatCast α] (a b : ℕ) (x y : α), ↑a = x → ↑b = y → a = b → x = y
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.merge.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (ys : List α) (h_1 : (ys : List α) → motive [] ys)
  (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match [], ys with
    | [], ys => h_1 ys
    | xs, [] => h_2 xs
    | x :: xs, y :: ys => h_3 x xs y ys) =
    h_1 ys
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  k ∉ m₂ → (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
complex normed space.  Let `f : E → F` be a function that is complex differentiable on `U` and is
continuous on its closure. Suppose that `‖f x‖` takes its maximum value on `U` at `c ∈ U`. Then
`f x = f c` for all `x ∈ closure U`.  -/
Complex.eqOn_closure_of_isPreconnected_of_isMaxOn_norm : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [StrictConvexSpace ℝ F] {f : E → F} {U : Set E} {c : E},
  IsPreconnected U →
    IsOpen U → DiffContOnCl ℂ f U → c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn f (Function.const E (f c)) (closure U)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of a finite affinely independent family has
dimension one less than its cardinality.  -/
AffineIndependent.finrank_vectorSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
  AffineIndependent k p → ∀ {n : ℕ}, Fintype.card ι = n + 1 → Module.finrank k ↥(vectorSpan k (Set.range p)) = n
-- Mathlib.Data.Finset.Empty
Finset.decidableNonempty : {α : Type u_1} → {s : Finset α} → Decidable s.Nonempty
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instInhabitedConfig.default : Mathlib.Tactic.RingNF.Config
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.findMin'.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → α → Sort u_2) →
    (x : Ordnode α) →
      (x_1 : α) →
        ((x : α) → motive Ordnode.nil x) →
          ((size : ℕ) →
              (l : Ordnode α) → (x : α) → (r : Ordnode α) → (x_2 : α) → motive (Ordnode.node size l x r) x_2) →
            motive x x_1
-- Mathlib.Topology.PartitionOfUnity
/-- If `X` is a paracompact normal topological space and `U` is an open covering of a closed set
`s`, then there exists a `BumpCovering ι X s` that is subordinate to `U`.  -/
BumpCovering.exists_isSubordinate : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X],
  IsClosed s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
-- Batteries.Lean.Syntax
/-- Applies the given function to every subsyntax.

Like `Syntax.replaceM` but for typed syntax.
(Note there are no guarantees of type correctness here.)
 -/
Lean.TSyntax.replaceM : {M : Type → Type} →
  {k : Lean.SyntaxNodeKinds} → [Monad M] → (Lean.Syntax → M (Option Lean.Syntax)) → Lean.TSyntax k → M (Lean.TSyntax k)
-- Lean.Parser.Basic
/-- Like `quotedCharFn` but enables escapes that are only valid inside strings.
In particular, string gaps (`"\" newline whitespace*`).
 -/
Lean.Parser.quotedStringFn : Lean.Parser.ParserFn
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.C_content_dvd : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R), Polynomial.C p.content ∣ p
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.isUniformEmbedding_restrictScalars : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_5 : AddCommGroup F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] [inst_8 : Module 𝕜 F] (𝕜' : Type u_4)
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F],
  IsUniformEmbedding (ContinuousLinearMap.restrictScalars 𝕜')
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- Let `S` be a short complex in an abelian category. Let `kf` be a
limit kernel fork of `S.g` and `cc` a limit cokernel cofork of `S.f`.
Let `kf.pt ⟶ H ⟶ cc.pt` be an epi-mono factorization of `kf.ι ≫ cc.π : kf.pt ⟶ cc.pt`.
This is the homology data expressing `H` as the homology of `S`.  -/
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) →
        {kf : CategoryTheory.Limits.KernelFork S.g} →
          {cc : CategoryTheory.Limits.CokernelCofork S.f} →
            CategoryTheory.Limits.IsLimit kf →
              CategoryTheory.Limits.IsColimit cc →
                {H : C} →
                  {π : kf.pt ⟶ H} →
                    {ι : H ⟶ cc.pt} →
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf)
                            (CategoryTheory.Limits.Cofork.π cc) =
                          CategoryTheory.CategoryStruct.comp π ι →
                        [CategoryTheory.Epi π] → [CategoryTheory.Mono ι] → S.HomologyData
-- Mathlib.Algebra.GCDMonoid.Finset
/-- Given a nonempty Finset `s` and a function `f` from `s` to `ℕ`, if `d = s.gcd`,
then the `gcd` of `(f i) / d` is equal to `1`.  -/
Finset.gcd_div_eq_one : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : Div α]
  [MulDivCancelClass α] {f : ι → α} {s : Finset ι} {i : ι}, i ∈ s → f i ≠ 0 → (s.gcd fun j => f j / s.gcd f) = 1
-- Mathlib.Data.Nat.Choose.Sum
Finset.sum_powerset_apply_card : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] (f : ℕ → α) {x : Finset β},
  ∑ m ∈ x.powerset, f m.card = ∑ m ∈ Finset.range (x.card + 1), x.card.choose m • f m
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instPartialOrder : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → PartialOrder (ProbabilityTheory.Kernel α β)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to a set `s` is `< r` iff there exists a point in `s` at distance `< r`.  -/
Metric.infDist_lt_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ},
  s.Nonempty → (Metric.infDist x s < r ↔ ∃ y ∈ s, dist x y < r)
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : 𝕜 → 𝕜` is concave on `s`, then for any point `x ∈ s` the slope of the secant line of `f`
through `x` is antitone on `s \ {x}`.  -/
ConcaveOn.slope_anti : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜},
  ConcaveOn 𝕜 s f → x ∈ s → AntitoneOn (slope f x) (s \ {x})
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.op_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {P : HomotopicalAlgebra.Precylinder X} {f g : X ⟶ Y}
  (h : P.LeftHomotopy f g), h.op.h = h.h.op
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `Over.pullback` commutes with composition.  -/
CategoryTheory.MorphismProperty.Over.pullbackComp : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        {X Y Z : T} →
          (f : X ⟶ Y) →
            (g : Y ⟶ Z) →
              [inst_2 : P.IsStableUnderBaseChangeAlong f] →
                [inst_3 : P.IsStableUnderBaseChangeAlong g] →
                  [inst_4 : P.HasPullbacksAlong f] →
                    [inst_5 : P.HasPullbacksAlong g] →
                      [Q.RespectsIso] →
                        [inst_7 : Q.IsStableUnderBaseChange] →
                          (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g)) →
                            (hfg :
                                autoParam (fg = CategoryTheory.CategoryStruct.comp f g)
                                  CategoryTheory.MorphismProperty.Over.pullbackComp._auto_1) →
                              CategoryTheory.MorphismProperty.Over.pullback P Q fg ≅
                                (CategoryTheory.MorphismProperty.Over.pullback P Q g).comp
                                  (CategoryTheory.MorphismProperty.Over.pullback P Q f)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- If all positive powers of a point on the circle lie in the right half centered arc,
then the point is `1`.  -/
Circle.eq_one_of_forall_pow_mem_centeredArc_pi_div_two : ∀ {z : Circle}, (∀ n > 0, z ^ n ∈ Circle.centeredArc (Real.pi / 2)) → z = 1
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.bdd_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜]
  {f g : α → 𝕜} {c : ℝ},
  MeasureTheory.Integrable g μ →
    MeasureTheory.AEStronglyMeasurable f μ →
      (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) → MeasureTheory.Integrable (fun x => f x * g x) μ
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwLemma.mk.sizeOf_spec : ∀ (name : Mathlib.Tactic.ClickSuggestions.Premise) (symm : Bool) (relName : Lean.Name),
  sizeOf { name := name, symm := symm, relName := relName } = 1 + sizeOf name + sizeOf symm + sizeOf relName