mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_sInf_l_image : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) (s : Set β), u (sInf (l '' s)) = sInf s
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.abelian_derivedAbelianOfIdeal : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  IsLieAbelian ↥(LieAlgebra.derivedAbelianOfIdeal I)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- Given a cocone `c` on a filtered diagram `F` which `IsEventuallyConstantFrom i₀`, such that
`c.π.app i₀` is an isomorphism, `c` a colimit cocone.  -/
CategoryTheory.Functor.IsEventuallyConstantFrom.isColimitOfIsIso : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} →
            F.IsEventuallyConstantFrom i₀ →
              [CategoryTheory.IsFiltered J] →
                (c : CategoryTheory.Limits.Cocone F) →
                  [CategoryTheory.IsIso (c.ι.app i₀)] → CategoryTheory.Limits.IsColimit c
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- commutation with `π`  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.commπ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) {Z : C} (h : h₂.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.CategoryStruct.comp self.φH h) =
    CategoryTheory.CategoryStruct.comp self.φK (CategoryTheory.CategoryStruct.comp h₂.π h)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_rpow_of_exponent_le : ∀ {x y z : ℝ}, 1 ≤ x → y ≤ z → x ^ y ≤ x ^ z
-- Mathlib.Topology.VectorBundle.Basic
VectorBundle.continuousOn_coordChange' : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} {inst : NontriviallyNormedField R}
  {inst_1 : (x : B) → AddCommMonoid (E x)} {inst_2 : (x : B) → Module R (E x)} {inst_3 : NormedAddCommGroup F}
  {inst_4 : NormedSpace R F} {inst_5 : TopologicalSpace B} {inst_6 : TopologicalSpace (Bundle.TotalSpace F E)}
  {inst_7 : (x : B) → TopologicalSpace (E x)} {inst_8 : FiberBundle F E} [self : VectorBundle R F E]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : MemTrivializationAtlas e]
  [inst_10 : MemTrivializationAtlas e'],
  ContinuousOn (fun b => ↑(Bundle.Trivialization.coordChangeL R e e' b)) (e.baseSet ∩ e'.baseSet)
-- Lean.Meta.HaveTelescope
/-- The expression `expr` in `have x := v; b` form.
 -/
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.exprResult : Lean.Meta.SimpHaveResult✝ → Lean.Expr
-- Mathlib.Order.Interval.Set.OrdConnected
/-- The preimage of an `OrdConnected` set under a map which is monotone on a set `t`,
when intersected with `t`, is `OrdConnected`. More precisely, it is the intersection with `t`
of an `OrdConnected` set.  -/
Set.OrdConnected.preimage_monotoneOn : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : β → α} {t : Set β} {s : Set α},
  s.OrdConnected → MonotoneOn f t → ∃ u, u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u
-- Mathlib.Tactic.NormNum.RealSqrt
Mathlib.Meta.NormNum.isNNRat_nnrealSqrt_of_isNNRat : ∀ {x : NNReal} {n sn d sd : ℕ},
  sn * sn = n → sd * sd = d → Mathlib.Meta.NormNum.IsNNRat x n d → Mathlib.Meta.NormNum.IsNNRat (NNReal.sqrt x) sn sd
-- Lean.EnvExtension
Lean.registerSimplePersistentEnvExtension : {α σ : Type} → [Inhabited σ] → Lean.SimplePersistentEnvExtensionDescr α σ → IO (Lean.SimplePersistentEnvExtension α σ)
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- The finite edge set of `G.deleteIncidenceSet x` is the finite edge set of the simple graph `G`
set difference the finite incidence set of the vertex `x`.  -/
SimpleGraph.edgeFinset_deleteIncidenceSet_eq_sdiff : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (x : V),
  (G.deleteIncidenceSet x).edgeFinset = G.edgeFinset \ G.incidenceFinset x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.condition_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g)
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp t.ι (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp t.ι (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.one_def : ∀ {G : Type u_1} [inst : Add G] {a : G}, 1 = AddConstMap.id
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfLax_toPrelaxFunctor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) (F' : F.PseudoCore),
  (CategoryTheory.Pseudofunctor.mkOfLax F F').toPrelaxFunctor = F.toPrelaxFunctor
-- Mathlib.Order.Hom.WithTopBot
WithTop.toDualBotEquiv_top : ∀ {α : Type u_1} [inst : LE α], WithTop.toDualBotEquiv ⊤ = ⊤
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- If an antitone sequence of functions has a lower bound and the sequence of integrals of these
functions tends to the integral of the lower bound, then the sequence of functions converges
almost everywhere to the lower bound.  -/
MeasureTheory.tendsto_of_integral_tendsto_of_antitone : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} {F : α → ℝ},
  (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
    MeasureTheory.Integrable F μ →
      Filter.Tendsto (fun i => ∫ (a : α), f i a ∂μ) Filter.atTop (nhds (∫ (a : α), F a ∂μ)) →
        (∀ᵐ (a : α) ∂μ, Antitone fun i => f i a) →
          (∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a) →
            ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (F a))
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.Ioi_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ioi ↑a = WithBot.some '' Set.Ioi a
-- Mathlib.Util.Superscript
/-- Formatter for the script parser.  -/
Mathlib.Tactic.Superscript.scriptParser.formatter : String →
  Mathlib.Tactic.Superscript.Mapping → Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Polynomial.GroupRingAction
Polynomial.eval_smul' : ∀ (S : Type u_3) [inst : CommSemiring S] (G : Type u_4) [inst_1 : Group G] [inst_2 : MulSemiringAction G S] (g : G)
  (f : Polynomial S) (x : S), Polynomial.eval (g • x) f = g • Polynomial.eval x (g⁻¹ • f)
-- Init.Prelude
Hashable.mk : {α : Sort u} → (α → UInt64) → Hashable α
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Proves the right to left direction of a generated iff theorem.
 -/
Mathlib.Tactic.MkIff.toInductive : Lean.MVarId → List Lean.Name → List Lean.Expr → List Mathlib.Tactic.MkIff.Shape → Lean.FVarId → Lean.MetaM Unit
-- Init.Data.Int.DivMod.Lemmas
Int.negSucc_emod_ofNat_succ_eq_zero_iff : ∀ {a b : ℕ}, Int.negSucc a % (↑b + 1) = 0 ↔ (a + 1) % (b + 1) = 0
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_compContinuousCLM_le_one : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] {𝕜 : Type u_2}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 β] [inst_4 : SeminormedAddCommGroup γ] (g : C(γ, α)),
  ‖BoundedContinuousFunction.compContinuousCLM β 𝕜 g‖ ≤ 1
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_ofNat' : ∀ (n : ℕ), (UInt64.ofNat n).toUInt8 = UInt8.ofNat n
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
/-- **Alias** of `Matroid.IsBasis.cardinalMk_sdiff_comm`. -/
Matroid.IsBasis.cardinalMk_diff_comm : ∀ {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank],
  M.IsBasis I X → M.IsBasis J X → Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)
