mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
LinearIsometryEquiv.coe_symm_toMeasurableEquiv : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : MeasurableSpace F] [inst_7 : BorelSpace F] (f : E ≃ₗᵢ[ℝ] F), ⇑f.toMeasurableEquiv.symm = ⇑f.symm
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- The equivalence between the projectivization and the
collection of subspaces of dimension 1.  -/
Projectivization.equivSubmodule : (K : Type u_1) →
  (V : Type u_2) →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Projectivization K V ≃ { H // Module.finrank K ↥H = 1 }
-- Mathlib.RingTheory.Congruence.Star
RingConGen.Rel.star : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R] {r : R → R → Prop},
  (∀ (a b : R), r a b → r (star a) (star b)) → ∀ ⦃a b : R⦄, RingConGen.Rel r a b → RingConGen.Rel r (star a) (star b)
-- Mathlib.Tactic.Linter.EmptyLine
/-- The "emptyLine" linter emits a warning on empty lines inside a command, but outside of a
doc-string/module-doc.

The linter is only active when there are no other warnings, so as to not add noise when developing
incomplete proofs.
 -/
Mathlib.Linter.linter.style.emptyLine : Lean.Option Bool
-- Mathlib.RingTheory.Congruence.Hom
RingCon.coe_comapQuotientEquivRangeₐ_symm_mk : ∀ {M : Type u_1} {N : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring N] [inst_4 : Algebra R N] (c : RingCon M) (f : N →ₐ[R] M) (x : N) {d : RingCon N}
  (h : d = c.comap f), (c.comapQuotientEquivRangeₐ f h).symm ⟨↑(f x), ⋯⟩ = ↑x
-- Init.Data.Nat.Basic
Nat.two_pos : 0 < 2
-- Mathlib.Order.Circular
not_sbtw_of_btw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬sbtw c b a
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.isIso_base : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f], CategoryTheory.IsIso f.base
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.has_succ_of_type_succ_lt : ∀ {α : Type u_4} {r : α → α → Prop} [wo : IsWellOrder α r],
  (∀ a < Ordinal.type r, Order.succ a < Ordinal.type r) → ∀ (x : α), ∃ y, r x y
-- Mathlib.CategoryTheory.Sites.Closed
/-- If `S` is `J₁`-closed, then `S` covers exactly the arrows it contains.  -/
CategoryTheory.GrothendieckTopology.covers_iff_mem_of_isClosed : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
  {S : CategoryTheory.Sieve X}, J₁.IsClosed S → ∀ {Y : C} (f : Y ⟶ X), J₁.Covers S f ↔ S.arrows f
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasProd_subtype_comap_iff_of_mulSupport_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α}
  {a : α} {s : Set β},
  Function.mulSupport f ⊆ s →
    (HasProd (f ∘ Subtype.val) a (L.comap (Function.Embedding.subtype fun x => x ∈ s)) ↔ HasProd f a L)
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} [inst_3 : CategoryTheory.Preadditive C]
  [∀ (a : M), (CategoryTheory.shiftFunctor C a).Additive] {a b c : M} (α : CategoryTheory.ShiftedHom X Y a)
  (β : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c), α.comp (-β) h = -α.comp β h
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.mkRBSet_eq : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering}, RBTree.mkRBMap α β cmp = ∅
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  {f : NormedAddGroupHom V W}, f.NormNoninc ↔ ‖f‖ ≤ 1
-- Mathlib.GroupTheory.Perm.Fin
Fin.coe_cycleRange_of_lt : ∀ {n : ℕ} {i j : Fin n}, i < j → ↑(j.cycleRange i) = ↑i + 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_map : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] [Std.LawfulEqOrd α] {f : α → β → γ} {k : α} {fallback : γ},
  t.WF →
    Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.map f t) k fallback =
      (Option.map (f k) (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.piecewise : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} [inst : TopologicalSpace β] {s : Set α}
  {x : DecidablePred fun x => x ∈ s},
  MeasurableSet s →
    MeasureTheory.StronglyMeasurable f →
      MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (s.piecewise f g)
-- Mathlib.Algebra.Tropical.Basic
Tropical.instDecidableEq : {R : Type u} → [DecidableEq R] → DecidableEq (Tropical R)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.continuousAt_arg : ∀ {x : ℂ}, x ∈ Complex.slitPlane → ContinuousAt Complex.arg x
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.coe_set_eq : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L₁' L₂' : LieRinehartSubalgebra A L), ↑L₁' = ↑L₂' ↔ L₁' = L₂'
-- Mathlib.Topology.Compactness.Lindelof
/-- A continuous image of a Lindelöf set is a Lindelöf set.  -/
IsLindelof.image_of_continuousOn : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  IsLindelof s → ContinuousOn f s → IsLindelof (f '' s)
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- Möbius inversion for functions to a `Ring`, where the equalities only hold on a well-behaved
set.  -/
ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on : ∀ {R : Type u_1} [inst : NonAssocRing R] {f g : ℕ → R} (s : Set ℕ),
  (∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) →
    ((∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔
      ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * g x.2 = f n)
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.exists_null_frontiers_thickening : ∀ {Ω : Type u_1} [inst : PseudoMetricSpace Ω] [inst_1 : MeasurableSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (s : Set Ω),
  ∃ rs, Filter.Tendsto rs Filter.atTop (nhds 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) s)) = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_mul_inter_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemigroup α] {s t : Finset α}, (s ∪ t) * (s ∩ t) ⊆ s * t
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.monomial_smul_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ℕ) (r : R)
  (g : PolynomialModule R M) (n : ℕ), ((Polynomial.monomial i) r • g).coeff n = if i ≤ n then r • g.coeff (n - i) else 0
