mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s)
  [inst_6 : T2Space M] [inst_7 : IsManifold I (↑⊤) M] {i : ι} {x : M},
  ↑(fs.toFun i) x = 0 → (fs.toSmoothPartitionOfUnity i) x = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_filter_key : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {f : α → Bool} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filter (fun k x => f k) m).getKey! k = (Option.filter f (m.getKey? k)).get!
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.insertMany_append : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {l₁ l₂ : List α},
  t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_const_mul_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜] {c : 𝕜},
  IsUnit c → ∀ (f : α → 𝕜), MeasureTheory.Integrable (fun x => c * f x) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.RingTheory.WittVector.Frobenius
/-- A key divisibility fact for the proof of `WittVector.map_frobeniusPoly`.  -/
WittVector.map_frobeniusPoly.key₁ : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n j : ℕ), j < p ^ n → p ^ (n - multiplicity p (j + 1)) ∣ (p ^ n).choose (j + 1)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_div_left₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Div β] [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) → ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (f i / f j) (f k) μ
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instT2Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T2Space M], T2Space Mᵈᵐᵃ
-- Mathlib.Analysis.Normed.Ring.Int
Int.enorm_natCast : ∀ (n : ℕ), ‖↑n‖ₑ = ↑n
-- Init.Data.Ord.Basic
instDecidableRelLt : {α : Type u_1} → [inst : Ord α] → DecidableRel LT.lt
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
/-- If `G` has a topology, and `H ≤ K` are
subgroups, then `H` as a subgroup of `K` is isomorphic, as a topological group, to `H` as a subgroup
of `G`. This is `addSubgroupOfEquivOfLe` upgraded to a `ContinuousAddEquiv`. -/
AddSubgroup.addSubgroupOfContinuousAddEquivOfLe : {G : Type u_1} →
  [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → {H K : AddSubgroup G} → H ≤ K → ↥(H.addSubgroupOf K) ≃ₜ+ ↥H
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.MemSobolev.add : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)]
  {f g : TemperedDistribution E F},
  TemperedDistribution.MemSobolev s p f →
    TemperedDistribution.MemSobolev s p g → TemperedDistribution.MemSobolev s p (f + g)
