mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Util
Lean.Meta.debug.terminalTacticsAsSorry : Lean.Option Bool
-- Mathlib.Tactic.Linter.MinImports
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.ImportState.mk.injEq : ∀ (transClosure : Option (Lean.NameMap Lean.NameSet)) (minImports : Lean.NameSet) (importSize : ℕ)
  (transClosure_1 : Option (Lean.NameMap Lean.NameSet)) (minImports_1 : Lean.NameSet) (importSize_1 : ℕ),
  ({ transClosure := transClosure, minImports := minImports, importSize := importSize } =
      { transClosure := transClosure_1, minImports := minImports_1, importSize := importSize_1 }) =
    (transClosure = transClosure_1 ∧ minImports = minImports_1 ∧ importSize = importSize_1)
-- Mathlib.Algebra.Category.ModuleCat.Ulift
/-- The `ULift` functor on `ModuleCat` is compatible with the one defined on categories of types.  -/
ModuleCat.uliftFunctorForgetIso : (R : Type u) →
  [inst : Ring R] →
    (ModuleCat.uliftFunctor.{v', u_1, u} R).comp (CategoryTheory.forget (ModuleCat R)) ≅
      (CategoryTheory.forget (ModuleCat R)).comp CategoryTheory.uliftFunctor.{v', u_1}
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.instIsIsoModuleCatStalkToLocalizationₗ : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : PrimeSpectrum R),
  CategoryTheory.IsIso (AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ✝ R M x)
-- Mathlib.Topology.Baire.BaireMeasurable
Homeomorph.residual_map_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (h : α ≃ₜ β),
  Filter.map (⇑h) (residual α) = residual β
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnected.mk : UInt64 → Lean.Lsp.RpcConnected
-- Mathlib.Topology.Algebra.InfiniteSum.Order
tsum_nonneg : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {g : ι → α},
  (∀ (i : ι), 0 ≤ g i) → 0 ≤ ∑'[L] (i : ι), g i
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A variant of `lift` with `Z` an initial object.  -/
CategoryTheory.WithInitial.liftToInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          CategoryTheory.Functor C D →
            CategoryTheory.Limits.IsInitial Z → CategoryTheory.Functor (CategoryTheory.WithInitial C) D
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inv_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero) (i : ℕ),
  ↑(f.inv hf) i = (↑f i)⁻¹
-- Mathlib.Analysis.Convex.Quasiconvex
MonotoneOn.quasilinearOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, MonotoneOn f s → Convex 𝕜 s → QuasilinearOn 𝕜 s f
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
CochainComplex.ConnectData.homologyIsoPos.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n : ℕ) [inst_2 : NeZero n]
  (m : ℤ) (hm : m = ↑n) [inst_3 : HomologicalComplex.HasHomology h.cochainComplex m]
  [inst_4 : HomologicalComplex.HasHomology L n], h.homologyIsoPos n m hm = h.homologyIsoPos n m hm
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
uniqueMDiffWithinAt_iff : ∀ {𝕜 : 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] {s : Set M} {x : M},
  UniqueMDiffAt[s] x ↔
    UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' s ∩ (extChartAt I x).target) (↑(extChartAt I x) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_right_inv : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ : CategoryTheory.Arrow C₁}
  {f₃ f₃' : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom)
  (iso : f₃ ≅ f₃'), (sq₁₃.π_iso_of_iso_right sq₁₃' iso).inv = sq₁₃'.mapArrowRight sq₁₃ iso.inv
-- Mathlib.Algebra.Ring.Equiv
/-- Reinterpret a ring equivalence as an `AddMonoid` homomorphism.  -/
RingEquiv.toAddMonoidHom : {R : Type u_4} → {S : Type u_5} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R ≃+* S → R →+ S
-- Batteries.Data.Fin.Lemmas
Fin.prod_zero : ∀ {α : Type u_1} [inst : One α] [inst_1 : Mul α] (x : Fin 0 → α), Fin.prod x = 1
-- Mathlib.Analysis.Calculus.FDeriv.Norm
HasFDerivAt.hasFDerivAt_norm_smul_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : StrongDual ℝ E} {x : E} {t : ℝ},
  0 < t → HasFDerivAt (fun x => ‖x‖) f x → HasFDerivAt (fun x => ‖x‖) f (t • x)
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
/-- Given `T : MorphismProperty C`, this is the class of morphisms that have the
left lifting property (llp) with respect to `T`.  -/
CategoryTheory.MorphismProperty.llp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_nonneg_of_neg_pi_div_two_le_of_le : ∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ Real.pi / 2 → 0 ≤ Real.cos x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  t.WF →
    ∀ {k a : α} {v : β},
      Std.DTreeMap.Raw.Const.get! (t.insertIfNew k v) a =
        if cmp k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Raw.Const.get! t a
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The objects for the Kleisli category of the monad `T : Monad C`, which are the same
thing as objects of the base category `C`.
 -/
