mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.wf.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] {inst_2 : DecidableLE α} [inst_3 : DecidableLE α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w}
  [inst_6 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxc.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) (upperBound : α) (acc acc_1 : γ),
  acc = acc_1 →
    ∀ (next next_1 : α) (e_next : next = next_1) (h : LargeEnough next)
      (f f_1 : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n { s // Pl out c s }),
      f = f_1 →
        Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f =
          Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl ⋯ LargeEnough hl upperBound acc_1 next_1 ⋯ f_1
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_of_le' : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  (l : Filter α), (∀ (x : α), ‖f x‖ ≤ c * ‖g x‖) → f =O[l] g
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.proj.injEq : ∀ (a : Lean.Name) (a_1 a_2 : ℕ) (a_3 : Lean.Name) (a_4 a_5 : ℕ),
  (Lean.Meta.DiscrTree.Key.proj a a_1 a_2 = Lean.Meta.DiscrTree.Key.proj a_3 a_4 a_5) =
    (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {x : ι → K},
  x ≠ 0 →
    Height.mulHeight x =
      (Multiset.map (fun v => ⨆ i, v (x i)) Height.AdmissibleAbsValues.archAbsVal).prod *
        ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), ⨆ i, ↑v (x i)
-- Mathlib.Analysis.Convex.Segment
/-- A point is in an `Ioc` iff it can be expressed as a semistrict convex combination of the
endpoints.  -/
Convex.mem_Ioc : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜},
  x < y → (z ∈ Set.Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Finset.tprod_subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α),
  ∏' (x : ↥s), f ↑x = ∏ x ∈ s, f x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- If a category `HasImageMaps`, then all commutative squares induce morphisms on images.  -/
CategoryTheory.Limits.HasImageMaps : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasImages C] → Prop
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_one : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → One (G i)] [inst_7 : One C] [∀ (i : ι), OneHomClass (H i) (G i) C]
  [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)), DirectLimit.lift f (fun x => ⇑(g x)) h 1 = 1
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- The "main pair" for an algebra `(A, α)` is the pair of morphisms `(F α, ε_FA)`. It is always a
`G`-split pair, and will be used to construct the left adjoint to the comparison functor and show it
is an equivalence.
 -/
CategoryTheory.Monad.MonadicityInternal.main_pair_G_split : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra),
  G.IsSplitPair (F.map A.a) (adj.counit.app (F.obj A.A))
-- Mathlib.Topology.MetricSpace.Basic
SeparationQuotient.dist_mk : ∀ {α : Type u} [inst : PseudoMetricSpace α] (p q : α),
  dist (SeparationQuotient.mk p) (SeparationQuotient.mk q) = dist p q
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_sInf : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (S : Set (ClosedSubmodule R M)), ↑(sInf S) = ⨅ s ∈ S, ↑s
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instWeakEquivalencePResolutionObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj X)
-- Mathlib.Topology.Order.Compact
ContinuousOn.image_Icc : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : TopologicalSpace β] [DenselyOrdered α] [inst_5 : ConditionallyCompleteLinearOrder β]
  [OrderTopology β] {f : α → β} {a b : α},
  a ≤ b → ContinuousOn f (Set.Icc a b) → f '' Set.Icc a b = Set.Icc (sInf (f '' Set.Icc a b)) (sSup (f '' Set.Icc a b))
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.of_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z},
  Continuous f → Function.Surjective f → Continuous g → IsOpenQuotientMap (g ∘ f) → IsOpenQuotientMap g
-- Mathlib.Data.Nat.Factorial.BigOperators
_private.Mathlib.Data.Nat.Factorial.BigOperators.0.Nat.factorial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.CategoryTheory.Limits.Final
/-- Alternative equational lemma for `(extendCocone c).ι.app` in case a lift of the object
is given explicitly.  -/
CategoryTheory.Functor.Final.extendCocone_obj_ι_app' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone (F.comp G)) {X : D} {Y : C} (f : X ⟶ F.obj Y),
  (CategoryTheory.Functor.Final.extendCocone.obj c).ι.app X = CategoryTheory.CategoryStruct.comp (G.map f) (c.ι.app Y)
