mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h₀ : S₁.X₁ ⟶ S₂.X₁)
  (h₀_f :
    autoParam (CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) CategoryTheory.ShortComplex.Homotopy.h₀_f._autoParam)
  (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ :
    autoParam (CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) CategoryTheory.ShortComplex.Homotopy.g_h₃._autoParam)
  (comm₁ :
    autoParam (φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f h₁ + h₀ + φ₂.τ₁)
      CategoryTheory.ShortComplex.Homotopy.comm₁._autoParam)
  (comm₂ :
    autoParam (φ₁.τ₂ = CategoryTheory.CategoryStruct.comp S₁.g h₂ + CategoryTheory.CategoryStruct.comp h₁ S₂.f + φ₂.τ₂)
      CategoryTheory.ShortComplex.Homotopy.comm₂._autoParam)
  (comm₃ :
    autoParam (φ₁.τ₃ = h₃ + CategoryTheory.CategoryStruct.comp h₂ S₂.g + φ₂.τ₃)
      CategoryTheory.ShortComplex.Homotopy.comm₃._autoParam)
  (h₀_1 : S₁.X₁ ⟶ S₂.X₁)
  (h₀_f_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h₀_1 S₂.f = 0) CategoryTheory.ShortComplex.Homotopy.h₀_f._autoParam)
  (h₁_1 : S₁.X₂ ⟶ S₂.X₁) (h₂_1 : S₁.X₃ ⟶ S₂.X₂) (h₃_1 : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp S₁.g h₃_1 = 0) CategoryTheory.ShortComplex.Homotopy.g_h₃._autoParam)
  (comm₁_1 :
    autoParam (φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f h₁_1 + h₀_1 + φ₂.τ₁)
      CategoryTheory.ShortComplex.Homotopy.comm₁._autoParam)
  (comm₂_1 :
    autoParam
      (φ₁.τ₂ = CategoryTheory.CategoryStruct.comp S₁.g h₂_1 + CategoryTheory.CategoryStruct.comp h₁_1 S₂.f + φ₂.τ₂)
      CategoryTheory.ShortComplex.Homotopy.comm₂._autoParam)
  (comm₃_1 :
    autoParam (φ₁.τ₃ = h₃_1 + CategoryTheory.CategoryStruct.comp h₂_1 S₂.g + φ₂.τ₃)
      CategoryTheory.ShortComplex.Homotopy.comm₃._autoParam),
  ({ h₀ := h₀, h₀_f := h₀_f, h₁ := h₁, h₂ := h₂, h₃ := h₃, g_h₃ := g_h₃, comm₁ := comm₁, comm₂ := comm₂,
        comm₃ := comm₃ } =
      { h₀ := h₀_1, h₀_f := h₀_f_1, h₁ := h₁_1, h₂ := h₂_1, h₃ := h₃_1, g_h₃ := g_h₃_1, comm₁ := comm₁_1,
        comm₂ := comm₂_1, comm₃ := comm₃_1 }) =
    (h₀ = h₀_1 ∧ h₁ = h₁_1 ∧ h₂ = h₂_1 ∧ h₃ = h₃_1)
-- Mathlib.Order.Defs.PartialOrder
Decidable.le_iff_lt_or_eq' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α} [DecidableLE α], b ≤ a ↔ b < a ∨ a = b
-- Mathlib.Tactic.NormNum.Result
/-- The result of `norm_num` running on an expression `x` of type `α`.  -/
Mathlib.Meta.NormNum.Result : {u : Lean.Level} → {α : Q(Type u)} → Q(«$α») → Type
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_zero_right : ∀ {R : Type u_1} (n : ℕ) [inst : Semiring R], (SkewPolynomial.monomial n) 0 = 0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_obj_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₁ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).functor.obj X).right = X.right
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerRight_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {Fₗ Gₗ : CategoryTheory.Functor C E} (α : Fₗ ≅ Gₗ)
  (H : CategoryTheory.Functor D E') (x : CategoryTheory.Join C D),
  (CategoryTheory.Join.mapIsoWhiskerRight α H).hom.app x =
    match x with
    | CategoryTheory.Join.left x => (CategoryTheory.Join.inclLeft E E').map (α.hom.app x)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right (H.obj x))
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The special case of the first simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_δ_self_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.δ i) h) =
    CategoryTheory.CategoryStruct.comp (X.δ i.succ) (CategoryTheory.CategoryStruct.comp (X.δ i) h)
