mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.linearIndependent_rows_iff_isUnit : ∀ {m : Type u} [inst : DecidableEq m] {K : Type u_3} [inst_1 : Field K] [inst_2 : Fintype m] {A : Matrix m m K},
  LinearIndependent K A.row ↔ IsUnit A
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsOrthogonal.coreflection_apply_right : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι},
  P.IsOrthogonal j i → (P.coreflection j) (P.coroot i) = P.coroot i
-- Mathlib.NumberTheory.FunctionField
/-- `K` is a function field over the field `F` if it is a finite
extension of the field of rational functions in one variable over `F`.

Note that `K` can be a function field over multiple, non-isomorphic, `F`.
 -/
FunctionField : (F : Type u_1) → (K : Type u_2) → [inst : Field F] → [inst_1 : Field K] → [Algebra (RatFunc F) K] → Prop
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_comap_eq_self : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R →+* S} {t : Subsemiring S},
  t ≤ f.rangeS → Subsemiring.map f (Subsemiring.comap f t) = t
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- A projective presentation of an object `X` consists of an epimorphism `f : P ⟶ X`
from some projective object `P`.
 -/
CategoryTheory.ProjectivePresentation : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Type (max u v)
-- Mathlib.LinearAlgebra.Span.TensorProduct
Submodule.finrank_span_eq_finrank_span : ∀ (R : Type u_1) (A : Type u_2) {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [Nontrivial A]
  [inst_3 : Algebra R A] [Algebra.IsEpi R A] [Module.Flat R A] [inst_6 : AddCommGroup M] [inst_7 : Module R M]
  [inst_8 : Module A M] [IsScalarTower R A M] [IsPrincipalIdealRing R] [IsDomain R] [Module.IsTorsionFree R M]
  (s : Set M) [Module.Finite R ↥(Submodule.span R s)],
  Module.finrank A ↥(Submodule.span A s) = Module.finrank R ↥(Submodule.span R s)
-- Mathlib.Order.CompleteLattice.Defs
/-- `(a ⇨ ·)` is right adjoint to `(a ⊓ ·)`  -/
CompleteLinearOrder.le_himp_iff : ∀ {α : Type u_8} [self : CompleteLinearOrder α] (a b c : α), a ≤ b ⇨ c ↔ min a b ≤ c
-- Mathlib.CategoryTheory.Skeletal
/-- A functor `C ⥤ D ⥤ E` computably lowers to a functor
`ThinSkeleton C ⥤ ThinSkeleton D ⥤ ThinSkeleton E`  -/
CategoryTheory.ThinSkeleton.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] →
            CategoryTheory.Functor C (CategoryTheory.Functor D E) →
              CategoryTheory.Functor (CategoryTheory.ThinSkeleton C)
                (CategoryTheory.Functor (CategoryTheory.ThinSkeleton D) (CategoryTheory.ThinSkeleton E))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.add_def : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} (P Q : W.Point), P + Q = P.add Q
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
/-- The Yoneda embedding for preadditive categories sends an object `X` to the copresheaf sending an
object `Y` to the `End X`-module of morphisms `X ⟶ Y`.
 -/
CategoryTheory.preadditiveCoyonedaObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (X : C) → CategoryTheory.Functor C (ModuleCat (CategoryTheory.End X)ᵐᵒᵖ)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- A measure `μ` is called σ-finite if there is a countable collection of sets
`{ A i | i ∈ ℕ }` such that `μ (A i) < ∞` and `⋃ i, A i = s`.  -/
MeasureTheory.SigmaFinite : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Aesop.RuleSet.Filter
/-- `#[]` means 'match any builder'
 -/