-- Init.Data.ToString.Basic
instToStringChar : ToString Char
-- Mathlib.Topology.NhdsWithin
eventually_mem_of_tendsto_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : β → α} {a : α} {s : Set α} {l : Filter β},
  Filter.Tendsto f l (nhdsWithin a s) → ∀ᶠ (i : β) in l, f i ∈ s
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.kernelCone.eq_1 : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f : M ⟶ N),
  ModuleCat.kernelCone f = CategoryTheory.Limits.KernelFork.ofι (ModuleCat.ofHom (ModuleCat.Hom.hom f).ker.subtype) ⋯
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.TZSpec.zoneId.injEq : ∀ (id id_1 : String),
  (Std.Time.Database.TZdb.TZSpec.zoneId id = Std.Time.Database.TZdb.TZSpec.zoneId id_1) = (id = id_1)
-- Std.Do.SPred.Laws
Std.Do.SPred.or_intro_r : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, Q ⊢ₛ P ∨ Q
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_mul : ∀ (m n : ℕ), ↑(m * n) = ↑m * ↑n
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` preserves limits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimits F],
  CategoryTheory.Limits.PreservesColimits F.op
-- Batteries.Data.Fin.Coding
Fin.getRepr_eq_getRepr_of_equiv : ∀ {n : ℕ} {x y : Fin n} (s : Setoid (Fin n)) [inst : DecidableRel ⇑s], s x y → Fin.getRepr s x = Fin.getRepr s y
-- Mathlib.Algebra.Azumaya.Defs
IsAzumaya.toProjective : ∀ {R : Type u_1} {A : Type u_2} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  [self : IsAzumaya R A], Module.Projective R A
-- Mathlib.Data.Finset.Max
Finset.coe_min' : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} (hs : s.Nonempty), ↑(s.min' hs) = s.min
-- Mathlib.Topology.SmallInductiveDimension
hasSmallInductiveDimensionLT_zero_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X], HasSmallInductiveDimensionLT X 0 ↔ IsEmpty X
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.mk : ∀ {S : Type u_1} {K : Type u_2} [inst : DivisionRing K] [inst_1 : SetLike S K] [toSubringClass : SubringClass S K]
  [toInvMemClass : InvMemClass S K], SubfieldClass S K
-- Mathlib.SetTheory.Cardinal.Order
_private.Mathlib.SetTheory.Cardinal.Order.0.Cardinal.cast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
-- Mathlib.CategoryTheory.Monad.Equalizer
/-- Construct the Beck fork in the category of coalgebras. This fork is coreflexive as well as an
equalizer.
 -/
CategoryTheory.Comonad.beckCoalgebraFork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} →
      (X : T.Coalgebra) →
        CategoryTheory.Limits.Fork (CategoryTheory.Comonad.CofreeEqualizer.topMap X)
          (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)
-- Mathlib.RepresentationTheory.Invariants
/-- The invariants of the representation `linHom X.ρ Y.ρ` correspond to the representation
homomorphisms from `X` to `Y`.  -/
Representation.linHom.invariantsEquivRepHom : {k : Type u} →
  [inst : CommRing k] →
    {G : Type v} → [inst_1 : Group G] → (X Y : Rep.{w, u, v} k G) → ↥(X.ρ.linHom Y.ρ).invariants ≃ₗ[k] X ⟶ Y
-- Mathlib.Analysis.Convex.Function
convexOn_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E} (c : β),
  Convex 𝕜 s → ConvexOn 𝕜 s fun x => c
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_nhds_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {s : Set α}, s ∈ nhds x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s
-- Lean.Expr
/-- Given `a b : Nat`, returns `a + b`  -/
Lean.mkNatAdd : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- A linear surjection between modules with the module topology is a quotient map.
Equivalently, the pushforward of the module topology along a surjective linear map is
again the module topology.  -/
IsModuleTopology.isQuotientMap_of_surjective : ∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Ring R] {A : Type u_3} [inst_1 : AddCommGroup A]
  [inst_2 : Module R A] [inst_3 : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_4} [inst_5 : AddCommGroup B]
  [inst_6 : Module R B] [τB : TopologicalSpace B] [IsModuleTopology R B] {φ : A →ₗ[R] B},
  Function.Surjective ⇑φ → Topology.IsQuotientMap ⇑φ
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.MonoidalCategory.inducingFunctorData_εIso : ∀ (R : Type u) [inst : CommRing R],
  (CoalgCat.MonoidalCategory.inducingFunctorData R).εIso =
    CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))
-- Init.Data.Array.MinMax
/-- Returns the smallest element of a non-empty array.

Examples:
* `#[4].min (by decide) = 4`
* `#[1, 4, 2, 10, 6].min (by decide) = 1`
 -/
