mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- Constructor for simple graphs using a symmetric irreflexive Boolean function.  -/
SimpleGraph.mk' : {V : Type u} → { adj // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true } ↪ SimpleGraph V
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.Types.end_.condition_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} {i j : J} (f : i ⟶ j)
  {Z : Type (max w u)} (h : (F.obj (Opposite.op i)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.end_.π F i)
      (CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op i)).map f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.end_.π F j)
      (CategoryTheory.CategoryStruct.comp ((F.map f.op).app j) h)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofπ'.eq_1 : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : π ∘ₗ relations.map = 0),
  Module.Relations.Solution.ofπ' π hπ = Module.Relations.Solution.ofπ π ⋯
-- Mathlib.Data.Set.Basic
Set.ssubset_union_left_iff : ∀ {α : Type u} {s t : Set α}, s ⊂ s ∪ t ↔ ¬t ⊆ s
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.valid.sizeOf_spec : ∀ (escaped : Bool) (acc : String),
  sizeOf (Std.Http.Internal.UnquoteState.valid✝ escaped acc) = 1 + sizeOf escaped + sizeOf acc
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.continuousWithinAt_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {b : β} {s : Set β},
  ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, dist (f x) (f b) < ε
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : C} (f : X ⟶ Y),
  J.uliftYonedaEquiv ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map f) = { down := f }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.Equation.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) (x y : R),
  W.Equation x y = (Polynomial.evalEval x y W.polynomial = 0)
-- Mathlib.Data.List.Sigma
List.kextract.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α), List.kextract a [] = (none, [])
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.residueField_map_bijective : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : IsLocalRing R],
  Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)))
-- Lean.Meta.Tactic.Induction
Lean.Meta.AltVarNames.mk.inj : ∀ {explicit : Bool} {varNames : List Lean.Name} {explicit_1 : Bool} {varNames_1 : List Lean.Name},
  { explicit := explicit, varNames := varNames } = { explicit := explicit_1, varNames := varNames_1 } →
    explicit = explicit_1 ∧ varNames = varNames_1
-- Mathlib.Data.Set.Functor
Set.coe_subset : ∀ {α : Type u} {β : Set α} {γ : Set ↑β},
  (do
      let a ← γ
      pure ↑a) ⊆
    β
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.algebraMap_intNorm_fractionRing : ∀ {A : Type u_1} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : IsIntegrallyClosed A] [inst_4 : IsDomain A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B]
  [inst_7 : Algebra.IsIntegral A B] [inst_8 : Module.IsTorsionFree A B] (x : B),
  (algebraMap A (FractionRing A)) ((Algebra.intNorm A B) x) =
    (Algebra.norm (FractionRing A)) ((algebraMap B (FractionRing B)) x)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Auxiliary definition for `inclusion`.  -/
