mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ProxyType
/-- Create a `Sum` of types, mildly optimized to not have a trailing `Empty`.

The `decorateSum` function is to wrap the `Sum` with a function such as `Lex`.
It should yield a definitionally equal type.  -/
Mathlib.ProxyType.defaultMkProxyType : Array (Lean.Name × Lean.Expr × Lean.Term) →
  optParam (Lean.Expr → Lean.Elab.TermElabM Lean.Expr) pure →
    Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic)
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.hasProductsOfShape : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.ContainsIdentities]
  (J : Type) [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J],
  CategoryTheory.Limits.HasProductsOfShape J D
-- Mathlib.Topology.GDelta.Basic
/-- The intersection of an encodable family of Gδ sets is a Gδ set.  -/
IsGδ.iInter : ∀ {X : Type u_1} {ι' : Sort u_4} [inst : TopologicalSpace X] [Countable ι'] {s : ι' → Set X},
  (∀ (i : ι'), IsGδ (s i)) → IsGδ (⋂ i, s i)
-- Init.Data.UInt.Bitwise
UInt32.or_self : ∀ {a : UInt32}, a ||| a = a
-- Mathlib.Tactic.Recover
/-- Get all metavariables which `mvarId` depends on. These are the metavariables
which occur in the target or local context or delayed assignment (if any) of
`mvarId`, plus the metavariables which occur in these metavariables, etc.
 -/
Mathlib.Tactic.getUnassignedGoalMVarDependencies : Lean.MVarId → Lean.MetaM (Std.HashSet Lean.MVarId)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Finset.Nat.antidiagonalTuple_zero_succ : ∀ (n : ℕ), Finset.Nat.antidiagonalTuple 0 n.succ = ∅
-- Mathlib.GroupTheory.Congruence.Defs
/-- The integer power induced on the quotient by a congruence relation on a type with a
division.  -/
Con.instZPow : {M : Type u_1} → [inst : Group M] → (c : Con M) → Pow c.Quotient ℤ
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.isLittleO_im_pow_exp_re : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → ∀ (n : ℕ), (fun z => z.im ^ n) =o[l] fun z => Real.exp z.re
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.sModNat.eq_1 : ∀ (q : ℕ), LucasLehmer.norm_num_ext.sModNat q 0 = 4 % q
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.image_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Functor C MonCat),
  CategoryTheory.SubmonoidFunctor.image (CategoryTheory.CategoryStruct.id M) ⊤ = ⊤
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instNonUnitalCommRing : {R : Type u_1} → [NonUnitalCommRing R] → NonUnitalCommRing Rᵒᵈ
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.isFiniteKernel_of_le : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ ν : ProbabilityTheory.Kernel α β}
  [hν : ProbabilityTheory.IsFiniteKernel ν], κ ≤ ν → ProbabilityTheory.IsFiniteKernel κ
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_map_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  {X_1 Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X} (g : X_1 ⟶ Y),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).map g).left.left = g.left
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E}, x ∈ s → (ContDiffWithinAt 𝕜 0 f s x ↔ ∃ u ∈ nhdsWithin x s, ContinuousOn f (s ∩ u))
-- Mathlib.GroupTheory.OrderOfElement
orderOf_ne_zero_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, orderOf x ≠ 0 ↔ IsOfFinOrder x
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.isPrimitiveRoot_exp_of_coprime : ∀ (i n : ℕ), n ≠ 0 → i.Coprime n → IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n))) n
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.mk : ∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty},
  P.toProperty.RespectsIso →
    (∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y)
        (r : ↑(Y.presheaf.obj (Opposite.op ⊤))), P f → P (f ∣_ Y.basicOpen r)) →
      (∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y)
          (s : Finset ↑(Y.presheaf.obj (Opposite.op ⊤))),
          Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (f ∣_ Y.basicOpen ↑r)) → P f) →
        P.IsLocal
-- Mathlib.Data.Rat.Defs
Rat.inv_mkRat : ∀ (a : ℤ) (b : ℕ), (mkRat a b)⁻¹ = Rat.divInt (↑b) a
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
/-- `a ⊭ f` reads formula `f` is false under assignment `a`.
 -/
