mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PicardGroup
Module.Flat.toAlgebra.eq_1 : ∀ {R : Type u} {M : Type v} {A : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A),
  Module.Flat.toAlgebra e =
    ↑(LinearEquiv.restrictScalars R e) ∘ₗ
      LinearMap.rTensor M (Algebra.ofId R A).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- Galois insertion between `adjoin` and `coe`.  -/
IntermediateField.gi : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → GaloisInsertion (IntermediateField.adjoin F) fun x => ↑x
-- Mathlib.Tactic.CrossRefAttribute
/-- The parenthesizer for Stacks Project Tags syntax.  -/
Lean.PrettyPrinter.Parenthesizer.stacksTagAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.Module.Complement
/-- **Alias** of `Submodule.IsCompl.isTopCompl_iff_projectionOnto`. -/
Submodule.IsCompl.isTopCompl_iff_linearProjOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : IsCompl p q),
  Submodule.IsTopCompl p q ↔ Continuous ⇑(p.projectionOnto q h)
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.homMap_comp_assoc : ∀ {C₁ : Type u_2} {C₂ : Type u_3} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_2, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁]
  [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] {X Y Z : C₁} (f : L₁.obj X ⟶ L₁.obj Y) (g : L₁.obj Y ⟶ L₁.obj Z) {Z_1 : D₂}
  (h : L₂.obj (Φ.functor.obj Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ f) (CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ g) h)
-- Init.Data.List.Find
List.findIdx?_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {p : α → Bool},
  List.findIdx? p (x :: xs) = if p x = true then some 0 else Option.map (fun i => i + 1) (List.findIdx? p xs)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.closure_le : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s : Set α} {t : TopologicalSpace.Closeds α},
  TopologicalSpace.Closeds.closure s ≤ t ↔ s ⊆ ↑t
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log_zero : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint], CFC.log 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.norm_mul_exp_arg_mul_I : ∀ (x : ℂ), ↑‖x‖ * Complex.exp (↑x.arg * Complex.I) = x
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_top_right : ∀ {E : Type v} [inst : Field E] (A : Subfield E), A.relfinrank ⊤ = Module.finrank (↥A) E
-- Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat : ∀ {n : ℕ} {h : 0 < n}, Mathlib.Tactic.Ring.CSLiftVal (n.toPNat h) n
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instCommGroupCoeOfSubgroupClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → CommGroup (R i)] [inst_2 : ∀ (i : ι), SubgroupClass (S i) (R i)],
  RestrictedProduct.instCommGroupCoeOfSubgroupClass R = Function.Injective.commGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_iSup : ∀ {V : Type u} {G : SimpleGraph V} [inst : Finite V] {ι : Sort u_1} (f : ι → G.Finsubgraph), ↑(⨆ i, f i) = ⨆ i, ↑(f i)
-- Mathlib.Analysis.Seminorm
/-- Alternative constructor for a `Seminorm` on an `AddCommGroup E` that is a module over a
`SeminormedRing 𝕜`.  -/
Seminorm.of : {𝕜 : Type u_3} →
  {E : Type u_7} →
    [inst : SeminormedRing 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          (f : E → ℝ) → (∀ (x y : E), f (x + y) ≤ f x + f y) → (∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x) → Seminorm 𝕜 E
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castLE_Iio_castLE : ∀ {m n : ℕ} (i : Fin m) (h : m ≤ n), Fin.castLE h ⁻¹' Set.Iio (Fin.castLE h i) = Set.Iio i
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.gc_map_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N),
  GaloisConnection (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
-- Init.Data.Iterators.Consumers.Monadic.Partial
/-- For an iterator `it`, `it.allowNontermination` provides potentially nonterminating variants of
consumers such as `toList`. They can be used without any proof of termination such as `Finite`
or `Productive`, but as they are implemented with the `partial` declaration modifier, they are
opaque for the kernel and it is impossible to prove anything about them.
 -/
Std.IterM.allowNontermination : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.IterM m β → Std.IterM.Partial m β
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_le_tsum_comp_of_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Surjective f → ∀ (g : β → ENNReal), ∑' (y : β), g y ≤ ∑' (x : α), g (f x)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey! k = m₁.getKey! k
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- A special case of `GradedRing` with `σ = Submodule R A`. This is useful both because it
can avoid typeclass search, and because it provides a more concise name.  -/
GradedAlgebra : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [DecidableEq ι] →
        [AddMonoid ι] →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (ι → Submodule R A) → Type (max u_1 u_3)
-- Mathlib.Order.Filter.Map
Filter.mem_bind' : ∀ {α : Type u_1} {β : Type u_2} {s : Set β} {f : Filter α} {m : α → Filter β}, s ∈ f.bind m ↔ {a | s ∈ m a} ∈ f
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
_private.Mathlib.LinearAlgebra.LinearIndependent.Lemmas.0.LinearIndependent.pair_add_smul_add_smul_iff_aux : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {S : Type u_6}
  [inst_3 : CommRing S] [IsDomain S] [inst_5 : Module S R] [inst_6 : Module S M] [SMulCommClass S R M]
  [IsScalarTower S R M] [Module.IsTorsionFree S R] (a b c d : S),
  a * d ≠ b * c → LinearIndependent R ![x, y] → LinearIndependent R ![a • x + b • y, c • x + d • y]
-- Lean.DocString.Extension
/-- Retrieves all builtin Verso docstrings.
 -/
Lean.getBuiltinVersoDocStrings : IO (Lean.NameMap Lean.VersoDocString)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log.eq_1 : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), CFC.log a = cfc Real.log a
-- Mathlib.Order.Completion
DedekindCut.factorEmbedding_principal : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : PartialOrder β] (f : β ↪o α) (x : β),
  (DedekindCut.factorEmbedding f) (DedekindCut.principal x) = f x
