mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GCDMonoid.Basic
instIsGCDMonoidOfGCDMonoid : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [GCDMonoid α], IsGCDMonoid α
-- Mathlib.Order.Interval.Finset.Basic
transGen_covBy_of_lt : ∀ {α : Type u_2} [inst : Preorder α] [LocallyFiniteOrder α] {x y : α},
  x < y → Relation.TransGen (fun x1 x2 => x1 ⋖ x2) x y
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.smul_def_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (r : R) (f : M →ₚₗ[R] N) (S : Type u) [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S] (m : TensorProduct R S M), (r • f).toFun' S m = r • f.toFun' S m
-- Mathlib.RingTheory.OreLocalization.Ring
/-- The ring homomorphism from `R` to `R[S⁻¹]`, mapping `r : R` to the fraction `r /ₒ 1`.  -/
OreLocalization.numeratorRingHom : {R : Type u_1} →
  [inst : Semiring R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → R →+* OreLocalization S R
-- Mathlib.Topology.Separation.Basic
/-- In an R₀ space, the closure of a singleton is a compact set.  -/
isCompact_closure_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R0Space X] {x : X}, IsCompact (closure {x})
-- Aesop.Tree.Data
Aesop.Rapp.elim : Aesop.Rapp → Aesop.RappData Aesop.Goal Aesop.MVarCluster
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  [inst_3 : DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i)
  (x : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker),
  (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπOdd A g hg i hi)) x = 0 ↔
    ↑x ∈ LinearMap.range A.ρ.norm
-- Mathlib.Tactic.Simps.Basic
Simps.ParsedProjectionData.mk.inj : ∀ {strName : Lean.Name} {strStx : Lean.Syntax} {newName : Lean.Name} {newStx : Lean.Syntax} {isDefault isPrefix : Bool}
  {expr? : Option Lean.Expr} {projNrs : Array ℕ} {isCustom : Bool} {strName_1 : Lean.Name} {strStx_1 : Lean.Syntax}
  {newName_1 : Lean.Name} {newStx_1 : Lean.Syntax} {isDefault_1 isPrefix_1 : Bool} {expr?_1 : Option Lean.Expr}
  {projNrs_1 : Array ℕ} {isCustom_1 : Bool},
  { strName := strName, strStx := strStx, newName := newName, newStx := newStx, isDefault := isDefault,
        isPrefix := isPrefix, expr? := expr?, projNrs := projNrs, isCustom := isCustom } =
      { strName := strName_1, strStx := strStx_1, newName := newName_1, newStx := newStx_1, isDefault := isDefault_1,
        isPrefix := isPrefix_1, expr? := expr?_1, projNrs := projNrs_1, isCustom := isCustom_1 } →
    strName = strName_1 ∧
      strStx = strStx_1 ∧
        newName = newName_1 ∧
          newStx = newStx_1 ∧
            isDefault = isDefault_1 ∧
              isPrefix = isPrefix_1 ∧ expr? = expr?_1 ∧ projNrs = projNrs_1 ∧ isCustom = isCustom_1
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesAt.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ},
  HasFiniteFPowerSeriesAt f p x n → f =ᶠ[nhds x] g → HasFiniteFPowerSeriesAt g p x n
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.RewriteLemma.mk.inj : ∀ {name : Lean.Name} {symm : Bool} {name_1 : Lean.Name} {symm_1 : Bool},
  { name := name, symm := symm } = { name := name_1, symm := symm_1 } → name = name_1 ∧ symm = symm_1
-- Init.Grind.Ordered.Order
Lean.Grind.Preorder.lt_of_le_of_lt : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α}, a ≤ b → b < c → a < c
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDualEquiv.congr_simp : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {inst_3 : DecidableEq ι} [inst_4 : DecidableEq ι] (b b_1 : Module.Basis ι R M),
  b = b_1 → ∀ [inst_5 : Finite ι], b.toDualEquiv = b_1.toDualEquiv
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeList.match_1.splitter : {α : Type u_1} →
  (motive : List (List α) × List α → Sort u_2) →
    (x : List (List α) × List α) → ((xss : List (List α)) → (rest : List α) → motive (xss, rest)) → motive x
