mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.DefView
Lean.Elab.DefsParsedSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (defs : Array Lean.Elab.DefParsed),
  sizeOf { toSnapshot := toSnapshot, defs := defs } = 1 + sizeOf toSnapshot + sizeOf defs
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.toAddCon : {S : Type u_2} → {M : Type u_3} → [inst : Add M] → [inst_1 : SMul S M] → ModuleCon S M → AddCon M
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.injective_of_ne_zero : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSimpleModule R M] {f : M →ₗ[R] N}, f ≠ 0 → Function.Injective ⇑f
-- Mathlib.Topology.EMetricSpace.Defs
PseudoEMetricSpace.uniformity_edist : ∀ {α : Type u} [self : PseudoEMetricSpace α],
  uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε}
-- Mathlib.Tactic.Widget.StringDiagram
/-- A type for Penrose variables.  -/
Mathlib.Tactic.Widget.StringDiagram.PenroseVar : Type
-- Mathlib.Tactic.NormNum.Result
/-- The result is `-lit` where `lit` is a raw nat literal
and `proof : isInt x (.negOfNat lit)`.  -/
Mathlib.Meta.NormNum.Result.isNegNat : {u : Lean.Level} →
  {α : Q(Type u)} →
    {x : Q(«$α»)} →
      (inst : autoParam Q(Ring «$α») Mathlib.Meta.NormNum.Result.isNegNat._auto_1) →
        (lit : Q(ℕ)) → Q(Mathlib.Meta.NormNum.IsInt «$x» (Int.negOfNat «$lit»)) → Mathlib.Meta.NormNum.Result x
-- Mathlib.Algebra.Algebra.Equiv
/-- If `A₁` is equivalent to `A₂` and `A₁'` is equivalent to `A₂'`, then the type of maps
`A₁ ≃ₐ[R] A₁'` is equivalent to the type of maps `A₂ ≃ₐ[R] A₂'`.

This is the `AlgEquiv` version of `AlgEquiv.arrowCongr`.  -/
AlgEquiv.equivCongr : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      {A₁' : Type uA₁'} →
        {A₂' : Type uA₂'} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A₁] →
              [inst_2 : Semiring A₂] →
                [inst_3 : Semiring A₁'] →
                  [inst_4 : Semiring A₂'] →
                    [inst_5 : Algebra R A₁] →
                      [inst_6 : Algebra R A₂] →
                        [inst_7 : Algebra R A₁'] →
                          [inst_8 : Algebra R A₂'] → (A₁ ≃ₐ[R] A₂) → (A₁' ≃ₐ[R] A₂') → (A₁ ≃ₐ[R] A₁') ≃ A₂ ≃ₐ[R] A₂'
-- Mathlib.Topology.ContinuousOn
continuousOn_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  ContinuousOn f Set.univ ↔ Continuous f
-- Init.Data.Order.Lemmas
Std.instLawfulOrderLeftLeaningMinOfIsLinearOrderOfLawfulOrderInf : ∀ {α : Type u} [inst : LE α] [inst_1 : Min α] [Std.IsLinearOrder α] [Std.LawfulOrderInf α],
  Std.LawfulOrderLeftLeaningMin α
-- Mathlib.Analysis.RCLike.Inner
RCLike.abs_wInner_le : ∀ {ι : Type u_1} [inst : Fintype ι] {w f g : ι → ℝ}, 0 ≤ w → |⟪f, g⟫_[ℝ, w]| ≤ ⟪|f|, |g|⟫_[ℝ, w]
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.card_mul_cast_subConst : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑A.card * ↑(A.subConst B) = ↑(A - B).card
-- Mathlib.Analysis.RCLike.Basic
RCLike.abs_im_le_norm : ∀ {K : Type u_1} [inst : RCLike K] (z : K), |RCLike.im z| ≤ ‖z‖
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf_map : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X Y : Cᵒᵖ}
  (f : X ⟶ Y),
  (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf data G₀).map f =
    CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ f.unop
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_iff_exists_add : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [CanonicallyOrderedAdd α] {a b : α}, a ≤ b ↔ ∃ c, b = a + c
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuousWithinAt.inf : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α} {a : α},
  LowerSemicontinuousWithinAt f s a →
    LowerSemicontinuousWithinAt g s a → LowerSemicontinuousWithinAt (fun x => min (f x) (g x)) s a
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instMul : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module A V] → (ρ : Representation A G V) → Mul (ρ.IntertwiningMap ρ)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_pow : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R) (n : ℕ), (p ^ n).roots = n • p.roots
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (w : D) {x y z : C} (f : x ⟶ y) (g : y ⟶ z) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj w z ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight w
        (CategoryTheory.CategoryStruct.comp f g))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight w f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight w g)
        h)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, k ∈ Std.TreeMap.ofList l cmp ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.isConnected_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y),
  IsConnected (⇑h '' s) ↔ IsConnected s
