mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toArray_filterMapWithPostcondition_filterMapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} {n : Type w → Type w''}
  {δ : Type w} [inst_1 : Monad m] [LawfulMonad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m (Option γ)}
  {g : γ → Std.Iterators.PostconditionT n (Option δ)},
  (Std.IterM.filterMapWithPostcondition g (Std.Iter.filterMapWithPostcondition f it)).toArray =
    (Std.Iter.filterMapWithPostcondition
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toArray
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.Bind.f.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Computation α ⊕ Computation β → Sort u_3) (cb : Computation β)
  (h_1 : (ca : Computation α) → motive (Sum.inl ca)) (h_2 : (cb : Computation β) → motive (Sum.inr cb)),
  (match Sum.inr cb with
    | Sum.inl ca => h_1 ca
    | Sum.inr cb => h_2 cb) =
    h_2 cb
-- Mathlib.Tactic.Ring.RingNF
/-- The tactic `ring` evaluates expressions in *commutative* (semi)rings.
This is the conv tactic version, which rewrites a target which is a ring equality to `True`.

See also the `ring` tactic.
 -/
Mathlib.Tactic.RingNF.convRing! : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_le_range : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y), A.image f ≤ SSet.Subcomplex.range f
-- Mathlib.Tactic.CasesM
/-- `cases_type I` searches for a hypothesis `h : type` where `I` has the form `(I ...)`, and splits the
main goal by cases on `h`. `cases_type p` fails if no hypothesis type has the identifier `I` as its
head symbol.

* `cases_type I_1 ... I_n` searches for a hypothesis `h : type` where `type` has one or more of
  `I_1`, ..., `I_n` as its head symbol, and splits the main goal by cases on `h`.
* `cases_type* I` repeatedly performs case splits until no more hypothesis type has `I` as its head
  symbol. This shorthand for `· repeat cases_type I`.
* `cases_type! p` and `cases_type!* p` skip a hypothesis if the main goal would be replaced with two
  or more subgoals.

Example:
```
example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  cases_type* Or And
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial
```
 -/
Mathlib.Tactic.casesType! : Lean.ParserDescr
-- Mathlib.Order.DirSupClosed
DirSupClosed.sInter : ∀ {α : Type u_1} [inst : Preorder α] {s : Set (Set α)}, (∀ x ∈ s, DirSupClosed x) → DirSupClosed (⋂₀ s)
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuous_restrict_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  LowerHemicontinuous (s.domRestrict f) ↔ LowerHemicontinuousOn f s
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {K : Type z} [inst_2 : CategoryTheory.Category.{z', z} K]
  [CategoryTheory.Limits.HasLimitsOfShape K D],
  CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape (CategoryTheory.Presheaf.IsSheaf J) K
-- Mathlib.GroupTheory.MonoidLocalization.DivPairs
AddSubmonoid.mem_subPairs : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] {f : ⊤.LocalizationMap G}
  {s : AddSubmonoid G} {x : M × M}, x ∈ AddSubmonoid.subPairs f s ↔ f x.1 - f x.2 ∈ s
-- Init.Grind.Offset
Lean.Grind.Nat.unsat_lo_ro : ∀ (u v k₁ k₂ : ℕ), Lean.Grind.isLt k₂ k₁ = true → u + k₁ ≤ v → v ≤ u + k₂ → False
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the denominator of the right fractions  -/
CategoryTheory.MorphismProperty.RightFraction₂.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.RightFraction₂ X Y) → self.X' ⟶ X
-- Init.Data.UInt.Bitwise
UInt16.ofBitVec_not : ∀ (a : BitVec 16), { toBitVec := ~~~a } = ~~~{ toBitVec := a }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpContext.mk.sizeOf_spec : ∀ (triggerKind : Lean.Lsp.SignatureHelpTriggerKind) (triggerCharacter? : Option String) (isRetrigger : Bool)
  (activeSignatureHelp? : Option Lean.Lsp.SignatureHelp),
  sizeOf
      { triggerKind := triggerKind, triggerCharacter? := triggerCharacter?, isRetrigger := isRetrigger,
        activeSignatureHelp? := activeSignatureHelp? } =
    1 + sizeOf triggerKind + sizeOf triggerCharacter? + sizeOf isRetrigger + sizeOf activeSignatureHelp?
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Construct a continuous linear map from `IsBoundedLinearMap`.  -/
IsBoundedLinearMap.toContinuousLinearMap : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring 𝕜] →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : SeminormedAddCommGroup F] →
              [inst_4 : Module 𝕜 F] → (f : E → F) → IsBoundedLinearMap 𝕜 f → E →L[𝕜] F
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaAssocProd_apply_fst : ∀ {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a : (a : α × β) × γ a.1 a.2),
  (Equiv.sigmaAssocProd a).fst = ((Equiv.sigmaEquivProd α β).symm.sigmaCongrLeft' a).fst.fst
-- Init.MetaTypes
Lean.Module.header : Lean.Module → Lean.Syntax
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.lift_of' : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι], Module.DirectLimit.lift R ι G f (Module.DirectLimit.of R ι G f) ⋯ = LinearMap.id
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk_out : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  (m : M ⧸ p), Submodule.Quotient.mk (Quotient.out m) = m
-- Mathlib.Order.Lattice
left_lt_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a < a ⊔ b ↔ ¬b ≤ a
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instMulZeroClass : MulZeroClass ONote
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_inf : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s t : Subsemiring R)
  (f : R →+* S), Function.Injective ⇑f → Subsemiring.map f (s ⊓ t) = Subsemiring.map f s ⊓ Subsemiring.map f t