CategoryTheory.Kleisli : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Monad C → Type u
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The linearization of a type `H` with a `G`-action is definitionally isomorphic to the
`k`-linear `G`-representation on `k[H]` induced by the `G`-action on `H`.  -/
Rep.linearizationOfMulActionIso : (k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        (H : Type u) →
          [inst_2 : MulAction G H] → (Rep.linearization k G).obj (Action.ofMulAction G H) ≅ Rep.ofMulAction k G H
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
MeasureTheory.closedCompactCylinders.isClosed : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)}
  (ht : t ∈ MeasureTheory.closedCompactCylinders X), IsClosed (MeasureTheory.closedCompactCylinders.set ht)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.Embeddings.coeff_bdd_of_norm_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {A : Type u_2} [inst_2 : NormedField A] [IsAlgClosed A]
  [NormedAlgebra ℚ A] {B : ℝ} {x : K},
  (∀ (φ : K →+* A), ‖φ x‖ ≤ B) →
    ∀ (i : ℕ),
      ‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ Module.finrank ℚ K * ↑((Module.finrank ℚ K).choose (Module.finrank ℚ K / 2))
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.self_comp_symm_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.toEmbedding.comp f.symm.toEmbedding = FirstOrder.Language.Embedding.refl L N
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.instIsZariskiLocalAtSource : AlgebraicGeometry.IsZariskiLocalAtSource @AlgebraicGeometry.SurjectiveOnStalks
-- Init.Data.SInt.Lemmas
Int8.sub_nonneg_of_le : ∀ {a b : Int8}, 0 ≤ b → b ≤ a → 0 ≤ a - b
-- Lean.DocString.Types
Lean.Doc.Block.ul.injEq : ∀ {i : Type u} {b : Type v} (items items_1 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))),
  (Lean.Doc.Block.ul items = Lean.Doc.Block.ul items_1) = (items = items_1)
-- Mathlib.Topology.Constructible
/-- An induction principle for constructible sets. If `p` holds for all open retrocompact
sets, and is preserved under union and complement, then `p` holds for all constructible sets.  -/
Topology.IsConstructible.empty_union_induction : ∀ {X : Type u_2} [inst : TopologicalSpace X] {p : (s : Set X) → Topology.IsConstructible s → Prop},
  (∀ (U : Set X) (hUopen : IsOpen U) (hUcomp : IsRetrocompact U), p U ⋯) →
    (∀ (s : Set X) (hs : Topology.IsConstructible s) (t : Set X) (ht : Topology.IsConstructible t),
        p s hs → p t ht → p (s ∪ t) ⋯) →
      (∀ (s : Set X) (hs : Topology.IsConstructible s), p s hs → p sᶜ ⋯) →
        ∀ {s : Set X} (hs : Topology.IsConstructible s), p s hs