-- Mathlib.Algebra.Quandle
/-- The homomorphism property of a Shelf Homomorphism  -/
ShelfHom.map_act' : ∀ {S₁ : Type u_1} {S₂ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] (self : ShelfHom S₁ S₂) {x y : S₁},
  self.toFun (Shelf.act x y) = Shelf.act (self.toFun x) (self.toFun y)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  {H : Type u_8} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H]
  [inst_4 : NormedField 𝕜] [inst_5 : NormedField 𝕜₂] [inst_6 : NormedField 𝕜₃] [inst_7 : NormedField 𝕜₄]
  [inst_8 : Module 𝕜 E] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₃ G] [inst_11 : Module 𝕜₄ H]
  [inst_12 : TopologicalSpace E] [inst_13 : TopologicalSpace F] [inst_14 : TopologicalSpace G]
  [inst_15 : TopologicalSpace H] [inst_16 : IsTopologicalAddGroup G] [inst_17 : IsTopologicalAddGroup H]
  [inst_18 : ContinuousConstSMul 𝕜₃ G] [inst_19 : ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
  [inst_20 : RingHomInvPair σ₁₂ σ₂₁] [inst_21 : RingHomInvPair σ₂₁ σ₁₂] [inst_22 : RingHomInvPair σ₃₄ σ₄₃]
  [inst_23 : RingHomInvPair σ₄₃ σ₃₄] [inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [inst_30 : RingHomIsometric σ₁₂]
  [inst_31 : RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : ⋯), ⋯
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.size_inner : ∀ {α : Type u} {β : α → Type v} {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).size = sz
-- Mathlib.Topology.Irreducible
irreducibleComponents_eq_maximals_closed : ∀ (X : Type u_3) [inst : TopologicalSpace X],
  irreducibleComponents X = {s | Maximal (fun x => IsClosed x ∧ IsIrreducible x) s}
-- Init.Data.BitVec.Lemmas
BitVec.le_toInt_mul_toInt : ∀ {w : ℕ} {x y : BitVec w}, -2 ^ (w * 2 - 2) ≤ x.toInt * y.toInt
-- Mathlib.Topology.Order.WithTop
WithBot.sumHomeomorph.eq_1 : ∀ (ι : Type u_1) [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : OrderBot ι],
  WithBot.sumHomeomorph ι =
    { toFun := fun x => if h : x = ⊥ then Sum.inr () else Sum.inl x.unbotA,
      invFun := fun x =>
        match x with
        | Sum.inl i => ↑i
        | Sum.inr PUnit.unit => ⊥,
      left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Data.Semiquot
/-- Construct a `Semiquot α` from `h : a ∈ s` where `s : Set α`.  -/
Semiquot.mk : {α : Type u_1} → {a : α} → {s : Set α} → a ∈ s → Semiquot α
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
/-- Circle average of the function `fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` that appears
in Cartan's formula, in the case where `f` has a pole at the origin.
 -/
ValueDistribution.circleAverage_log_norm_meromorphicTrailingCoeffAt_of_meromorphicOrderAt_lt_zero : ∀ {f : ℂ → ℂ},
  meromorphicOrderAt f 0 < 0 →
    Real.circleAverage (fun a => Real.log ‖meromorphicTrailingCoeffAt (fun x => f x - a) 0‖) 0 1 =
      Real.log ‖meromorphicTrailingCoeffAt f 0‖
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.iff_flat_and_proper_ideal : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔ Module.Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → I • ⊤ ≠ ⊤
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_const_add_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [MeasureTheory.IsFiniteMeasure μ] {f : α → β} {c : β},
  MeasureTheory.Integrable (fun x => c + f x) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- We have that `η ^ 2 + η + 1 = 0`.  -/
IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3), ↑⋯.unit ^ 2 + ↑⋯.unit + 1 = 0
-- Mathlib.Computability.Reduce
equivalence_of_oneOneEquiv : ∀ {α : Type u_1} [inst : Primcodable α], Equivalence OneOneEquiv
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.unitOfList_eq_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α},
  Std.ExtDTreeMap.Const.unitOfList l cmp = List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.InlayHintClientCapabilities
-- Mathlib.Tactic.DeriveTraversable
/-- Similar to `mkInstanceName`, but for a `Expr` type.  -/
Mathlib.Deriving.Traversable.mkInstanceNameForTypeExpr : Lean.Expr → Lean.Elab.TermElabM Lean.Name
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- Nondegenerate `d`-dimensional simplices of the standard simplex `Δ[n]`
identify to order embeddings `Fin (d + 1) ↪o Fin (n + 1)`.  -/
SSet.stdSimplex.nonDegenerateEquiv : {n d : ℕ} → ↑((SSet.stdSimplex.obj { len := n }).nonDegenerate d) ≃ (Fin (d + 1) ↪o Fin (n + 1))
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae.congr_simp : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  (μ μ_1 : F), μ = μ_1 → MeasureTheory.ae μ = MeasureTheory.ae μ_1
-- Mathlib.Dynamics.Ergodic.Ergodic
PreErgodic.mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) PreErgodic._auto_1},
  (∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → Filter.EventuallyConst s (MeasureTheory.ae μ)) → PreErgodic f μ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The unoriented angles at `p₂` between `p₁` and `p₃`, and between `p₃` and `p₄`, are equal if