-- Mathlib.Topology.FiberBundle.Constructions
/-- The topology on the total space of a pullback bundle is the coarsest topology for which both
the projections to the base and the map to the original bundle are continuous.  -/
Pullback.TotalSpace.topologicalSpace : {B : Type u} →
  (F : Type v) →
    (E : B → Type w₁) →
      {B' : Type w₂} →
        (f : B' → B) →
          [TopologicalSpace B'] →
            [TopologicalSpace (Bundle.TotalSpace F E)] → TopologicalSpace (Bundle.TotalSpace F (f *ᵖ E))
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces,
which is smooth, symmetric, with support equal to the ball of radius `D` and integral `1`.  -/
ExistsContDiffBumpBase.w : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] → [FiniteDimensional ℝ E] → [inst_3 : MeasurableSpace E] → [BorelSpace E] → ℝ → E → ℝ
-- Mathlib.RingTheory.PicardGroup
Module.Flat.tensorSubmoduleAlgebraEquiv.congr_simp : ∀ {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) [inst_5 : Module.Flat R M]
  [inst_6 : FaithfulSMul R A], Module.Flat.tensorSubmoduleAlgebraEquiv e = Module.Flat.tensorSubmoduleAlgebraEquiv e
-- Mathlib.Geometry.Euclidean.Simplex
/-- In a triangle, the distance from a vertex to the `faceOppositeCentroid` equals three times the
distance from the `centroid` to the `faceOppositeCentroid`.  -/
Affine.Triangle.dist_point_faceOppositeCentroid : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) (i : Fin 3),
  dist (t.points i) (Affine.Simplex.faceOppositeCentroid t i) =
    3 * dist (Affine.Simplex.centroid t) (Affine.Simplex.faceOppositeCentroid t i)
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.unbot.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : WithBot α) → x ≠ ⊥ → Sort u_2) (x : α) (x_1 : ↑x ≠ ⊥)
  (h_1 : (x : α) → (x_2 : ↑x ≠ ⊥) → motive (some x) x_2),
  (match some x, x_1 with
    | some x, x_2 => h_1 x x_2) =
    h_1 x x_1
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Composition on the left by a continuous linear map, as a `ContinuousLinearMap`.
Similar to `LinearMap.compLeft`.  -/
ContinuousLinearMap.compLeftContinuous : (R : Type u_3) →
  {M : Type u_5} →
    [inst : TopologicalSpace M] →
      {M₂ : Type u_6} →
        [inst_1 : TopologicalSpace M₂] →
          [inst_2 : Semiring R] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : AddCommMonoid M₂] →
                [inst_5 : ContinuousAdd M] →
                  [inst_6 : Module R M] →
                    [inst_7 : ContinuousConstSMul R M] →
                      [inst_8 : ContinuousAdd M₂] →
                        [inst_9 : Module R M₂] →
                          [inst_10 : ContinuousConstSMul R M₂] →
                            (α : Type u_7) → [inst_11 : TopologicalSpace α] → (M →L[R] M₂) → C(α, M) →L[R] C(α, M₂)
