mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace.congr_simp : ∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.LocallyRingedSpace)
  (f f_1 : X ⟶ Y.toPresheafedSpace) (e_f : f = f_1) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f =
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f_1
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Quot.instMeasurableSpace : {α : Type u_6} → {r : α → α → Prop} → [m : MeasurableSpace α] → MeasurableSpace (Quot r)
-- Mathlib.Topology.Connected.PathConnected
Joined.neg : ∀ {G : Type u_4} [inst : Neg G] [inst_1 : TopologicalSpace G] [ContinuousNeg G] {x y : G}, Joined x y → Joined (-x) (-y)
-- Aesop.Search.Expansion.Norm
/-- On success, returns the rule tactic's result, the new forward state and the
new forward rule matches. If `rule` corresponds to some forward rule matches,
returns the matches as well.  -/
Aesop.runNormRuleTac : Aesop.NormRule →
  Aesop.RuleTacInput →
    Aesop.ForwardState →
      Aesop.LocalRuleSet →
        Aesop.NormM
          (Option (Aesop.NormRuleResult × Aesop.ForwardState × Std.HashSet Lean.FVarId) × Array Aesop.ForwardRuleMatch)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.intervalIntegrable_sqrt_one_sub_sq_inv : IntervalIntegrable (fun x => √(1 - x ^ 2)⁻¹) MeasureTheory.volume (-1) 1
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isCobounded_iff_closedBall_compl_subset : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} (c : α),
  Bornology.IsCobounded s ↔ ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.insertListConst : {α : Type u} → {β : Type v} → [BEq α] → List ((_ : α) × β) → List (α × β) → List ((_ : α) × β)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.mul_ne_cert.eq_1 : ∀ (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.mul_ne_cert p₁ k p = (k != 0 && (Lean.Grind.CommRing.Poly.mulConst_k k p₁).beq' p)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DTreeMap.Raw.Const.get? (m₁ ∩ m₂) k = none
-- Mathlib.Data.EReal.Operations
/-- Extension for the `positivity` tactic: sum of two `EReal`s.  -/
Mathlib.Meta.Positivity.evalERealAdd : Mathlib.Meta.Positivity.PositivityExt
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.delete.injEq : ∀ (a a_1 : Lean.Lsp.DeleteFile), (Lean.Lsp.DocumentChange.delete a = Lean.Lsp.DocumentChange.delete a_1) = (a = a_1)
-- Init.Data.List.Nat.Range
/-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction.  -/
List.mk_mem_zipIdx_iff_getElem? : ∀ {α : Type u_1} {i : ℕ} {x : α} {l : List α}, (x, i) ∈ l.zipIdx ↔ l[i]? = some x
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.subsemigroupMap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) (x : ↥M'),
  ↑((f.subsemigroupMap M') x) = f ↑x
-- Mathlib.RingTheory.Ideal.Maps
Ideal.mem_map_iff_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S], Function.Surjective ⇑f → ∀ {I : Ideal R} {y : S}, y ∈ Ideal.map f I ↔ ∃ x ∈ I, f x = y
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.instPartialOrder : {X : AlgebraicGeometry.Scheme} → PartialOrder X.AffineZariskiSite
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (motive : aig.BinaryRefVec w → Sort u_1) (lhs rhs : aig.RefVec w)
  (h_1 : (lhs rhs : aig.RefVec w) → motive { lhs := lhs, rhs := rhs }),
  (match { lhs := lhs, rhs := rhs } with
    | { lhs := lhs, rhs := rhs } => h_1 lhs rhs) =
    h_1 lhs rhs
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.ucs_comap_incl : ∀ {R : Type u} {L : Type v} {M : Type w} [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] (N : LieSubmodule R L M)
  [inst_6 : LieModule R L M] (k : ℕ), LieSubmodule.comap N.incl (LieSubmodule.ucs k ⊥) = LieSubmodule.ucs k ⊥
-- Mathlib.Topology.Separation.Regular
/-- A subspace of a completely normal space is a completely normal space.  -/
instCompletelyNormalSpaceSubtype : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompletelyNormalSpace X] {p : X → Prop},
  CompletelyNormalSpace { x // p x }
-- Lean.DocString.Types
Lean.Doc.Inline.image.inj : ∀ {i : Type u} {alt url alt_1 url_1 : String},
  Lean.Doc.Inline.image alt url = Lean.Doc.Inline.image alt_1 url_1 → alt = alt_1 ∧ url = url_1
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (CategoryTheory.Comon D)) (X : C),
  CategoryTheory.ComonObj.comul.app X = CategoryTheory.ComonObj.comul
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.prop_iff_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f], P X ↔ P Y
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Restrict the codomain of an `AlgHom` `f` to `f.range`.

This is the bundled version of `Set.rangeFactorization`.  -/
AlgHom.rangeRestrict : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → (f : A →ₐ[R] B) → A →ₐ[R] ↥f.range
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.mem_restrictSupport_iff : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] {s : Set (σ →₀ ℕ)} {r : MvPolynomial σ R},
  r ∈ MvPolynomial.restrictSupport R s ↔ ↑r.support ⊆ s
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Tensoring on the left with `X ⊗ Y` is naturally isomorphic to
tensoring on the left with `Y`, and then again with `X`.
 -/