-- Mathlib.Data.Sigma.Basic
/-- A specialized ext lemma for equality of sigma types over an indexed subtype.  -/
Sigma.subtype_ext : ∀ {α : Type u_1} {β : Type u_7} {p : α → β → Prop} {x₀ x₁ : (a : α) × Subtype (p a)},
  x₀.fst = x₁.fst → ↑x₀.snd = ↑x₁.snd → x₀ = x₁
-- Mathlib.Algebra.Group.Defs
AddRightCancelMonoid.toAddRightCancelSemigroup : {M : Type u} → [self : AddRightCancelMonoid M] → AddRightCancelSemigroup M
-- Mathlib.RingTheory.WittVector.WittPolynomial
xInTermsOfW_eq : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible ↑p] {n : ℕ},
  xInTermsOfW p R n =
    (MvPolynomial.X n - ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) *
      MvPolynomial.C (⅟↑p ^ n)
-- Mathlib.Data.Finset.Max
/-- If finsets `s` and `t` are interleaved, then `Finset.card s ≤ Finset.card (t \ s) + 1`.  -/
Finset.card_le_sdiff_of_interleaved : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α},
  (∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y) → s.card ≤ (t \ s).card + 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
instLEAdditive : {α : Type u_1} → [LE α] → LE (Additive α)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.LocalTimeType.mk : Std.Time.TimeZone.Offset →
  Bool → String → Std.Time.TimeZone.StdWall → Std.Time.TimeZone.UTLocal → String → Std.Time.TimeZone.LocalTimeType
-- Mathlib.FieldTheory.Normal.Closure
normalClosure_eq_iSup_adjoin : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [inst_5 : Algebra K L] [IsScalarTower F K L] [Normal F L],
  IntermediateField.normalClosure F K L = ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.algebraMap_apply : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CommSemiring S] [inst_6 : Algebra S A]
  [inst_7 : SMulCommClass R S A] (r : S), (algebraMap S (TensorProduct R A B)) r = (algebraMap S A) r ⊗ₜ[R] 1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian
PresheafOfModules.instIsNormalEpiCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  CategoryTheory.IsNormalEpiCategory (PresheafOfModules R)
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_append : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []),
  List.maxIdxOn f (xs ++ ys) ⋯ =
    if f (List.maxOn f ys hys) ≤ f (List.maxOn f xs hxs) then List.maxIdxOn f xs hxs
    else xs.length + List.maxIdxOn f ys hys
-- Mathlib.Topology.Category.TopCommRingCat
/-- Construct a bundled `TopCommRingCat` from the underlying type and the appropriate typeclasses.
 -/
