mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- If `f : X → Y` is an `IsUniformInducing` map, the image `f '' s` of a set `s` is complete
if and only if `s` is complete.  -/
IsUniformInducing.isComplete_iff : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  IsUniformInducing f → (IsComplete (f '' s) ↔ IsComplete s)
-- Mathlib.Topology.Order.LiminfLimsup
limsup_eq_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [FirstCountableTopology α]
  [OrderTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α}, Filter.limsup u f = ⊥ ↔ u =ᶠ[f] ⊥
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], Set.Ioi ⊤ = ∅
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_neg' : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M}
  {s : Finset ι} [AddLeftStrictMono M], (∀ i ∈ s, f i ≤ 0) → (∃ i ∈ s, f i < 0) → ∑ i ∈ s, f i < 0
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.degree_le_one_of_irreducible : ∀ {R : Type u_1} [inst : CommSemiring R] {f : Polynomial R}, f.Splits → Irreducible f → f.degree ≤ 1
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.addUnit_neg : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a), ⋯.addUnit = -h.addUnit
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_smul_left : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F) (r : ℝ),
  inner ℝ (r • x) y = r * inner ℝ x y
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X)
  [∀ (x : ↥U), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C ↑x).map f.hom)],
  CategoryTheory.IsIso (f.hom.app (Opposite.op U))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α} {v : β}, (m.insert k v).getKey! k = k
-- Std.Data.TreeMap.Raw.Basic
/-- Partitions a tree map into two tree maps based on a predicate.  -/
Std.TreeMap.Raw.partition : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      (α → β → Bool) → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp × Std.TreeMap.Raw α β cmp
-- Mathlib.Combinatorics.Young.YoungDiagram
_private.Mathlib.Combinatorics.Young.YoungDiagram.0.YoungDiagram.cellsOfRowLens.match_1.splitter : (motive : List ℕ → Sort u_1) →
  (x : List ℕ) → (Unit → motive []) → ((w : ℕ) → (ws : List ℕ) → motive (w :: ws)) → motive x
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.instFinitenessRelation : {α₁ α₂ : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Monad m] →
        [inst_1 : Std.Iterator α₁ m β] →
          [inst_2 : Std.Iterator α₂ m β] →
            [Std.Iterators.Finite α₁ m] →
              [Std.Iterators.Finite α₂ m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.Append α₁ α₂ m β) m
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.ExtendByOne.hom.eq_1 : ∀ {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [inst : MulOneClass R],
  Function.ExtendByOne.hom R s = { toFun := fun f => Function.extend s f 1, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addZeroClass.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : AddZeroClass β],
  e.addZeroClass = Function.Injective.addZeroClass ⇑e ⋯ ⋯ ⋯
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.ofPointTensor t))
      (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).SpecTensorTo =
    (CategoryTheory.Limits.pullback f g).fromSpecResidueField t
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.sUnion : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {S : Set (Set X)},
  DirectedOn (fun x1 x2 => x1 ⊆ x2) S → (∀ s ∈ S, Convexity.IsConvexSet R s) → Convexity.IsConvexSet R (⋃₀ S)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_right : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Add β]
  [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.Kernel.IndepFun (f i) (f j + f k) κ μ
-- Mathlib.Order.CompleteBooleanAlgebra
inf_iSup₂_eq : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : Order.Frame α] {f : (i : ι) → κ i → α} (a : α),
  a ⊓ ⨆ i, ⨆ j, f i j = ⨆ i, ⨆ j, a ⊓ f i j
-- Batteries.Data.List.Lemmas
List.isChain_lt_range' : ∀ {step : ℕ} (s n : ℕ), 0 < step → List.IsChain (fun x1 x2 => x1 < x2) (List.range' s n step)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddLeftCancelSemigroupOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddLeftCancelSemigroup Mᵃᵒᵖ], DomAddAct.instAddLeftCancelSemigroupOfAddOpposite = inst
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- If the summation filter is the trivial filter `⊥`, then the topological sum is
equal to the finite sum (which is taken to be 1 if the support of `f` is infinite).