CategoryTheory.MonoidalCategory.tensorLeftTensor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ≅
          (CategoryTheory.MonoidalCategory.tensorLeft Y).comp (CategoryTheory.MonoidalCategory.tensorLeft X)
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `edist (f n) (f (n+1))` is bounded by `C * 2^-n`, then the distance from
`f n` to the limit of `f` is bounded above by `2 * C * 2^-n`.  -/
edist_le_of_edist_le_geometric_two_of_tendsto : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (C : ENNReal) {f : ℕ → α},
  (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), edist (f n) a ≤ 2 * C / 2 ^ n
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.hom_tensorHom : ∀ {R : Type u} [inst : CommRing R] {K L M N : AlgCat R} (f : K ⟶ L) (g : M ⟶ N),
  AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    Algebra.TensorProduct.map (AlgCat.Hom.hom f) (AlgCat.Hom.hom g)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.isoSheafify_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D}
  (hP : CategoryTheory.Presheaf.IsSheaf J P),
  (J.isoSheafify hP).inv = J.sheafifyLift (CategoryTheory.CategoryStruct.id P) hP
-- Mathlib.RingTheory.Ideal.Maps
Submodule.mem_annihilator_span_singleton : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (g : M)
  (r : R), r ∈ (R ∙ g).annihilator ↔ r • g = 0
-- Mathlib.Analysis.Complex.Trigonometric
Complex.nnnorm_exp_I_mul_ofReal : ∀ (x : ℝ), ‖Complex.exp (Complex.I * ↑x)‖₊ = 1
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.of_left_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y)
  [CategoryTheory.IsIso i], CategoryTheory.HasLiftingProperty i p
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2_inv : ∀ {F : Type u_1} [inst : Field F] (a : F) (ha : a ≠ 0),
  (Matrix.SpecialLinearGroup.diag2 a ha)⁻¹ = Matrix.SpecialLinearGroup.diag2 a⁻¹ ⋯
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.subAt_mono : ∀ {A : Type u_1} {S : ↥(Descriptive.tree A)} (T : ↥(Descriptive.tree A)) (x : List A),
  S ≤ T → Descriptive.Tree.subAt S x ≤ Descriptive.Tree.subAt T x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedLetValue : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.LetValue a)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.cancelAux.eq_2 : ∀ (m₁ r₁ r₂ : Nat.Internal.Linear.Poly) (fuel_2 : ℕ),
  Nat.Internal.Linear.Poly.cancelAux fuel_2.succ m₁ [] r₁ r₂ = (List.reverse r₁ ++ m₁, List.reverse r₂)
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Generates a proof of `P' → ∃ a, p a`. We assume that `fvars = [f₁, ..., fₙ]` are free variables
and `P' = ∃ f₁ ... fₙ, newBody`, and `path` leads to `a = a'` in `∃ a, p a`.