Std.Tactic.BVDecide.LRAT.Internal.«term_⊭_» : Lean.TrailingParserDescr
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.typeName : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Cases pu → Lean.Name
-- Init.Data.SInt.Basic
Int64.instNeg : Neg Int64
-- Init.Data.Vector.Lemmas
Vector.eq_of_mem_singleton : ∀ {α : Type u_1} {b a : α}, a ∈ #v[b] → a = b
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.divisionCommMonoid : {α : Type u} → [SubtractionCommMonoid α] → DivisionCommMonoid (Multiplicative α)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.valuation_single_zpow : ∀ (K : Type u_2) [inst : Field K] (s : ℤ), Valued.v ((HahnSeries.single s) 1) = WithZero.exp (-s)
-- Init.SimpLemmas
eq_self : ∀ {α : Sort u_1} (a : α), (a = a) = True
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The naturality of `HomotopyCategory.BinaryProduct.inverse`
with respect to the first variable.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategoryProdIdCompInverseIso : {X X' : SSet.Truncated 2} →
  (Y : SSet.Truncated 2) →
    (f : X ⟶ X') →
      ((SSet.Truncated.mapHomotopyCategory f).prod (CategoryTheory.Functor.id Y.HomotopyCategory)).comp
          (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X' Y) ≅
        (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
          (SSet.Truncated.mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_id_f_hom_eq_mapRange : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (i : ℕ) (φ : A ⟶ B),
  ModuleCat.Hom.hom ((groupHomology.chainsMap (MonoidHom.id G) φ).f i) =
    Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofOptionInfo.sizeOf_spec : ∀ (i : Lean.Elab.OptionInfo), sizeOf (Lean.Elab.Info.ofOptionInfo i) = 1 + sizeOf i
-- Mathlib.RingTheory.Extension.Generators
Algebra.Extension.defaultHom_toRingHom_apply : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (p : MvPolynomial S R),
  (Algebra.Extension.defaultHom R S P).toRingHom p = MvPolynomial.eval₂ (algebraMap R P.Ring) P.σ p
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_var_const_cert.eq_1 : ∀ (lhs rhs : Int.Internal.Linear.Expr) (x : Int.Internal.Linear.Var) (k : ℤ),
  Int.Internal.Linear.norm_eq_var_const_cert lhs rhs x k =
    (lhs.sub rhs).norm.beq' (Int.Internal.Linear.Poly.add 1 x (Int.Internal.Linear.Poly.num (-k)))
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side, version subtracting vectors.  -/
InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → Real.sin (InnerProductGeometry.angle x (x - y)) * ‖x - y‖ = ‖y‖
-- Mathlib.Data.Finset.Card
Finset.strongDownwardInductionOn_eq : ∀ {α : Type u_1} {n : ℕ} {p : Finset α → Sort u_4} (s : Finset α)
  (H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁),
  (fun a => s.strongDownwardInductionOn H a) = H s fun {t} ht x => t.strongDownwardInductionOn H ht
-- Mathlib.Condensed.Discrete.Colimit
/-- A presheaf, which takes a profinite set written as a cofiltered limit to the corresponding
colimit, agrees with the left Kan extension of its restriction.
 -/
Condensed.lanPresheafIso : {S : Profinite} →
  {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} →
    CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op) →
      ((Condensed.lanPresheaf F).obj (Opposite.op S) ≅ F.obj (Opposite.op S))
-- Std.Internal.Do.PredTrans
/-- Extensionality for predicate transformers.  -/
Std.Internal.Do.PredTrans.ext : ∀ {Pred : Type u_1} {EPred : Type u_2} {α : Type u_3} {x y : Std.Internal.Do.PredTrans Pred EPred α},
  (∀ (post : α → Pred) (epost : EPred), x.apply post epost = y.apply post epost) → x = y
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Connected.coeSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (G'' : G'.coe.Subgraph),
  G''.Connected → (SimpleGraph.Subgraph.coeSubgraph G'').Connected
-- Batteries.Control.LawfulMonadState
liftM_getModify : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [inst : MonadStateOf σ m] [inst_1 : MonadLift m n]
  (f : σ → σ), liftM (getModify f) = getModify f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_stepkC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k₁ k : ℤ) (init p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.d_stepk_certC k₁ p₁ k₂ m₂ p₂ p c = true →
    ↑k * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p₁ →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 →
        ↑(k₁ * k) * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Z : ChainComplex C ℕ}
  (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty
      (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty h) =
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty h
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_lt_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α} {a : α},
  ⊥ < a → (s.sup f < a ↔ ∀ b ∈ s, f b < a)
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.unop_le_unop : ∀ {α : Type u_1} [inst : Preorder α] {a b : αᵐᵒᵖ}, MulOpposite.unop a ≤ MulOpposite.unop b ↔ a ≤ b
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ext_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {p q : SkewMonoidAlgebra k G},
  p = q ↔ ∀ (n : G), p.coeff n = q.coeff n
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.IsStronglyPredictable.predictablePart_eq : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.SigmaFiniteFiltration μ ℱ],
  MeasureTheory.IsStronglyPredictable ℱ f →
    (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) → ∀ (n : ℕ), MeasureTheory.predictablePart f ℱ μ n =ᵐ[μ] f n - f 0
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.Result.map.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.error e s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_2 e s'
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {f : (a : α) → β a → Bool} {k : α},
  (Std.ExtDHashMap.filter f m).getKey! k = ((m.getKey? k).pfilter fun x_2 h' => f x_2 (m.get x_2 ⋯)).get!
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₂ → (t₁ \ t₂).get! k = t₁.get! k
-- Mathlib.Data.List.Induction
List.bidirectionalRec.eq_def : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a])
  (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (x : List α),
  List.bidirectionalRec nil singleton cons_append x =
    match x with
    | [] => nil
    | [a] => singleton a
    | a :: b :: l =>
      ⋯ ▸
        cons_append a (b :: l).dropLast ((b :: l).getLast ⋯)
          (List.bidirectionalRec nil singleton cons_append (b :: l).dropLast)
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.submoduleImage.eq_1 : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_10}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {O : Submodule R M} (ϕ : ↥O →ₗ[R] M') (N : Submodule R M),
  ϕ.submoduleImage N = Submodule.map ϕ (Submodule.comap O.subtype N)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- `SL(2, ℝ)` acts transitively on the upper half-plane.  -/
UpperHalfPlane.isPretransitiveSL2R : MulAction.IsPretransitive (Matrix.SpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.val_step_intermediateDropWhile.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.GroupTheory.Perm.ViaEmbedding
Equiv.Perm.viaEmbedding_apply_of_notMem : ∀ {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (ι : α ↪ β), ∀ x ∉ Set.range ⇑ι, (e.viaEmbedding ι) x = x
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_sdiff_distrib_right : ∀ {α : Type u_1} (s t u : Set α), s \ t ∩ u = (s ∩ u) \ (t ∩ u)
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Ordinal.isPrincipal_opow_ord`. -/
Ordinal.principal_opow_ord : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Ordinal.IsPrincipal (fun x1 x2 => x1 ^ x2) c.ord
-- Mathlib.Order.Atoms
IsCoatom.ne_top : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, IsCoatom a → a ≠ ⊤
-- Lean.Server.References
/-- Location of the reference.  -/
Lean.Server.References.DocumentRefInfo.location : Lean.Server.References.DocumentRefInfo → Lean.Lsp.Location
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgStrLit : Lean.Doc.FromDocArg Lean.StrLit
-- Mathlib.Topology.Order.Completion
/-- A dense linear order into which α embeds continuously, formed by "filling in" the blanks.  -/
Order.Fill : (α : Type u_2) → [LinearOrder α] → Type u_2
-- Std.Http.Data.URI
/-- Parses a `RequestTarget` from the given string. Panics if parsing fails. Use `parse?`
if you need a safe option-returning version.
 -/
Std.Http.RequestTarget.parse! : String → Std.Http.RequestTarget
-- Mathlib.Order.Antisymmetrization
AntisymmRel.antisymmRel_congr_left : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b →
    (AntisymmRel (fun x1 x2 => x1 ≤ x2) a c ↔ AntisymmRel (fun x1 x2 => x1 ≤ x2) b c)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_op_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] (s : Finset α),
  Finset.map AddOpposite.opEquiv.toEmbedding (-s) = -Finset.map AddOpposite.opEquiv.toEmbedding s
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.Options.ignoreIfExists : Lean.Lsp.CreateFile.Options → Bool
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_const_mul_self : ∀ {a : EReal}, (LinearGrowth.linearGrowthSup fun n => a * ↑n) = a
-- Init.System.IOError
instCoeStringError : Coe String IO.Error
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingCompOf_eq_bot_of_isNilpotent : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [LieModule.IsNilpotent L M] (x : L), LieModule.posFittingCompOf R M x = ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.mem_degenerate_iff : ∀ (X : SSet) {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  x ∈ X.degenerate n ↔
    ∃ m,
      ∃ (_ : m < n),
        ∃ f, ∃ (_ : CategoryTheory.Epi f), x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (X.map f.op))
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))
  (Z : CategoryTheory.Limits.WalkingParallelPair),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj F U c).π.app Z =
    CategoryTheory.Limits.WalkingParallelPair.casesOn Z
      (CategoryTheory.Limits.Pi.lift fun i => c.π.app (Opposite.op (CategoryTheory.Pairwise.single i)))
      (CategoryTheory.Limits.Pi.lift fun b => c.π.app (Opposite.op (CategoryTheory.Pairwise.pair b.1 b.2)))
-- Mathlib.CategoryTheory.MarkovCategory.Basic
CategoryTheory.MarkovCategory.toCopyDiscardCategory : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.MarkovCategory C] → CategoryTheory.CopyDiscardCategory C
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the monadic predicate `p` returns `ULift.up true` for
any element emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first match. The outputs of `it` are
examined in order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.anyM`.
 -/
Std.IterM.Total.anyM : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] →
          [Std.Iterators.Finite α m] → (β → m (ULift.{w, 0} Bool)) → Std.IterM.Total m β → m (ULift.{w, 0} Bool)
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.of_compatible : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β},
  G.Compatible H → e ∈ H.edgeSet → G.Inc e x → H.Inc e x
-- Std.Async.Basic
Std.Async.ETask.instFunctor : {ε : Type} → Functor (Std.Async.ETask ε)
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.mulSupport_add_one' : ∀ {ι : Type u_1} {R : Type u_5} [inst : One R] [inst_1 : AddRightCancelMonoid R] (f : ι → R),
  Function.mulSupport (f + 1) = Function.support f
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom : ∀ {A : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} A] [inst_1 : CategoryTheory.Abelian A]
  {Y : CategoryTheory.SimplicialObject A},
  AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.hom =
    AlgebraicTopology.inclusionOfMooreComplexMap Y
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.CotangentSpace.fst_compEquiv_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ)
  (x : (Q.comp P).toExtension.CotangentSpace),
  ((Algebra.Generators.CotangentSpace.compEquiv Q P) x).1 =
    (Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) x
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- Constructor for isomorphisms in `P.FullSubcategory` when
`P : ObjectProperty C`.  -/
CategoryTheory.ObjectProperty.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.ObjectProperty C) → {X Y : P.FullSubcategory} → (X.obj ≅ Y.obj) → (X ≅ Y)
-- Mathlib.Data.List.Sort
List.sortedLT_finRange : ∀ (n : ℕ), (List.finRange n).SortedLT
-- Mathlib.Topology.Connected.PathConnected
Joined.mul : ∀ {M : Type u_4} [inst : Mul M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {a b c d : M},
  Joined a b → Joined c d → Joined (a * c) (b * d)
-- Mathlib.Util.AtLocation
/-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).