Note that in this case `HasSum f a` is satisfied for *every* element `a` of the target, so the
value assigned to the `tsum` is a question of conventions.  -/
tsum_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  ¬L.NeBot → ∀ (f : β → α), ∑'[L] (b : β), f b = ∑ᶠ (b : β), f b
-- Mathlib.Order.Hom.Lex
/-- `Equiv.sumProdDistrib` promoted to an order isomorphism of lexicographic products.

Right distributivity doesn't hold. A counterexample is `ℕ ×ₗ (Unit ⊕ₗ Unit) ≃o ℕ`
which is not isomorphic to `ℕ ×ₗ Unit ⊕ₗ ℕ ×ₗ Unit ≃o ℕ ⊕ₗ ℕ`.  -/
Prod.Lex.sumLexProdLexDistrib : (α : Type u_4) →
  (β : Type u_5) →
    (γ : Type u_6) →
      [inst : Preorder α] →
        [inst_1 : Preorder β] → [inst_2 : Preorder γ] → Lex ((α ⊕ₗ β) × γ) ≃o Lex (α × γ) ⊕ₗ Lex (β × γ)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ_natCast : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (n : ℕ),
  ↑(Lean.Grind.Ring.OfSemiring.natCast n) = Lean.Grind.Ring.OfSemiring.natCast n
-- Mathlib.MeasureTheory.Group.Measure
/-- **Alias** of `MeasureTheory.eventually_nhds_one_measure_smul_sdiff_lt`.

---

Continuity of the measure of translates of a compact set: Given a compact set `k` in a
topological group, for `g` close enough to the origin, `μ (g • k \ k)` is arbitrarily small.  -/
MeasureTheory.eventually_nhds_one_measure_smul_diff_lt : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [μ.InnerRegularCompactLTTop] {k : Set G},
  IsCompact k → IsClosed k → ∀ {ε : ENNReal}, ε ≠ 0 → ∀ᶠ (g : G) in nhds 1, μ (g • k \ k) < ε
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v : β k') → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)),
  (match Std.DTreeMap.Internal.Impl.inner size k' v l r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v l r => h_2 size k' v l r) =
    h_2 size k' v l r
-- Mathlib.CategoryTheory.Types.Basic
/-- Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms
of types.  -/
equivIsoIso : {X Y : Type u} → X ≃ Y ≅ X ≅ Y
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgEquiv.toBialgIso_hom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : Bialgebra R X]
  [inst_4 : Bialgebra R Y] (e : X ≃ₐc[R] Y), e.toBialgIso.hom = BialgCat.ofHom ↑e