-- Mathlib.Analysis.Calculus.FDeriv.Pow
_private.Mathlib.Analysis.Calculus.FDeriv.Pow.0.aux_sum_eq_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E} (n : ℕ), ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f' = (n • f x ^ (n - 1)) • f'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_cos_eq_of_two_zsmul_eq : ∀ {θ ψ : Real.Angle}, 2 • θ = 2 • ψ → |θ.cos| = |ψ.cos|
-- Mathlib.CategoryTheory.Galois.Examples
/-- The category of finite `G`-sets is a `GaloisCategory`.  -/
CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCat : ∀ (G : Type u) [inst : Group G], CategoryTheory.GaloisCategory (Action FintypeCat G)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_injective : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, Function.Injective SimpleGraph.Walk.support
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.ordConnected : ∀ {α : Type v} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {s : Set α},
  IsPreconnected s → s.OrdConnected
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.preorder : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → Preorder (CategoryTheory.ThinSkeleton C)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.coe_mul_star_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(pinGroup Q)), ↑x * ↑(star x) = 1
-- Mathlib.Order.Filter.TendstoCofinite
Filter.tendstoCofinite_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Filter.TendstoCofinite f
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.OuterRegular.comap' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {mβ : MeasurableSpace β}
  [inst_2 : TopologicalSpace β] (μ : MeasureTheory.Measure β) [μ.OuterRegular] {f : α → β},
  Continuous f → MeasurableEmbedding f → (MeasureTheory.Measure.comap f μ).OuterRegular
-- Mathlib.NumberTheory.LSeries.Basic
/-- If `f` is bounded, then its `LSeries` is summable at `s` when `re s > 1`.  -/
LSeriesSummable_of_bounded_of_one_lt_re : ∀ {f : ℕ → ℂ} {m : ℝ}, (∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ m) → ∀ {s : ℂ}, 1 < s.re → LSeriesSummable f s
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.IsIntegral.isLocalHom : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.IsIntegral → Function.Injective ⇑f → IsLocalHom f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ},
  CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeLeftOp c),
            map := fun {Y X} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun c => CategoryTheory.Limits.coneLeftOpOfCocone (Opposite.unop c),
          map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
-- Mathlib.Analysis.Normed.Group.Ultra
/-- **Alias** of `IsUltrametricDist.exists_norm_finsetSum_le_of_nonempty`.

---

Given a function `f : ι → M` and a nonempty finite set `t ⊆ ι`, we can always find
`i ∈ t` such that `‖∑ j ∈ t, f j‖ ≤ ‖f i‖`.  -/
IsUltrametricDist.exists_norm_finset_sum_le_of_nonempty : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {t : Finset ι},
  t.Nonempty → ∀ (f : ι → M), ∃ i ∈ t, ‖∑ j ∈ t, f j‖ ≤ ‖f i‖
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Negating the second vector passed to `oangle` adds `π` to the angle.  -/
Orientation.oangle_neg_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, x ≠ 0 → y ≠ 0 → o.oangle x (-y) = o.oangle x y + ↑Real.pi
-- Mathlib.Probability.Process.PartitionFiltration
/-- A filtration built from the measurable spaces generated by `countablePartition α n` for
all `n : ℕ`.  -/
ProbabilityTheory.countableFiltration : (α : Type u_2) → [m : MeasurableSpace α] → [MeasurableSpace.CountablyGenerated α] → MeasureTheory.Filtration ℕ m
-- Mathlib.Topology.LocallyClosed
coborder_eq_compl_frontier_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, coborder s = (frontier s)ᶜ ↔ IsOpen s
-- Mathlib.Algebra.Order.SuccPred
Order.sub_one_lt_iff : ∀ {α : Type u_1} {x y : α} [inst : LinearOrder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α] [NoMinOrder α],
  x - 1 < y ↔ x ≤ y
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
/-- If a sequence of continuous functions `f i x` on an open compact `K` have norms eventually
bounded by a summable function, then `∏' i, (1 + f i x)` is uniformly convergent on `K`.  -/
Summable.hasProdUniformlyOn_one_add : ∀ {α : Type u_1} {ι : Type u_2} {K : Set α} {u : ι → ℝ} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R]
  [CompleteSpace R] [inst_3 : TopologicalSpace α] {f : ι → α → R},
  IsCompact K →
    Summable u →
      (∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) →
        (∀ (i : ι), ContinuousOn (f i) K) →
          HasProdUniformlyOn (fun i x => 1 + f i x) (fun x => ∏' (i : ι), (1 + f i x)) K
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_map₂ : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C) {x y : B} {f g : x ⟶ y} (η : f ⟶ g),
  F.toStrictlyUnitaryLaxFunctor.map₂ η = F.map₂ η