-- Lean.Syntax
Lean.Syntax.MonadTraverser.setCur : {m : Type → Type} → [t : Lean.Syntax.MonadTraverser m] → Lean.Syntax → m Unit
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Multiset.prod_map_prod : ∀ {ι : Type u_1} {M : Type u_4} {α : Type u_5} [inst : CommMonoid M] {m : Multiset ι} {s : Finset α} {f : ι → α → M},
  (Multiset.map (fun i => ∏ a ∈ s, f i a) m).prod = ∏ a ∈ s, (Multiset.map (fun i => f i a) m).prod
-- Mathlib.Analysis.Normed.Operator.Basic
SemilinearMapClass.nnbound_of_continuous : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} {𝓕 : Type u_8} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : FunLike 𝓕 E F]
  [RingHomIsometric σ₁₂] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕),
  Continuous ⇑f → ∃ C, 0 < C ∧ ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.zero : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] [VectorBundle 𝕜 F V]
  (cov : CovariantDerivative I F V), ↑cov 0 = 0
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.eball_eq_empty_iff`. -/
EMetric.ball_eq_empty_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, Metric.eball x ε = ∅ ↔ ε = 0
-- Lean.Expr
/-- Return `true` if the given expression is a free variable.  -/
Lean.Expr.isFVar : Lean.Expr → Bool
-- Mathlib.Computability.PartrecCode
Nat.Partrec.rfind' : ∀ {f : ℕ →. ℕ},
  Nat.Partrec f →
    Nat.Partrec
      (Nat.unpaired fun a m =>
        Part.map (fun x => x + m) (Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + m))))
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.isHomogeneous_iff_eq_homogeneousComponent : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {p : ℕ},
  f.IsHomogeneous p ↔ f = (MvPowerSeries.homogeneousComponent p) f
-- Mathlib.AlgebraicGeometry.Normalization
/-- The comparison lemma between the normalization of the pullback to the pullback of the
normalization. This is an isomorphism when `g` is smooth.  -/
AlgebraicGeometry.Scheme.Hom.normalizationPullback : {X S Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ S) →
    (g : Y ⟶ S) →
      [inst : AlgebraicGeometry.QuasiCompact f] →
        [inst_1 : AlgebraicGeometry.QuasiSeparated f] →
          AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.Limits.pullback.snd f g) ⟶
            CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.fromNormalization f) g
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isPrestackFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [F.IsPrestack J] {S : C} (R : CategoryTheory.Presieve S),
  CategoryTheory.Sieve.generate R ∈ J S → F.IsPrestackFor R
-- Mathlib.Algebra.Group.Commute.Units
Commute.units_of_val : ∀ {M : Type u_1} [inst : Monoid M] {u₁ u₂ : Mˣ}, Commute ↑u₁ ↑u₂ → Commute u₁ u₂
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instCoeSortType : (R : Type u) → [inst : Ring R] → [inst_1 : TopologicalSpace R] → CoeSort (TopModuleCat R) (Type v)
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.extend_zero : ∀ {α : Type u_2} {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace α']
  [inst_2 : Zero β] {f : α → β} [T2Space α'],
  HasCompactSupport f → ∀ {g : α → α'}, Continuous g → HasCompactSupport (Function.extend g f 0)
-- Aesop.Tree.Data
Aesop.Rapp.successProbability : Aesop.Rapp → Aesop.Percent
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_finite_of_isCompact_uniformContinuous : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} [inst : UniformSpace X],
  IsCompact F → UniformContinuous T → U ∈ uniformity X → ∀ (n : ℕ), Dynamics.coverMincard T F U n < ⊤
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- the underlying continuous representation of an object in `TopRep k G`  -/
TopRep.ρ : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] →
      [inst_1 : TopologicalSpace k] → [inst_2 : Monoid G] → (self : TopRep k G) → ContRepresentation k G ↑self
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.comap' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [BorelSpace α]
  {mβ : MeasurableSpace β} [inst_3 : TopologicalSpace β] [BorelSpace β] (μ : MeasureTheory.Measure β)
  [H : μ.InnerRegular] {f : α → β}, Topology.IsOpenEmbedding f → (MeasureTheory.Measure.comap f μ).InnerRegular
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (f : E ≅ F),
  (CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso f).functor =
    CategoryTheory.PreOneHypercover.Hom.mapMulticospan f.hom
-- Aesop.BuiltinRules
Aesop.BuiltinRules.heq_iff_eq : ∀ {α : Sort u_1} (x y : α), x ≍ y ↔ x = y
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensRange_comp_of_isIso : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : CategoryTheory.IsIso f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g],
  AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.CategoryStruct.comp f g) =
    AlgebraicGeometry.Scheme.Hom.opensRange g
-- Mathlib.Data.Analysis.Filter
CFilter.mk.congr_simp : ∀ {α : Type u_1} {σ : Type u_2} [inst : PartialOrder α] (f f_1 : σ → α) (e_f : f = f_1) (pt pt_1 : σ),
  pt = pt_1 →
    ∀ (inf inf_1 : σ → σ → σ) (e_inf : inf = inf_1) (inf_le_left : ∀ (a b : σ), f (inf a b) ≤ f a)
      (inf_le_right : ∀ (a b : σ), f (inf a b) ≤ f b),
      { f := f, pt := pt, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right } =
        { f := f_1, pt := pt_1, inf := inf_1, inf_le_left := ⋯, inf_le_right := ⋯ }
-- Mathlib.Analysis.Convex.Integral
/-- If an integrable function `f : α → E` takes values in a convex set `s` and for some set `t` of
positive measure, the average value of `f` over `t` belongs to the interior of `s`, then the average
of `f` over the whole space belongs to the interior of `s`.  -/
Convex.average_mem_interior_of_set : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} [MeasureTheory.IsFiniteMeasure μ],
  Convex ℝ s →
    μ t ≠ 0 →
      (∀ᵐ (x : α) ∂μ, f x ∈ s) →
        MeasureTheory.Integrable f μ → ⨍ (x : α) in t, f x ∂μ ∈ interior s → ⨍ (x : α), f x ∂μ ∈ interior s
-- LeanSearchClient.Basic
leansearch.queries : Lean.Option ℕ
-- Mathlib.Order.Hom.Basic
OrderIso.trans_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ]
  [inst_3 : LE δ] (f : α ≃o β) (g : β ≃o γ) (h : γ ≃o δ), (f.trans g).trans h = f.trans (g.trans h)
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` is a type, then `FreeAddGroup α` is the free additive group generated by `α`.
This is a group equipped with a function `FreeAddGroup.of : α → FreeAddGroup α` which has
the following universal property: if `G` is any group, and `f : α → G` is any function,
then this function is the composite of `FreeAddGroup.of` and a unique group homomorphism
`FreeAddGroup.lift f : FreeAddGroup α →+ G`.

