mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_toAddMonoidHom : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), ⇑f.toAddMonoidHom = ⇑f
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddLeftCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddLeftCancelMonoid α],
  Lex.instAddLeftCancelMonoid = { toAddMonoid := Lex.instAddMonoid, toIsLeftCancelAdd := ⋯ }
-- Mathlib.Data.Pi.Interval
Pi.instLocallyFiniteOrder : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [Fintype ι] →
      [DecidableEq ι] →
        [(i : ι) → DecidableEq (α i)] →
          [inst : (i : ι) → PartialOrder (α i)] →
            [(i : ι) → LocallyFiniteOrder (α i)] → LocallyFiniteOrder ((i : ι) → α i)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.Const.balanced_modify : ∀ {α : Type u} {β : Type v} [inst : Ord α] {k : α} {f : β → β} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.Balanced → (Std.DTreeMap.Internal.Impl.Const.modify k f t).Balanced
-- Lean.Elab.Do.Basic
Lean.Elab.Do.Context.mk.injEq : ∀ (monadInfo : Lean.Elab.Do.MonadInfo) (mutVars : Array Lean.Elab.Do.MutVar)
  (mutVarDefs : Std.HashMap Lean.Name Lean.Elab.Do.MutVar) (doBlockResultType : Lean.Expr)
  (contInfo : Lean.Elab.Do.ContInfoRef) (deadCode : Lean.Elab.Do.CodeLiveness) (ops : Lean.Elab.Do.DoOpsRef)
  (monadInfo_1 : Lean.Elab.Do.MonadInfo) (mutVars_1 : Array Lean.Elab.Do.MutVar)
  (mutVarDefs_1 : Std.HashMap Lean.Name Lean.Elab.Do.MutVar) (doBlockResultType_1 : Lean.Expr)
  (contInfo_1 : Lean.Elab.Do.ContInfoRef) (deadCode_1 : Lean.Elab.Do.CodeLiveness) (ops_1 : Lean.Elab.Do.DoOpsRef),
  ({ monadInfo := monadInfo, mutVars := mutVars, mutVarDefs := mutVarDefs, doBlockResultType := doBlockResultType,
        contInfo := contInfo, deadCode := deadCode, ops := ops } =
      { monadInfo := monadInfo_1, mutVars := mutVars_1, mutVarDefs := mutVarDefs_1,
        doBlockResultType := doBlockResultType_1, contInfo := contInfo_1, deadCode := deadCode_1, ops := ops_1 }) =
    (monadInfo = monadInfo_1 ∧
      mutVars = mutVars_1 ∧
        mutVarDefs = mutVarDefs_1 ∧
          doBlockResultType = doBlockResultType_1 ∧ contInfo = contInfo_1 ∧ deadCode = deadCode_1 ∧ ops = ops_1)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
/-- The value of the quadratic character at an odd prime `p` different from `ringChar F`.  -/
quadraticChar_odd_prime : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 →
    ∀ {p : ℕ} [inst_3 : Fact (Nat.Prime p)],
      p ≠ 2 →
        ringChar F ≠ p →
          (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑(ZMod.χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F))
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.revSkipWhile_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos},
  pos.revSkipWhile pat = ((pos.cast hst).revSkipWhile pat).cast ⋯