Assumes `proc` is not surrounded by backticks.  -/
Mathlib.Tactic.transformAtLocation : (Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) →
  String →
    Lean.Elab.Tactic.Location →
      optParam Mathlib.Tactic.BehaviorIfUnchanged Mathlib.Tactic.BehaviorIfUnchanged.error →
        optParam Bool false → optParam Lean.Meta.Simp.Context default → Lean.Elab.Tactic.TacticM Unit
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.hasMVarAtCurrDepth : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.inter_isBasis_biInter : ∀ {α : Type u_2} {M : Matroid α} {I : Set α} {ι : Type u_4},
  M.Indep I →
    ∀ {X : ι → Set α} {A : Set ι},
      A.Nonempty → (∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)) → M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)
-- Mathlib.FieldTheory.IsSepClosed
/-- If `E / F` is a field extension and `E` is separably closed, then the separable closure
of `F` in `E` is equal to `F` if and only if `F` is separably closed.  -/
IsSepClosed.separableClosure_eq_bot_iff : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsSepClosed E],
  separableClosure F E = ⊥ ↔ IsSepClosed F
-- Mathlib.RingTheory.WittVector.Identities
WittVector.mul_charP_coeff_zero : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x : WittVector p R),
  (x * ↑p).coeff 0 = 0
-- Aesop.Rule.Name
Aesop.BuilderName.apply.sizeOf_spec : sizeOf Aesop.BuilderName.apply = 1
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_comp_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {i : ℕ} (a : 𝕜),
  ContDiff 𝕜 (↑i) f → (iteratedFDeriv 𝕜 i fun z => f (a • z)) = fun x => a ^ i • iteratedFDeriv 𝕜 i f (a • x)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_single : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : SMulWithZero R S]
  [inst_3 : Monoid S] (x : Sˣ) (n : ℤ) (r : R), LaurentPolynomial.smeval (AddMonoidAlgebra.single n r) x = r • ↑(x ^ n)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_mul : ∀ {a b : Ordinal.{u_1}}, a ≠ 0 → Order.IsSuccPrelimit b → (a * b).cof = b.cof
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Presieve.preZeroHypercover_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (R : CategoryTheory.Presieve S) (i : ↑R.uncurry),
  R.preZeroHypercover.f i = (↑i).snd
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNorm_sub_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} {f g : α → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      1 ≤ p → MeasureTheory.eLpNorm (f - g) p μ ≤ MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