-- Mathlib.Tactic.Algebra.Basic
/-- `ExSum BaseType sα e` stores the structure of a normalized polynomial expression `e`, which is
a sum of monomials.  -/
Mathlib.Tactic.Algebra.ExSum : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} → {sR : Q(CommSemiring «$R»)} → {sA : Q(CommSemiring «$A»)} → Q(Algebra «$R» «$A») → Q(«$A») → Type
-- Init.Data.BitVec.Bitblast
/-- At least two out of three Booleans are true.

This function is typically used to model addition of binary numbers, to combine a carry bit with two
addend bits.
 -/
Bool.atLeastTwo : Bool → Bool → Bool → Bool
-- Init.Prelude
/-- Locally modifies the reader monad's value while running an action, with the reader monad's local
value type specified explicitly. This is useful when a monad supports reading more than one type of
value.

During the inner action `x`, reading the value returns `f` applied to the original value. After
control returns from `x`, the reader monad's value is restored.

Use `withReader` for a version that expects the local value's type to be inferred from `m`.
 -/
withTheReader : (ρ : Type u) → {m : Type u → Type v} → [MonadWithReaderOf ρ m] → {α : Type u} → (ρ → ρ) → m α → m α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k k' fallback : α} {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if (f (Std.DTreeMap.Const.get? t k)).isSome = true then k else fallback
    else t.getKeyD k' fallback
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `s` is a monotone family of sets and `f` tends to `atBot` along a nontrivial filter,
then the indexed union of `s ∘ f` is equal to the indexed union of `s`.  -/
Antitone.iUnion_comp_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ},
  Antitone s → ∀ {f : α → β}, Filter.Tendsto f l Filter.atBot → ⋃ a, s (f a) = ⋃ b, s b
-- Mathlib.Data.Seq.Basic
Stream'.Seq.set_all : ∀ {α : Type u} {p : α → Prop} {s : Stream'.Seq α}, (∀ x ∈ s, p x) → ∀ {n : ℕ} {x : α}, p x → ∀ y ∈ s.set n x, p y
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_ratCast : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ), (↑q).valuation = padicValRat p q
-- Init.Data.UInt.Lemmas
UInt16.toFin_mul : ∀ (a b : UInt16), (a * b).toFin = a.toFin * b.toFin
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_nonneg_iff : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b : R}, 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.simpUsingDecide : Lean.Meta.Simp.Simproc
-- Mathlib.FieldTheory.Normal.Defs
Normal.splits : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K],
  Normal F K → ∀ (x : K), (Polynomial.map (algebraMap F K) (minpoly F x)).Splits
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.instSMulNNRat : {K : Type u} →
  [inst : DivisionRing K] → {S : Type u_1} → [inst_1 : SetLike S K] → [h : SubfieldClass S K] → (s : S) → SMul ℚ≥0 ↥s
-- Mathlib.Data.Multiset.UnionInter
Multiset.mem_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
-- Mathlib.Order.Filter.Basic
Filter.Frequently.eq_1 : ∀ {α : Type u_1} (p : α → Prop) (f : Filter α), Filter.Frequently p f = ¬∀ᶠ (x : α) in f, ¬p x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toZeroAtInftyCLM_apply : ∀ (𝕜 : Type u_2) (E : Type u_5) (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : ProperSpace E] [inst_5 : RCLike 𝕜]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x : E),
  ((SchwartzMap.toZeroAtInftyCLM 𝕜 E F) f) x = f x
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instFunLike : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → FunLike (ρ.IntertwiningMap σ) V W
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.mem_pi : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] (I : Set η) {H : (i : η) → AddSubgroup (f i)}
  {p : (i : η) → f i}, p ∈ AddSubgroup.pi I H ↔ ∀ i ∈ I, p i ∈ H i
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_add_right_of_mutuallySingular : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite ν'],
  ν.MutuallySingular ν' → μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν
-- Mathlib.Order.Category.DistLat
DistLat.mk.sizeOf_spec : ∀ (carrier : Type u_1) [str : DistribLattice carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Topology.Algebra.Group.Basic
DenseRange.topologicalClosure_map_subgroup : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : Group H] [inst_4 : TopologicalSpace H] [inst_5 : IsTopologicalGroup H] {f : G →* H},
  Continuous ⇑f →
    DenseRange ⇑f → ∀ {s : Subgroup G}, s.topologicalClosure = ⊤ → (Subgroup.map f s).topologicalClosure = ⊤
-- Init.Data.BitVec.Bitblast
/-- Show that `x >>> y` can be written in terms of `ushiftRightRec`.
This can be unfolded in terms of `ushiftRightRec_zero`, `ushiftRightRec_succ` for bit blasting.
 -/
BitVec.shiftRight_eq_ushiftRightRec : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂), x >>> y = x.ushiftRightRec y (w₂ - 1)
-- Mathlib.Computability.DFA
/-- Regular languages are closed under intersection.  -/
Language.IsRegular.inf : ∀ {T : Type u} {L1 L2 : Language T}, L1.IsRegular → L2.IsRegular → (L1 ⊓ L2).IsRegular
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_singleton : ∀ {α : Type u_2} [inst : InvolutiveNeg α] (a : α), -{a} = {-a}
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquivClass.edist_eq' : ∀ {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} {inst : PseudoEMetricSpace X}
  {inst_1 : PseudoEMetricSpace Y} {inst_2 : EquivLike F X Y} [self : DilationEquivClass F X Y] (f : F),
  ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (f x) (f y) = ↑r * edist x y
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.setLIntegral_const_lt_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (s : Set α)
  {c : ENNReal}, c ≠ ⊤ → ∫⁻ (x : α) in s, c ∂μ < ⊤
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.snd : ∀ {α : Type u_4} {β : Type u_5} [inst : AddMonoid α] [inst_1 : AddMonoid β] {x : α × β},
  IsOfFinAddOrder x → IsOfFinAddOrder x.2
-- Init.Data.Vector.Lemmas
Vector.extract_size : ∀ {α : Type u_1} {n : ℕ} {as : Vector α n}, as.extract = Vector.cast ⋯ as
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Limits.FormalCoproduct C} (i : Y.I)
  (f : X ⟶ Y.obj i) (x : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I),
  (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i f).f x = i