A typical element of `FreeAddGroup α` is a formal sum of
elements of `α` and their formal inverses, quotient by reduction.
For example if `x` and `y` are terms of type `α` then `-x + y + y + x + -y` is a
"typical" element of `FreeAddGroup α`. In particular if `α` is empty
then `FreeAddGroup α` is isomorphic to the trivial group, and if `α` has one term
then `FreeAddGroup α` is isomorphic to `ℤ`.
If `α` has two or more terms then `FreeAddGroup α` is not commutative. 

[Wikidata Q431078](https://www.wikidata.org/wiki/Q431078) -/
FreeAddGroup : Type u → Type u
-- Mathlib.Tactic.Widget.StringDiagram
/-- The horizontal position of a node in a string diagram, counting strings in domains.  -/
Mathlib.Tactic.Widget.StringDiagram.Node.hPosSrc : Mathlib.Tactic.Widget.StringDiagram.Node → ℕ
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.trans_toCoalgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : AddCommMonoid C] [inst_4 : Module R A] [inst_5 : Module R B]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C]
  {e₁₂ : A ≃ₗc[R] B} {e₂₃ : B ≃ₗc[R] C}, ↑(e₁₂.trans e₂₃) = e₂₃.comp ↑e₁₂
-- Mathlib.CategoryTheory.Quotient
/-- The condition that a `HomRel` is stable under postcomposition.  -/
CategoryTheory.HomRel.IsStableUnderPostcomp : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → HomRel C → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformly.hasProd : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {x : β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasProdLocallyUniformly f g → HasProd (fun x_1 => f x_1 x) (g x)
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
HasStrictDerivAt.log : ∀ {f : ℝ → ℝ} {x f' : ℝ}, HasStrictDerivAt f f' x → f x ≠ 0 → HasStrictDerivAt (fun y => Real.log (f y)) (f' / f x) x
-- Mathlib.Order.Disjoint
Codisjoint.mono : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b c d : α},
  b ≤ a → d ≤ c → Codisjoint b d → Codisjoint a c
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Which variables are plugged as arguments to the cost function  -/
ValuedCSP.Term.app : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] → {Γ : ValuedCSP D C} → {ι : Type u_3} → (self : Γ.Term ι) → Fin self.n → ι
-- Init.Data.Int.Basic
/-- Negation of integers, usually accessed via the `-` prefix operator.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
 * `-(6 : Int) = -6`
 * `-(-6 : Int) = 6`
 * `(12 : Int).neg = -12`
 -/
Int.neg : ℤ → ℤ
-- Mathlib.LinearAlgebra.Prod
Submodule.snd_map_fst : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Submodule.map (LinearMap.fst R M M₂) (Submodule.snd R M M₂) = ⊥
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ.inj : ∀ {n n' : Q(ℕ)} {pf : «$n» =Q «$n'».succ} {n'_1 : Q(ℕ)} {pf_1 : «$n» =Q «$n'_1».succ},
  Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ n' pf = Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ n'_1 pf_1 → n' = n'_1
-- Mathlib.RingTheory.TensorProduct.Nontrivial
/-- If `A`, `B` are `R`-algebras, `R` injects into `A` and `B`, and `A` and `B` are domains
(which implies `R` is also a domain), then `A ⊗[R] B` is nontrivial.  -/
Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_isDomain : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B],
  Function.Injective ⇑(algebraMap R A) →
    Function.Injective ⇑(algebraMap R B) → ∀ [IsDomain A] [IsDomain B], Nontrivial (TensorProduct R A B)