and only if the oriented angles are equal (`p₃` lies on the angle bisector) or one of `p₁` and `p₄`
is weakly between `p₂` and the other.  -/
EuclideanGeometry.angle_eq_iff_oangle_eq_or_wbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P},
  p₁ ≠ p₂ →
    p₄ ≠ p₂ →
      (EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₃ p₂ p₄ ↔
        EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄ ∨ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.sInf_eq : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α] {s : Set (WithTop α)},
  ¬s ⊆ {⊤} → BddBelow s → sInf s = ↑(sInf (WithTop.some ⁻¹' s))
-- Mathlib.GroupTheory.Coset.Basic
/-- The natural embedding `H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H`.  -/
Subgroup.quotientiInfSubgroupOfEmbedding : {α : Type u_1} →
  [inst : Group α] →
    {ι : Type u_2} →
      (f : ι → Subgroup α) → (H : Subgroup α) → ↥H ⧸ (⨅ i, f i).subgroupOf H ↪ (i : ι) → ↥H ⧸ (f i).subgroupOf H
-- Mathlib.MeasureTheory.Group.Measure
/-- An alternative way to prove that `μ` is left invariant under multiplication.  -/
MeasureTheory.forall_measure_preimage_mul_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G),
  (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => g * h) ⁻¹' A) = μ A) ↔ μ.IsMulLeftInvariant
-- Init.Prelude
/-- A string name. The name `Lean.Meta.run` is represented as
```lean
.str (.str (.str .anonymous "Lean") "Meta") "run"
```
 -/
Lean.Name.str : Lean.Name → String → Lean.Name
-- Mathlib.Algebra.Lie.Submodule
Submodule.exists_lieSubmodule_coe_eq_iff : ∀ {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] (p : Submodule R M), (∃ N, ↑N = p) ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- `smoothingSeminormSeq` is bounded below (by zero).  -/
smoothingSeminormSeq_bddBelow : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) (x : R), BddBelow (Set.range fun n => μ (x ^ ↑n) ^ (1 / ↑↑n))
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
left_le_midpoint : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E}, a ≤ midpoint k a b ↔ a ≤ b
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.startPos_cast : ∀ {s t : String.Slice} (hst : s.copy = t.copy) {st : String.Slice.Pattern.SearchStep s},
  (String.Slice.Pattern.SearchStep.cast hst st).startPos = st.startPos.cast hst