-- Mathlib.Algebra.Lie.Solvable
LieIdeal.coe_derivedSeries_eq_int : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (k : ℕ),
  ↑(LieAlgebra.derivedSeries R L k) = ↑(LieAlgebra.derivedSeries ℤ L k)
-- Mathlib.Data.Finite.Prod
Finite.Set.finite_image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β) [Finite ↑s] [Finite ↑t],
  Finite ↑(Set.image2 f s t)
-- Mathlib.Algebra.Group.TypeTags.Basic
isAddRegular_toAdd : ∀ {α : Type u} [inst : AddMonoid α] {a : Multiplicative α}, IsAddRegular (Multiplicative.toAdd a) ↔ IsRegular a
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.TensorProduct.map_map_comp_assoc_eq_assoc : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15}
  {N₃ : Type u_16} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid N₁] [inst_7 : AddCommMonoid N₂]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₁] [inst_13 : Module R N₂] [inst_14 : Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂)
  (f₃ : M₃ →ₗ[R] N₃) (f : M →ₗ[R] TensorProduct R (TensorProduct R M₁ M₂) M₃),
  TensorProduct.map f₁ (TensorProduct.map f₂ f₃) ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃) ∘ₗ f =
    ↑(TensorProduct.assoc R N₁ N₂ N₃) ∘ₗ TensorProduct.map (TensorProduct.map f₁ f₂) f₃ ∘ₗ f
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.equivEssImageOfReflective_unitIso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i],
  CategoryTheory.equivEssImageOfReflective.unitIso =
    (CategoryTheory.asIso (CategoryTheory.reflectorAdjunction i).counit).symm
-- Mathlib.Geometry.Convex.Cone.Basic
Convex.subset_toCone : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s), s ⊆ ↑(Convex.toCone s hs)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_base_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : TopCat} (h : ↑Z.toPresheafedSpace ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).base h =
    CategoryTheory.CategoryStruct.comp f.base (CategoryTheory.CategoryStruct.comp g.base h)
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.star_mul_self_ne_zero_iff : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] (x : E), star x * x ≠ 0 ↔ x ≠ 0
-- Mathlib.Order.SupClosed
supClosure_idem : ∀ {α : Type u_3} [inst : SemilatticeSup α] (s : Set α), supClosure (supClosure s) = supClosure s
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
/-- Functoriality of `Proj`.  -/
AlgebraicGeometry.Proj.map : {A B σ τ : Type u} →
  [inst : CommRing A] →
    [inst_1 : SetLike σ A] →
      [inst_2 : AddSubgroupClass σ A] →
        [inst_3 : CommRing B] →
          [inst_4 : SetLike τ B] →
            [inst_5 : AddSubgroupClass τ B] →
              {𝒜 : ℕ → σ} →
                {ℬ : ℕ → τ} →
                  [inst_6 : GradedRing 𝒜] →
                    [inst_7 : GradedRing ℬ] →
                      (f : 𝒜 →+*ᵍ ℬ) →
                        HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜) →
                          (AlgebraicGeometry.Proj ℬ ⟶ AlgebraicGeometry.Proj 𝒜)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.lt_norm : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.core_cert lhs rhs p = true →
    Lean.Grind.CommRing.Expr.denote ctx lhs < Lean.Grind.CommRing.Expr.denote ctx rhs →
      Lean.Grind.CommRing.Poly.denote ctx p < 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.DTreeMap.Const.getD (Std.DTreeMap.Const.ofList l cmp) k' fallback = v
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Given `data : F.PreOneHypercoverDenseData X`, an object `W₀ : C₀` and two
morphisms `p₁ : W₀ ⟶ data.X i₁` and `p₂ : W₀ ⟶ data.X i₂`, this is the sieve of `W₀`
consisting of morphisms `g : Z₀ ⟶ W₀` such that there exists a morphism `Z₀ ⟶ data.Y j`
such that `g ≫ p₁ = h ≫ data.p₁ j` and `g ≫ p₂ = h ≫ data.p₂ j`.  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.sieve₁₀ : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {X : C} →
            (data : F.PreOneHypercoverDenseData X) →
              {i₁ i₂ : data.I₀} → {W₀ : C₀} → (W₀ ⟶ data.X i₁) → (W₀ ⟶ data.X i₂) → CategoryTheory.Sieve W₀
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.mono_homologyMap_of_mono_of_not_rel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (j : ι) [inst_2 : K.HasHomology j]
  [inst_3 : L.HasHomology j] [CategoryTheory.Mono (φ.f j)],
  (∀ (i : ι), ¬c.Rel i j) → CategoryTheory.Mono (HomologicalComplex.homologyMap φ j)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.mkEMatchTheoremForDecl : Lean.Name →
  Lean.Meta.Grind.EMatchTheoremKind →
    Lean.Meta.Grind.SymbolPriorities →
      optParam Bool false → optParam Bool false → Lean.MetaM Lean.Meta.Grind.EMatchTheorem
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pos.skip?_prop_eq_skip?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  pos.skip? p = pos.skip? fun x => decide (p x)
-- Mathlib.Algebra.Ring.CharZero
RingHom.charZero_iff : ∀ {R : Type u_2} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {ϕ : R →+* S},
  Function.Injective ⇑ϕ → (CharZero R ↔ CharZero S)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getDₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α fun x => β) (k : α) (fallback : β),
  Std.DTreeMap.Internal.Impl.Const.getDₘ l k fallback = (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).getD fallback