Aesop.RuleFilter.builders : Aesop.RuleFilter → Array Aesop.BuilderName
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.image_source_eq_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e '' e.source = e.target
-- Mathlib.Data.Prod.TProd
_private.Mathlib.Data.Prod.TProd.0.Set.tprod.match_1.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} (motive : List ι → ((i : ι) → Set (α i)) → Sort u_3) (x : (i : ι) → Set (α i))
  (h_1 : (x : (i : ι) → Set (α i)) → motive [] x)
  (h_2 : (i : ι) → (is : List ι) → (t : (i : ι) → Set (α i)) → motive (i :: is) t),
  (match [], x with
    | [], x => h_1 x
    | i :: is, t => h_2 i is t) =
    h_1 x
-- Mathlib.Topology.Algebra.Monoid
/-- If a subsemigroup of a topological semigroup is commutative, then so is its topological
closure.

See note [reducible non-instances]  -/
Subsemigroup.commSemigroupTopologicalClosure : {M : Type u_3} →
  [inst : TopologicalSpace M] →
    [inst_1 : Semigroup M] →
      [inst_2 : SeparatelyContinuousMul M] →
        [T2Space M] → (s : Subsemigroup M) → (∀ (x y : ↥s), x * y = y * x) → CommSemigroup ↥s.topologicalClosure
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.connected_or_preconnected_compl : ∀ {V : Type u} (G : SimpleGraph V), G.Connected ∨ Gᶜ.Preconnected
-- Init.Data.UInt.Lemmas
USize.toUInt16_toUInt32 : ∀ (n : USize), n.toUInt32.toUInt16 = n.toUInt16
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
/-- Given a `ContDiff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible
derivative at `a`, returns an `OpenPartialHomeomorph` with `to_fun = f` and `a ∈ source`.  -/
ContDiffAt.toOpenPartialHomeomorph : {𝕂 : Type u_1} →
  [inst : RCLike 𝕂] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕂 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕂 F] →
                [CompleteSpace E] →
                  (f : E → F) →
                    {f' : E ≃L[𝕂] F} →
                      {a : E} →
                        {n : WithTop ℕ∞} →
                          ContDiffAt 𝕂 n f a → HasFDerivAt f (↑f') a → n ≠ 0 → OpenPartialHomeomorph E F
-- Mathlib.GroupTheory.GroupAction.Pointwise
Group.preimage_smul_set : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} {β : Type u_3} [inst_1 : MulAction G α] [inst_2 : MulAction G β]
  {F : Type u_4} [inst_3 : FunLike F α β] [MulActionHomClass F G α β] (f : F) (c : G) (t : Set β),
  ⇑f ⁻¹' (c • t) = c • ⇑f ⁻¹' t
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Std.Iterators.Vector.isPlausibleStep_iterM_of_not_pos : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} {xs : Vector β n},
  ¬0 < n → (xs.iterM m).IsPlausibleStep Std.IterStep.done
-- Init.Data.String.Defs
String.Pos.ext : ∀ {s : String} {x y : s.Pos}, x.offset = y.offset → x = y
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_mem_mul : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R} {m n : R}, m ∈ M → n ∈ N → m * n ∈ M * N
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.mem_cardSuppLTAddSubmonoid : ∀ {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [inst : PartialOrder Γ] [inst_1 : AddMonoid R]
  [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R}, x ∈ HahnSeries.cardSuppLTAddSubmonoid Γ R κ ↔ x.cardSupp < κ
-- Init.Data.Int.Lemmas
Int.sub_zero : ∀ (a : ℤ), a - 0 = a
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.setTag.injEq : ∀ (x : Lean.IR.VarId) (cidx : ℕ) (b : Lean.IR.FnBody) (x_1 : Lean.IR.VarId) (cidx_1 : ℕ) (b_1 : Lean.IR.FnBody),
  (Lean.IR.FnBody.setTag x cidx b = Lean.IR.FnBody.setTag x_1 cidx_1 b_1) = (x = x_1 ∧ cidx = cidx_1 ∧ b = b_1)
-- Lean.Data.PrefixTree
_private.Lean.Data.PrefixTree.0.Lean.PrefixTreeNode.foldMatchingM.fold : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_4} →
      {σ : Type u_1} → [Monad m] → (cmp : α → α → Ordering) → (β → σ → m σ) → Lean.PrefixTreeNode α β cmp → σ → m σ
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_uIcc_castSucc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc ⁻¹' Set.uIcc i.castSucc j.castSucc = Set.uIcc i j
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.isoMk_symm : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}
  (φ : (CategoryTheory.forget₂ (ModuleCat R) Ab).obj M ≅ (CategoryTheory.forget₂ (ModuleCat R) Ab).obj N)
  (hφ :
    ∀ (r : R),
      CategoryTheory.CategoryStruct.comp φ.hom (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ.hom),
  (ModuleCat.isoMk φ hφ).symm = ModuleCat.isoMk φ.symm ⋯
-- Mathlib.Order.SuccPred.Basic
/-- Proof of interaction between `pred` and minimal element  -/
PredOrder.min_of_le_pred : ∀ {α : Type u_3} {inst : Preorder α} [self : PredOrder α] {a : α}, a ≤ PredOrder.pred a → IsMin a
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rco_ne_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m...n).toList[i]! ≠ 0 ↔ i < (n - m).toNat ∧ m + ↑i ≠ 0
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.isIso_toLRSHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.toLRSHom f)
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lcs_le_self : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ) (N : LieSubmodule R L M),
  LieSubmodule.lcs k N ≤ N
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- the underlying type of an object in `SemimoduleCat R`  -/
SemimoduleCat.carrier : {R : Type u} → [inst : Semiring R] → SemimoduleCat R → Type v
-- Mathlib.Data.Set.Order
AntitoneOn.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α} {s : Set β},
  AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => f x ∩ g x) s
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.integral_truncation_le_integral_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → 0 ≤ f → ∀ {A : ℝ}, ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ ≤ ∫ (x : α), f x ∂μ
-- Mathlib.Data.Pi.Interval
Pi.card_Iio : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrderBot (α i)] (b : (i : ι) → α i),
  (Finset.Iio b).card = ∏ i, (Finset.Iic (b i)).card - 1
-- Mathlib.Data.Option.Defs
Option.iget_some : ∀ {α : Type u_1} [inst : Inhabited α] {a : α}, (some a).iget = a
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeMonoid.symbols_mul : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : FreeMonoid α}, (a * b).symbols = a.symbols ∪ b.symbols
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H2π_comp_map_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : groupCohomology B 2 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.H2π A)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.map f φ 2) h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₂ f φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H2π B) h)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.getElem?_toArray_eq : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {i : ℕ},
  r.toArray[i]? =
    Option.filter (fun x => decide (x ≤ r.upper)) (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least)
-- Lean.Elab.DeclModifiers
Lean.Elab.RecKind.nonrec : Lean.Elab.RecKind
-- Init.Data.String.Iterate
/-- Creates an iterator over all bytes in `s`.

Examples:

* `"abc".byteIterator.toList = [97, 98, 99]`

* `"ab∀c".byteIterator.toList = [97, 98, 226, 136, 128, 99]`
 -/
String.byteIterator : String → Std.Iter UInt8
-- Aesop.RuleSet
Aesop.LocalRuleSet.modifyBaseM : {m : Type → Type u_1} →
  [Monad m] → (Aesop.BaseRuleSet → m Aesop.BaseRuleSet) → Aesop.LocalRuleSet → m Aesop.LocalRuleSet
-- Mathlib.Logic.Relation
Relation.map_apply_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ},
  Function.Injective f →
    Function.Injective g → ∀ (r : α → β → Prop) (a : α) (b : β), Relation.Map r f g (f a) (g b) ↔ r a b
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_apply : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ)
  (x_1 : (SSet.stdSimplex.obj { len := c.dim + 1 }).obj x),
  (CategoryTheory.ConcreteCategory.hom ((f.b j).app x))
      ((CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app x)) x_1) =
    (CategoryTheory.ConcreteCategory.hom (c.mapToSucc.app x)) x_1
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.center_eq_top : ∀ (R : Type u_1) [inst : NonUnitalCommRing R], NonUnitalSubring.center R = ⊤
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instRxiHasSize.eq_1 : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β]
  [inst_8 : Std.Rxi.HasSize β],
  HasModel.instRxiHasSize✝ = { size := fun lo => Std.Rxi.HasSize.size (HasModel.encode✝ lo) }
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_g : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_3),
  (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g =
    X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.boundaries₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.boundaries₁ A = (ModuleCat.Hom.hom (groupHomology.d₂₁ A)).range
-- Init.Data.String.Lemmas.TakeDrop
String.toList_copy_drop : ∀ {s : String} {n : ℕ}, (s.drop n).copy.toList = List.drop n s.toList
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.aestronglyMeasurable_trim_condExpKernel : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  (hm : m ≤ mΩ) (hf : MeasureTheory.AEStronglyMeasurable f μ),
  ∀ᵐ (ω : Ω) ∂μ.trim hm, f =ᵐ[(ProbabilityTheory.condExpKernel μ m) ω] MeasureTheory.AEStronglyMeasurable.mk f hf
-- Init.Data.Array.Basic
Array.set.congr_simp : ∀ {α : Type u_1} (xs xs_1 : Array α) (e_xs : xs = xs_1) (i i_1 : ℕ) (e_i : i = i_1) (v v_1 : α),
  v = v_1 → ∀ (h : i < xs.size), xs.set i v h = xs_1.set i_1 v_1 ⋯
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.P_corec : ∀ {F : PFunctor.{uA, uB}} {X : Type w} (f : X → ↑F X) (i : X) (n : ℕ),
  PFunctor.Approx.Agree (PFunctor.Approx.sCorec f i n) (PFunctor.Approx.sCorec f i n.succ)
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.liftHomotopy.congr_simp : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p p_1 : E → X} (e_p : p = p_1) (cov : IsCoveringMap p)
  (H H_1 : C(↑unitInterval × A, X)) (e_H : H = H_1) (f f_1 : C(A, E)) (e_f : f = f_1)
  (H_0 : ∀ (a : A), H (0, a) = p (f a)), cov.liftHomotopy H f H_0 = ⋯.liftHomotopy H_1 f_1 ⋯
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.insertListₘ.eq_2 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  (hd : α × β) (tl : List (α × β)),
  Std.DHashMap.Internal.Raw₀.Const.insertListₘ m (hd :: tl) =
    Std.DHashMap.Internal.Raw₀.Const.insertListₘ (m.insert hd.1 hd.2) tl
-- Mathlib.Order.Minimal
/-- **Alias** of the reverse direction of `maximal_toDual`. -/
Maximal.dual : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α],
  Minimal P x → Maximal (fun x => P (OrderDual.ofDual x)) (OrderDual.toDual x)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C}
  (h : V₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst
            (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
            (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
          h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) h
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.append.injEq : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j k l : ι} (_w₁ : Monoid.CoprodI.NeWord M i j)
  (_hne : j ≠ k) (_w₂ : Monoid.CoprodI.NeWord M k l) (j_1 k_1 : ι) (_w₁_1 : Monoid.CoprodI.NeWord M i j_1)
  (_hne_1 : j_1 ≠ k_1) (_w₂_1 : Monoid.CoprodI.NeWord M k_1 l),
  (_w₁.append _hne _w₂ = _w₁_1.append _hne_1 _w₂_1) = (j = j_1 ∧ k = k_1 ∧ _w₁ ≍ _w₁_1 ∧ _w₂ ≍ _w₂_1)
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ioo (f n) (f (Order.pred n))` are pairwise disjoint.  -/
Antitone.pairwise_disjoint_on_Ioo_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Function.onFun Disjoint fun n => Set.Ioo (f n) (f (Order.pred n)))
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_sdiff : ∀ {α : Type u} {s t : Set α} [inst : DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s \ t).Finite),
  h.toFinset = hs.toFinset \ ht.toFinset
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.comp_id_right : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (l : M →ₗ[R] M), B.comp l LinearMap.id = B.compLeft l
-- Mathlib.Topology.Constructions
/-- **Alias** of `Pi.induced_domRestrict`. -/
Pi.induced_restrict : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] (S : Set ι),
  TopologicalSpace.induced S.domRestrict Pi.topologicalSpace = ⨅ i ∈ S, TopologicalSpace.induced (Function.eval i) (T i)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℂ.eq_1 : ∀ (s : ℂ), s.Gammaℂ = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Empty multiseries approximates (eventually) zero function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ},
  f =ᶠ[Filter.atTop] 0 →
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
        f).Approximates