-- Lean.Elab.DefView
Lean.Elab.DefKind.opaque : Lean.Elab.DefKind
-- Mathlib.Algebra.Algebra.Unitization
/-- The identity map between `Unitization R A` and `R × A` as an `AddEquiv`.  -/
Unitization.addEquiv : (R : Type u_3) → (A : Type u_4) → [inst : Add R] → [inst_1 : Add A] → Unitization R A ≃+ R × A
-- Mathlib.Data.Finset.NAry
Finset.image₂_singleton_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {t : Finset β} {a : α},
  Finset.image₂ f {a} t = Finset.image (fun b => f a b) t
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderivWithin_sub` -/
mvfderivWithin_fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {s : Set M} {g g' : M → F} {x : M},
  MDiffAt[s] g x → MDiffAt[s] g' x → UniqueMDiffAt[s] x → (d[s] fun i => g i - g' i) x = d[s] g x - d[s] g' x
-- Mathlib.Order.Interval.Multiset
Multiset.Ioo_self : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a : α), Multiset.Ioo a a = 0
-- Init.Data.Iterators.ToIterator
/-- Replaces `ToIterator.iterM` with its definition.  -/
Std.ToIterator.iterM_eq : ∀ {γ : Type u} {α β : Type v} {it : γ → Std.IterM Id β} {x : γ}, Std.ToIterator.iterM x = it x
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.compactSpace_iff : ∀ {α : Type u_1} [inst : UniformSpace α], CompactSpace (TopologicalSpace.Closeds α) ↔ CompactSpace α
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.builder : Aesop.Frontend.DBuilderName → Aesop.Frontend.Feature
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The pentagon identity relating the isomorphism between `X ⊗ (Y ⊗ (Z ⊗ W))` and `((X ⊗ Y) ⊗ Z) ⊗ W`
 -/
CategoryTheory.MonoidalCategory.pentagon : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
        Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.pow_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (n : ℕ)
  (a : DoubleCentralizer 𝕜 A), (a ^ n).toProd.2 = a.toProd.2 ^ n
-- Mathlib.Dynamics.Ergodic.Conservative
/-- The identity map is conservative w.r.t. any measure.  -/
MeasureTheory.Conservative.id : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α), MeasureTheory.Conservative id μ
-- Lean.Compiler.IR.Basic
Lean.IR.Arg.beq : Lean.IR.Arg → Lean.IR.Arg → Bool
-- Mathlib.Topology.Bases
isOpenMap_eval : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] (i : ι), IsOpenMap (Function.eval i)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
NormedSpace.exp_continuousMap_eq : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace α] [inst_2 : CompactSpace α] (f : C(α, 𝕜)),
  NormedSpace.exp f = { toFun := NormedSpace.exp ∘ ⇑f, continuous_toFun := ⋯ }
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.eventuallyLE_zero_add_atBot : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M}, f ≤ᶠ[l] 0 → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.equivalenceOfReindexing_functor : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  (CategoryTheory.Limits.Cone.equivalenceOfReindexing e α).functor =
    (CategoryTheory.Limits.Cone.whiskering e.functor).comp (CategoryTheory.Limits.Cone.postcompose α.hom)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.mul_nc_go_NonnegCoeffs : ∀ (p₁ p₂ acc : Lean.Grind.CommRing.Poly),
  p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (Lean.Grind.CommRing.Poly.mul_nc.go p₂ p₁ acc).NonnegCoeffs
-- Mathlib.Order.Defs.PartialOrder
lt_trans : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.instHasLimitsOfShapeOfHasLimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  [CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C], CategoryTheory.Limits.HasLimitsOfShape J C
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_inter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂
-- Lean.Declaration
Lean.ConstantInfo.numLevelParams : Lean.ConstantInfo → ℕ
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.link2.congr_simp : ∀ {α : Type u} {β : α → Type v} (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced),
  l.link2 r hl hr = l.link2 r hl hr
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condIndep_iSup_limsup : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [inst : StandardBorelSpace Ω] (hm : m ≤ m0)
  [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) →
            (∀ (n : ι), ∃ a, n ∈ ns a) → ProbabilityTheory.CondIndep m (⨆ n, s n) (Filter.limsup s f) hm μ
-- Mathlib.Computability.ContextFreeGrammar
/-- The replacement is at the start of the remaining string.  -/
ContextFreeRule.Rewrites.head : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} (s : List (Symbol T N)),
  r.Rewrites (Symbol.nonterminal r.input :: s) (r.output ++ s)
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.concreteCategory : (P : TopCat → Prop) → CategoryTheory.ConcreteCategory (CompHausLike P) fun x1 x2 => C(↑x1.toTop, ↑x2.toTop)
-- Mathlib.Algebra.Category.Ring.Limits
RingCat.ringObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J RingCat) → (j : J) → Ring ((F.comp (CategoryTheory.forget RingCat)).obj j)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → W'.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 ≠ Q 1 * P 2 → W'.dblZ P ≠ 0
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.eqLocus.eq_1 : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : Monoid M] (f g : G →* M),
  f.eqLocus g = { toSubmonoid := f.eqLocusM g, inv_mem' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.biconeFinCategory : (J : Type v₁) →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] → CategoryTheory.FinCategory (CategoryTheory.Bicone J)
-- Mathlib.Analysis.Calculus.TangentCone.Defs
/-- The set of all tangent directions to the set `s` at the point `x`.

A point `y` belongs to the tangent cone of `s` at `x` iff
there exist a family of scalars `c n`, a family of vectors `d n`,
and a nontrivial filter in the index type such that

- `d n → 0` along the filter;
- `x + d n ∈ s` eventually along the filter;
- `c n • d n → y` along the filter,

The actual definition is given in terms of cluster points of a filter,
see `mem_tangentConeAt_of_seq` and `exists_fun_of_mem_tangentConeAt`
for the two implications unfolding this definition in more convenient way.

In a space with first countable topology,
one can assume that the index type is `ℕ` and the filter is `atTop`,
but the definition we use is more useful without that assumption.
 -/
tangentConeAt : (R : Type u_1) → {E : Type u_2} → [AddCommGroup E] → [SMul R E] → [TopologicalSpace E] → Set E → E → Set E
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.isRightDerivedFunctor_iff_isLeftKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W],
  RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α
-- Mathlib.RingTheory.Polynomial.Opposites
/-- Ring isomorphism between `R[X]ᵐᵒᵖ` and `Rᵐᵒᵖ[X]` sending each coefficient of a polynomial
to the corresponding element of the opposite ring.  -/
Polynomial.opRingEquiv : (R : Type u_2) → [inst : Semiring R] → (Polynomial R)ᵐᵒᵖ ≃+* Polynomial Rᵐᵒᵖ
-- Mathlib.Algebra.Order.Monovary
Antivary.sub_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β}, Antivary f₁ g → Monovary f₂ g → Antivary (f₁ - f₂) g
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SimpleGraph.nonuniformWitness.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst_3 : DecidableRel G.Adj} [inst_4 : DecidableRel G_1.Adj] (ε ε_1 : 𝕜),
      ε = ε_1 →
        ∀ (s s_1 : Finset α),
          s = s_1 → ∀ (t t_1 : Finset α), t = t_1 → G.nonuniformWitness ε s t = G_1.nonuniformWitness ε_1 s_1 t_1
-- Mathlib.Algebra.Star.Basic
/-- **Alias** of `starRingEnd_self_apply`. -/
Complex.conj_conj : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] (x : R), (starRingEnd R) ((starRingEnd R) x) = x
-- Init.Data.Option.List
Option.toList_eq_singleton_iff : ∀ {α : Type u_1} {a : α} {o : Option α}, o.toList = [a] ↔ o = some a
-- Mathlib.NumberTheory.Divisors
Nat.divisors_eq_empty : ∀ {n : ℕ}, n.divisors = ∅ ↔ n = 0
-- Mathlib.Order.Monotone.Basic
StrictAntiOn.le_iff_ge : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → (f a ≤ f b ↔ b ≤ a)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons.injEq : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (v_1 : V) (h_1 : G.Adj u v_1)
  (p_1 : G.Walk v_1 w), (SimpleGraph.Walk.cons h p = SimpleGraph.Walk.cons h_1 p_1) = (v = v_1 ∧ p ≍ p_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.convexOn_cfcₙ_of_convexOn_cfc : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {f : ℝ → ℝ} {s : Set A},
  ConvexOn ℝ (Unitization.inr '' s) (cfc f) → ConvexOn ℝ s (cfcₙ f)
-- Mathlib.Order.SuccPred.Limit
SuccOrder.limitRecOn_isMin : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  [inst_2 : WellFoundedLT α] (isMin : (a : α) → IsMin a → motive a)
  (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) (hb : IsMin b),
  SuccOrder.limitRecOn b isMin succ isSuccLimit = isMin b hb
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- If two expansions (along the positive characteristic) of two separable polynomials `g` and `g'`
agree, then they have the same degree.  -/
Polynomial.contraction_degree_eq_or_insep : ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g g' : Polynomial F) (m m' : ℕ),
  (Polynomial.expand F (q ^ m)) g = (Polynomial.expand F (q ^ m')) g' →
    g.Separable → g'.Separable → g.natDegree = g'.natDegree
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The left homotopy relation on the category of fibrant objects.  -/
HomotopicalAlgebra.FibrantObject.homRel : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] → HomRel (HomotopicalAlgebra.FibrantObject C)
-- Mathlib.Data.Fin.Embedding
Fin.coe_castSuccEmb : ∀ {n : ℕ}, ⇑Fin.castSuccEmb = Fin.castSucc
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- A *generalised continued fraction* (gcf) is a potentially infinite expression of the form
$$
  h + \dfrac{a_0}
            {b_0 + \dfrac{a_1}
                         {b_1 + \dfrac{a_2}
                                      {b_2 + \dfrac{a_3}
                                                   {b_3 + \dots}}}}
$$
where `h` is called the *head term* or *integer part*, the `aᵢ` are called the
*partial numerators* and the `bᵢ` the *partial denominators* of the gcf.
We store the sequence of partial numerators and denominators in a sequence of `GenContFract.Pair`s
`s`.
For convenience, one often writes `[h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...]`.
 -/
GenContFract : Type u_1 → Type u_1
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.toCycles_Ψ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.toCycles_Ψ._auto_1),
  CategoryTheory.CategoryStruct.comp (X.toCycles f₂ f₃ f₂₃ h₂₃ n₀) (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) =
    CategoryTheory.CategoryStruct.comp (X.δ f₁ f₂₃ n₀ n₁ hn₁) (X.pOpcycles f₁ f₂ n₁)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instMulActionOfIsScalarTower.eq_1 : ∀ {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] {R : Type u_5} [inst_3 : Monoid R] [inst_4 : MulAction R M] [inst_5 : IsScalarTower R M M]
  [inst_6 : MulAction R X] [inst_7 : IsScalarTower R M X],
  OreLocalization.instMulActionOfIsScalarTower =
    { toSMul := OreLocalization.instSMulOfIsScalarTower, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Order.SuccPred.Basic
Order.min_of_le_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, a ≤ Order.pred a → IsMin a
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Characterization of multiplicative inverse  -/
HomotopyGroup.inv_spec : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] [inst_2 : Nonempty N]
  {i : N} {p : ↑(GenLoop N X x)}, (⟦p⟧)⁻¹ = ⟦GenLoop.symmAt i p⟧
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_add_distrib_aux : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] {s : Finset α} {f g : α → β},
  (↑s).Pairwise (Function.onFun AddCommute f) →
    (↑s).Pairwise (Function.onFun AddCommute g) →
      ((↑s).Pairwise fun x y => AddCommute (g x) (f y)) → (↑s).Pairwise fun x y => AddCommute ((f + g) x) ((f + g) y)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.inl_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.map f g) =
    CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.instDecidableEq.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], FreeGroup.instDecidableEq = ⋯.decidableEq
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {s : Set α} {β : Type u_9} [inst : NormedAddCommGroup β]
  (μ : autoParam (MeasureTheory.Measure α) MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd._auto_1),
  p ≠ ⊤ →
    MeasurableSet s →
      ∀ {f g : α → β} {c : ℝ},
        0 ≤ c →
          (∀ x ∈ s, dist (f x) (g x) ≤ c) →
            MeasureTheory.eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