-- Mathlib.Algebra.BigOperators.Fin
Finset.prod_range : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : ℕ → M), ∏ i ∈ Finset.range n, f i = ∏ i, f ↑i
-- Mathlib.RingTheory.Valuation.AlgebraInstances
/-- A ring equivalence between the integral closure of the valuation subring of `K` in `L`
and a ring `R` satisfying `isIntegralClosure R v.valuationSubring L`.  -/
ValuationSubring.equiv : {K : Type u_1} →
  [inst : Field K] →
    (v : Valuation K (WithZero (Multiplicative ℤ))) →
      (L : Type u_2) →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            (R : Type u_3) →
              [inst_3 : CommRing R] →
                [inst_4 : Algebra (↥v.valuationSubring) R] →
                  [inst_5 : Algebra R L] →
                    [IsScalarTower (↥v.valuationSubring) R L] →
                      [IsIntegralClosure R (↥v.valuationSubring) L] → ↥(integralClosure (↥v.valuationSubring) L) ≃+* R
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The selected hypothesis, if any.  -/
Mathlib.Tactic.ClickSuggestions.Context.hyp? : Mathlib.Tactic.ClickSuggestions.Context → Option Lean.FVarId
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_le_size_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, m.size ≤ (m.erase k).size + 1
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `fallback` if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryLTD : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → α × β → α × β
-- Mathlib.FieldTheory.Perfect
PerfectField.of_ringEquiv : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] (h : K ≃+* L) [PerfectField K], PerfectField L
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RoiSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : Ord α] [inst_1 : SizeOf α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (range : Std.Roi α), sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instMul : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] → [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → Mul (M₁ →L[R₁] M₁)
-- Mathlib.Algebra.Group.ULift
ULift.addRightCancelMonoid : {α : Type u} → [AddRightCancelMonoid α] → AddRightCancelMonoid (ULift.{u_1, u} α)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, m.WF → (Std.HashMap.Raw.map f m).getKey? k = m.getKey? k
-- Lean.Parser.Command
/-- `/-! <text> -/` defines a *module docstring* that can be displayed by documentation generation
tools. The string is associated with the corresponding position in the file. It can be used
multiple times in the same file.
 -/
Lean.Parser.Command.moduleDoc : Lean.Parser.Parser
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.isNormal_gamma : Order.IsNormal Ordinal.gamma
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffAt_of_notMem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  [inst_11 : Zero M'] {x : M}, x ∉ tsupport f → ∀ (n : WithTop ℕ∞), ContMDiffAt I I' n f x
-- Lean.Elab.Tactic.Induction
/-- Interprets a `Lean.Parser.Tactic.elimTarget`.  -/
Lean.Elab.Tactic.mkTargetView : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.ElimTargetView
-- Mathlib.Order.Comparable
/-- **Alias** of `CompRel.of_lt`. -/
LT.lt.compRel : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], a < b → CompRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_sub_theta_le : ∀ {x : ℝ}, 1 ≤ x → Chebyshev.psi x - Chebyshev.theta x ≤ 2 * √x * Real.log x
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.utf8DecodeChar?_append_eq_assemble₄ : ∀ {l : List UInt8} {b : ByteArray} (hl : l.length = 4),
  ByteArray.utf8DecodeChar?.parseFirstByte l[0] = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
    (l.toByteArray ++ b).utf8DecodeChar? 0 = ByteArray.utf8DecodeChar?.assemble₄ l[0] l[1] l[2] l[3]
-- Mathlib.Topology.Algebra.Ring.Basic
Subsemiring.topologicalClosure_coe : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [inst_2 : IsSemitopologicalSemiring R]
  (s : Subsemiring R), ↑s.topologicalClosure = closure ↑s
-- Mathlib.CategoryTheory.Category.RelCat
/-- `RelCat` is self-dual: The map that swaps the argument order of a
relation induces an equivalence between `RelCat` and its opposite.  -/
CategoryTheory.RelCat.opEquivalence : CategoryTheory.RelCat ≌ CategoryTheory.RelCatᵒᵖ
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- Any integrable function can be approximated by bounded continuous functions,
version in terms of `∫⁻`.  -/
MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [μ.WeaklyRegular] {f : α → E},
  MeasureTheory.Integrable f μ →
    ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ MeasureTheory.Integrable (⇑g) μ
-- Mathlib.RingTheory.Coalgebra.Hom
Coalgebra.ext_to_ring_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {f g : A →ₗc[R] R}, f = g ↔ True
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.eq_adjoin_of_eq_algebra_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E)
  (K : IntermediateField F E), K.toSubalgebra = Algebra.adjoin F S → K = IntermediateField.adjoin F S
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Two n-simplices among cospherical points in an n-dimensional
subspace have the same circumcenter.  -/
EuclideanGeometry.circumcenter_eq_of_cospherical_subset : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
  ps ⊆ ↑s →
    ∀ [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction],
      Module.finrank ℝ ↥s.direction = n →
        EuclideanGeometry.Cospherical ps →
          ∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
            Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumcenter = sx₂.circumcenter
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.not_step_singleton : ∀ {α : Type u} {L : List (α × Bool)} {p : α × Bool}, ¬FreeGroup.Red.Step [p] L
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PullbackCone.op_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g), c.op.pt = Opposite.op c.pt
-- Lean.Meta.Match.CaseValues
Lean.Meta.CaseValuesSubgoal.mvarId : Lean.Meta.CaseValuesSubgoal → Lean.MVarId
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Two morphisms `a b : c ⟶ hf.pullback g` are equal if
* Their compositions (in `C`) with `hf.snd g : hf.pullback  ⟶ X` are equal.
* The compositions of `F.map a` and `F.map b` with `hf.fst g` are equal.  -/
CategoryTheory.Functor.relativelyRepresentable.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y}
  [F.Faithful] {c : C} {a_1 b : c ⟶ hf.pullback g},
  CategoryTheory.CategoryStruct.comp (F.map a_1) (hf.fst g) = CategoryTheory.CategoryStruct.comp (F.map b) (hf.fst g) →
    CategoryTheory.CategoryStruct.comp a_1 (hf.snd g) = CategoryTheory.CategoryStruct.comp b (hf.snd g) → a_1 = b
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_lt_iff : ∀ {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n), i.castPred hi < j ↔ i < j.castSucc
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n`-th iterated derivative within a set with unique derivatives can be obtained by
iterating `n` times the differentiation operation.  -/
iteratedDerivWithin_eq_iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜},
  iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
CategoryTheory.Functor.mapVertexGroup_apply : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type v} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (c : C) (a : c ⟶ c), (φ.mapVertexGroup c) a = φ.map a
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceRpcConnectParams : Lean.Lsp.FileSource Lean.Lsp.RpcConnectParams
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Alt.mk : Lean.Name → Lean.Meta.ElimAltInfo → Lean.MVarId → Lean.Elab.Tactic.ElimApp.Alt
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.homInduction_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P : {x y : CategoryTheory.Join C D} → (x ⟶ y) → Sort u_1}
  (left : (x y : C) → (f : x ⟶ y) → P ((CategoryTheory.Join.inclLeft C D).map f))
  (right : (x y : D) → (f : x ⟶ y) → P ((CategoryTheory.Join.inclRight C D).map f))
  (edge : (c : C) → (d : D) → P (CategoryTheory.Join.edge c d)) {x y : D} (f : x ⟶ y),
  CategoryTheory.Join.homInduction left right edge ((CategoryTheory.Join.inclRight C D).map f) = right x y f
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- Auxiliary structure used to glue metric spaces below, recording an isometric embedding
of a type `A` in another metric space.  -/
GromovHausdorff.AuxGluingStruct : (A : Type) → [MetricSpace A] → Type 1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.leadingExp_def : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)), ms.leadingExp = ms.seq.leadingExp
-- Mathlib.CategoryTheory.Presentable.Finite
/-- A functor `F : C ⥤ D` is finitely accessible if it is `ℵ₀`-accessible.
Equivalently, it preserves all filtered colimits.
See `CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimits`.  -/
CategoryTheory.Functor.IsFinitelyAccessible : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} → [inst_1 : CategoryTheory.Category.{v', u'} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.triangle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Dial C)) Y).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.id Y)
-- Lean.Meta.Tactic.Apply
_private.Lean.Meta.Tactic.Apply.0.Lean.Meta.dependsOnOthers : Lean.Expr → Array Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_revPerm_Iio : ∀ {n : ℕ} (i : Fin n), Finset.map (Equiv.toEmbedding Fin.revPerm) (Finset.Iio i) = Finset.Ioi i.rev
-- Lean.Meta.HaveTelescope
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.mk.injEq : ∀ (expr exprType exprInit exprResult proof : Lean.Expr) (modified : Bool)
  (expr_1 exprType_1 exprInit_1 exprResult_1 proof_1 : Lean.Expr) (modified_1 : Bool),
  ({ expr := expr, exprType := exprType, exprInit := exprInit, exprResult := exprResult, proof := proof,
        modified := modified } =
      { expr := expr_1, exprType := exprType_1, exprInit := exprInit_1, exprResult := exprResult_1, proof := proof_1,
        modified := modified_1 }) =
    (expr = expr_1 ∧
      exprType = exprType_1 ∧
        exprInit = exprInit_1 ∧ exprResult = exprResult_1 ∧ proof = proof_1 ∧ modified = modified_1)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ v₁_1 : Module.Basis n R M₁),
  v₁ = v₁_1 → ∀ (v₂ v₂_1 : Module.Basis m R M₂), v₂ = v₂_1 → LinearMap.toMatrix v₁ v₂ = LinearMap.toMatrix v₁_1 v₂_1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (g : Z ⟶ X) {Z_1 : A}
  (h : F.obj.obj (Opposite.op Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F f)
      (CategoryTheory.CategoryStruct.comp (F.obj.map g.op) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F (CategoryTheory.CategoryStruct.comp (G.map g) f)) h
-- Mathlib.Order.Partition.Finpartition
Finpartition.exists_enumeration : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s),
  ∃ f, ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
-- Mathlib.Algebra.Order.Floor.Semifield
Nat.ceil_le_two_mul : ∀ {K : Type u_2} [inst : Field K] [inst_1 : LinearOrder K] [IsOrderedRing K] [inst_3 : FloorSemiring K] {a : K},
  2⁻¹ ≤ a → ↑⌈a⌉₊ ≤ 2 * a
-- Lean.Meta.Tactic.Intro
/-- Introduce one object from the goal `mvarid`, without preserving the name used in the binder.
Returns a pair made of the newly introduced variable (which will have an inaccessible name)
and the new goal. This will fail if there is nothing to introduce, ie when the goal
does not start with a forall, lambda or let.  -/
Lean.MVarId.intro1 : Lean.MVarId → Lean.MetaM (Lean.FVarId × Lean.MVarId)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- If `A` has doubling strictly less than `2`, then `A * A⁻¹ = A⁻¹ * A`.  -/
Finset.mul_inv_eq_inv_mul_of_doubling_lt_two : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G}, (A * A).card < 2 * A.card → A * A⁻¹ = A⁻¹ * A
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.coindResAdjunction_homEquiv_symm_apply : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S)
  {B : Rep.{max (max u v) w, u, v} k G} (f : A ⟶ Rep.res S.subtype B),
  ((Rep.coindResAdjunction k S).homEquiv A B).symm f =
    CategoryTheory.CategoryStruct.comp A.indCoindIso.inv ((Rep.indResHomEquiv S.subtype A B).symm f)
-- Mathlib.Data.Num.ZNum
ZNum.cast_inj : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {m n : ZNum}, ↑m = ↑n ↔ m = n
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_one : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero ι] [inst_2 : Semiring M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)], DirectSum.toAddMonoidAlgebra 1 = 1
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.iselect.eq_1 : ∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (ps : PFunctor.Approx.Path F) (x : F.M),
  PFunctor.M.iselect ps x = (PFunctor.M.isubtree ps x).head
-- Std.Http.Internal.Char
/-- Checks if a byte is a decimal digit (0-9).
 -/
Std.Http.Internal.Char.isDigitByte : UInt8 → Bool
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.center_le_normalizer : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.center G ≤ Subgroup.normalizer s
-- Init.Data.List.Find
List.findIdx_getElem : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {w : List.findIdx p xs < xs.length}, p xs[List.findIdx p xs] = true
-- Mathlib.Order.Monotone.MonovaryOrder
monovary_iff_exists_monotone : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Monovary f g ↔ ∃ x, Monotone f ∧ Monotone g
-- Init.Data.Int.DivMod.Lemmas
Int.add_neg_emod_self : ∀ (a b : ℤ), (a + -b) % b = a % b
-- Mathlib.Algebra.Module.Equiv.Basic
addMonoidHomLequivNat_apply : ∀ {A : Type u_9} {B : Type u_10} (R : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R B] (f : A →+ B), (addMonoidHomLequivNat R) f = f.toNatLinearMap
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If the multiplicative action of `M` on `α` is faithful,
then `fixedBy α m = Set.univ` implies that `m = 1`.  -/
MulAction.fixedBy_eq_univ_iff_eq_one : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] [FaithfulSMul M α] {m : M},
  MulAction.fixedBy α m = Set.univ ↔ m = 1
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_toENNReal_add : ∀ (r : ENNReal) (n : ℕ∞), ⌊↑n + r⌋ₑ = n + ⌊r⌋ₑ
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.exists_mul_lt_of_lt_opNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  {r : ℝ}, 0 ≤ r → r < ‖f‖ → ∃ x, r * ‖x‖ < ‖f x‖
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If `s` is a colimit cofork over `f` and `g`, then a morphism `k : Y ⟶ W` satisfying
`f ≫ k = g ≫ k` induces a morphism `l : s.pt ⟶ W` such that `cofork.π s ≫ l = k`.  -/
CategoryTheory.Limits.Cofork.IsColimit.desc' : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {s : CategoryTheory.Limits.Cofork f g} →
          CategoryTheory.Limits.IsColimit s →
            {W : C} →
              (k : Y ⟶ W) →
                CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k →
                  { l // CategoryTheory.CategoryStruct.comp s.π l = k }
-- Mathlib.Topology.Separation.Basic
minimal_nonempty_open_subsingleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X},
  IsOpen s → (∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) → s.Subsingleton
-- Mathlib.Computability.TuringMachine.Tape
/-- The `cons` and `head`/`tail` functions are mutually inverse, unlike in the case of `List` where
this only holds for nonempty lists.  -/
Turing.ListBlank.exists_cons : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : Turing.ListBlank Γ), ∃ a l', l = Turing.ListBlank.cons a l'
-- Mathlib.GroupTheory.GroupAction.SubMulAction
Units.smul_coe : ∀ (R : Type u_1) (M : Type u_2) [inst : Monoid R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M] (a : Rˣ)
  (x : { x // x ≠ 0 }), ↑(a • x) = a • ↑x
-- Mathlib.Analysis.Convex.Star
StarConvex.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E}, StarConvex 𝕜 x s → ∀ (c : 𝕜), StarConvex 𝕜 (c • x) (c • s)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.subset_closure_of_specializes : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α}, s ⤳ t → t ⊆ closure s