CategoryTheory.FreeMonoidalCategory.inclusionObj : {C : Type u} → CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → CategoryTheory.FreeMonoidalCategory C
-- Mathlib.Topology.Instances.AddCircle.Real
ZMod.toAddCircle_inj : ∀ {N : ℕ} [inst : NeZero N] {j k : ZMod N}, ZMod.toAddCircle j = ZMod.toAddCircle k ↔ j = k
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Subalgebra.bot_eq_top_iff_finrank_eq_one : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [StrongRankCondition F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  [Nontrivial E] [Module.Free F E], ⊥ = ⊤ ↔ Module.finrank F E = 1
-- Mathlib.Topology.Path
Path.reparam_id : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ.reparam id ⋯ ⋯ ⋯ = γ
-- Lean.Util.ShareCommon
Lean.ShareCommon.PShareCommonM.run : {α : Type u_1} → Lean.ShareCommon.PShareCommonM α → α
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.rightDerivedUnique.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (RF RF' : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α α_1 : F ⟶ L.comp RF) (e_α : α = α_1) (α'₂ α'₂_1 : F ⟶ L.comp RF') (e_α'₂ : α'₂ = α'₂_1)
  (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] [inst_5 : RF'.IsRightDerivedFunctor α'₂ W],
  RF.rightDerivedUnique RF' α α'₂ W = RF.rightDerivedUnique RF' α_1 α'₂_1 W_1
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsLimitsOfShape.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F : CategoryTheory.Functor C D},
  autoParam (∀ {K : CategoryTheory.Functor J C}, CategoryTheory.Limits.ReflectsLimit K F)
      CategoryTheory.Limits.ReflectsLimitsOfShape.reflectsLimit._autoParam →
    CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcKeepAliveParams.toJson : Lean.Lsp.RpcKeepAliveParams → Lean.Json
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.map_implicitFunction_nhdsWithin_preimage : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) (s : Set E),
  Filter.map (φ.implicitFunction (φ.leftFun φ.pt))
      (nhdsWithin (φ.rightFun φ.pt) (φ.implicitFunction (φ.leftFun φ.pt) ⁻¹' s)) =
    nhdsWithin φ.pt (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})
-- Init.Data.String.Iterate
String.Slice.instInhabitedRevPosIterator : {a : String.Slice} → Inhabited a.RevPosIterator
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.map_subtype_mem_of_mem_invtSubmodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p : Submodule R M} (hp : p ∈ f.invtSubmodule) {q : Submodule R ↥p},
  q ∈ Module.End.invtSubmodule (LinearMap.restrict f hp) → Submodule.map p.subtype q ∈ f.invtSubmodule
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.pow_mem : ∀ {M : Type u_5} [inst : Monoid M] (S : Submonoid M) {x : M}, x ∈ S → ∀ (n : ℕ), x ^ n ∈ S
-- Init.Data.Array.Lemmas
Array.eq_empty_of_size_eq_zero : ∀ {α : Type u_1} {xs : Array α}, xs.size = 0 → xs = #[]
-- Mathlib.Analysis.Calculus.FDeriv.Pow
fderiv_pow_ring : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {x : 𝔸} (n : ℕ),
  fderiv 𝕜 (fun x => x ^ n) x = (n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸
-- Init.Data.String.Lemmas.Order
String.Pos.next_eq_iff : ∀ {s : String} {p q : s.Pos} {h : p ≠ s.endPos}, p.next h = q ↔ p < q ∧ ∀ (q' : s.Pos), p < q' → q ≤ q'
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Render the list of rewrite results in one section.  -/
_private.Mathlib.Tactic.Widget.LibraryRewrite.0.Mathlib.Tactic.LibraryRewrite.renderRewrites.renderSectionCore : Lean.Lsp.Range →
  Lean.Server.FileWorker.EditableDocument →
    Bool → Array Mathlib.Tactic.LibraryRewrite.RewriteInterface → ProofWidgets.Html
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.IsExtensionBy.congr_simp : ∀ {aig : Std.Sat.AIG ℕ} (state1 state1_1 : Std.Sat.AIG.toCNF.State✝ aig),
  state1 = state1_1 →
    ∀ (state2 state2_1 : Std.Sat.AIG.toCNF.State✝ aig),
      state2 = state2_1 →
        ∀ (new new_1 : ℕ) (e_new : new = new_1) (hnew : new < aig.decls.size),
          Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state1 state2 new hnew =
            Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state1_1 state2_1 new_1 ⋯
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.homMk.congr_simp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.LeftLift f g} (η η_1 : s.lift ⟶ t.lift) (e_η : η = η_1)
  (w : CategoryTheory.CategoryStruct.comp s.unit (CategoryTheory.Bicategory.whiskerRight η f) = t.unit),
  CategoryTheory.Bicategory.LeftLift.homMk η w = CategoryTheory.Bicategory.LeftLift.homMk η_1 ⋯
-- Mathlib.Order.Bounds.Basic
not_bddAbove_univ : ∀ {α : Type u_1} [inst : Preorder α] [NoTopOrder α], ¬BddAbove Set.univ
-- Mathlib.Algebra.Jordan.Basic
IsCommJordan.lmul_comm_rmul_rmul : ∀ {A : Type u_1} {inst : CommMagma A} [self : IsCommJordan A] (a b : A), a * b * (a * a) = a * (b * (a * a))
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_ofNatLT : ∀ {n : ℕ} (hn : n < USize.size) (h : System.Platform.numBits = 32), (USize.ofNatLT n hn).toBitVec32 h = n#'⋯
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero₁_of_isThirdQuadrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Y : CategoryTheory.Abelian.SpectralObject C EInt) [Y.IsThirdQuadrant] (i j : EInt) (hij : i ≤ j),
  WithBotTop.coe 0 < i →
    ∀ (n : ℤ),
      CategoryTheory.Limits.IsZero ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))
