mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinderHom_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  (p : (CategoryTheory.PreOneHypercover.cylinder f g).I₀),
  (CategoryTheory.PreOneHypercover.cylinderHom f g).s₀ p = p.fst
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.flipFunctor_map_app_app : ∀ (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]
  {F₁ F₂ : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C),
  (((CategoryTheory.flipFunctor C D E).map φ).app Y).app X = (φ.app X).app Y
-- Mathlib.Dynamics.Flow
/-- A flow on a topological space `α` by an additive topological
monoid `τ` is a continuous monoid action of `τ` on `α`.  -/
Flow : (τ : Type u_1) → (α : Type u_2) → [TopologicalSpace τ] → [TopologicalSpace α] → [AddZero τ] → Type (max u_1 u_2)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coeNat_ofPrime : ∀ (p : Nat.Primes), (PrimeMultiset.ofPrime p).toNatMultiset = {↑p}
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.vadd_closedEBall : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal), c +ᵥ Metric.closedEBall x r = Metric.closedEBall (c +ᵥ x) r
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- A module has dimension 1 iff there is some nonzero `v : V` so every vector is a multiple of `v`.
 -/
finrank_eq_one_iff' : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V], Module.finrank K V = 1 ↔ ∃ v, v ≠ 0 ∧ ∀ (w : V), ∃ c, c • v = w
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_lift_iff : ∀ (X : Type v) (κ : Cardinal.{w}), HasCardinalLT X (Cardinal.lift.{u, w} κ) ↔ HasCardinalLT X κ
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- A more general version of `multipliable_congr`, allowing the functions to
disagree on a finite set.  -/
multipliable_congr_cofinite : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α},
  f =ᶠ[Filter.cofinite] g → (Multipliable f ↔ Multipliable g)
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : DecidablePred fun x => x = 0] (m : G₀ˣ) (n : H₀ˣ),
  (MonoidWithZeroHom.inl G₀ H₀) ↑m * (MonoidWithZeroHom.inr G₀ H₀) ↑n = ↑(m, n)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_sInter : ∀ {x : ZFSet.{u}}, x.Nonempty → ↑x.sInter = ⋂₀ (SetLike.coe '' ↑x)