TopCommRingCat.of : (α : Type u) →
  [isCommRing : CommRing α] →
    [isTopologicalSpace : TopologicalSpace α] → [isTopologicalRing : IsTopologicalRing α] → TopCommRingCat
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.rightRelDecidable : {α : Type u_1} →
  [inst : AddGroup α] →
    (s : AddSubgroup α) → [DecidablePred fun x => x ∈ s] → DecidableRel ⇑(QuotientAddGroup.rightRel s)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂'_apply : ∀ {R : Type u_1} {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring S₁]
  [inst_4 : Semiring S₂] [inst_5 : Module S₁ N₂] [inst_6 : Module S₂ N₂] [inst_7 : SMulCommClass S₁ R N₂]
  [inst_8 : SMulCommClass S₂ R N₂] [inst_9 : SMulCommClass S₂ S₁ N₂] [inst_10 : Fintype n] [inst_11 : Fintype m]
  [inst_12 : DecidableEq n] [inst_13 : DecidableEq m] (M : Matrix n m N₂) (x : n → S₁) (y : m → S₂),
  (((Matrix.toLinearMap₂' R) M) x) y = ∑ i, ∑ j, x i • y j • M i j
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.iUnion_toPrepartition : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), π.iUnion = π.iUnion
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.nfpFamily_lt_ord_lift_of_isRegular : ∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {c : Cardinal.{max u v}},
  c.IsRegular →
    Cardinal.lift.{v, u} (Cardinal.mk ι) < c →
      c ≠ Cardinal.aleph0 →
        (∀ (i : ι), ∀ b < c.ord, f i b < c.ord) → ∀ {a : Ordinal.{max u v}}, a < c.ord → Ordinal.nfpFamily f a < c.ord
-- Mathlib.Algebra.Group.Commute.Defs
Commute.semiconjBy : ∀ {S : Type u_3} [inst : Mul S] {a b : S}, Commute a b → SemiconjBy a b b
-- Mathlib.Data.List.Triplewise
List.triplewise_map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {p' : β → β → β → Prop},
  List.Triplewise p' (List.map f l) ↔ List.Triplewise (fun a b c => p' (f a) (f b) (f c)) l
-- Mathlib.GroupTheory.NoncommCoprod
AddHom.noncommCoprod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : AddSemigroup P] (f : M →ₙ+ P)
  (g : N →ₙ+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)),
  f.noncommCoprod g comm = { toFun := fun mn => f mn.1 + g mn.2, map_add' := ⋯ }
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_mul_left_of_ge' : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  (∀ᶠ (x : α) in l, f x ≤ C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.Nondegenerate.flip : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.Nondegenerate → B.flip.Nondegenerate
-- Mathlib.Algebra.Polynomial.GroupRingAction
MulSemiringActionHom.coe_polynomial : ∀ {M : Type u_1} [inst : Monoid M] {P : Type u_2} [inst_1 : CommSemiring P] [inst_2 : MulSemiringAction M P]
  {Q : Type u_3} [inst_3 : CommSemiring Q] [inst_4 : MulSemiringAction M Q] (g : P →+*[M] Q),
  ⇑g.polynomial = Polynomial.map ↑g
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
/-- The functor `PartOrd ⥤ SSet` which sends a partially ordered type to its nerve.  -/
PartOrd.nerveFunctor : CategoryTheory.Functor PartOrd SSet
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] [Nontrivial R] (s : σ), (MvPolynomial.X s).totalDegree = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.Equiv.beq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq β] [ReflBEq β], m₁.WF → m₂.WF → m₁.Equiv m₂ → Std.DTreeMap.Raw.Const.beq m₁ m₂ = true
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- The Dirichlet density of `S` is nonnegative.  -/
NumberField.Set.dirichletDensity_nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))), 0 ≤ NumberField.Set.dirichletDensity S
-- Mathlib.Analysis.Normed.Operator.Basic
ball_subset_range_iff_surjective : ∀ {𝕜 : 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]
  [SemilinearMapClass 𝓕 σ₁₂ E F] [RingHomSurjective σ₁₂] {f : 𝓕} {x : F} {r : ℝ},
  0 < r → (Metric.ball x r ⊆ Set.range ⇑f ↔ Function.Surjective ⇑f)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- **Alias** of `SheafOfModules.ιFree_mapFreeIso_hom`. -/