-- Mathlib.LinearAlgebra.Basis.Exact
Submodule.projectionOnto_comp_surjective_of_exact : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    ∀ {p q : Submodule R M} (hpq : IsCompl p q),
      Submodule.map g q = ⊤ → Function.Surjective ⇑(p.projectionOnto q hpq ∘ₗ f)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_neg_shift' : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i : A),
  (CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C (-i)).map f) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C (-i) i ⋯).hom.app X)
      (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C (-i) i ⋯).inv.app Y))
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findExpectedTypeAt : Lean.Elab.InfoTree → String.Pos.Raw → Option (Lean.Elab.ContextInfo × Lean.Expr)
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.mkPure : Lean.Elab.Do.ControlStack → Lean.Name → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instPow : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : Monoid R] → [BoundedMul R] → [ContinuousMul R] → Pow (BoundedContinuousFunction α R) ℕ
-- Mathlib.Data.Matrix.Basic
Matrix.entryLinearMap_toAddHom : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α] {i : m} {j : n}, ↑(Matrix.entryLinearMap R α i j) = Matrix.entryAddHom α i j
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquivAlg_symm : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Ring B] [inst_4 : Algebra R₁ B] {I : Ideal A} (J : Ideal B) [inst_5 : I.IsTwoSided] [inst_6 : J.IsTwoSided]
  (f : A ≃ₐ[R₁] B) (hIJ : J = Ideal.map (↑f) I), (I.quotientEquivAlg J f hIJ).symm = J.quotientEquivAlg I f.symm ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {c d : E → 𝔸'} {c' d' : E →L[𝕜] 𝔸'},
  HasStrictFDerivAt c c' x → HasStrictFDerivAt d d' x → HasStrictFDerivAt (c * d) (c x • d' + d x • c') x
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeEquivRight_apply_coe : ∀ {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (a : { a // p a }), ↑((Equiv.subtypeEquivRight e) a) = ↑a