-- Mathlib.RepresentationTheory.Maschke
LinearMap.equivariantProjection.eq_1 : ∀ {k : Type u_1} [inst : CommRing k] (G : Type u_2) [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [inst_10 : Fintype G],
  LinearMap.equivariantProjection G π = Ring.inverse ↑(Fintype.card G) • LinearMap.sumOfConjugatesEquivariant G π
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_iff_subset_ball : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] (c : α), Bornology.IsBounded s ↔ ∃ r, s ⊆ Metric.ball c r
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- Inducts on the base `b` expansion of an ordinal.  -/
Ordinal.CNF.rec : (b : Ordinal.{u_2}) →
  {C : Ordinal.{u_2} → Sort u_1} →
    C 0 → ((o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ Ordinal.log b o) → C o) → (o : Ordinal.{u_2}) → C o
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker.inj : ∀ {e : Mathlib.Tactic.BicategoryLike.Mor₂} {f : Mathlib.Tactic.BicategoryLike.Atom₁}
  {η : Mathlib.Tactic.BicategoryLike.WhiskerLeft} {e_1 : Mathlib.Tactic.BicategoryLike.Mor₂}
  {f_1 : Mathlib.Tactic.BicategoryLike.Atom₁} {η_1 : Mathlib.Tactic.BicategoryLike.WhiskerLeft},
  Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker e f η =
      Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker e_1 f_1 η_1 →
    e = e_1 ∧ f = f_1 ∧ η = η_1
-- Aesop.RuleSet
Aesop.LocalRuleSet.onBase : {α : Type u_1} → (Aesop.BaseRuleSet → Aesop.BaseRuleSet × α) → Aesop.LocalRuleSet → Aesop.LocalRuleSet × α
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.instIsEquivalenceRightExtensionCompPrecomp : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C) [G.IsEquivalence],
  (CategoryTheory.Functor.RightExtension.precomp L F G).IsEquivalence
-- Mathlib.Analysis.Convex.Quasiconvex
ConvexOn.quasiconvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulMono 𝕜 β] {s : Set E} {f : E → β}, ConvexOn 𝕜 s f → QuasiconvexOn 𝕜 s f
-- Init.Data.List.ControlImpl
_private.Init.Data.List.ControlImpl.0.List.flatMapMTR.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List (List β) → Sort u_3) →
      (x : List α) →
        (x_1 : List (List β)) →
          ((bs : List (List β)) → motive [] bs) →
            ((a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs) → motive x x_1
-- Mathlib.Data.Fin.Basic
Fin.one_eq_mk_of_lt : ∀ {n : ℕ} (h : 1 < n),
  have this := ⋯;
  1 = ⟨1, h⟩
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.domain_sup : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f g : E →ₛₗ.[σ] F)
  (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y), (f.sup g h).domain = f.domain ⊔ g.domain
-- Mathlib.Analysis.Convex.Combination
/-- Universe polymorphic version of the reverse implication of `mem_convexHull_iff_exists_fintype`.
 -/