SheafOfModules.ιFree_mapFree_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  [inst_6 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I),
  CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (SheafOfModules.mapFreeIso F I η).hom =
    CategoryTheory.CategoryStruct.comp η.hom (F.map (SheafOfModules.ιFree i))
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ioc_mul_Ico_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [MulLeftStrictMono α]
  [MulRightStrictMono α] [inst_5 : LocallyFiniteOrder α] (a b c d : α),
  Finset.Ioc a b * Finset.Ico c d ⊆ Finset.Ioo (a * c) (b * d)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.mk₂.congr_simp : ∀ (R : Type u_2) [inst : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8} {Pₗ : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ] [inst_4 : Module R M] [inst_5 : Module R Nₗ]
  [inst_6 : Module R Pₗ] (f f_1 : M → Nₗ → Pₗ) (e_f : f = f_1)
  (H1 : ∀ (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (H2 : ∀ (c : R) (m : M) (n : Nₗ), f (c • m) n = c • f m n)
  (H3 : ∀ (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂)
  (H4 : ∀ (c : R) (m : M) (n : Nₗ), f m (c • n) = c • f m n),
  LinearMap.mk₂ R f H1 H2 H3 H4 = LinearMap.mk₂ R f_1 ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_add_of_le_add_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddRightMono α] {a b c d : α}, a ≤ b + c → b ≤ d → a ≤ d + c
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, (m.insert k v).contains a = (k == a || m.contains a)
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.nsmul_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (m n : ℕ), AddCommute (m • a) (n • b)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_mul : ∀ {n k s : ℕ}, s ≤ k → n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
-- Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
Subalgebra.isSimpleOrder_of_finrank_prime : ∀ (F : Type u_1) (A : Type u_2) [inst : Field F] [inst_1 : Ring A] [IsDomain A] [inst_3 : Algebra F A],
  Nat.Prime (Module.finrank F A) → IsSimpleOrder (Subalgebra F A)
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ]
  {g₁ g₂ : β →Co γ} {f : α →Co β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the right half-plane. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open right half-plane and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open right half-plane
  for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the imaginary axis;
* `f x → 0` as `x : ℝ` tends to infinity.

Then `‖f z‖` is bounded from above by the same constant on the closed right half-plane.
See also `PhragmenLindelof.right_half_plane_of_bounded_on_real` for a stronger version.  -/
PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
  DiffContOnCl ℂ f {z | 0 < z.re} →
    (∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => Real.exp (B * ‖z‖ ^ c)) →
      Filter.Tendsto (fun x => f ↑x) Filter.atTop (nhds 0) →
        (∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) → 0 ≤ z.re → ‖f z‖ ≤ C
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- Alternative constructor for symmetric categories, where the symmetry of the braiding is phrased
as an equality of natural transformation of bifunctors.
 -/
CategoryTheory.SymmetricCategory.ofCurried : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.BraidedCategory.curriedBraidingNatIso C).hom
              ((CategoryTheory.flipFunctor C C C).map (CategoryTheory.BraidedCategory.curriedBraidingNatIso C).hom) =
            CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.curriedTensor C) →
          CategoryTheory.SymmetricCategory C
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.GeometricallyIntegral.eq_geometrically : @AlgebraicGeometry.GeometricallyIntegral = AlgebraicGeometry.geometrically AlgebraicGeometry.IsIntegral
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_top' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊤.starProjection = 1
-- Init.Omega.Int
Lean.Omega.Int.lt_le_asymm : ∀ {x y : ℤ}, y < x → x ≤ y → False
-- Init.NotationExtra
Lean.expandExplicitBinders : Lean.Name → Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.nsmul_apply : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {n : ℕ} {x : PreLp E} {i : α},
  (n • x) i = n • x i
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Γ_map_op : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y),
  AlgebraicGeometry.LocallyRingedSpace.Γ.map f.op = f.c.app (Opposite.op ⊤)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.null_iff_toMeasure_null : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.FiniteMeasure Ω) (s : Set Ω), ν s = 0 ↔ ↑ν s = 0