-- Std.Time.Date.PlainDate
/-- Adds `Year.Offset` to a `PlainDate`, clipping the day to the last valid day of the month.
 -/
Std.Time.PlainDate.addYearsClip : Std.Time.PlainDate → Std.Time.Year.Offset → Std.Time.PlainDate
-- Lean.Level
Lean.LevelMVarId.mk : Lean.Name → Lean.LevelMVarId
-- Mathlib.Order.Filter.Extr
/-- `IsMinOn f s a` means that `f a ≤ f x` for all `x ∈ s`. Note that we do not assume `a ∈ s`.  -/
IsMinOn : {α : Type u} → {β : Type v} → [Preorder β] → (α → β) → Set α → α → Prop
-- Mathlib.CategoryTheory.Limits.Final
/-- If a functor `L : C ⥤ D` is a left adjoint, it is initial.  -/
CategoryTheory.Functor.initial_of_adjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R), L.Initial
-- Mathlib.Topology.Connected.Basic
IsConnected.subset_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {s : Set α}, IsConnected s → x ∈ s → s ⊆ connectedComponent x
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.instHasPluralDefaultsString : Lean.HasPluralDefaults✝ String
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.any_eq_false_iff_forall_mem_get : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α] [EquivBEq α]
  {p : α → Bool}, m.WF → (m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p (m.get a h) = false)
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.isArtinianScheme_iff : ∀ (X : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.IsArtinianScheme X ↔ AlgebraicGeometry.IsLocallyArtinian X ∧ CompactSpace ↥X
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- Given a morphism of short complexes `φ : S₁ ⟶ S₂` in an abelian category, if `S₁.g = 0`
(e.g when `S₁` is of the form `S₁.X₁ ⟶ S₁.X₂ ⟶ 0`) and both `S₂.f` and `S₂.g` are zero
(e.g when `S₂` is of the form `0 ⟶ S₂.X₂ ⟶ 0`), then `φ` is a quasi-isomorphism iff
the obvious short complex `S₁.X₁ ⟶ S₁.X₂ ⟶ S₂.X₂` is exact and `φ.τ₂` is an epi.  -/
CategoryTheory.ShortComplex.quasiIso_iff_of_zeros' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  S₁.g = 0 →
    ∀ (hf₂ : S₂.f = 0),
      S₂.g = 0 →
        (CategoryTheory.ShortComplex.QuasiIso φ ↔
          { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ CategoryTheory.Epi φ.τ₂)
-- Mathlib.GroupTheory.FiniteAbelian.Basic
/-- If `A` and `B` are two `R`-submodules of the `R`-algebra `M`, where `R` is finitely generated
as a `ℤ`-module, `A` is finitely generated, and `B` contains `n • A`, then `B` has finite
relative index in `A`.  -/
Submodule.isFiniteRelIndex_of_map_linearMapMulLeft_le : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : CommRing K] [inst_2 : Algebra R K] [Module.Finite ℤ R]
  {A B : Submodule R K} {n : ℕ},
  n ≠ 0 → A.FG → Submodule.map (LinearMap.mulLeft R ↑n) A ≤ B → B.toAddSubgroup.IsFiniteRelIndex A.toAddSubgroup
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The inner product of a column of `A` and a column of `B` is an entry of `Aᴴ * B`.  -/
inner_matrix_col_col : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype m] (A B : Matrix m n 𝕜) (i j : n),
  inner 𝕜 (WithLp.toLp 2 (A.transpose i)) (WithLp.toLp 2 (B.transpose j)) = (A.conjTranspose * B) i j
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).hom
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.equalizer.ι f g)
        (CategoryTheory.Limits.pullback.fst s v)) =
    CategoryTheory.Limits.equalizer.ι
      (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
        (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
      (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
        (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
-- Mathlib.Order.Filter.Pointwise
Filter.zero_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] {l : Filter β}, 0 ×ˢ l = Filter.map (fun x => (0, x)) l
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.coe_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubsemigroup M), ↑s.topologicalClosure = closure ↑s
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.prod_pi_mulSingle`.  -/
Fintype.prod_pi_mulSingle : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {M : ι → Type u_6} [inst_2 : (i : ι) → CommMonoid (M i)]
  (i : ι) (f : (i : ι) → M i), ∏ j, Pi.mulSingle j (f j) i = f i
-- Init.Sym.Simp.SimprocDSL
/-- Simplify arrow telescopes (`p₁ → p₂ → ... → q`) without entering binders.
Simplifies each `pᵢ` and `q` individually. Intended as a `pre` simproc.  -/
Lean.Parser.Sym.Simp.arrowTelescope : Lean.ParserDescr
-- Mathlib.Order.Bounds.Basic
/-- If `a` is the least element of a set `s`, then subtype `s` is an order with bottom element.  -/
IsLeast.orderBot : {α : Type u_1} → [inst : Preorder α] → {s : Set α} → {a : α} → IsLeast s a → OrderBot ↑s
-- Mathlib.RingTheory.LocalProperties.Exactness
bijective_of_isLocalization_of_span_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] {s : Set R},
  Ideal.span s = ⊤ →
    ∀ (Rᵣ : ↑s → Type u_3) [inst_2 : (r : ↑s) → CommSemiring (Rᵣ r)] [inst_3 : (r : ↑s) → Algebra R (Rᵣ r)]
      (Sᵣ : ↑s → Type u_4) [inst_4 : (r : ↑s) → CommSemiring (Sᵣ r)] [inst_5 : (r : ↑s) → Algebra S (Sᵣ r)]
      (f : R →+* S) [inst_6 : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)]
      [inst_7 : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)],
      (∀ (r : ↑s), Function.Bijective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)) → Function.Bijective ⇑f
-- Mathlib.RepresentationTheory.Coinvariants
Rep.instPreservesZeroMorphismsModuleCatCoinvariantsFunctor : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G],
  (Rep.coinvariantsFunctor k G).PreservesZeroMorphisms
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.Hom.w : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (φ : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left φ) g.hom = f.hom
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
_private.Mathlib.Combinatorics.SimpleGraph.Bipartite.0.SimpleGraph.bipartiteDoubleCover.match_1.splitter : {V : Type u_1} →
  (motive : V ⊕ V → V ⊕ V → Sort u_2) →
    (x x_1 : V ⊕ V) →
      ((v' w' : V) → motive (Sum.inl v') (Sum.inr w')) →
        ((v' w' : V) → motive (Sum.inr v') (Sum.inl w')) →
          ((x x_2 : V ⊕ V) →
              (∀ (v' w' : V), x = Sum.inl v' → x_2 = Sum.inr w' → False) →
                (∀ (v' w' : V), x = Sum.inr v' → x_2 = Sum.inl w' → False) → motive x x_2) →
            motive x x_1
-- Lean.Setup
Lean.ModuleHeader.mk.injEq : ∀ (imports : Array Lean.Import) (isModule : Bool) (imports_1 : Array Lean.Import) (isModule_1 : Bool),
  ({ imports := imports, isModule := isModule } = { imports := imports_1, isModule := isModule_1 }) =
    (imports = imports_1 ∧ isModule = isModule_1)
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- Given `a : 𝒳`, `b : Fib p R`, and a diagram
```
  b --φ--> a
  -        -
  |        |
  v        v
  R --f--> S
```
It can be factorized as
```
  b --τ--> b'--ψ--> a
  -        -        -
  |        |        |
  v        v        v
  R ====== R --f--> S
```
with `ψ` Cartesian over `f` and `τ` a map in `Fib p R`.  -/
HasFibers.fiber_factorization : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] [p.IsFibered] {R S : 𝒮} {a : 𝒳},
  p.obj a = S →
    ∀ {b : HasFibers.Fib p R} (f : R ⟶ S) (φ : (HasFibers.ι R).obj b ⟶ a) [p.IsHomLift f φ],
      ∃ b' τ ψ, p.IsStronglyCartesian f ψ ∧ CategoryTheory.CategoryStruct.comp ((HasFibers.ι R).map τ) ψ = φ
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.projIccCM.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b : α}
  [inst_3 : Fact (a ≤ b)], ContinuousMap.projIccCM = { toFun := Set.projIcc a b ⋯, continuous_toFun := ⋯ }
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.ApplyResult : Type
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The equivalence between `AddCircle p` and the half-open interval `(a, a + p]`, whose inverse
is the natural quotient map.  -/
AddCircle.equivIoc : {𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    (p : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsOrderedAddMonoid 𝕜] → [hp : Fact (0 < p)] → (a : 𝕜) → [Archimedean 𝕜] → AddCircle p ≃ ↑(Set.Ioc a (a + p))
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.apply_le_edist_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f : BoundedContinuousFunction X NNReal) (x : X), ↑(f x) ≤ edist 0 f
-- Mathlib.NumberTheory.ModularForms.Basic
ModularFormClass.continuous : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k]
  (f : F), Continuous ⇑f
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.exists_zpowers : ∀ {G : Type u_1} [inst : Group G] {x : G} {p : ↥(Subgroup.zpowers x) → Prop}, (∃ g, p g) ↔ ∃ m, p ⟨x ^ m, ⋯⟩
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapLeftHomologyIso_inv_naturality : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasLeftHomology]
  [inst_6 : S₂.HasLeftHomology] [inst_7 : F.PreservesLeftHomologyOf S₁] [inst_8 : F.PreservesLeftHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
      (S₂.mapLeftHomologyIso F).inv =
    CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).inv
      (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ))
-- Mathlib.RingTheory.Smooth.Basic
/-- An `R`-algebra `A` is formally smooth if `Ω[A⁄R]` is `A`-projective and `H¹(L_{A/R}) = 0`.
For the infinitesimal lifting definition,
see `FormallySmooth.lift` and `FormallySmooth.iff_comp_surjective`.
 -/
Algebra.FormallySmooth : (R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.mk.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {binderName : Lean.Name}
  {params : Array (Lean.Compiler.LCNF.Param pu)} {type : Lean.Expr} {value : Lean.Compiler.LCNF.Code pu}
  {fvarId_1 : Lean.FVarId} {binderName_1 : Lean.Name} {params_1 : Array (Lean.Compiler.LCNF.Param pu)}
  {type_1 : Lean.Expr} {value_1 : Lean.Compiler.LCNF.Code pu},
  Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value =
      Lean.Compiler.LCNF.FunDecl.mk fvarId_1 binderName_1 params_1 type_1 value_1 →
    fvarId = fvarId_1 ∧ binderName = binderName_1 ∧ params = params_1 ∧ type = type_1 ∧ value = value_1
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.getVert_eq_start_iff : ∀ {V : Type u} {G : SimpleGraph V} {u w : V} {i : ℕ} {p : G.Walk u w},
  p.IsPath → i ≤ p.length → (p.getVert i = u ↔ i = 0)
-- Lean.Widget.UserWidget
/-- Keeps track of panel widget instances that should be displayed.

Instances can be registered for display global
(i.e., persisted in `.olean`s) and locally (not persisted)

For globally displayed widgets
we cannot store a `WidgetInstance` in the persistent state
because it contains a `StateM` closure.
Instead, we add a global constant of type `WidgetInstance`
to the environment, and store its name in the extension.

For locally displayed ones, we just store a `WidgetInstance`
in the extension directly.
This is okay because it is never persisted.

The (persistent) entries are then of the form `(h, n)`
where `h` is a hash stored in the `moduleRegistry`
and `n` is the name of a `WidgetInstance` global constant.

The extension state maps each `h` as above
to a list of entries that can be either global or local ones.
Each element of the state indicates that the widget module `h`
should be displayed with the given `WidgetInstance` as its arguments.

This is similar to a parametric attribute, except that:
- parametric attributes map at most one parameter to one tagged declaration,
  whereas we may display multiple instances of a single widget module; and
- parametric attributes use the same type for local and global entries,
  which we cannot do owing to the closure.  -/
_private.Lean.Widget.UserWidget.0.Lean.Widget.PanelWidgetsExt : Type
-- Mathlib.Topology.Order.LowerUpperTopology
/-- Every set open in the upper topology is an upper set.  -/
Topology.IsUpper.isUpperSet_of_isOpen : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α] {s : Set α},
  IsOpen s → IsUpperSet s
-- Mathlib.Data.Nat.Factors
Nat.Prime.primeFactorsList_pow : ∀ {p : ℕ}, Nat.Prime p → ∀ (n : ℕ), (p ^ n).primeFactorsList = List.replicate n p
-- Mathlib.Order.Bounds.Image
bddBelow_pi : ∀ {α : Type u} {π : α → Type u_1} [inst : (a : α) → Preorder (π a)] {s : Set ((a : α) → π a)},
  BddBelow s ↔ ∀ (a : α), BddBelow (Function.eval a '' s)
-- Mathlib.Algebra.Algebra.Equiv
/-- See also `Finite.algHom`  -/
Finite.algEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] [Finite (A₁ →ₐ[R] A₂)], Finite (A₁ ≃ₐ[R] A₂)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.rw : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {combined : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig combined → ℕ
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Construct a cone for a right Kan extension `F' : D ⥤ H` of `F : C ⥤ H` along a functor
`L : C ⥤ D` given a cone for `F`.  -/
CategoryTheory.Functor.coneOfIsRightKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : L.comp F' ⟶ F) →
                    [F'.IsRightKanExtension α] → CategoryTheory.Limits.Cone F → CategoryTheory.Limits.Cone F'
-- Mathlib.Algebra.Group.Even
Even.sub : ∀ {α : Type u_2} [inst : SubtractionCommMonoid α] {a b : α}, Even a → Even b → Even (a - b)
-- Batteries.Data.ByteArray
ByteArray.ofFn_zero : ∀ (f : Fin 0 → UInt8), ByteArray.ofFn f = ByteArray.empty
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.ae_toFinite : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ],
  MeasureTheory.ae μ.toFinite = MeasureTheory.ae μ
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coe_mk : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph Z (B × F)) (i : Set B) (j : IsOpen i)
  (k : e.source = proj ⁻¹' i) (l : e.target = i ×ˢ Set.univ) (m : ∀ p ∈ e.source, (↑e p).1 = proj p) (x : Z),
  ↑{ toOpenPartialHomeomorph := e, baseSet := i, open_baseSet := j, source_eq := k, target_eq := l, proj_toFun := m }
      x =
    ↑e x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_pos_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddLeftStrictMono α] (a : α) {b : α}, 0 < b → a < a + b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.comp_nsmul_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X) {Z : C} (h_1 : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp (n • f) h_1) =
    CategoryTheory.CategoryStruct.comp (n • CategoryTheory.CategoryStruct.comp h f) h_1
-- Mathlib.Dynamics.Ergodic.Conservative
MeasureTheory.Conservative.toQuasiMeasurePreserving : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ → MeasureTheory.Measure.QuasiMeasurePreserving f μ μ
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instAddMonoid : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddMonoid β] → [ContinuousAdd β] → AddMonoid (ZeroAtInftyContinuousMap α β)
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight₁_nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K), 0 ≤ Height.mulHeight₁ x