mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, (m.insert k v).get? a = if (k == a) = true then some v else m.get? a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyLT_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, cmp a k = Ordering.lt} (h : t₁.Equiv t₂), t₁.getKeyLT k h' = t₂.getKeyLT k ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_sub_int_mul_pi : ∀ (x : ℝ) (n : ℤ), Real.cos (x - ↑n * Real.pi) = (-1) ^ n * Real.cos x
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- This is often wrapped in parentheses to distinguish with the forgetful functor.  -/
_private.Mathlib.Geometry.RingedSpace.OpenImmersion.0.AlgebraicGeometry.SheafedSpace.IsOpenImmersion.termForget : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.refl_apply : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (m : M), LieModuleEquiv.refl m = m
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_sign_iff : ∀ {z : ℤ}, Odd z.sign ↔ z ≠ 0
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Interpreting the legs of a cone as a structured arrow, interpreting this arrow as an arrow over
the cone point, and finally forgetting the arrow is the same as just applying the functor the
cone was over.  -/
CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) →
            c.toStructuredArrow.comp
                ((CategoryTheory.StructuredArrow.toUnder c.pt F).comp (CategoryTheory.Under.forget c.pt)) ≅
              F
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The subsemigroup of elements `x : M` such that `f x = g x`  -/
MulHom.eqLocus : {M : Type u_1} → {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → (M →ₙ* N) → Subsemigroup M
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.toCotangent_apply : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (a : ↥I), I.toCotangent a = Submodule.Quotient.mk a
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- Given an open cover `{ Zᵢ }` of `Z`, then `X ×[Z] Y` is covered by `Xᵢ ×[Zᵢ] Yᵢ`, where
`Xᵢ = X ×[Z] Zᵢ` and `Yᵢ = Y ×[Z] Zᵢ` is the preimage of `Zᵢ` in `X` and `Y`.  -/
AlgebraicGeometry.Scheme.Pullback.openCoverOfBase : {X Y Z : AlgebraicGeometry.Scheme} →
  Z.OpenCover → (f : X ⟶ Z) → (g : Y ⟶ Z) → (CategoryTheory.Limits.pullback f g).OpenCover
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.hasBinaryCoproduct_zero_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasZeroMorphisms C] (X : C), CategoryTheory.Limits.HasBinaryCoproduct X 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- If the cokernel comparison map for `G` at `f` is an isomorphism, then `G` preserves the
cokernel of `f`.
 -/