-- Init.Data.SInt.Lemmas
Int8.toInt_mod : ∀ (a b : Int8), (a % b).toInt = a.toInt.tmod b.toInt
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Constant multiseries always approximates its attached function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.const : ∀ (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion []), ms.Approximates
-- Mathlib.Data.Int.GCD
_private.Mathlib.Data.Int.GCD.0.Nat.xgcdAux.match_1.eq_1 : ∀ (motive : (n : ℕ) → ((m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → Sort u_1)
  (ih : (m : ℕ) → m < 0 → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
  (h_1 : (ih : (m : ℕ) → m < 0 → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive 0 ih)
  (h_2 : (k : ℕ) → (ih : (m : ℕ) → m < k.succ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive k.succ ih),
  (match 0, ih with
    | 0, ih => h_1 ih
    | k.succ, ih => h_2 k ih) =
    h_1 ih
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.id_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (x : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (X_1 : X), (CategoryTheory.CategoryStruct.id x).snd.app X_1 = CategoryTheory.CategoryStruct.id (x.snd.obj X_1)
-- Init.Data.Option.Attach
Option.toList_unattach : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }}, o.unattach.toList = o.toList.unattach
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCocone_pt : ∀ {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.Cocone F),
  (CategoryTheory.Limits.coneRightOpOfCocone c).pt = Opposite.op c.pt
-- Mathlib.Order.Bounded
Set.Bounded.rel_mono : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop}, Set.Bounded r s → r ≤ r' → Set.Bounded r' s
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsSwap.isCycle : ∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α], f.IsSwap → f.IsCycle
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_zero : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.roots 0 = 0