-- Init.Data.UInt.Lemmas
UInt64.ofNat_eq_iff_mod_eq_toNat : ∀ (a : ℕ) (b : UInt64), UInt64.ofNat a = b ↔ a % 2 ^ 64 = b.toNat
-- Mathlib.Order.Monotone.Basic
StrictAnti.le_iff_ge : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → ∀ {a b : α}, f a ≤ f b ↔ b ≤ a
-- Lean.Elab.InfoTree.Main
Lean.Elab.OptionInfo.format : Lean.Elab.ContextInfo → Lean.Elab.OptionInfo → IO Std.Format
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- The sum of two left homotopies is a left homotopy between the sum of the respective
morphisms.  -/
CategoryTheory.Arrow.LeftHomotopy.add : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f₁ g₁ f₂ g₂ : u ⟶ v} →
          CategoryTheory.Arrow.LeftHomotopy f₁ g₁ →
            CategoryTheory.Arrow.LeftHomotopy f₂ g₂ → CategoryTheory.Arrow.LeftHomotopy (f₁ + f₂) (g₁ + g₂)
-- Init.Core
/-- `LawfulIdentity op o` indicates `o` is a verified left and right
identity of `op`.
 -/
Std.LawfulIdentity : {α : Sort u} → (α → α → α) → outParam α → Prop
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_closedEBall_le : ∀ {X : Type u_2} {x : X} [inst : PseudoEMetricSpace X] {r : ENNReal}, Metric.ediam (Metric.closedEBall x r) ≤ 2 * r
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- The composite of two `IsLocalRing.ResidueField.map`s is the `IsLocalRing.ResidueField.map` of
the composite.  -/
IsLocalRing.ResidueField.map_comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] [inst_4 : CommRing T] [inst_5 : IsLocalRing T] (f : T →+* R) (g : R →+* S)
  [inst_6 : IsLocalHom f] [inst_7 : IsLocalHom g],
  IsLocalRing.ResidueField.map (g.comp f) = (IsLocalRing.ResidueField.map g).comp (IsLocalRing.ResidueField.map f)