-- Init.System.IOError
IO.Error.noSuchThing.inj : ∀ {filename : Option String} {osCode : UInt32} {details : String} {filename_1 : Option String} {osCode_1 : UInt32}
  {details_1 : String},
  IO.Error.noSuchThing filename osCode details = IO.Error.noSuchThing filename_1 osCode_1 details_1 →
    filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- This may be a more useful form of `ReflPrefunctor.ext`.  -/
CategoryTheory.ReflPrefunctor.ext' : ∀ {V W : Type u} [inst : CategoryTheory.ReflQuiver V] [inst_1 : CategoryTheory.ReflQuiver W] {F G : V ⥤rq W}
  (h_obj : ∀ (X : V), F.obj X = G.obj X), (∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯) → F = G
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_power_sum : ∀ {ι : Type u} (a : Cardinal.{v}) (f : ι → Cardinal.{v}),
  Cardinal.lift.{u, v} a ^ Cardinal.sum f = Cardinal.prod fun i => a ^ f i
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.mdifferentiable_denom : ∀ (g : GL (Fin 2) ℝ), MDiff fun τ => UpperHalfPlane.denom g ↑τ
-- Init.Data.String.Basic
String.Pos.le_of_lt : ∀ {s : String} {p q : s.Pos}, p < q → p ≤ q
-- Std.Http.Data.URI.Basic
/-- Optional user information (username and password).
 -/
Std.Http.URI.Authority.userInfo : Std.Http.URI.Authority → Option Std.Http.URI.UserInfo
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.condition_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (t : CategoryTheory.Limits.PullbackCone f g),
  t.π.app CategoryTheory.Limits.WalkingCospan.one = CategoryTheory.CategoryStruct.comp t.fst f
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- **Alias** of `Matroid.IsRkFinite.sdiff_singleton_iff`. -/
Matroid.IsRkFinite.diff_singleton_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α}, M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.ComposableArrows.Precomp.map.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) (isLt isLt_1 : 0 < n + 1 + 1) (x_3 : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩),
  CategoryTheory.ComposableArrows.Precomp.map F f ⟨0, isLt⟩ ⟨0, isLt_1⟩ x_3 = CategoryTheory.CategoryStruct.id X
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.exists_eccent_eq_ediam_of_finite : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α], ∃ u, G.eccent u = G.ediam
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.tensorObj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F G : CategoryTheory.Functor C D} {X Y : C} {f : X ⟶ Y},
  (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).map f =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (G.map f)