-- Std.Data.Internal.List.Associative
Std.Internal.List.min?_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [Std.LawfulEqOrd α] [inst_3 : LE α]
  [Std.LawfulOrderOrd α] [inst_5 : Min α] [Std.LawfulOrderLeftLeaningMin α] (l : List ((a : α) × β a)),
  (Std.Internal.List.keys l).min? = Std.Internal.List.minKey? l
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.instEffectiveEpiFamilyOfIsIsoDesc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} (X : α → C)
  (π : (a : α) → X a ⟶ B) [inst_1 : CategoryTheory.Limits.HasCoproduct X]
  [CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)], CategoryTheory.EffectiveEpiFamily X π
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Opens.complOrderIso_symm_apply : ∀ (α : Type u_2) [inst : TopologicalSpace α] (a : (TopologicalSpace.Closeds α)ᵒᵈ),
  (RelIso.symm (TopologicalSpace.Opens.complOrderIso α)) a = (TopologicalSpace.Closeds.compl ∘ ⇑OrderDual.ofDual) a
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.ne_of_isReal_isComplex : ∀ {K : Type u_1} [inst : Field K] {w w' : NumberField.InfinitePlace K}, w.IsReal → w'.IsComplex → w ≠ w'
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioc_inr_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (b₁ b₂ : β),
  Finset.Ioc (Sum.inrₗ b₁) (Sum.inrₗ b₂) =
    Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioc b₁ b₂)
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.mk.sizeOf_spec : ∀ (α : Type u) [isUniformSpace : UniformSpace α] [isCompleteSpace : CompleteSpace α] [isT0 : T0Space α],
  sizeOf { α := α, isUniformSpace := isUniformSpace, isCompleteSpace := isCompleteSpace, isT0 := isT0 } =
    1 + sizeOf α + sizeOf isUniformSpace + sizeOf isCompleteSpace + sizeOf isT0
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function has a power series within a set on a ball, then so does its derivative.  -/
HasFPowerSeriesWithinOnBall.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F],
  HasFPowerSeriesWithinOnBall f p s x r →
    UniqueDiffOn 𝕜 (insert x s) → HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r
-- Mathlib.Data.FP.Basic
FP.prec : [C : FP.FloatCfg] → ℕ
-- Mathlib.Data.Finset.Sort
Finset.sort_empty : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r]
  [inst_3 : Std.Total r], ∅.sort r = []
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.isValue.injEq : ∀ (bvarIdx : ℕ) (strict : Bool) (bvarIdx_1 : ℕ) (strict_1 : Bool),
  (Lean.Meta.Grind.EMatchTheoremConstraint.isValue bvarIdx strict =
      Lean.Meta.Grind.EMatchTheoremConstraint.isValue bvarIdx_1 strict_1) =
    (bvarIdx = bvarIdx_1 ∧ strict = strict_1)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.nsmul.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.nsmul = { smul := fun n a => ⟨n • ↑a, ⋯⟩ }