-- Mathlib.Analysis.Normed.Affine.Ceva
/-- **Ceva's theorem** for a triangle, expressed using division of distances.  -/
Affine.Triangle.prod_dist_div_dist_eq_one_of_mem_line_of_mem_line : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : NormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {t : Affine.Triangle 𝕜 P}
  {p : Fin 3 → P} {p' : P},
  (∀ (i : Fin 3), p i ≠ t.points (i + 2)) →
    (∀ (i : Fin 3), p i ∈ line[𝕜, t.points (i + 1), t.points (i + 2)]) →
      (∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]) →
        ∏ i, dist (t.points (i + 1)) (p i) / dist (p i) (t.points (i + 2)) = 1
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousAt.neg : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Neg G]
  [ContinuousNeg G] {f : X → G} {x : X}, ContinuousAt f x → ContinuousAt (-f) x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arccos`.  -/
EuclideanGeometry.oangle_right_eq_arccos_of_oangle_eq_pi_div_two : ∀ {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},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
    EuclideanGeometry.oangle p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))
-- Mathlib.CategoryTheory.Sites.Adjunction
CategoryTheory.Sheaf.instIsLeftAdjointComposeAndSheafify : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {G : CategoryTheory.Functor E D} [inst_3 : CategoryTheory.HasWeakSheafify J D] [G.IsLeftAdjoint],
  (CategoryTheory.Sheaf.composeAndSheafify J G).IsLeftAdjoint
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.Iso.op.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y),
  α.op = { hom := α.hom.op, inv := α.inv.op, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.insertMany_list_singleton : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {k : α} {v : β k},
  t.insertMany [⟨k, v⟩] = t.insert k v
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatch.le_of_isMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos → String.Slice.Pattern.Model.IsMatch pat pos' → pos' ≤ pos
-- Mathlib.Combinatorics.SimpleGraph.Operations
/-- There is never an `s-t` edge in `G.replaceVertex s t`.  -/
SimpleGraph.not_adj_replaceVertex_same : ∀ {V : Type u_1} (G : SimpleGraph V) (s t : V) [inst : DecidableEq V], ¬(G.replaceVertex s t).Adj s t
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
/-- Shorthand for the "forward" arrow corresponding to `f` in `paths <| symmetrify V`  -/
Quiver.Hom.toNegPath : {V : Type u} → [inst : Quiver V] → {X Y : V} → (X ⟶ Y) → (Y ⟶ X)
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.finitenessRelation : {ρ : Type} →
  {ρ_1 : ρ} →
    {σ : String.Slice → Type} →
      [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
        [inst_1 : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ] →
          {s : String.Slice} →
            [Std.Iterators.Finite (σ s) Id] → Std.Iterators.FinitenessRelation (String.Slice.RevSplitIterator ρ_1 s) Id
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_prod_of_submultiplicative : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] [inst_2 : Preorder β] [IsOrderedMonoid β]
  (f : α → β), f 1 ≤ 1 → (∀ (a b : α), f (a * b) ≤ f a * f b) → ∀ (s : Multiset α), f s.prod ≤ (Multiset.map f s).prod
-- Init.Data.Fin.Lemmas
Fin.castSucc_mk : ∀ (n i : ℕ) (h : i < n), ⟨i, h⟩.castSucc = ⟨i, ⋯⟩
-- Mathlib.NumberTheory.Padics.AddChar
/-- The unique continuous additive character of `ℤ_[p]` mapping `1` to `1 + r`.  -/
PadicInt.addChar_of_value_at_one : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : NormedRing R] →
        [inst_2 : Algebra ℤ_[p] R] →
          [IsBoundedSMul ℤ_[p] R] →
            [IsUltrametricDist R] →
              [CompleteSpace R] → (r : R) → Filter.Tendsto (fun x => r ^ x) Filter.atTop (nhds 0) → AddChar ℤ_[p] R
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.StrictSegal.spineEquiv.eq_1 : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1),
  sx.spineEquiv m h = { toFun := X.spine m h, invFun := sx.spineToSimplex m h, left_inv := ⋯, right_inv := ⋯ }
-- Init.Sym.Lemmas
Lean.Sym.Int16.lt_eq_true : ∀ (a b : Int16), decide (a < b) = true → (a < b) = True