-- Mathlib.Algebra.Opposites
AddOpposite.unop_add : ∀ {α : Type u_1} [inst : Add α] (x y : αᵃᵒᵖ), AddOpposite.unop (x + y) = AddOpposite.unop y + AddOpposite.unop x
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac_apply_eq_zero_or_one : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α},
  (MeasureTheory.Measure.dirac a) s = 0 ∨ (MeasureTheory.Measure.dirac a) s = 1
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- The tagged partition made of boxes of `π` that satisfy predicate `p`.  -/
BoxIntegral.TaggedPrepartition.filter : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    BoxIntegral.TaggedPrepartition I → (BoxIntegral.Box ι → Prop) → BoxIntegral.TaggedPrepartition I
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [inst_3 : Inhabited (β k')],
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (m.insertMany l).get! k' = cast ⋯ v
-- Mathlib.Algebra.Field.Defs
/-- However `Rat.cast q` is defined, it must be propositionally equal to `q.num / q.den`.

Do not use this lemma directly. Use `Rat.cast_def` instead.  -/
DivisionRing.ratCast_def : ∀ {K : Type u_2} [self : DivisionRing K] (q : ℚ), ↑q = ↑q.num / ↑q.den
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- The second morphism of triangles given by an `Octahedron'`.  -/
CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) →
                        {v₁₂ : Z₁₂ ⟶ X₁} →
                          {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂} →
                            (h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles) →
                              {v₂₃ : Z₂₃ ⟶ X₂} →
                                {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃} →
                                  (h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                    {v₁₃ : Z₁₃ ⟶ X₁} →
                                      {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃} →
                                        (h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                          CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃ →
                                            (CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ⟶
                                              CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃)
-- Mathlib.Analysis.Normed.Group.Completion
UniformSpace.Completion.instNorm : (E : Type u_1) → [inst : UniformSpace E] → [Norm E] → Norm (UniformSpace.Completion E)
-- Std.Sync.Broadcast
/-- Tried to send to a closed broadcast channel.
 -/
Std.Broadcast.Error.closed : Std.Broadcast.Error
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.restrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] (s : Set α) {f : α → ε},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp f p (μ.restrict s)
-- Lean.Elab.App
Lean.Elab.Term.ElabElimInfo.mk.sizeOf_spec : ∀ (elimExpr elimType : Lean.Expr) (motivePos : ℕ) (majorsPos : Array ℕ),
  sizeOf { elimExpr := elimExpr, elimType := elimType, motivePos := motivePos, majorsPos := majorsPos } =
    1 + sizeOf elimExpr + sizeOf elimType + sizeOf motivePos + sizeOf majorsPos
-- Std.Http.Data.URI.Basic
Std.Http.URI.Query.instToString : ToString Std.Http.URI.Query
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.HasLeftDual.exact : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {Y : C} → [self : CategoryTheory.HasLeftDual Y] → CategoryTheory.ExactPairing (ᘁY) Y
-- Lean.Environment
_private.Lean.Environment.0.Lean.exportIREntries : Lean.Environment → Array (Lean.Name × Array Lean.EnvExtensionEntry)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ}
  (A B : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  B ≠ A → CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (s.πSummand B) = 0
-- Lean.Compiler.IR.Basic
Lean.IR.LitVal.num.inj : ∀ {v v_1 : ℕ}, Lean.IR.LitVal.num v = Lean.IR.LitVal.num v_1 → v = v_1
-- Lean.Parser.Do
Lean.Parser.Term.doLetArrow.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.liff_iff_limplies_and_limplies : ∀ {α : Type u} {σ1 : Type v} {σ2 : Type w} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2 ↔
    Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f2 ∧ Std.Tactic.BVDecide.LRAT.Internal.Limplies α f2 f1
-- Init.Data.List.Monadic
List.zipWithM_nil_left : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {l : List β} [inst : Monad m]
  {f : α → β → m γ}, List.zipWithM f [] l = pure []
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.mapIso_hom_π : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).hom (CategoryTheory.Limits.Pi.π g b) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (p b).hom
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod_id_fst : ∀ (C : Type u₁) [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] (D : Type u₂)
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] (X : C × D),
  (CategoryTheory.CategoryStruct.id X).1 = CategoryTheory.CategoryStruct.id X.1
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.Hom.id_single : {ι : Type v} → (i : ι) → (CategoryTheory.Pairwise.single i).Hom (CategoryTheory.Pairwise.single i)
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.incSteps : Lean.Meta.Grind.GoalM Unit
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.contains (t.maxKeyD fallback) = true
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, ∅.maxKey? = none
-- Mathlib.Topology.Sequences
seqClosure_eq_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FrechetUrysohnSpace X] (s : Set X), seqClosure s = closure s
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.coinduced_continuous : ∀ {R : Type u_2} {S : Type u_3} [t : TopologicalSpace R] [inst : Ring S] (f : R → S), Continuous f
-- Mathlib.Algebra.Group.Action.End
/-- `Equiv.Perm.applyMulAction` is faithful.  -/
Equiv.Perm.applyFaithfulSMul : ∀ (α : Type u_6), FaithfulSMul (Equiv.Perm α) α
-- Std.Async.UDP
Std.Async.UDP.Membership.enterGroup : Std.Async.UDP.Membership
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop)
  {L₁ L₂ : FiniteGaloisIntermediateField k K} (h : L₁ ⟶ L₂),
  (CategoryTheory.ConcreteCategory.hom ((finGaloisGroupFunctor k K).map h.op)) ((InfiniteGalois.proj L₂) g) =
    (InfiniteGalois.proj L₁) g