The proof follows the following structure:
```
example {α β : Type} (f : β → α) {p : α → Prop} :
    (∃ b, p (f b) ∧ f b = f b) → (∃ a, p a ∧ ∃ b, a = f b) := by
  -- withLocalDeclQ
  intro h
  -- withNestedExistsElim : we unpack all quantifiers in `P` to get `h : newBody`.
  refine h.elim (fun b h ↦ ?_)
  -- use `a'` in the leading existential quantifier
  refine Exists.intro (f b) ?_
  -- then we traverse `newBody` and goal simultaneously
  refine And.intro ?_ ?_
  -- at branches outside the path `h` must coincide with goal
  · replace h := h.left
    exact h
  -- inside path we substitute variables from `fvars` into existential quantifiers.
  · replace h := h.right
    refine Exists.intro b ?_
    -- at the end the goal must be `x' = x'`.
    rfl
```  -/
ExistsAndEq.mkAfterToBefore : {u : Lean.Level} →
  {α : Q(Sort u)} →
    {p : Q(«$α» → Prop)} →
      {P' : Q(Prop)} → Q(«$α») → Q(Prop) → List ExistsAndEq.VarQ → ExistsAndEq.Path → Lean.MetaM Q(«$P'» → ∃ a, «$p» a)
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_pos_iff : ∀ {α : Type u_1} [Finite α], 0 < Nat.card α ↔ Nonempty α
-- Mathlib.LinearAlgebra.Ray
SameRay.zero_left : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (y : M), SameRay R 0 y
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.below : {α : Type u} →
  {g : Set (Set α)} →
    {motive : (a : Set α) → TopologicalSpace.GenerateOpen g a → Prop} →
      {a : Set α} → TopologicalSpace.GenerateOpen g a → Prop
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.fromSkeleton_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (a : Quotient (CategoryTheory.isIsomorphicSetoid C)),
  (CategoryTheory.fromSkeleton C).obj a = a.out
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.aeval_val_eq_zero : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {x : P.Ring}, x ∈ P.ker → (MvPolynomial.aeval P.val) x = 0
-- Mathlib.Order.WellFoundedSet
/-- A version of **Dickson's lemma** on finite product of well-quasi-ordered sets. See
`WellQuasiOrdered.pi` when the type `α i` is well-quasi-ordered.  -/
Set.PartiallyWellOrderedOn.pi : ∀ {ι : Type u_1} {α : ι → Type u_6} [Finite ι] {r : (i : ι) → α i → α i → Prop} [∀ (i : ι), IsPreorder (α i) (r i)]
  {s : (i : ι) → Set (α i)},
  (∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)) →
    (Set.univ.pi s).PartiallyWellOrderedOn fun a b => ∀ (i : ι), r i (a i) (b i)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.forIn'_toArray_eq_forIn' : ∀ {α : Type u} {r : Std.Rii α} [inst : LT α] [inst_1 : Std.PRange.Least? α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_3 : Std.Rxi.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ}
  {m : Type u → Type w} [inst_5 : Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)},
  forIn' r.toArray init f = forIn' r init fun a x acc => f a ⋯ acc
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.sharesVar.eq_def : ∀ (s₁ s₂ : Lean.Grind.AC.Seq),
  s₁.sharesVar s₂ =
    match s₁, s₂ with
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y => x == y
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s₂ => x == y || (Lean.Grind.AC.Seq.var x).sharesVar s₂
    | Lean.Grind.AC.Seq.cons x s₁, Lean.Grind.AC.Seq.var y => x == y || s₁.sharesVar (Lean.Grind.AC.Seq.var y)
    | Lean.Grind.AC.Seq.cons x s₁, Lean.Grind.AC.Seq.cons y s₂ =>
      if (x == y) = true then true
      else if x < y then s₁.sharesVar (Lean.Grind.AC.Seq.cons y s₂) else (Lean.Grind.AC.Seq.cons x s₁).sharesVar s₂
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.full_whiskeringLeft_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D],
  ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Quotient r) D).obj (CategoryTheory.Quotient.functor r)).Full
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.ConfigWithKey.mk.sizeOf_spec : ∀ (config : Lean.Meta.Config) (key : UInt64), sizeOf { config := config, key := key } = 1 + sizeOf config + sizeOf key
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.opCompYonedaSectionsEquiv_apply_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor J C) (X : C)
  (s : ↑(F.op.comp (CategoryTheory.yoneda.obj X)).sections) (j : J),
  ((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X) s).app j = ↑s (Opposite.op j)
-- Mathlib.Data.Finset.Insert
Finset.nonempty_mk : ∀ {α : Type u_1} {m : Multiset α} {hm : m.Nodup}, { val := m, nodup := hm }.Nonempty ↔ m ≠ 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_insert_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, Std.DHashMap.Raw.Const.get? (m.insert k v) k = some v
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {h' : k ∈ Std.TreeMap.filter f t}, (Std.TreeMap.filter f t)[k] = t[k]
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {km : α},
  t.min? = some km → t.contains km = true
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι),
  ((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P).X n).p = P.p.f n
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.ext_iff : ∀ {C D : CategoryTheory.Cat} {F G : C ⟶ D}, F = G ↔ F.toFunctor = G.toFunctor
-- Mathlib.Data.Matrix.Reflection
/-- `Matrix.transpose` with better defeq for `Fin`  -/
Matrix.transposeᵣ : {α : Type u_1} → {m n : ℕ} → Matrix (Fin m) (Fin n) α → Matrix (Fin n) (Fin m) α
-- Std.Do.SPred.SPred
/-- Conjunction in `SPred`: states that satisfy `P` and satisfy `Q` satisfy `spred(P ∧ Q)`.  -/
Std.Do.SPred.and : {σs : List (Type u)} → Std.Do.SPred σs → Std.Do.SPred σs → Std.Do.SPred σs
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_sub : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (f g : CompactlySupportedContinuousMap α β), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Data.List.Induction
List.bidirectionalRec.hcongr_6 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (motive : List α → Sort u_2) (motive' : List α' → Sort u_2),
      motive ≍ motive' →
        ∀ (nil : motive []) (nil' : motive' []),
          nil ≍ nil' →
            ∀ (singleton : (a : α) → motive [a]) (singleton' : (a : α') → motive' [a]),
              singleton ≍ singleton' →
                ∀ (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b])))
                  (cons_append' : (a : α') → (l : List α') → (b : α') → motive' l → motive' (a :: (l ++ [b]))),
                  cons_append ≍ cons_append' →
                    ∀ (l : List α) (l' : List α'),
                      l ≍ l' →
                        List.bidirectionalRec nil singleton cons_append l ≍
                          List.bidirectionalRec nil' singleton' cons_append' l'
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.right.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (a a_1 : D), (CategoryTheory.Join.right a = CategoryTheory.Join.right a_1) = (a = a_1)
-- Mathlib.Algebra.Order.Monoid.Submonoid
AddSubmonoid.coe_nonneg : ∀ (M : Type u_1) [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftMono M],
  ↑(AddSubmonoid.nonneg M) = Set.Ici 0
-- Std.Async.ContextAsync
Std.Async.ContextAsync.instMonadFinally : MonadFinally Std.Async.ContextAsync
-- Mathlib.Order.BooleanAlgebra.Basic
Prod.instBooleanAlgebra : {α : Type u} → {β : Type u_1} → [BooleanAlgebra α] → [BooleanAlgebra β] → BooleanAlgebra (α × β)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.eq_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.FreeGroupoid C),
  X = CategoryTheory.FreeGroupoid.mk X.as.as
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.limsup_neg : ∀ {α : Type u_3} {f : Filter α} {v : α → EReal}, Filter.limsup (-v) f = -Filter.liminf v f
-- Lean.Expr
/-- Return `true` if the given `BinderInfo` is a strict implicit annotation (e.g., `⦃α : Type u⦄`)  -/
Lean.BinderInfo.isStrictImplicit : Lean.BinderInfo → Bool
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.add_bddBelow_range_add : ∀ {E : Type u_3} [inst : AddCommGroup E] {p q : AddGroupSeminorm E} {x : E},
  BddBelow (Set.range fun y => p y + q (x - y))
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.iso_symm_apply_aux : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M'),
  (IsLocalizedModule.iso S f).symm m = LocalizedModule.mk ⋯.choose.1 ⋯.choose.2
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Being a limiting fan is stable under equivalences in the index type.  -/
CategoryTheory.Limits.Fan.isLimitEquivOfEquiv : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {γ : Type w'} →
        (ε : β ≃ γ) →
          {f : γ → C} →
            (c : CategoryTheory.Limits.Fan f) →
              CategoryTheory.Limits.IsLimit c ≃
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk c.pt fun i => c.proj (ε i))
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.IsGood.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P P_1 : HomotopicalAlgebra.PathObject A),
  P = P_1 →
    ∀ [inst_2 : CategoryTheory.Limits.HasBinaryProduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C],
      P.IsGood = P_1.IsGood
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.MemLp.smul : ∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E]
  {p q r : ENNReal} {f : α → E} {φ : α → 𝕜},
  MeasureTheory.MemLp f q μ → MeasureTheory.MemLp φ p μ → ∀ [hpqr : p.HolderTriple q r], MeasureTheory.MemLp (φ • f) r μ
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_algHom_apply : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {F : Type u_3} [inst_5 : FunLike F A B] [AlgHomClass F R A B] (f : F)
  (x : A) (p : Polynomial R), (Polynomial.aeval (f x)) p = f ((Polynomial.aeval x) p)
-- Mathlib.Data.Set.Image
Function.LeftInverse.image_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.LeftInverse g f → ∀ (s : Set α), g '' f '' s = s
-- Mathlib.SetTheory.Ordinal.Basic
/-- The ordinal corresponding to a cardinal `c` is the least ordinal
whose cardinal is `c`. This is the order-embedding version. For the regular function, see `ord`.
 -/
Cardinal.ord.orderEmbedding : Cardinal.{u_1} ↪o Ordinal.{u_1}
-- Mathlib.Topology.Filter
Filter.HasBasis.nhds' : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (nhds l).HasBasis p fun i => {l' | s i ∈ l'}
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.rightUnitor_inv : ∀ (C : CategoryTheory.Cat),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor C).inv =
    (CategoryTheory.Prod.sectL ↑C { down := { as := PUnit.unit } }).toCatHom
-- Init.Data.SInt.Lemmas
ISize.toBitVec_div : ∀ {a b : ISize}, (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.map_sub_atTop_eq_nat : ∀ (k : ℕ), Filter.map (fun a => a - k) Filter.atTop = Filter.atTop
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter_succ' : ∀ (i : ℕ) {n m : ℕ} (h : autoParam (n + i = m) SimplexCategory.σ₀Iter_succ'._auto_1),
  SimplexCategory.σ₀Iter (i + 1) ⋯ =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ 0) (SimplexCategory.σ₀Iter i h)
-- Lean.Expr
Lean.mkDecIsFalse : Lean.Expr → Lean.Expr → Lean.Expr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey!
-- Init.Data.Array.Lemmas
Array.fst_unzip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array (α × β)}, xs.unzip.1 = Array.map Prod.fst xs
-- Init.Data.UInt.Lemmas
UInt8.toFin_toUInt16 : ∀ (n : UInt8), n.toUInt16.toFin = Fin.castLE UInt8.toFin_toUInt16._proof_1 n.toFin