-- Mathlib.CategoryTheory.Localization.Predicate
/-- Given a localization functor `L : C ⥤ D` for `W : MorphismProperty C`,
if `F₁' : D ⥤ E` lifts a functor `F₁ : C ⥤ D`, then a functor `F₂'` which
is isomorphic to `F₁'` also lifts a functor `F₂` that is isomorphic to `F₁`.  -/
CategoryTheory.Localization.Lifting.ofIsos : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            {E : Type u_3} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                {F₁ F₂ : CategoryTheory.Functor C E} →
                  {F₁' F₂' : CategoryTheory.Functor D E} →
                    (F₁ ≅ F₂) →
                      (F₁' ≅ F₂') →
                        [CategoryTheory.Localization.Lifting L W F₁ F₁'] →
                          CategoryTheory.Localization.Lifting L W F₂ F₂'
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkSeq : Array (Lean.TSyntax `tactic) → Bool → Lean.CoreM (Lean.TSyntax `tactic)
-- Mathlib.Combinatorics.Configuration
/-- Line through two points  -/
Configuration.HasLines.mkLine : {P : Type u_1} →
  {L : Type u_2} → {inst : Membership P L} → [self : Configuration.HasLines P L] → {p₁ p₂ : P} → p₁ ≠ p₂ → L
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitResults.instAppend : {α : Type} → Append (Lean.Meta.LazyDiscrTree.InitResults α)
-- Mathlib.Tactic.Linter.Style
/-- The `cdot` linter flags uses of the "cdot" `·` that are achieved by typing a character
different from `·`.
For instance, a "plain" dot `.` is allowed syntax, but is flagged by the linter.
It also flags "isolated cdots", i.e. when the `·` is on its own line.  -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.cdotLinter : Lean.Linter
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ_coeff_φ_natDegree' : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → (RatFunc.Luroth.Φ✝ E).coeff (RatFunc.Luroth.φ✝ E).natDegree = (RatFunc.Luroth.c✝ E).num
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.map_repr : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (b : Module.Basis ι R M) (f : M ≃ₗ[R] M'),
  (b.map f).repr = f.symm ≪≫ₗ b.repr
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.QuotientTop.fintype : {R : Type u_1} → {M : Type u_2} → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Fintype (M ⧸ ⊤)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_const_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜}, iteratedDerivWithin n 0 s x = 0
-- Lean.LibrarySuggestions.Basic
/-- Combine two premise selectors by interspersing their results (ignoring scores).
The parameter `ratio` (defaulting to 0.5) controls the fraction of suggestions drawn from
`selector₁` while results are available from both. It is clamped to `[0, 1]`, and ties are
resolved in favour of `selector₁`.

Both selectors are asked for the full `maxSuggestions`, rather than a `ratio`-split share, so that
if one selector returns fewer than its share the other can compensate. This doubles the retrieval
work compared to splitting the budget.
 -/
Lean.LibrarySuggestions.Selector.intersperse : Lean.LibrarySuggestions.Selector →
  Lean.LibrarySuggestions.Selector → optParam Float 0.5 → Lean.LibrarySuggestions.Selector
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is right distributive over addition  -/
NonUnitalNonAssocSemiring.right_distrib : ∀ {α : Type u} [self : NonUnitalNonAssocSemiring α] (a b c : α), (a + b) * c = a * c + b * c
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.instIsAnisotropicFlip : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], P.flip.IsAnisotropic
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofTacticInfo.sizeOf_spec : ∀ (i : Lean.Elab.TacticInfo), sizeOf (Lean.Elab.Info.ofTacticInfo i) = 1 + sizeOf i
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- Let `D` be the decomposition field of `P` in `L/K`. Let `𝓟D` be a prime ideal of `D` below `P`,
then the inertia degree of `𝓟D` in `L` is equal to the inertia degree of `p` in `L`.
 -/
IsDecompositionField.inertiaDegIn_eq : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [inst_7 : Algebra A K] [IsFractionRing A K] [inst_9 : Algebra A L] [IsScalarTower A K L] [inst_11 : Algebra B L]
  [IsScalarTower A B L] [IsFractionRing B L] [inst_14 : MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L]
  (D : Type u_5) (𝓞D : Type u_6) [inst_16 : Field D] [inst_17 : Algebra D L] [IsDecompositionField K L P D]
  [inst_19 : CommRing 𝓞D] [inst_20 : Algebra 𝓞D D] [IsFractionRing 𝓞D D] [inst_22 : Algebra 𝓞D B]
  [inst_23 : Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D]
  [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B]
  [inst_31 : Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [𝓟D.LiesOver p]
  [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal],
  p ≠ ⊥ → 𝓟D.inertiaDegIn B = p.inertiaDegIn B
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.instInhabitedNormedSpaceInfo : Inhabited Manifold.Elab.NormedSpaceInfo
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} {fallback : β a}, (↑m).isEmpty = true → m.getD a fallback = fallback
-- Mathlib.Topology.UniformSpace.Basic
image_entourageProd_prod : ∀ {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β) (s : Set α) (t : Set β),
  (entourageProd u v).image (s ×ˢ t) = u.image s ×ˢ v.image t
-- Mathlib.RingTheory.RingHom.Integral
RingHom.isIntegral_isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β},
  k ∉ m₂ → Std.DHashMap.Const.getD (m₁.diff m₂) k fallback = Std.DHashMap.Const.getD m₁ k fallback