-- Init.Data.UInt.Bitwise
UInt8.shiftRight_eq_shiftRight_mod : ∀ (a b : UInt8), a >>> b = a >>> (b % 8)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.isCyclic_iff_card_le_three : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], IsCyclic ↥(alternatingGroup α) ↔ Nat.card α ≤ 3
-- Mathlib.Logic.Denumerable
Denumerable.mk : {α : Type u_3} →
  [toEncodable : Encodable α] → (∀ (n : ℕ), ∃ a ∈ Encodable.decode n, Encodable.encode a = n) → Denumerable α
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- Taking a limit after whiskering by `G` is the same as using `G` and then taking a limit.  -/
CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : Type u₁} →
          [inst_2 : CategoryTheory.Category.{v₁, u₁} J] →
            {K : Type u₂} →
              [inst_3 : CategoryTheory.Category.{v₂, u₂} K] →
                (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                  (G : CategoryTheory.Functor D K) →
                    [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C] →
                      CategoryTheory.Limits.limit (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) ≅
                        G.comp (CategoryTheory.Limits.limit F)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insertMany_list_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)}, m.insertMany l = ∅ ↔ m = ∅ ∧ l = []
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableWithinAt_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  DifferentiableWithinAt 𝕜 Φ s x ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => Φ x i) s x
-- Init.Data.Array.Basic
Array.instBEq : {α : Type u} → [BEq α] → BEq (Array α)
-- Init.Omega.Int
Lean.Omega.Int.ofNat_sub_dichotomy : ∀ {a b : ℕ}, b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0
-- Init.Data.Vector.Lemmas
Vector.and_any_distrib_left : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool} {q : Bool}, (q && xs.any p) = xs.any fun a => q && p a
-- Mathlib.Data.Seq.Computation
Computation.Bind.g.eq_2 : ∀ {α : Type u} {β : Type v} (ca : Computation β), Computation.Bind.g (Sum.inr ca) = Sum.inr (Sum.inr ca)
-- Mathlib.Tactic.Basic
/-- The `variables` command: this is just a stub,
and merely warns that it has been renamed to `variable` in Lean 4.  -/
Mathlib.Tactic.elabVariables : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.divInvMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst_1 : One M₂] [inst_2 : Pow M₂ ℕ] [inst_3 : Inv M₂]
  [inst_4 : Div M₂] [inst_5 : Pow M₂ ℤ] [inst_6 : DivInvMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Surjective.divInvMonoid f hf one mul inv div npow zpow =
    { toMonoid := Function.Surjective.monoid f hf one mul npow, toInv := inst_3, toDiv := inst_4,
      zpow := fun n x => x ^ n, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯ }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.branch.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Γ → σ → Bool) (a_1 a_2 : Turing.TM1.Stmt Γ Λ σ) (a_3 : Γ → σ → Bool)
  (a_4 a_5 : Turing.TM1.Stmt Γ Λ σ),
  (Turing.TM1.Stmt.branch a a_1 a_2 = Turing.TM1.Stmt.branch a_3 a_4 a_5) = (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.id_apply : ∀ (M : Type u_10) [inst : Zero M] (x : M), (ZeroHom.id M) x = x
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuous_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  LowerSemicontinuous f ↔ ∀ (x : α), LowerSemicontinuousAt f x
-- Mathlib.Condensed.Discrete.LocallyConstant
CondensedSet.LocallyConstant.instFullFunctor : CondensedSet.LocallyConstant.functor.Full
-- Mathlib.Order.Partition.Equipartition
Finpartition.IsEquipartition.card_parts_eq_average : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {P : Finpartition s},
  P.IsEquipartition → t ∈ P.parts → t.card = s.card / P.parts.card ∨ t.card = s.card / P.parts.card + 1
-- Std.Async.System
Std.Async.System.GroupInfo.mk.injEq : ∀ (groupName : String) (groupId : Std.Async.System.GroupId) (members : Array String) (groupName_1 : String)
  (groupId_1 : Std.Async.System.GroupId) (members_1 : Array String),
  ({ groupName := groupName, groupId := groupId, members := members } =
      { groupName := groupName_1, groupId := groupId_1, members := members_1 }) =
    (groupName = groupName_1 ∧ groupId = groupId_1 ∧ members = members_1)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.toGradedRingHom_injective : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  Function.Injective GradedAlgHom.toGradedRingHom
-- Mathlib.Tactic.FunProp.Elab
/-- `fun_prop` config elaborator  -/
Mathlib.Meta.FunProp.elabFunPropConfig : Lean.Syntax →
  optParam Mathlib.Meta.FunProp.Config { } → optParam Bool true → Lean.Elab.Tactic.TacticM Mathlib.Meta.FunProp.Config