-- Init.Data.Nat.Gcd
/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`.  -/
Nat.dvdProdDvdOfDvdProd : {k m n : ℕ} → k ∣ m * n → { d // k = ↑d.1 * ↑d.2 }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_image_preimage_expMapBasis : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (s : Set (NumberField.mixedEmbedding.realSpace K)),
  NumberField.mixedEmbedding.normAtAllPlaces ''
      NumberField.mixedEmbedding.normAtAllPlaces ⁻¹' ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis '' s =
    ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis '' s
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
continuous_nndist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α], Continuous fun p => nndist p.1 p.2
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.toEnd_apply : ∀ {R : Type u_1} {A : Type u_6} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] {𝒜 : ι → Submodule R A} [inst_5 : GradedAlgebra 𝒜]
  (self : 𝒜 →ₐᵍ[R] 𝒜), GradedAlgHom.toEnd self = ↑self
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_uInt8ToBitVec : ∀ (n : UInt8), { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64
-- Mathlib.Data.Nat.GCD.BigOperators
Nat.coprime_multiset_prod_right_iff : ∀ {k : ℕ} {m : Multiset ℕ}, k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n
-- Mathlib.RingTheory.Valuation.Integers
Valuation.integer.v_irreducible_pos : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {ϖ : ↥v.integer}, Irreducible ϖ → 0 < v ↑ϖ
-- Mathlib.Data.Int.Range
Int.decidableLTLT : (P : ℤ → Prop) → [DecidablePred P] → (m n : ℤ) → Decidable (∀ (r : ℤ), m < r → r < n → P r)
-- Mathlib.Order.KonigLemma
/-- **Kőnig's infinity lemma** : if each element in a strongly atomic order
is covered by only finitely many others, and `b` is an element with infinitely many things above it,
then there is a sequence starting with `b` in which each element is covered by the next.  -/
exists_seq_covby_of_forall_covby_finite : ∀ {α : Type u_1} [inst : PartialOrder α] [IsStronglyAtomic α] {b : α},
  (∀ (a : α), {x | a ⋖ x}.Finite) → (Set.Ici b).Infinite → ∃ f, f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)
-- Mathlib.Algebra.Module.Submodule.Range
/-- If `p ⊆ M` is a submodule, the ordering of submodules of `p` is embedded in the ordering of
submodules of `M`.  -/
Submodule.MapSubtype.orderEmbedding : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (p : Submodule R M) → Submodule R ↥p ↪o Submodule R M
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_lt : ∀ {a b : UInt32}, a.toUInt16 < b.toUInt16 ↔ a % 65536 < b % 65536
-- Mathlib.Topology.Bornology.Absorbs
/-- The filter of sets that absorb `u`.  -/
Filter.absorbing : (G₀ : Type u_1) → {α : Type u_2} → [inst : GroupWithZero G₀] → [Bornology G₀] → [MulAction G₀ α] → Set α → Filter α
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_injOn : Set.InjOn Real.artanh (Set.Ioo (-1) 1)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getLT!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getLT! k = t₂.getLT! k
-- Mathlib.Analysis.SumIntegralComparisons
/-- Converse to the integral test: a nonnegative, integrable, summable function is integrable.  -/
AntitoneOn.integrableOn_Ioi_zero_of_summable : ∀ {f : ℝ → ℝ},
  AntitoneOn f (Set.Ici 0) →
    (Summable fun n => f ↑n) →
      (∀ t ∈ Set.Ioi 0, 0 ≤ f t) → MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.iter_eq_iterFromIdx : ∀ {β : Type w} {n : ℕ} {xs : Vector β n}, xs.iter = xs.iterFromIdx 0
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.subsetSum_nonempty : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M}, A.subsetSum.Nonempty
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.nthRoots_nodup : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
  IsPrimitiveRoot ζ n → ∀ {a : R}, a ≠ 0 → (Polynomial.nthRoots n a).Nodup
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool},
  t.WF → ((Std.TreeSet.Raw.filter f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), f (t.get k h) = true)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.right_continuous : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) (x : R),
  ContinuousWithinAt (↑f) (Set.Ici x) x
-- Mathlib.RingTheory.Flat.Equalizer
Module.Flat.ker_lTensor_eq : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f : N →ₗ[R] P) [Module.Flat R M],
  ((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker =
    ((TensorProduct.AlgebraTensorModule.lTensor S M) f.ker.subtype).range
-- Mathlib.ModelTheory.Syntax
/-- Restricts a term to use only a set of the given variables on the left side of a sum.  -/
FirstOrder.Language.Term.restrictVarLeft : {L : FirstOrder.Language} →
  {α : Type u'} →
    {β : Type v'} →
      [inst : DecidableEq α] → {γ : Type u_2} → (t : L.Term (α ⊕ γ)) → (↥t.varFinsetLeft → β) → L.Term (β ⊕ γ)
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtTreeMap.get : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (a : α) → a ∈ t → β
-- Aesop.Tree.Data
Aesop.MVarClusterUnsafe.brecOn.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} (t : Aesop.MVarClusterUnsafe)
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_2 t (Aesop.MVarClusterUnsafe.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Mathlib.Logic.Basic
Function.Injective.ite : ∀ {α : Sort u_3} {β : Sort u_4} {p : β → Prop} [inst : DecidablePred p] {g : β → α},
  Function.Injective g →
    ∀ {f : β → α},
      Function.Injective f → (∀ (x y : β), g x = f y → x = y) → Function.Injective fun x => if p x then g x else f x
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.mk.sizeOf_spec : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} [inst_2 : SizeOf V] (hom : u.right ⟶ v.left)
  (comm :
    autoParam
      (CategoryTheory.Arrow.Hom.left f - CategoryTheory.Arrow.Hom.left g = CategoryTheory.CategoryStruct.comp u.hom hom)
      CategoryTheory.Arrow.LeftHomotopy.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1 + sizeOf hom + sizeOf comm
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.zmultiples_le : ∀ {G : Type u_1} [inst : AddGroup G] {g : G} {H : AddSubgroup G}, AddSubgroup.zmultiples g ≤ H ↔ g ∈ H
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVec.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} [inst_2 : SizeOf α]
  (refs : Vector Std.Sat.AIG.Fanin w) (hrefs : ∀ {i : ℕ} (h : i < w), refs[i].gate < aig.decls.size),
  sizeOf { refs := refs, hrefs := hrefs } = 1 + sizeOf refs
-- Mathlib.Logic.Hydra
/-- `CutExpand` preserves leftward-closedness under a relation.  -/
Relation.cutExpand_closed : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] (p : α → Prop),
  (∀ {a' a : α}, r a' a → p a → p a') →
    ∀ {s' s : Multiset α}, Relation.CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.srangeRestrict_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), Function.Surjective ⇑f.srangeRestrict
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearEquiv_commIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F],
  (TensorProduct.commIsometry 𝕜 E F).toLinearEquiv = TensorProduct.comm 𝕜 E F
-- Lean.Data.LOption
Lean.LOption.toOption : {α : Type u_1} → Lean.LOption α → Option α
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) (X : B),
  self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
-- Init.Data.Vector.OfFn
Vector.ofFnM_succ : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α},
  Vector.ofFnM f = do
    let as ← Vector.ofFnM fun i => f i.castSucc
    let a ← f (Fin.last n)
    pure (as.push a)
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_extractLsb'_of_le : ∀ {w start len len' : ℕ} {x : BitVec w},
  start + len ≤ len' → BitVec.extractLsb' start len (BitVec.extractLsb' 0 len' x) = BitVec.extractLsb' start len x
-- Mathlib.Order.Interval.Basic
/-- Pushforward of intervals.  -/
Interval.map : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → Interval α → Interval β
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.inducedFunctor_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) [inst_2 : HasFibers p] (S : 𝒮),
  HasFibers.ι S = (HasFibers.inducedFunctor p S).comp CategoryTheory.Functor.Fiber.fiberInclusion
-- Mathlib.Tactic.ClickSuggestions.FindPremises
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.mk : Array
    (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.RwLemma) →
  Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.GrwLemma) →
    Array
        (Lean.Meta.RefinedDiscrTree.Key ×
          Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyLemma) →
      Array
          (Lean.Meta.RefinedDiscrTree.Key ×
            Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyAtLemma) →
        Mathlib.Tactic.ClickSuggestions.Entries✝
-- Mathlib.LinearAlgebra.Matrix.Dual
dotProductEquiv_apply_apply : ∀ (R : Type u_1) (n : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (v w : n → R),
  ((dotProductEquiv R n) v) w = v ⬝ᵥ w
-- Mathlib.Logic.Equiv.PartialEquiv
/-- A map injective on a subset of its domain provides a partial equivalence.  -/
Set.InjOn.toPartialEquiv : {α : Type u_1} → {β : Type u_2} → [Nonempty α] → (f : α → β) → (s : Set α) → Set.InjOn f s → PartialEquiv α β
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for isomorphisms `F ≅ G` in `ComposableArrows C n` which takes as inputs
a family of isomorphisms `F.obj i ≅ G.obj i` and the naturality condition only for the
maps in `Fin (n + 1)` given by inequalities of the form `i ≤ i + 1`.  -/
CategoryTheory.ComposableArrows.isoMk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      {F G : CategoryTheory.ComposableArrows C n} →
        (app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i) →
          (∀ (i : ℕ) (hi : i < n),
              CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom =
                CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' i (i + 1) ⋯ hi)) →
            (F ≅ G)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α], MeasureTheory.Measure.InnerRegular 0
-- Init.Data.UInt.Bitwise
instCommutativeUInt8HOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Mathlib.Order.RelIso.Set
Subrel.instIsStrictOrderSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [IsStrictOrder α r] (p : α → Prop), IsStrictOrder (Subtype p) (Subrel r p)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_list_map_count : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (l : List ι) (f : ι → M),
  (List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ List.count m l
-- Lean.Language.Basic
Lean.Language.TransformedSnap.mk : {α : Type} → α → Lean.Language.SnapshotTreeTransform → Lean.Language.TransformedSnap α
-- Mathlib.Order.Hom.Basic
OrderIso.funUnique_toEquiv : ∀ (α : Type u_6) (β : Type u_7) [inst : Unique α] [inst_1 : Preorder β],
  (OrderIso.funUnique α β).toEquiv = Equiv.funUnique α β
-- Mathlib.Algebra.DirectSum.Basic
/-- The `DirectSum` formed by a collection of additive submonoids (or subgroups, or submodules) of
`M` is said to be internal if the canonical map `(⨁ i, A i) →+ M` is bijective.

For the alternate statement in terms of independence and spanning, see
`DirectSum.subgroup_isInternal_iff_iSupIndep_and_supr_eq_top` and
`DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top`.  -/
DirectSum.IsInternal : {ι : Type v} →
  {M : Type u_1} →
    {S : Type u_2} →
      [DecidableEq ι] → [inst : AddCommMonoid M] → [inst_1 : SetLike S M] → [AddSubmonoidClass S M] → (ι → S) → Prop
-- Aesop.ElabM
Aesop.ElabM.Context.forGlobalErasing : Lean.MetaM Aesop.ElabM.Context
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instSemilatticeSup : {α : Type u_1} → [inst : TopologicalSpace α] → SemilatticeSup (TopologicalSpace.Compacts α)
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.MonadGetStruct : (Type → Type) → Type
-- Mathlib.Logic.Basic
forall₂_comm : ∀ {ι₁ : Sort u_3} {ι₂ : Sort u_4} {κ₁ : ι₁ → Sort u_5} {κ₂ : ι₂ → Sort u_6}
  {p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop},
  (∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ↔
    ∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instLeftCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : LeftCancelMonoid α],
  Colex.instLeftCancelMonoid = { toMonoid := Colex.instMonoid, toIsLeftCancelMul := ⋯ }
-- Mathlib.RingTheory.Polynomial.ShiftedLegendre
Polynomial.neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq : ∀ (n : ℕ), (-1) ^ n * (Polynomial.shiftedLegendre n).comp (1 - Polynomial.X) = Polynomial.shiftedLegendre n
-- Init.Data.BitVec.Lemmas
BitVec.zero_mul : ∀ {w : ℕ} {x : BitVec w}, 0#w * x = 0#w
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- Throws an exception if a contradictory `PComp` is contained in the current state.  -/
Mathlib.Tactic.Linarith.validate : Mathlib.Tactic.Linarith.LinarithM Unit
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Ici.inj : ∀ {n n_1 : Lean.Term}, BigOperators.FinsetResult.Ici✝ n = BigOperators.FinsetResult.Ici✝ n_1 → n = n_1
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
lt_of_mul_lt_mul_of_nonpos_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b c : R} [ExistsAddOfLE R] [PosMulMono R]
  [AddRightMono R] [AddRightReflectLE R], c * a < c * b → c ≤ 0 → b < a
-- Mathlib.Topology.CompactOpen
ContinuousMap.compactOpen_le_induced : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X),
  ContinuousMap.compactOpen ≤ TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.map_id : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (S : NonUnitalSubalgebra R A), NonUnitalSubalgebra.map (NonUnitalAlgHom.id R A) S = S
-- Init.Data.Option.Lemmas
Option.isSome_of_any : ∀ {α : Type u_1} {x : Option α} {p : α → Bool}, Option.any p x = true → x.isSome = true
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- Given an adjunction `F ⊣ G`, the functor that associates to a coalgebra over `G` an algebra over
`F` defined via adjunction applied to the structure map.  -/
CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      (F ⊣ G) → CategoryTheory.Functor (CategoryTheory.Endofunctor.Coalgebra G) (CategoryTheory.Endofunctor.Algebra F)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given `F : D ⥤ C`, this is the partial adjoint functor `F.PartialLeftAdjointSource ⥤ D`.  -/
CategoryTheory.Functor.partialLeftAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D C) → CategoryTheory.Functor F.PartialLeftAdjointSource D
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.isBasis_iff_nbhd : ∀ {α : Type u_2} [inst : TopologicalSpace α] {B : Set (TopologicalSpace.Opens α)},
  TopologicalSpace.Opens.IsBasis B ↔ ∀ {U : TopologicalSpace.Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_mul_leadingCoeff_inv : ∀ {K : Type u_1} [inst : DivisionRing K] (p : Polynomial K) {q : Polynomial K},
  q ≠ 0 → (p * Polynomial.C q.leadingCoeff⁻¹).degree = p.degree
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The property of reflecting pushouts expressed in terms of binary cofans.  -/
CategoryTheory.Limits.isColimitOfIsColimitPushoutCoconeMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {W X Y Z : C} →
            {h : X ⟶ Z} →
              {k : Y ⟶ Z} →
                {f : W ⟶ X} →
                  {g : W ⟶ Y} →
                    (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                      [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) G] →
                        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map h) (G.map k) ⋯) →
                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ici_succ : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n),
  ∑ i ≥ a.succ, f i = ∑ i ≥ a, f i.succ
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_eq_zero_iff : ∀ {α : Type u_1} {ι : Type u_2} {β : Type u_7} [inst : Zero α] [inst_1 : CommMonoidWithZero β] [Nontrivial β]
  [NoZeroDivisors β] {f : ι →₀ α} {g : ι → α → β}, f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_min?_eq_not_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.min?.isSome = !t.isEmpty