mem_convexHull_of_exists_fintype : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {s : Set E} {x : E} [inst_5 : Fintype ι] (w : ι → R) (z : ι → E),
  (∀ (i : ι), 0 ≤ w i) → ∑ i, w i = 1 → (∀ (i : ι), z i ∈ s) → ∑ i, w i • z i = x → x ∈ (convexHull R) s
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.revMatchesAt_iff_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt pat pos ↔ String.Slice.Pattern.Model.RevMatchesAt pat.toSlice pos
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.size_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → m₁.size = m₂.size
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_map_of_stronglyMeasurable : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {β : Type u_6} [inst_2 : MeasurableSpace β] {φ : α → β},
  Measurable φ →
    ∀ {f : β → G},
      MeasureTheory.StronglyMeasurable f → ∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.eq_1 : ∀ (pat : ByteArray) (stackPos : ℕ) (hst : stackPos < pat.size),
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst =
    String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go✝ pat stackPos hst stackPos
-- Init.Data.Slice.Array.Lemmas
Subarray.size_toArray : ∀ {α : Type u_1} {xs : Subarray α}, (Std.Slice.toArray xs).size = Std.Slice.size xs
-- Init.Data.Bool
Bool.toNat_eq_zero : ∀ {b : Bool}, b.toNat = 0 ↔ b = false
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The arrow isomorphism `X □ (∅ ⟶ ⋆) ≅ X` in a CCC with pushouts, an initial object, and a
terminal object.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [CategoryTheory.MonoidalClosed C] →
          (X : CategoryTheory.Arrow C) →
            {I : C} →
              CategoryTheory.Limits.IsInitial I →
                {T : C} → (t : CategoryTheory.Limits.IsTerminal T) → (X □ CategoryTheory.Arrow.mk (t.from I)) ≅ X
-- Mathlib.Data.Set.Basic
Subsingleton.eq_univ_of_nonempty : ∀ {α : Type u_1} [Subsingleton α] {s : Set α}, s.Nonempty → s = Set.univ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point.0.termY : Lean.ParserDescr
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- If `s ⊆ t` modulo a set of measure `0`, then `μ s ≤ μ t`.  -/
MeasureTheory.measure_mono_ae : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s ≤ᵐ[μ] t → μ s ≤ μ t
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.mk.inj : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} {toHom : X.Hom Y.toPresheafedSpace}
  {prop : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom.stalkMap x))}
  {toHom_1 : X.Hom Y.toPresheafedSpace}
  {prop_1 : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom_1.stalkMap x))},
  { toHom := toHom, prop := prop } = { toHom := toHom_1, prop := prop_1 } → toHom = toHom_1
-- Lean.Elab.ConfigEval.Util
_private.Lean.Elab.ConfigEval.Util.0.Lean.Elab.ConfigEval.makeStringMatcher.build : Lean.Ident → Lean.Term → ℕ → ℕ → Array (String × Lean.Term) → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_add_lt_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] {a b c d : α}, a + b < c → d ≤ b → a + d < c
-- Lean.Meta.Tactic.Grind.MatchDiscrOnly
/-- Returns `Grind.simpMatchDiscrsOnly e`. Recall that `Grind.simpMatchDiscrsOnly` is
a gadget for instructing the `grind` simplifier to only normalize/simplify
the discriminants of a `match`-expression. See `reduceSimpMatchDiscrsOnly`.
 -/
Lean.Meta.Grind.markAsSimpMatchDiscrsOnly : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- If `α` is an isomorphism between left adjoints, then its conjugate 2-morphism is an
isomorphism. The converse is given in `conjugateEquiv_of_iso`.
 -/
CategoryTheory.Bicategory.conjugateEquiv_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : l₂ ⟶ l₁)
  [CategoryTheory.IsIso α], CategoryTheory.IsIso ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂) α)
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.instBEqCastMode.beq : Mathlib.Tactic.DepRewrite.CastMode → Mathlib.Tactic.DepRewrite.CastMode → Bool
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union_congr_of_subset : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ t₁ t₂ : Set α},
  s₁ ⊆ s₂ →
    μ.real s₂ ≤ μ.real s₁ →
      t₁ ⊆ t₂ →
        μ.real t₂ ≤ μ.real t₁ →
          autoParam (μ s₂ ≠ ⊤) MeasureTheory.measureReal_union_congr_of_subset._auto_1 →
            autoParam (μ t₂ ≠ ⊤) MeasureTheory.measureReal_union_congr_of_subset._auto_3 →
              μ.real (s₁ ∪ t₁) = μ.real (s₂ ∪ t₂)
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.ProofInstInfo.mk.sizeOf_spec : ∀ (argsInfo : Array Lean.Meta.Sym.ProofInstArgInfo), sizeOf { argsInfo := argsInfo } = 1 + sizeOf argsInfo