-- Mathlib.Order.SuccPred.Limit
/-- Successor limits aren't minimal.  -/
Order.IsSuccLimit.not_isMin : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Order.IsSuccLimit a → ¬IsMin a
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The under category has as objects arrows with domain `X` and as morphisms commutative
triangles.  -/
CategoryTheory.Under : {T : Type u₁} → [CategoryTheory.Category.{v₁, u₁} T] → T → Type (max u₁ v₁)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin_eq_starClosure_adjoin : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (s : Set A), NonUnitalStarAlgebra.adjoin R s = (NonUnitalAlgebra.adjoin R s).starClosure
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The Sierpiński topology on `Prop` is the upper topology  -/
instIsUpperProp : Topology.IsUpper Prop
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.assoc_symm_tmul : ∀ {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R P] [inst_9 : Module S M]
  [inst_10 : IsScalarTower R S M] [inst_11 : Coalgebra S M] [inst_12 : Module S N] [inst_13 : IsScalarTower R S N]
  [inst_14 : Coalgebra S N] [inst_15 : Coalgebra R P] (x : M) (y : N) (z : P),
  (Coalgebra.TensorProduct.assoc R S M N P).symm (x ⊗ₜ[S] (y ⊗ₜ[R] z)) = x ⊗ₜ[S] y ⊗ₜ[R] z
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.disjoint_neighborFinset_of_disjoint : ∀ {V : Type u_1} (G H : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)]
  [inst_1 : Fintype ↑(H.neighborSet v)], Disjoint G H → Disjoint (G.neighborFinset v) (H.neighborFinset v)
-- Lean.Declaration
Lean.ReducibilityHints.lt : Lean.ReducibilityHints → Lean.ReducibilityHints → Bool
-- Init.Data.SInt.Basic
/-- Converts a word-sized integer to a 16-bit integer by truncating its bitvector representation.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.toInt16 : ISize → Int16
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_multiset_prod : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)),
  0 ∉ t → t.prod.natDegree = (Multiset.map Polynomial.natDegree t).sum
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.instNonUnitalRingHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β],
  NonUnitalRingHomClass (α →ₙ+* β) α β
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The composition of morphisms between algebras of endofunctor `F`  -/
CategoryTheory.Endofunctor.Coalgebra.Hom.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      {V₀ V₁ V₂ : CategoryTheory.Endofunctor.Coalgebra F} → V₀.Hom V₁ → V₁.Hom V₂ → V₀.Hom V₂
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_pos_iff_exists_mem : ∀ {α : Type u_1} {s : Multiset α}, 0 < s.card ↔ ∃ a, a ∈ s
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.span_union : ∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (s t : Set L),
  LieSubalgebra.lieSpan R L (s ∪ t) = LieSubalgebra.lieSpan R L s ⊔ LieSubalgebra.lieSpan R L t
-- Mathlib.Algebra.Free
FreeMagma.traverse_mul' : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β),
  Function.comp (traverse F) ∘ HMul.hMul = fun x y => (fun x1 x2 => x1 * x2) <$> traverse F x <*> traverse F y