CategoryTheory.Limits.PreservesCokernel.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.cokernelComparison f G)],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.commGroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : Inv M₁]
  [inst_4 : Div M₁] [inst_5 : Pow M₁ ℤ] [inst_6 : CommGroup M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Injective.commGroup f hf one mul inv div npow zpow =
    { toGroup := Function.Injective.group f hf one mul inv div npow zpow, mul_comm := ⋯ }
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.cells_inf : ∀ (μ ν : YoungDiagram), (μ ⊓ ν).cells = μ.cells ∩ ν.cells
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(a | b)` is nonzero when `a` and `b` are coprime.  -/
jacobiSym.ne_zero : ∀ {a : ℤ} {b : ℕ}, a.gcd ↑b = 1 → jacobiSym a b ≠ 0
-- Init.Data.List.Lemmas
List.getLast!_eq_getElem! : ∀ {α : Type u_1} [inst : Inhabited α] {l : List α}, l.getLast! = l[l.length - 1]!
-- Mathlib.Order.Filter.Extr
IsMaxFilter.comp_tendsto : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
  {b : δ}, IsMaxFilter f l (g b) → Filter.Tendsto g l' l → IsMaxFilter (f ∘ g) l' b
-- Mathlib.Topology.Sets.OpenCover
/-- An indexed family of open sets whose union is `X`.  -/
TopologicalSpace.IsOpenCover : {ι : Type u_1} → {X : Type u_2} → [inst : TopologicalSpace X] → (ι → TopologicalSpace.Opens X) → Prop
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.mk.injEq : ∀ {α : Type u_4} [inst : TopologicalSpace α] (toCompacts : TopologicalSpace.Compacts α)
  (isOpen' : IsOpen toCompacts.carrier) (toCompacts_1 : TopologicalSpace.Compacts α)
  (isOpen'_1 : IsOpen toCompacts_1.carrier),
  ({ toCompacts := toCompacts, isOpen' := isOpen' } = { toCompacts := toCompacts_1, isOpen' := isOpen'_1 }) =
    (toCompacts = toCompacts_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.nnnorm_quasispectrum_le : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄,
  x ∈ quasispectrum 𝕜 a →
    autoParam (p a) NonUnitalIsometricContinuousFunctionalCalculus.nnnorm_quasispectrum_le._auto_1 → ‖x‖₊ ≤ ‖a‖₊
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.awful : Lean.FuzzyMatching.Score✝
-- Mathlib.Analysis.Matrix.Order
Matrix.IsHermitian.det_abs : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜},
  A.IsHermitian → (CFC.abs A).det = ↑‖A.det‖
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_comp_inl : ∀ {R : Type u} (M : Type v) [inst : Zero M], TrivSqZeroExt.fst ∘ TrivSqZeroExt.inl = id
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- Restrict a permutation to a Finset containing its support  -/
Equiv.Perm.subtypePerm_of_support_le : {α : Type u_2} →
  [inst : Fintype α] → [inst_1 : DecidableEq α] → (c : Equiv.Perm α) → {s : Finset α} → c.support ⊆ s → Equiv.Perm ↥s
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.indexConfig : Lean.Meta.Simp.Context → Lean.Meta.ConfigWithKey
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- An alias of `ContinuousMultilinearMap.hasOpNorm` with non-dependent types to help typeclass
search.  -/
ContinuousMultilinearMap.hasOpNorm' : {𝕜 : Type u} →
  {ι : Type v} →
    {G : Type wG} →
      {G' : Type wG'} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup G] →
            [inst_2 : NormedSpace 𝕜 G] →
              [inst_3 : SeminormedAddCommGroup G'] →
                [inst_4 : NormedSpace 𝕜 G'] → [Fintype ι] → Norm (ContinuousMultilinearMap 𝕜 (fun x => G) G')
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.gamma_pos : ∀ {o : Ordinal.{u}}, 0 < o.gamma
-- Mathlib.MeasureTheory.Measure.FiniteMeasurePi
/-- The product of finitely many probability measures.  -/
MeasureTheory.ProbabilityMeasure.pi : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [Fintype ι] →
      [inst : (i : ι) → MeasurableSpace (α i)] →
        ((i : ι) → MeasureTheory.ProbabilityMeasure (α i)) → MeasureTheory.ProbabilityMeasure ((i : ι) → α i)
-- Mathlib.Computability.NFA
DFA.toNFA_correct : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), M.toNFA.accepts = M.accepts
-- Mathlib.Order.Category.CompleteLat
CompleteLat.dualEquiv_functor : CompleteLat.dualEquiv.functor = CompleteLat.dual
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_X : ∀ {R : Type u_1} [inst : CommSemiring R], Polynomial.Bivariate.swap (Polynomial.C Polynomial.X) = Polynomial.X
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracket_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V : E → E}, VectorField.lieBracket 𝕜 V V = 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability at filter in both endpoints.

If `f` is a measurable function integrable on `a..b`, `(la, la')` is an `intervalIntegral.FTCFilter`
pair around `a`, and `(lb, lb')` is an `intervalIntegral.FTCFilter` pair around `b`, and `f` has
finite limits `ca` and `cb` almost surely at `la'` and `lb'`, respectively, then
`(∫ x in va..vb, f x) - ∫ x in ua..ub, f x = (vb - ub) • cb - (va - ua) • ca +
  o(‖va - ua‖ + ‖vb - ub‖)` as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`.

This lemma could've been formulated using `HasStrictFDerivAtFilter` if we had this
definition.  -/
intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E}
  {ca cb : E} {la la' lb lb' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {ua ub va vb : ι → ℝ}
  [intervalIntegral.FTCFilter a la la'] [intervalIntegral.FTCFilter b lb lb'],
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f la' MeasureTheory.volume →
      StronglyMeasurableAtFilter f lb' MeasureTheory.volume →
        Filter.Tendsto f (la' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca) →
          Filter.Tendsto f (lb' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb) →
            Filter.Tendsto ua lt la →
              Filter.Tendsto va lt la →
                Filter.Tendsto ub lt lb →
                  Filter.Tendsto vb lt lb →
                    (fun t =>
                        ((∫ (x : ℝ) in va t..vb t, f x) - ∫ (x : ℝ) in ua t..ub t, f x) -
                          ((vb t - ub t) • cb - (va t - ua t) • ca)) =o[lt]
                      fun t => ‖va t - ua t‖ + ‖vb t - ub t‖
-- Mathlib.Topology.Order
instDiscreteTopologyNat : DiscreteTopology ℕ
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.isCasesAttrPredicateCandidate? : Lean.Name → Bool → Lean.MetaM (Option Lean.InductiveVal)
-- Lean.Meta.Tactic.LibrarySearch
/-- Return an action that returns true when the remaining heartbeats is less
than the currently remaining heartbeats * leavePercent / 100.
 -/
Lean.Meta.LibrarySearch.mkHeartbeatCheck : ℕ → Lean.MetaM (Lean.MetaM Bool)
-- Mathlib.CategoryTheory.FintypeCat
/-- Constructor for morphisms in `FintypeCat`.  -/
FintypeCat.homMk : {X Y : FintypeCat} → (X.obj → Y.obj) → (X ⟶ Y)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.toContinuousMapMonoidHom_apply : ∀ (α : Type u) (R : Type u_2) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Monoid R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R] (self : BoundedContinuousFunction α R),
  (BoundedContinuousFunction.toContinuousMapMonoidHom α R) self = self.toContinuousMap
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_congr : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↥X) (hxx' : x = x'),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x) (X.presheaf.stalkCongr ⋯).hom =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (AlgebraicGeometry.Scheme.Hom.stalkMap g x')
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_nhds_of_im_neg : ∀ {z : ℂ}, z.im < 0 → Complex.arg =ᶠ[nhds z] fun x => -Real.arccos (x.re / ‖x‖)
-- Mathlib.Algebra.Group.Irreducible.Defs
irreducible_iff : ∀ {M : Type u_1} [inst : Monoid M] {p : M}, Irreducible p ↔ ¬IsUnit p ∧ ∀ ⦃a b : M⦄, p = a * b → IsUnit a ∨ IsUnit b
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_5 : ∀ {C : Type u} (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (CategoryTheory.FreeMonoidalCategory.Hom.l_inv x) =
    id (CategoryTheory.Discrete.natTrans fun x_1 => CategoryTheory.CategoryStruct.id (x.normalizeObj'.obj x_1))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- An alternative to `biprod.map` constructed via colimits.
This construction only exists in order to show it is equal to `biprod.map`.  -/
CategoryTheory.Limits.biprod.map' : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {W X Y Z : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X] →
          [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] → (W ⟶ Y) → (X ⟶ Z) → (W ⊞ X ⟶ Y ⊞ Z)
-- Mathlib.RingTheory.Perfection
/-- The `p`-th root of an element of the perfection.

The preferred way to use this is `(frobeniusEquiv (Perfection R p) p).symm`.  -/
Perfection.pthRoot : (R : Type u_1) →
  [inst : CommSemiring R] →
    (p : ℕ) → [hp : Fact (Nat.Prime p)] → [inst_1 : CharP R p] → Perfection R p →+* Perfection R p
-- Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
LinearMap.span_singleton_inf_orthogonal_eq_bot : ∀ {K : Type u_7} {K₁ : Type u_8} {V₁ : Type u_10} {V₂ : Type u_11} [inst : Field K] [inst_1 : Field K₁]
  [inst_2 : AddCommGroup V₁] [inst_3 : Module K₁ V₁] [inst_4 : AddCommGroup V₂] [inst_5 : Module K V₂]
  {J₁ J₁' : K₁ →+* K} (B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂) (x : V₁),
  (B x) x ≠ 0 → K₁ ∙ x ⊓ Submodule.orthogonalBilin B (K₁ ∙ x) = ⊥
-- Init.GetElem
some_getElem_eq_getElem?_iff : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i), some c[i] = c[i]? ↔ True
-- Mathlib.RingTheory.NoetherNormalization
/-- **Noether normalization lemma**
For a finitely generated algebra `A` over a field `k`,
there exists a natural number `s` and an injective homomorphism
from `k[X_0, X_1, ..., X_(s-1)]` to `A` such that `A` is integral over `k[X_0, X_1, ..., X_(s-1)]`.
 -/
exists_integral_inj_algHom_of_fg : ∀ (k : Type u_2) (R : Type u_3) [inst : Field k] [inst_1 : CommRing R] [Nontrivial R] [a : Algebra k R]
  [fin : Algebra.FiniteType k R], ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral
-- Mathlib.GroupTheory.Commutator.Basic
commutator_centralizer_commutator_le_center : ∀ (G : Type u_1) [inst : Group G],
  ⁅Subgroup.centralizer ↑(commutator G), Subgroup.centralizer ↑(commutator G)⁆ ≤ Subgroup.center G
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- If `P` is closed under limits of shape `J`, then the inclusion creates such limits.  -/
CategoryTheory.Limits.createsLimitsOfShapeFullSubcategoryInclusion : (J : Type w) →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (P : CategoryTheory.ObjectProperty C) →
          [P.IsClosedUnderLimitsOfShape J] →
            [CategoryTheory.Limits.HasLimitsOfShape J C] → CategoryTheory.CreatesLimitsOfShape J P.ι
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.booleanAlgebra : {α : Type u_1} → [Fintype α] → [DecidableEq α] → BooleanAlgebra (Finset α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  t.isEmpty = true → t.getKeyD a fallback = fallback
-- Init.Data.Vector.Lemmas
Vector.getElem?_set!_self : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {x : α}, (xs.set! i x)[i]? = if i < n then some x else none
-- Init.Data.Vector.Lemmas
Vector.set_append_right : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {i : ℕ} {x : α} (h' : i < n + m) (h : n ≤ i),
  (xs ++ ys).set i x h' = xs ++ ys.set (i - n) x ⋯
-- Mathlib.Analysis.Convex.Between
not_sbtw_self_right : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), ¬Sbtw R x y y
-- Mathlib.CategoryTheory.PEmpty
/-- Any two functors out of the empty category are isomorphic.  -/
CategoryTheory.Functor.emptyExt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C) → F ≅ G
-- Mathlib.Topology.Constructions
Continuous.finCons : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] {f : X → A 0} {g : X → (j : Fin n) → A j.succ},
  Continuous f → Continuous g → Continuous fun a => Fin.cons (f a) (g a)
-- Mathlib.Algebra.DirectSum.Ring
/-- The `CommSemiring` structure derived from `GCommSemiring A`.  -/
DirectSum.commSemiring : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommMonoid (A i)] →
        [inst_1 : AddCommMonoid ι] → [DirectSum.GCommSemiring A] → CommSemiring (DirectSum ι fun i => A i)
-- Mathlib.Algebra.Group.Defs
AddLeftCancelSemigroup.mk : {G : Type u} → [toAddSemigroup : AddSemigroup G] → [toIsLeftCancelAdd : IsLeftCancelAdd G] → AddLeftCancelSemigroup G
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsMarkovKernelProdOfSectL : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel (α × β) γ}
  [∀ (b : β), ProbabilityTheory.IsMarkovKernel (κ.sectL b)], ProbabilityTheory.IsMarkovKernel κ
-- Mathlib.Geometry.Manifold.Instances.Real
/-- Charted space structure on `[x, y]`, using only two charts taking values in
`EuclideanHalfSpace 1`.
 -/
instIccChartedSpace : (x y : ℝ) → [h : Fact (x < y)] → ChartedSpace (EuclideanHalfSpace 1) ↑(Set.Icc x y)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.inducedStructure : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → {S : L.Substructure M} → L.Structure ↥S
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- Addition of morphisms in a `NonPreadditiveAbelian` category.  -/
CategoryTheory.NonPreadditiveAbelian.hasAdd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.NonPreadditiveAbelian C] → {X Y : C} → Add (X ⟶ Y)
-- Mathlib.GroupTheory.GroupAction.Jordan
/-- Simultaneously prove `MulAction.IsPreprimitive.is_two_pretransitive`
and `MulAction.IsPreprimitive.is_two_preprimitive`.  -/
MulAction.IsPreprimitive.is_two_motive_of_is_motive : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  MulAction.IsPreprimitive G α →
    ∀ {s : Set α} {n : ℕ},
      s.ncard = n + 1 →
        n + 2 < Nat.card α →
          (MulAction.IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              MulAction.IsMultiplyPretransitive G α 2) ∧
            (MulAction.IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              MulAction.IsMultiplyPreprimitive G α 2)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.finsetWalkLength.eq_2 : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : G.LocallyFinite] (u v : V) (n_2 : ℕ),
  G.finsetWalkLength n_2.succ u v =
    Finset.univ.biUnion fun w =>
      Finset.map { toFun := fun p => SimpleGraph.Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n_2 (↑w) v)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ) {Z : Cᵒᵖ}
  (h : F.op.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.op j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).op h
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.span_root'_eq_top : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) [P.IsRootSystem],
  Submodule.span R (Set.range P.root') = ⊤
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of two monotone functions is monotone.  -/
MonotoneOn.mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [MulLeftMono α] [MulRightMono α], MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => f x * g x) s
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
sub_mul_sub_neg_iff : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R]
  [AddLeftMono R] (x : R), a ≤ b → ((x - a) * (x - b) < 0 ↔ a < x ∧ x < b)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.factors.congr_simp : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a a_1 : α),
  a = a_1 → UniqueFactorizationMonoid.factors a = UniqueFactorizationMonoid.factors a_1
-- Mathlib.Order.CompleteBooleanAlgebra
OrderDual.instCompletelyDistribLattice : {α : Type u} → [CompletelyDistribLattice α] → CompletelyDistribLattice αᵒᵈ
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- There is a morphism from any cone point to `t.pt`  -/
CategoryTheory.Limits.IsWeakLimit.lift : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsWeakLimit t → (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_one : ∀ {R : Type u_1} [inst : Semiring R] (x : R), ∑ i ∈ Finset.range 1, x ^ i = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        k ∈ m₂ → Std.DHashMap.Raw.Const.getD (m₁ ∩ m₂) k fallback = Std.DHashMap.Raw.Const.getD m₁ k fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelIsoOfEq h).hom (CategoryTheory.Limits.kernel.ι g) =
    CategoryTheory.Limits.kernel.ι f
-- Init.Data.Array.MapIdx
List.mapFinIdxM_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  {f : (i : ℕ) → α → i < l.length → m β}, l.toArray.mapFinIdxM f = List.toArray <$> l.mapFinIdxM f