-- Mathlib.Probability.Martingale.Upcrossing
/-- **Doob's upcrossing estimate**: given a real-valued discrete submartingale `f` and real
values `a` and `b`, we have `(b - a) * 𝔼[upcrossingsBefore a b f N] ≤ 𝔼[(f N - a)⁺]` where
`upcrossingsBefore a b f N` is the number of times the process `f` crossed from below `a` to above
`b` before the time `N`.  -/
MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ] (a b : ℝ),
  MeasureTheory.Submartingale f ℱ μ →
    ∀ (N : ℕ),
      (b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The weighted sum, added to the base point, is independent of the
base point when the sum of the weights is 1.  -/
Finset.weightedVSubOfPoint_vadd_eq_of_sum_eq_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
  ∑ i ∈ s, w i = 1 → ∀ (b₁ b₂ : P), (s.weightedVSubOfPoint p b₁) w +ᵥ b₁ = (s.weightedVSubOfPoint p b₂) w +ᵥ b₂
-- Mathlib.Topology.Algebra.Group.Basic
continuous_div_right' : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Div G] [ContinuousDiv G] (a : G), Continuous fun x => x / a
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.quot_mk_eq_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  (x : M), Quot.mk (⇑p.quotientRel) x = Submodule.Quotient.mk x
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroNatCiOfNatInt : Lean.Grind.ToInt.Zero ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instInfSet.eq_1 : ∀ (M : Type u_1) [inst : MulOneClass M],
  SaturatedSubmonoid.instInfSet M =
    { sInf := fun f => { carrier := ⋂ s ∈ f, ↑s, mul_mem' := ⋯, one_mem' := ⋯, mulSaturated := ⋯ } }
-- Lean.Expr
/-- A lambda abstraction (aka anonymous functions). It introduces a new binder for
variable `x` in scope for the lambda body.

For example, the expression `fun x : Nat => x` is represented as
```
Expr.lam `x (.const `Nat []) (.bvar 0) .default
```
 -/
Lean.Expr.lam : Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
-- Std.Internal.UV.UDP
/-- Enables or disables multicast loopback for a UDP socket.
 -/
Std.Internal.UV.UDP.Socket.setMulticastLoop : Std.Internal.UV.UDP.Socket → Bool → IO Unit
-- Mathlib.Data.Int.Bitwise
Int.xor.eq_4 : ∀ (m n : ℕ), (Int.negSucc m).xor (Int.negSucc n) = ↑(m ^^^ n)
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The Laplacian defined by iterated `lineDerivOp` as a continuous linear map.  -/
LineDeriv.laplacianCLM : (R : Type u_4) →
  (E : Type u_6) →
    (V₁ : Type u_8) →
      {V₂ : Type u_9} →
        {V₃ : Type u_10} →
          [inst : LineDeriv E V₁ V₂] →
            [inst_1 : LineDeriv E V₂ V₃] →
              [inst_2 : AddCommGroup V₁] →
                [inst_3 : AddCommGroup V₂] →
                  [inst_4 : AddCommGroup V₃] →
                    [inst_5 : NormedAddCommGroup E] →
                      [inst_6 : InnerProductSpace ℝ E] →
                        [FiniteDimensional ℝ E] →
                          [inst_8 : CommRing R] →
                            [inst_9 : Module R V₁] →
                              [inst_10 : Module R V₂] →
                                [inst_11 : Module R V₃] →
                                  [inst_12 : TopologicalSpace V₁] →
                                    [inst_13 : TopologicalSpace V₂] →
                                      [inst_14 : TopologicalSpace V₃] →
                                        [IsTopologicalAddGroup V₃] →
                                          [LineDerivAdd E V₁ V₂] →
                                            [LineDerivSMul R E V₁ V₂] →
                                              [ContinuousLineDeriv E V₁ V₂] →
                                                [LineDerivAdd E V₂ V₃] →
                                                  [LineDerivSMul R E V₂ V₃] →
                                                    [ContinuousLineDeriv E V₂ V₃] → V₁ →L[R] V₃
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- **Alias** of `ModularForm.cuspFunction_smul`. -/
ModularFormClass.cuspFunction_smul : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (a : ℂ) (f : F) [ModularFormClass F Γ k],
        UpperHalfPlane.cuspFunction h (a • ⇑f) = a • UpperHalfPlane.cuspFunction h ⇑f
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_apply_prime : ∀ {p : ℕ}, Nat.Prime p → ArithmeticFunction.cardDistinctFactors p = 1
-- Mathlib.CategoryTheory.Filtered.Final
/-- `StructuredArrow.map` is final if the functor `T` is final and its domain is filtered.  -/
CategoryTheory.StructuredArrow.final_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFiltered C] {S S' : D} (f : S ⟶ S') (T : CategoryTheory.Functor C D) [T.Final],
  (CategoryTheory.StructuredArrow.map f).Final
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.range_enumOrd : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → Set.range (Ordinal.enumOrd s) = s
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.nontrivial_of_nonZeroDivisors : ∀ {R : Type u_1} [inst : MonoidWithZero R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] [Nontrivial R],
  S ≤ nonZeroDivisors R → Nontrivial (OreLocalization S R)