-- Mathlib.Order.Category.BoolAlg
/-- The type of morphisms in `BoolAlg R`.  -/
BoolAlg.Hom : BoolAlg → BoolAlg → Type u
-- Mathlib.Order.SuccPred.Limit
/-- The lemma formerly named `not_isSuccPrelimit_iff` is now
`not_isSuccPrelimit_iff_succ_eq`  -/
Order.not_isSuccPrelimit_iff_exists_covBy : ∀ {α : Type u_1} [inst : LT α] {a : α}, ¬Order.IsSuccPrelimit a ↔ ∃ b, b ⋖ a
-- Mathlib.Order.Sublattice
/-- Two sublattices are equal if they have the same elements.  -/
Sublattice.ext : ∀ {α : Type u_2} [inst : Lattice α] {L M : Sublattice α}, (∀ (a : α), a ∈ L ↔ a ∈ M) → L = M
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.enorm_setIntegral_le_of_enorm_le_const : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {C : ENNReal}, (∀ x ∈ s, ‖f x‖ₑ ≤ C) → ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.LawfulEqCmp cmp]
  [Std.TransCmp cmp], t.WF → ∀ {k : α}, k ∈ t.keysArray ↔ k ∈ t
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_extendDomain`. -/
Equiv.Perm.SameCycle.extendDomain : ∀ {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {x y : α} {p : β → Prop} [inst : DecidablePred p]
  {f : α ≃ Subtype p}, g.SameCycle x y → (g.extendDomain f).SameCycle ↑(f x) ↑(f y)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.subset : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α), (L.lhomWithConstants α).onTheory T ⊆ ↑p
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getLE_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, (cmp a k).isLE = true} (h : t₁.Equiv t₂), t₁.getLE k h' = t₂.getLE k ⋯
-- Lean.Meta.Basic
Lean.Meta.Context.mk.injEq : ∀ (keyedConfig : Lean.Meta.ConfigWithKey) (trackZetaDelta : Bool) (zetaDeltaSet : Lean.FVarIdSet)
  (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances) (defEqCtx? : Option Lean.Meta.DefEqContext)
  (synthPendingDepth : ℕ) (canUnfold? : Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool))
  (univApprox inTypeClassResolution cacheInferType : Bool) (keyedConfig_1 : Lean.Meta.ConfigWithKey)
  (trackZetaDelta_1 : Bool) (zetaDeltaSet_1 : Lean.FVarIdSet) (lctx_1 : Lean.LocalContext)
  (localInstances_1 : Lean.LocalInstances) (defEqCtx?_1 : Option Lean.Meta.DefEqContext) (synthPendingDepth_1 : ℕ)
  (canUnfold?_1 : Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool))
  (univApprox_1 inTypeClassResolution_1 cacheInferType_1 : Bool),
  ({ keyedConfig := keyedConfig, trackZetaDelta := trackZetaDelta, zetaDeltaSet := zetaDeltaSet, lctx := lctx,
        localInstances := localInstances, defEqCtx? := defEqCtx?, synthPendingDepth := synthPendingDepth,
        canUnfold? := canUnfold?, univApprox := univApprox, inTypeClassResolution := inTypeClassResolution,
        cacheInferType := cacheInferType } =
      { keyedConfig := keyedConfig_1, trackZetaDelta := trackZetaDelta_1, zetaDeltaSet := zetaDeltaSet_1,
        lctx := lctx_1, localInstances := localInstances_1, defEqCtx? := defEqCtx?_1,
        synthPendingDepth := synthPendingDepth_1, canUnfold? := canUnfold?_1, univApprox := univApprox_1,
        inTypeClassResolution := inTypeClassResolution_1, cacheInferType := cacheInferType_1 }) =
    (keyedConfig = keyedConfig_1 ∧
      trackZetaDelta = trackZetaDelta_1 ∧
        zetaDeltaSet = zetaDeltaSet_1 ∧
          lctx = lctx_1 ∧
            localInstances = localInstances_1 ∧
              defEqCtx? = defEqCtx?_1 ∧
                synthPendingDepth = synthPendingDepth_1 ∧
                  canUnfold? = canUnfold?_1 ∧
                    univApprox = univApprox_1 ∧
                      inTypeClassResolution = inTypeClassResolution_1 ∧ cacheInferType = cacheInferType_1)
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.go : {β : Type u_1} → {α : Type u_2} → [inst : LE β] → [DecidableLE β] → (α → β) → α → ℕ → ℕ → List α → ℕ
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.ComposableArrows.Precomp.map.eq_4 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) (i : ℕ) (hi : i + 1 < n + 1 + 1) (j : ℕ) (hj : j + 1 < n + 1 + 1) (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩),
  CategoryTheory.ComposableArrows.Precomp.map F f ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij = F.map' i j ⋯ ⋯
-- Batteries.Classes.Order
/-- `cmp x y = .lt` holds iff `x < y` is true.  -/
Std.LawfulCmp.eq_lt_iff_lt : ∀ {α : Type u_1} {inst : LE α} {inst_1 : LT α} {cmp : α → α → Ordering} [self : Std.LawfulCmp cmp] {x y : α},
  cmp x y = Ordering.lt ↔ x < y
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.toList_flatMapAfterM.match_1.eq_1 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m γ) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (it₂ : Std.IterM m γ) → motive (some it₂)),
  (match none with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.zero_of_comp_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f : X ⟶ Y} (g : Y ⟶ Z) [CategoryTheory.Mono g], CategoryTheory.CategoryStruct.comp f g = 0 → f = 0
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.cocycle_fst_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
              (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
            (CategoryTheory.Limits.pullback.snd
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
              (𝒰.f j))))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j))
-- Init.Meta.Defs
/-- Filters an array of syntax, treating every other element as a separator rather than an element to
test with the predicate `p`. The resulting array contains the tested elements for which `p` returns
`true`, separated by the corresponding separator elements.
 -/
Array.filterSepElems : Array Lean.Syntax → (Lean.Syntax → Bool) → Array Lean.Syntax
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Construct the `RefinedDiscrTree` of all local hypotheses.  -/
Mathlib.Tactic.LibraryRewrite.getHypotheses : Option Lean.FVarId → Lean.MetaM (Lean.Meta.RefinedDiscrTree (Lean.FVarId × Bool))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_of_powerRevlex : ∀ {k₁ k₂ : ℕ}, Lean.Grind.CommRing.powerRevlex k₁ k₂ = Ordering.eq → k₁ = k₂
-- Std.Http.Data.URI.Basic
/-- Sets the host as a domain name, panicking if the name contains invalid characters.
The domain name will be automatically lowercased.
Only ASCII alphanumeric characters, hyphens, and dots are allowed.
Each label cannot start or end with `-` and is limited to 63 characters.
Internationalized domain names must be converted to punycode before use.
 -/
Std.Http.URI.Builder.setHost! : Std.Http.URI.Builder → String → Std.Http.URI.Builder
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- A match result contains the results from matching a term against
patterns in the discrimination tree.
 -/
Lean.Meta.RefinedDiscrTree.MatchResult : Type → Type
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balLeft.match_4.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α)
  (h_1 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b))
  (h_2 : (l : RBTree.RBNode α) → motive l),
  (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α), l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
    (match l with
      | RBTree.RBNode.node RBTree.RBColor.red a x b => h_1 a x b
      | l => h_2 l) =
      h_2 l
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.pred.inj : ∀ {q₁ q₂ q₁_1 q₂_1 : Turing.PartrecToTM2.Λ'}, q₁.pred q₂ = q₁_1.pred q₂_1 → q₁ = q₁_1 ∧ q₂ = q₂_1
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.iSup_min : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {ι : Sort u_1}
  (S : ι → CategoryTheory.Subfunctor F) (T : CategoryTheory.Subfunctor F), (⨆ i, S i) ⊓ T = ⨆ i, S i ⊓ T
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.coe_sdiff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} (s t : L.DefinableSet A α),
  ↑(s \ t) = ↑s \ ↑t