-- Mathlib.FieldTheory.CardinalEmb
/-- `leastExt i` is defined to be the smallest `k : ι` that generates a nontrivial extension over
(i.e. does not lie in) the subalgebra (= intermediate field) generated by all previous
`leastExt j`, `j < i`. For cardinality reasons, such `k` always exist if `ι` is infinite.  -/
Field.Emb.Cardinal.leastExt : (F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [Algebra.IsAlgebraic F E] → (Module.rank F E).ord.ToType → (Module.rank F E).ord.ToType
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `F : X → R → R` tends to `f : R → R` uniformly on the spectrum of `a`, and all
these functions are continuous on the spectrum, then `fun x ↦ cfc (F x) a` tends
to `cfc f a`.  -/
tendsto_cfc_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A]
  [inst_9 : ContinuousFunctionalCalculus R A p] {l : Filter X} {F : X → R → R} {f : R → R} {a : A},
  TendstoUniformlyOn F f l (spectrum R a) →
    (∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)) → Filter.Tendsto (fun x => cfc (F x) a) l (nhds (cfc f a))
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_eq_zero_iff : ∀ {n : ℕ}, ArithmeticFunction.vonMangoldt n = 0 ↔ ¬IsPrimePow n
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- Consider a diagram where the outer square involving types `X₁`, `X₂`, `X₃` and `X₅`
is a pullback, where the two bottom and right triangles commute:
```
     t
 X₁  ⟶  X₂
l|     |r  \
 v   b  v   \ r'
 X₃  ⟶  X₄   \
  \       k\  |
   \ b'     v v
    \______> X₅
```
Assume that `r'` and `k` are monomorphisms, that `r` and `b` are jointly surjective,
and that `b'` is injective on the complement of the range of `l`, then
the top-left square is a pushout.  -/
CategoryTheory.Limits.Types.isPushout_of_isPullback_of_mono : ∀ {X₁ X₂ X₃ X₄ X₅ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄} {k : X₄ ⟶ X₅} {r' : X₂ ⟶ X₅}
  {b' : X₃ ⟶ X₅},
  CategoryTheory.IsPullback t l r' b' →
    CategoryTheory.CategoryStruct.comp r k = r' →
      CategoryTheory.CategoryStruct.comp b k = b' →
        ∀ [CategoryTheory.Mono r'] [CategoryTheory.Mono k],
          Set.range ⇑(CategoryTheory.ConcreteCategory.hom r) ⊔ Set.range ⇑(CategoryTheory.ConcreteCategory.hom b) =
              Set.univ →
            (∀ (x₃ y₃ : X₃),
                x₃ ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom l) →
                  y₃ ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom l) →
                    (CategoryTheory.ConcreteCategory.hom b') x₃ = (CategoryTheory.ConcreteCategory.hom b') y₃ →
                      x₃ = y₃) →
              CategoryTheory.IsPushout t l r b
-- Mathlib.Algebra.Group.Commute.Hom
AddCommute.of_map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {x y : M} [inst_2 : FunLike F M N]
  [AddHomClass F M N] {f : F}, Function.Injective ⇑f → AddCommute (f x) (f y) → AddCommute x y
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.toInvariantForm_form : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R], B.toInvariantForm.form = B.form
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getUInt32Value? : Lean.Expr → OptionT Id UInt32
-- Mathlib.SetTheory.Ordinal.Basic
List.SortedGT.lt_ord_of_lt : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] {l m : List α} {o : Ordinal.{u}},
  l.SortedGT →
    m.SortedGT →
      m < l →
        (∀ i ∈ l, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o) →
          ∀ i ∈ m, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The forgetful functor from lax braided functors to lax monoidal functors
is fully faithful.  -/
CategoryTheory.LaxBraidedFunctor.fullyFaithfulForget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] → CategoryTheory.LaxBraidedFunctor.forget.FullyFaithful
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_prod_iff : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {F : Filter (α × β)},
  Cauchy F ↔ Cauchy (Filter.map Prod.fst F) ∧ Cauchy (Filter.map Prod.snd F)
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- Use `Algebra.QuasiFiniteAt.eq_of_le_of_under_eq` instead for `Algebra.QuasiFiniteAt R p`.  -/
Algebra.WeaklyQuasiFiniteAt.eq_of_le_of_under_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P Q : Ideal S}
  [P.IsPrime] [inst_4 : Q.IsPrime],
  P ≤ Q → Ideal.under R P = Ideal.under R Q → ∀ [Algebra.WeaklyQuasiFiniteAt R Q], P = Q
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.instInhabited : (α : Type u_2) → [inst : Bornology α] → Inhabited (LocallyBoundedMap α α)
-- Mathlib.Order.Hom.Order
OrderHom.instMin : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : SemilatticeInf β] → Min (α →o β)
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t ∈ ∂^k 𝒜` iff `t` is exactly `k` elements less than something in `𝒜`.

See also `Finset.mem_shadow_iterate_iff_exists_sdiff`.  -/
Finset.mem_shadow_iterate_iff_exists_mem_card_add : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α} {k : ℕ},
  t ∈ Finset.shadow^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ s.card = t.card + k
-- Mathlib.Order.Disjoint
Disjoint.ne : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, a ≠ ⊥ → Disjoint a b → a ≠ b