Array.min : {α : Type u_1} → [Min α] → (arr : Array α) → arr ≠ #[] → α
-- Mathlib.LinearAlgebra.BilinearMap
/-- Scalar multiplication as a bilinear map `R → M → M`.  -/
LinearMap.lsmul : (R : Type u_2) →
  [inst : CommSemiring R] → (M : Type u_5) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → R →ₗ[R] M →ₗ[R] M
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- If `S` is `R`-flat, `S ⊗[R] eq(f, g)` is isomorphic to `eq(𝟙 ⊗[R] f, 𝟙 ⊗[R] g)`.  -/
CommRingCat.Under.equalizerForkTensorProdIso : {R S : CommRingCat} →
  [inst : Algebra ↑R ↑S] →
    [Module.Flat ↑R ↑S] →
      {A B : CategoryTheory.Under R} →
        (f g : A ⟶ B) →
          CommRingCat.Under.tensorProdEqualizer f g ≅
            CommRingCat.Under.equalizerFork' (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom f))
              (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom g))
-- Mathlib.MeasureTheory.Integral.Prod
/-- Integrals commute with subtraction inside another integral.
`F` can be any measurable function.  -/
MeasureTheory.integral_fn_integral_sub : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {E' : Type u_4} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace ℝ E'] ⦃f g : α × β → E⦄ (F : E → E'),
  MeasureTheory.Integrable f (μ.prod ν) →
    MeasureTheory.Integrable g (μ.prod ν) →
      ∫ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
        ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ
-- Batteries.Data.List.Basic
/-- `go : List α → Array (List α) → Array (List α)` inserts one list into the accumulated
list of sections `acc`: `go [a, b] #[l₁, l₂] = [a::l₁, b::l₁, a::l₂, b::l₂]`.  -/
List.sectionsTR.go : {α : Type u_1} → List α → Array (List α) → Array (List α)
-- Mathlib.Order.PropInstances
Prop.decidableRelTop : {α : Type u} → DecidableRel ⊤
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.pred.eq_1 : Turing.ToPartrec.Code.pred = Turing.ToPartrec.Code.zero.case Turing.ToPartrec.Code.head
-- Mathlib.RingTheory.HahnSeries.PowerSeries
/-- Casting a power series as a Hahn series with coefficients from a strictly ordered semiring.  -/
HahnSeries.ofPowerSeriesAlg : (Γ : Type u_1) →
  (R : Type u_2) →
    [inst : CommSemiring R] →
      {A : Type u_3} →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring Γ] →
              [inst_4 : PartialOrder Γ] → [inst_5 : IsStrictOrderedRing Γ] → PowerSeries A →ₐ[R] HahnSeries Γ A
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `map₂` of the identity is the identity.  -/
CategoryTheory.CostructuredArrow.map₂IdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor C D} →
          (α : (CategoryTheory.Functor.id C).comp S ⟶ S.comp (CategoryTheory.Functor.id D)) →
            (T : D) →
              (β : (CategoryTheory.Functor.id D).obj T ⟶ T) →
                autoParam (α = CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv)
                    CategoryTheory.CostructuredArrow.map₂IdIso._auto_1 →
                  autoParam (β = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T))
                      CategoryTheory.CostructuredArrow.map₂IdIso._auto_3 →
                    (CategoryTheory.CostructuredArrow.map₂ α β ≅
                      CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow S T))