-- Init.Data.Fin.Fold
Fin.foldrM_zero : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (f : Fin 0 → α → m α), Fin.foldrM 0 f = pure
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  (ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM 𝕜) f =
    { toFun := ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- A typeclass describing the property that an explicit pullback is stable under the property `P`.
 -/
CompHausLike.HasExplicitPullback : {P : TopCat → Prop} → {X Y B : CompHausLike P} → (X ⟶ B) → (Y ⟶ B) → Prop
-- Mathlib.RingTheory.LocalProperties.InjectiveDimension
ModuleCat.instPreservesInjectiveObjectsLocalizationLocalizedModuleFunctorOfIsNoetherianRing : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (S : Submonoid R),
  (ModuleCat.localizedModuleFunctor S).PreservesInjectiveObjects
-- Mathlib.Algebra.Group.Defs
DivisionCommMonoid.mk : {G : Type u} → [toDivisionMonoid : DivisionMonoid G] → (∀ (a b : G), a * b = b * a) → DivisionCommMonoid G
-- Mathlib.Order.NonemptyFiniteChains
/-- Given a partially ordered type `X`, this is the type of nonempty finite
subsets `A` of `X` such that all the elements of `A` are comparable.  -/
PartialOrder.NonemptyFiniteChains : (X : Type u) → [PartialOrder X] → Type u
-- Mathlib.Algebra.Category.Grp.LargeColimits
/-- If `c` is a cocone of `F` such that `Quot.desc F c` is bijective, then `c` is a colimit
cocone of `F`.
 -/
AddCommGrpCat.isColimit_iff_bijective_desc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J AddCommGrpCat}
  (c : CategoryTheory.Limits.Cocone F) [inst_1 : DecidableEq J],
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Function.Bijective ⇑(AddCommGrpCat.Colimits.Quot.desc F c)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_mono : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K K' : AddSubgroup G},
  K ≤ K' → AddSubgroup.map f K ≤ AddSubgroup.map f K'
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_succ_succ : ∀ {m n : ℤ}, ((m + 1)...=n + 1).toArray = Array.map (fun x => x + 1) (m...=n).toArray
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.brecOn.eq : ∀ {pu : Lean.Compiler.LCNF.Purity} {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u}
  {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u}
  {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u}
  {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} (t : Lean.Compiler.LCNF.Alt pu)
  (F_1 : (t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t)
  (F_2 : (t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t)
  (F_3 : (t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t)
  (F_4 : (t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t)
  (F_5 : (t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t)
  (F_6 : (t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 = F_1 t (Lean.Compiler.LCNF.Alt.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.Algebra.Group.Submonoid.Defs
MonoidHom.eq_of_eqOn_topM : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {f g : M →* N},
  Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Mathlib.Data.Set.Prod
/-- The projection from the fiber product to the second factor.  -/
Function.Pullback.snd : {X : Type u_1} → {Y : Sort u_2} → {Z : Type u_3} → {f : X → Y} → {g : Z → Y} → Function.Pullback f g → Z
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.ne_bot_of_mem_vertexSet : ∀ {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β}, x ∈ G.vertexSet → G ≠ ⊥
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius_singleton_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), 0 < s.exradius {i}
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.instIsIsoColimitPointwiseProductToProductColimitOfIsIPCOfShapeOfIsFiltered : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape ι C] [CategoryTheory.Limits.IsIPCOfShape.{w, u_2, v_1, u_1} ι C]
  {J : ι → Type w} [inst_3 : (i : ι) → CategoryTheory.SmallCategory (J i)] [∀ (i : ι), CategoryTheory.IsFiltered (J i)]
  (F : (i : ι) → CategoryTheory.Functor (J i) C) [inst_5 : ∀ (i : ι), CategoryTheory.Limits.HasColimit (F i)]
  [inst_6 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pointwiseProduct F)],
  CategoryTheory.IsIso (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F)
-- Mathlib.Analysis.Analytic.Composition
/-- Given a formal multilinear series `p`, a composition `c` of `n` and a continuous multilinear
map `f` in `c.length` variables, one may form a continuous multilinear map in `n` variables by
applying the right coefficient of `p` to each block of the composition, and then applying `f` to
the resulting vector. It is called `f.compAlongComposition p c`.  -/
ContinuousMultilinearMap.compAlongComposition : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        [inst : CommRing 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : AddCommGroup F] →
              [inst_3 : AddCommGroup G] →
                [inst_4 : Module 𝕜 E] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : Module 𝕜 G] →
                      [inst_7 : TopologicalSpace E] →
                        [inst_8 : TopologicalSpace F] →
                          [inst_9 : TopologicalSpace G] →
                            [inst_10 : IsTopologicalAddGroup E] →
                              [inst_11 : ContinuousConstSMul 𝕜 E] →
                                [inst_12 : IsTopologicalAddGroup F] →
                                  [inst_13 : ContinuousConstSMul 𝕜 F] →
                                    {n : ℕ} →
                                      FormalMultilinearSeries 𝕜 E F →
                                        (c : Composition n) → (F [×c.length]→L[𝕜] G) → E [×n]→L[𝕜] G
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.le_max?_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k km : α}
  (hc : t.contains k = true), t.max?.get ⋯ = km → (cmp k km).isLE = true
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.withPositionAfterLinebreak.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Types.Coequalizers
/-- Show that the quotient by the relation generated by `f(x) ~ g(x)`
is a coequalizer for the pair `(f, g)`.
 -/
CategoryTheory.Limits.Types.coequalizerColimit : {X Y : Type u} → (f g : X ⟶ Y) → CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.parallelPair f g)
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_pos : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
-- Mathlib.Data.Nat.Find
Nat.find_le_iff : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) (n : ℕ), Nat.find h ≤ n ↔ ∃ m ≤ n, p m
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableAt_symm_of_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {e : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I 1 M → ∀ {x : H}, x ∈ e.target → MDiffAt ↑e.symm x
-- Mathlib.GroupTheory.Index
Subgroup.index_eq_one : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 1 ↔ H = ⊤
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  {F G : CategoryTheory.Functor C V} (H : CategoryTheory.Functor C V) (η : F ⟶ G)
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution H F]
  [inst_8 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_9 : CategoryTheory.MonoidalCategory.DayConvolution H G],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id H) η)
      (CategoryTheory.MonoidalCategory.DayConvolution.braiding H G).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding H F).hom
      (CategoryTheory.MonoidalCategory.DayConvolution.map η (CategoryTheory.CategoryStruct.id H))
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_map_natCast : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℕ),
  (A.map Nat.cast).num = A.map Nat.cast
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  [inst_6 : SizeOf M] [inst_7 : SizeOf N] [inst_8 : SizeOf A] [inst_9 : SizeOf B] (toMulActionHom : A →ₑ[⇑φ] B)
  (map_one' : toMulActionHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : A), toMulActionHom.toFun (x * y) = toMulActionHom.toFun x * toMulActionHom.toFun y),
  sizeOf { toMulActionHom := toMulActionHom, map_one' := map_one', map_mul' := map_mul' } =
    1 + sizeOf toMulActionHom + sizeOf map_one'
-- Mathlib.Algebra.Colimit.Ring
Ring.instZeroDirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] → (f : (i j : ι) → i ≤ j → G i → G j) → Zero (Ring.DirectLimit G f)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.brange.eq_1 : ∀ {α : Type u_1} (o : Ordinal.{u_3}) (f : (a : Ordinal.{u_3}) → a < o → α),
  o.brange f = {a | ∃ i, ∃ (hi : i < o), f i hi = a}
-- Lean.Parser.Syntax
Lean.Parser.Command.macro.formatter : Lean.PrettyPrinter.Formatter