-- Init.Data.Vector.Algebra
Vector.getElem_sub : ∀ {α : Type u_1} {n : ℕ} [inst : Sub α] (xs ys : Vector α n) (i : ℕ) (h : i < n), (xs - ys)[i] = xs[i] - ys[i]
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `fallback` if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryGTD : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Sigma β → (a : α) × β a
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
_private.Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence.0.AlgebraicTopology.DoldKan.homotopyPToId.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (q : ℕ) (h_1 : Unit → motive 0) (h_2 : (q : ℕ) → motive q.succ),
  (match q.succ with
    | 0 => h_1 ()
    | q.succ => h_2 q) =
    h_2 q
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termF₄ : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.Instances.Real
interior_range_modelWithCornersEuclideanHalfSpace : ∀ (n : ℕ) [inst : NeZero n], interior (Set.range ↑(modelWithCornersEuclideanHalfSpace n)) = {y | 0 < y.ofLp 0}
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.instFloorRing : {K : Type u_1} →
  [inst : LinearOrder K] →
    [inst_1 : Field K] → [inst_2 : IsOrderedRing K] → FloorRing (ArchimedeanClass.FiniteElement K)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.comap_upperCentralSeries`. -/
comap_upperCentralSeries : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (e : H ≃* G) (n : ℕ),
  Subgroup.comap (↑e) (Subgroup.upperCentralSeries G n) = Subgroup.upperCentralSeries H n
-- Mathlib.Tactic.Linarith.NNRealPreprocessor
/-- If `e` is of the form `((x : ℝ≥0) : ℝ)`, `NNReal.toReal e` returns `x`.  -/
Mathlib.Tactic.Linarith.getNNRealToRealArg? : Lean.Expr → Option Lean.Expr
-- Init.Data.Subtype.Order
Subtype.instLT : {α : Type u} → [LT α] → {P : α → Prop} → LT (Subtype P)
-- Mathlib.Order.Lattice
/-- Pointwise infimum of two antitone functions is an antitone function.  -/
Antitone.inf : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeInf β] {f g : α → β},
  Antitone f → Antitone g → Antitone (f ⊓ g)
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.ofPersistentHashSet : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashSet α → Aesop.UnorderedArraySet α
-- Mathlib.FieldTheory.Fixed
FixedPoints.normal : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [Finite G],
  Normal (↥(FixedPoints.subfield G F)) F
-- Mathlib.Algebra.Order.IsBotOne
IsBotOneClass.mk : ∀ {α : Type u_1} [inst : LE α] [inst_1 : One α], IsBot 1 → IsBotOneClass α
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.isSome_least? : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α] [hn : Nonempty α], Std.PRange.least?.isSome = true
-- Mathlib.Tactic.Simps.Basic
/-- simplify the left-hand side of the generated lemmas using `dsimp`.  -/
Simps.Config.dsimpLhs : Simps.Config → Bool
-- Mathlib.Data.Multiset.ZeroCons
Multiset.ssubset_cons : ∀ {α : Type u_1} {s : Multiset α} {a : α}, a ∉ s → s ⊂ a ::ₘ s
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_refl : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x : AlgebraicGeometry.Scheme.Pullback.Triplet f g},
  AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯ = CategoryTheory.Iso.refl x.tensor
-- Mathlib.Data.Finset.Image
Function.Embedding.trans.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α ↪ β) (g : β ↪ γ), f.trans g = { toFun := ⇑g ∘ ⇑f, inj' := ⋯ }
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instSemilatticeInfFiniteIndexNormalSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  FiniteIndexNormalSubgroup.instSemilatticeInfFiniteIndexNormalSubgroup =
    Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.Germ
Germ.coe_prod : ∀ {α : Type u_4} (l : Filter α) (R : Type u_5) [inst : CommMonoid R] {ι : Type u_6} (f : ι → α → R) (s : Finset ι),
  ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.asEmptyCocone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), (CategoryTheory.Limits.asEmptyCocone X).pt = X
-- Mathlib.Computability.Primrec.Basic
Primrec.subtype_val : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p] {hp : PrimrecPred p},
  Primrec Subtype.val
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Data.Finite.Defs
/-- A type is said to be infinite if it is not finite. Note that `Infinite α` is equivalent to
`IsEmpty (Fintype α)` or `IsEmpty (Finite α)`.  -/
Infinite : Sort u_3 → Prop
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.mk_trans : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ x₂ : X} (P₀ : Path x₀ x₁) (P₁ : Path x₁ x₂),
  Path.Homotopic.Quotient.mk (P₀.trans P₁) = (Path.Homotopic.Quotient.mk P₀).trans (Path.Homotopic.Quotient.mk P₁)
-- Mathlib.Analysis.Normed.Module.RCLike.Real
/-- In a nontrivial real normed space, a sphere is nonempty if and only if its radius is
nonnegative.  -/
NormedSpace.sphere_nonempty : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E] {x : E} {r : ℝ},
  (Metric.sphere x r).Nonempty ↔ 0 ≤ r
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofInjective_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [inst_4 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_5 : RingHomInvPair σ₂₁ σ₁₂] {h : Function.Injective ⇑f} (x : M), ↑((LinearEquiv.ofInjective f h) x) = f x
-- Mathlib.Data.Nat.Squarefree
Nat.prod_primeFactors_of_squarefree : ∀ {n : ℕ}, Squarefree n → ∏ p ∈ n.primeFactors, p = n
-- Mathlib.Data.Set.Countable
Set.subset_range_enumerate : ∀ {α : Type u} {s : Set α} (h : s.Countable) (default : α), s ⊆ Set.range (Set.enumerateCountable h default)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_union_Ici_eq_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → Set.Ioo a b ∪ Set.Ici b = Set.Ioi a
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.closure_nsmul_anti : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {m n : ℕ},
  m ∣ n → AddSubgroup.closure (n • s) ≤ AddSubgroup.closure (m • s)
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr : Lean.FromJson Lean.Lsp.RefIdent.RefIdentJsonRepr
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_le_iff : ∀ {R : Type u_2} [inst : NonAssocRing R] {S₁ : Subring R} {S₂ : Subring Rᵐᵒᵖ}, S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [inst_4 : CategoryTheory.Limits.HasProduct X]
  [inst_5 : CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Fibration (f i)]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)],
  HomotopicalAlgebra.Fibration (CategoryTheory.Limits.Pi.map f)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_apply_smul_mem_of_le_comap' : ∀ {R : Type u} {A : Type z} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {q : Submodule R M} {m : M} [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M],
  m ∈ q → ∀ (p : Polynomial R) (a : A), q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q → (Polynomial.aeval a) p • m ∈ q
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by swapping components.  -/
ContinuousAddMonoidHom.swap : (A : Type u_2) →
  (B : Type u_3) →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → A × B →ₜ+ B × A
-- Mathlib.MeasureTheory.SetSemiring
/-- The set of open-closed intervals is a semi-ring of sets.  -/
MeasureTheory.IsSetSemiring.Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [Nonempty α], MeasureTheory.IsSetSemiring {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
-- Mathlib.Data.List.Iterate
List.iterate_add : ∀ {α : Type u_1} (f : α → α) (a : α) (m n : ℕ),
  List.iterate f a (m + n) = List.iterate f a m ++ List.iterate f (f^[m] a) n
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.mk : ℕ →
  Lean.Expr →
    Lean.Level →
      Lean.Expr →
        Option Lean.Expr → Option Lean.Expr → Option Lean.Expr → Option Lean.Expr → Lean.Meta.Sym.Arith.Semiring
-- Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
/-- Returns `some p` if `e` is of the form `Decidable p`  -/
_private.Lean.Meta.Tactic.Grind.MarkNestedSubsingletons.0.Lean.Meta.Grind.isDecidable : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.map_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} {f'' : X'' ⟶ Z''} {g'' : Y'' ⟶ Z''} (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y')
  (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z') (j₃ : Z' ⟶ Z'') [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' g'] [inst_3 : CategoryTheory.Limits.HasPullback f'' g'']
  (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
  (e₃ : CategoryTheory.CategoryStruct.comp f' j₃ = CategoryTheory.CategoryStruct.comp j₁ f'')
  (e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₂ g''),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
      (CategoryTheory.Limits.pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) =
    CategoryTheory.Limits.pullback.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₁ j₁)
      (CategoryTheory.CategoryStruct.comp i₂ j₂) (CategoryTheory.CategoryStruct.comp i₃ j₃) ⋯ ⋯
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.divByMonic_eq_div : ∀ {R : Type u} [inst : Field R] {q : Polynomial R} (p : Polynomial R), q.Monic → p /ₘ q = p / q