-- Mathlib.Order.SupIndep
/-- **Alias** of the reverse direction of `Finset.supIndep_attach`. -/
Finset.SupIndep.attach : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  s.SupIndep f → s.attach.SupIndep fun a => f ↑a
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The canonical isomorphism `(homotopyCofiber φ).X i ≅ G.X i` when `¬ c.Rel i (c.next i)`.  -/
HomologicalComplex.homotopyCofiber.XIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  (i : ι) → ¬c.Rel i (c.next i) → (HomologicalComplex.homotopyCofiber.X φ i ≅ G.X i)
-- Mathlib.Analysis.InnerProductSpace.l2Space
lp.summable_inner : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {G : ι → Type u_4} [inst_1 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_2 : (i : ι) → InnerProductSpace 𝕜 (G i)] (f g : ↥(lp G 2)), Summable fun i => inner 𝕜 (↑f i) (↑g i)
-- Init.Data.ByteArray.Lemmas
ByteArray.copySlice_eq_append : ∀ {src : ByteArray} {srcOff : ℕ} {dest : ByteArray} {destOff len : ℕ} {exact : Bool},
  src.copySlice srcOff dest destOff len exact =
    dest.extract 0 destOff ++ src.extract srcOff (srcOff + len) ++
      dest.extract (destOff + min len (src.data.size - srcOff)) dest.data.size
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.mk.injEq : ∀ {α : Type u} {β : Type v} (inner inner_1 : Std.DHashMap.Raw α fun x => β),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Data.Finset.Image
Finset.image_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] (f : α → β) (a : α) (s : Finset α),
  Finset.image f (insert a s) = insert (f a) (Finset.image f s)
-- Mathlib.Topology.EMetricSpace.Defs
uniformity_basis_edist_inv_two_pow : ∀ {α : Type u} [inst : PseudoEMetricSpace α],
  (uniformity α).HasBasis (fun x => True) fun n => {p | edist p.1 p.2 < 2⁻¹ ^ n}
-- Init.Data.Option.Lemmas
Option.isSome_of_isSome_pbind : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β},
  (o.pbind f).isSome = true → o.isSome = true
-- Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
CategoryTheory.Functor.eqvGen_colimitTypeRel_iff_of_isFiltered : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J (Type w₀)) (x y : (j : J) × F.obj j),
  Relation.EqvGen F.ColimitTypeRel x y ↔
    ∃ k f g,
      (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSet.measure_inter_eq_mul : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {s t : Set Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.IndepSet s t μ → μ (s ∩ t) = μ s * μ t
-- Mathlib.CategoryTheory.CatCommSq
/-- Vertical composition of 2-commutative squares  -/
CategoryTheory.CatCommSq.vComp : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₅ : Type u_5} →
          {C₆ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} C₅] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} C₆] →
                        (L₁ : CategoryTheory.Functor C₁ C₂) →
                          (L₂ : CategoryTheory.Functor C₂ C₃) →
                            (H₁ : CategoryTheory.Functor C₁ C₄) →
                              (H₂ : CategoryTheory.Functor C₂ C₅) →
                                (H₃ : CategoryTheory.Functor C₃ C₆) →
                                  (R₁ : CategoryTheory.Functor C₄ C₅) →
                                    (R₂ : CategoryTheory.Functor C₅ C₆) →
                                      [CategoryTheory.CatCommSq H₁ L₁ R₁ H₂] →
                                        [CategoryTheory.CatCommSq H₂ L₂ R₂ H₃] →
                                          CategoryTheory.CatCommSq H₁ (L₁.comp L₂) (R₁.comp R₂) H₃
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.pushforwardEq.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} {f g : X ⟶ Y} (h : f = g)
  (ℱ : TopCat.Presheaf C X),
  TopCat.Presheaf.pushforwardEq h ℱ =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.NatIso.op (TopologicalSpace.Opens.mapIso f g h).symm) ℱ
-- Mathlib.Topology.Inseparable
inseparable_prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₁ x₂ : X} {y₁ y₂ : Y},
  Inseparable (x₁, y₁) (x₂, y₂) ↔ Inseparable x₁ x₂ ∧ Inseparable y₁ y₂
-- Mathlib.Order.Bounded
Set.unbounded_lt_iff : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Set.Unbounded (fun x1 x2 => x1 < x2) s ↔ ∀ (a : α), ∃ b ∈ s, a ≤ b
-- Mathlib.Computability.TuringMachine.Computable
/-- **Alias** of `StateTransition.EvalsTo`. -/
Turing.EvalsTo : {σ : Type u_1} → (σ → Option σ) → σ → Option σ → Type
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsRat.to_isInt : ∀ {α : Type u_1} [inst : Ring α] {a : α} {n : ℤ}, Mathlib.Meta.NormNum.IsRat a n 1 → Mathlib.Meta.NormNum.IsInt a n
-- Mathlib.Topology.Defs.Filter
/-- In a noncompact space, `Set.univ` is not a compact set.  -/
NoncompactSpace.noncompact_univ : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : NoncompactSpace X], ¬IsCompact Set.univ
-- Init.Data.BitVec.Lemmas
BitVec.smtUDiv.eq_1 : ∀ {n : ℕ} (x y : BitVec n), x.smtUDiv y = if y = 0 then BitVec.allOnes n else x.udiv y
-- Mathlib.Combinatorics.Digraph.Basic
instFintypeDigraphOfDecidableEq : {V : Type u_1} → [DecidableEq V] → [Fintype V] → Fintype (Digraph V)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.instMulActionProjGenLinGroupFinOfNatNatReal : MulAction (Matrix.ProjGenLinGroup (Fin 2) ℝ) UpperHalfPlane
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Convert the heap to a list in increasing order.  -/
Batteries.BinomialHeap.toList : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → List α
-- Mathlib.Data.Sum.Interval
Sum.Ici_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : LocallyFiniteOrderTop β] (b : β), Finset.Ici (Sum.inr b) = Finset.map Function.Embedding.inr (Finset.Ici b)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_natCast : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (n : ℕ), WithVal.toVal v ↑n = ↑n
-- Init.Data.Option.Attach
Option.isSome_attachWith : ∀ {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), o = some a → p a), (o.attachWith p H).isSome = o.isSome
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instHasSizeNat : Std.Rxc.HasSize ℕ
-- Mathlib.FieldTheory.Galois.Basic
/-- Let $E / K / F$ be a tower of field extensions.
If $E$ is Galois over $F$, then $E$ is Galois over $K$.  -/
IsGalois.tower_top_of_isGalois : ∀ (F : Type u_1) (K : Type u_2) (E : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field E]
  [inst_3 : Algebra F K] [inst_4 : Algebra F E] [inst_5 : Algebra K E] [IsScalarTower F K E] [IsGalois F E],
  IsGalois K E