mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.Separation
geometric_hahn_banach_open_open : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s t : Set E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E],
  Convex ℝ s → IsOpen s → Convex ℝ t → IsOpen t → Disjoint s t → ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgebra.instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat_1 : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {S : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] →
              [inst_3 : DecidableEq ι] →
                [inst_4 : AddCommMonoid ι] →
                  [inst_5 : CommSemiring A] →
                    [inst_6 : Algebra R A] →
                      (𝒜 : ι → Submodule R A) →
                        [inst_7 : GradedAlgebra 𝒜] → Algebra (↥(Submodule.baseChange S (𝒜 0))) (TensorProduct R S A)
-- Mathlib.Analysis.Convex.Topology
Convex.openSegment_self_interior_subset_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ interior s → openSegment 𝕜 x y ⊆ interior s
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.zero_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (n : N), 0 ⊗ₜ[R] n = 0
-- Mathlib.Topology.Separation.Regular
exists_open_nhds_disjoint_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T25Space X] {x y : X},
  x ≠ y → ∃ u, x ∈ u ∧ IsOpen u ∧ ∃ v, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v)
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.instIsCofilteredElementsEtaleCompOverForgetObjOppositeFunctorTypeCoyonedaOpMk : ∀ {S : AlgebraicGeometry.Scheme} {Ω : Type u} [inst : Field Ω] (s : AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S),
  CategoryTheory.IsCofiltered
    ((AlgebraicGeometry.Scheme.Etale.forget S).comp
        (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Over.mk s)))).Elements
-- Mathlib.Order.Filter.Germ.OrderedMonoid
Filter.Germ.instIsOrderedAddMonoid : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : AddCommMonoid β] [inst_1 : Preorder β] [IsOrderedAddMonoid β],
  IsOrderedAddMonoid (l.Germ β)
-- Mathlib.Topology.ContinuousOn
Continuous.continuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  Continuous f → ContinuousOn f s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.ModObj.comp_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] {Z Z' : C} (g : Z' ⟶ Z) (m : Z ⟶ M)
  (x : Z ⟶ X),
  CategoryTheory.CategoryStruct.comp g (m • x) =
    CategoryTheory.CategoryStruct.comp g m • CategoryTheory.CategoryStruct.comp g x
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.congr_inv.injEq : ∀ {R : Type u} [inst : Rack R] {a a' : Rack.PreEnvelGroup R} (ha ha_1 : Rack.PreEnvelGroupRel' R a a'),
  (ha.congr_inv = ha_1.congr_inv) = (ha = ha_1)
-- Batteries.Data.Array.Basic
/-- Find the first maximal element of an array. If the array is empty, `default` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.maxI : {α : Type u_1} → [ord : Ord α] → [Inhabited α] → (xs : Array α) → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.norm_orthogonalProjectionOnto_apply_le`.

---

The orthogonal projection onto a closed subspace is norm non-increasing.  -/
Submodule.norm_orthogonalProjection_apply_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (v : E), ‖K.orthogonalProjectionOnto v‖ ≤ ‖v‖
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coeFn_smul : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {S : Type u_10} [inst_5 : Monoid S]
  [inst_6 : DistribMulAction S N] [inst_7 : SMulCommClass R S N] (c : S) (f : M [⋀^ι]→ₗ[R] N), ⇑(c • f) = c • ⇑f
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- `CategoryStruct` on `OplaxFunctor B C` where the (1-)morphisms are given by lax
transformations.  -/
CategoryTheory.Oplax.LaxTrans.instCategoryStructOplaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁}
          (CategoryTheory.OplaxFunctor B C)
-- Init.Data.Option.Lemmas
Option.elim_some : ∀ {β : Sort u_1} {α : Type u_2} (x : β) (f : α → β) (a : α), (some a).elim x f = f a
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.inclRightCompOpEquivInverse_inv_app_op : ∀ {C : Type u₁} (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (c : C),
  (CategoryTheory.Join.inclRightCompOpEquivInverse C D).inv.app (Opposite.op c) =
    CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Join.left c))
-- Mathlib.CategoryTheory.Monoidal.Braided.Opposite
instBraidedCategoryOpposite : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory Cᵒᵖ
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Wedge.ext_hom_hom : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {W₁ W₂ : CategoryTheory.Limits.Wedge F}
  (e : W₁.pt ≅ W₂.pt)
  (he :
    autoParam
      (∀ (j : J),
        CategoryTheory.Limits.Multifork.ι W₁ j =
          CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.Multifork.ι W₂ j))
      CategoryTheory.Limits.Wedge.ext._auto_1),
  (CategoryTheory.Limits.Wedge.ext e he).hom.hom = e.hom
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.contMDiffAt_ofComplex : ∀ {n : WithTop ℕ∞} {z : ℂ},
  0 < z.im → ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n (↑UpperHalfPlane.ofComplex) z
-- Mathlib.Topology.Compactness.SigmaCompact
/-- The empty set is σ-compact.  -/
isSigmaCompact_empty : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsSigmaCompact ∅
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsMinOn.lineDeriv_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E},
  IsMinOn f s a → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → lineDeriv ℝ f a b = 0
-- Init.Data.Int.Lemmas
Int.eq_neg_of_eq_neg : ∀ {a b : ℤ}, a = -b → b = -a
-- Mathlib.CategoryTheory.Galois.Decomposition
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.selfProd.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) (X : C), CategoryTheory.PreGaloisCategory.selfProd✝ F X = ∏ᶜ fun x => X
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Theory.IsUniversal.insert : ∀ {L : FirstOrder.Language} {T : L.Theory} [hT : T.IsUniversal] {φ : L.Sentence},
  FirstOrder.Language.BoundedFormula.IsUniversal φ → (insert φ T).IsUniversal
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffWithinAt.continuousWithinAt_fderivWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E}
  {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → UniqueDiffOn 𝕜 s → n ≠ 0 → x ∈ s → ContinuousWithinAt (fderivWithin 𝕜 f s) s x
-- Mathlib.CategoryTheory.MarkovCategory.Basic
/-- The monoidal unit is a terminal object.  -/
CategoryTheory.MarkovCategory.isTerminalUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.MarkovCategory C] →
        CategoryTheory.Limits.IsTerminal (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.id.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithInitial C → Sort u_2) →
    (x : CategoryTheory.WithInitial C) →
      ((a : C) → motive (CategoryTheory.WithInitial.of a)) → (Unit → motive CategoryTheory.WithInitial.star) → motive x
-- Mathlib.Analysis.Oscillation
/-- The oscillation of `f` at `x` within `univ` is equal to `oscillation f x`  -/
oscillationWithin_univ_eq_oscillation : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : TopologicalSpace E] (f : E → F) (x : E),
  oscillationWithin f Set.univ x = oscillation f x
-- Mathlib.Order.Hom.Order
OrderHom.top_def : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : OrderTop β],
  ⊤ = (OrderHom.const α) ⊤
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- If two ring homomorphisms from `SkewMonoidAlgebra k G` are equal on all `single a 1`
and `single 1 b`, then they are equal.

See note [partially-applied ext lemmas].  -/
SkewMonoidAlgebra.ringHom_ext' : ∀ (k : Type u_1) (G : Type u_2) [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k]
  {f g : SkewMonoidAlgebra k G →+* k},
  f.comp SkewMonoidAlgebra.singleOneRingHom = g.comp SkewMonoidAlgebra.singleOneRingHom →
    (↑f).comp (SkewMonoidAlgebra.of k G) = (↑g).comp (SkewMonoidAlgebra.of k G) → f = g
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.toBoxAdditive_apply : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  [inst_5 : CompleteSpace F] (h : BoxIntegral.Integrable I l f vol) (J : BoxIntegral.Box ι),
  h.toBoxAdditive J = BoxIntegral.integral J l f vol
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.reflectsLimitsOfShapeOfCreatesLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.CreatesLimitsOfShape J F], CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Mathlib.Geometry.Manifold.Submersion
/-- The identity map is an submersion.  -/
Manifold.IsSubmersion.id : ∀ {𝕜 : Type u_1} {H : Type u_7} {E : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M],
  Manifold.IsSubmersion I I n id
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.size_eq : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.size = t.toList.length
-- Mathlib.Order.OrderDual
Equiv.bot_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : Bot β], ⊥ = e.symm ⊥
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_C_of_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] {a : R} {n : ℕ}, n ≠ 0 → (PowerSeries.coeff n) (PowerSeries.C a) = 0
-- Init.Data.SInt.Lemmas
Int16.toISize_div_of_ne_right : ∀ (a b : Int16), b ≠ -1 → (a / b).toISize = a.toISize / b.toISize
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTop_isNonZero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [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] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α β : LieModule.Weight R L M),
  α.IsNonZero → (LieModule.chainTop (⇑α) β).IsNonZero
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LeftLinear C] (c : C) (d : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d)
      (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d) =
    CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d))
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.ext_iff : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {x y : P.Cotangent}, x = y ↔ x.val = y.val
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasStrongEpiMonoFactorisations.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ {X Y : C} (f : X ⟶ Y), Nonempty (CategoryTheory.Limits.StrongEpiMonoFactorisation f)) →
    CategoryTheory.Limits.HasStrongEpiMonoFactorisations C
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃Obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
  ((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).obj X₃ = (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_cpop_not : ∀ {w : ℕ} {x : BitVec w}, (~~~x).cpop.toNat = w - x.cpop.toNat
-- Mathlib.Algebra.Group.WithOne.Basic
/-- Given a multiplicative map from `α → β` returns a monoid homomorphism
from `WithOne α` to `WithOne β`  -/
WithOne.mapMulHom : {α : Type u} → {β : Type v} → [inst : Mul α] → [inst_1 : Mul β] → (α →ₙ* β) → WithOne α →* WithOne β
-- Mathlib.Algebra.BigOperators.Finprod
/-- See also `finprod_mem_finset_product'`.  -/
finprod_mem_finset_product : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] (s : Finset (α × β)) (f : α × β → M),
  ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.Adjunction.mk.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (unit unit_1 : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g) (e_unit : unit = unit_1)
  (counit counit_1 : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b)
  (e_counit : counit = counit_1)
  (left_triangle :
    CategoryTheory.Bicategory.leftZigzag unit counit =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
        (CategoryTheory.Bicategory.rightUnitor f).inv)
  (right_triangle :
    CategoryTheory.Bicategory.rightZigzag unit counit =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
        (CategoryTheory.Bicategory.leftUnitor g).inv),
  { unit := unit, counit := counit, left_triangle := left_triangle, right_triangle := right_triangle } =
    { unit := unit_1, counit := counit_1, left_triangle := ⋯, right_triangle := ⋯ }
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuousAt_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α},
  UpperHemicontinuousAt (fun x => {f x}) x ↔ ContinuousAt f x
-- Mathlib.Data.Set.Image
/-- **Alias** of `Set.preimage_ofPred_eq`. -/
Set.preimage_setOf_eq : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : β → α}, f ⁻¹' {a | p a} = {a | p (f a)}
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.comap_eval_surjective : ∀ (K : Type uK) (V : Type uV) [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], Function.Surjective (Submodule.comap (Module.Dual.eval K V))
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.coe_trans : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α ↪ β) (g : β ↪ γ), ⇑(f.trans g) = ⇑g ∘ ⇑f
-- Aesop.Tree.Data
Aesop.MVarClusterData.isIrrelevant : {Goal Rapp : Type} → Aesop.MVarClusterData Goal Rapp → Bool
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.isEmpty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true ↔ t = ∅
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom : @AlgebraicGeometry.IsIntegralHom = @AlgebraicGeometry.UniversallyClosed ⊓ @AlgebraicGeometry.IsAffineHom
-- Mathlib.Analysis.Analytic.IsolatedZeros
HasFPowerSeriesAt.has_fpower_series_dslope_fslope : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜},
  HasFPowerSeriesAt f p z₀ → HasFPowerSeriesAt (dslope f z₀) p.fslope z₀
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_zero_eq_top : SimpleGraph.cycleGraph 0 = ⊤
-- Std.Data.ExtHashMap.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`, then
the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.ExtHashMap.containsThenInsertIfNew : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → β → Bool × Std.ExtHashMap α β
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.id_apply : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) → C i) (i : I),
  CategoryTheory.CategoryStruct.id X i = CategoryTheory.CategoryStruct.id (X i)
-- Mathlib.Topology.Constructions
isOpen_sigma_fst_preimage : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] (s : Set ι), IsOpen (Sigma.fst ⁻¹' s)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationDiagram.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Hom.normalizationDiagram f =
    {
      obj := fun U =>
        CommRingCat.of
          ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op (Opposite.unop U)))
              ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj (Opposite.unop U))))),
      map := fun {V U} i =>
        CommRingCat.ofHom
          ((CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)).restrict
            (integralClosure ↑(Y.presheaf.obj (Opposite.op (Opposite.unop V)))
              ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj (Opposite.unop V)))))
            (integralClosure ↑(Y.presheaf.obj (Opposite.op (Opposite.unop U)))
              ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj (Opposite.unop U)))))
            ⋯),
      map_id := ⋯, map_comp := ⋯ }
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.size_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} (t : RBTree.RBSet α cmp), t.size = t.toList.length
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.map_id : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C],
  CategoryTheory.Limits.chosenCoend.map (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.chosenCoend F)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.fst_comp_inl : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂],
  ContinuousLinearMap.fst R M₁ M₂ ∘SL ContinuousLinearMap.inl R M₁ M₂ = ContinuousLinearMap.id R M₁
-- Batteries.Recycling.RBTree.Basic
/-- Rebalancing a tree which has shrunk on the right.  -/
RBTree.RBNode.balRight : {α : Type u_1} → RBTree.RBNode α → α → RBTree.RBNode α → RBTree.RBNode α
-- Batteries.Data.Fin.Lemmas
Fin.find?_eq_none_iff : ∀ {n : ℕ} {p : Fin n → Bool}, Fin.find? p = none ↔ ∀ (i : Fin n), p i = false
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is `C^n` within a set at a point, for `n : ℕ`, if and only if it is `C^n` on
a neighborhood of this point.  -/
contDiffWithinAt_iff_contDiffOn_nhds : ∀ {𝕜 : 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} {n : WithTop ℕ∞},
  n ≠ ↑⊤ → (ContDiffWithinAt 𝕜 n f s x ↔ ∃ u ∈ nhdsWithin x (insert x s), ContDiffOn 𝕜 n f u)
-- Mathlib.ModelTheory.Syntax
/-- The equality of two terms as a bounded formula.  -/
FirstOrder.Language.Term.bdEqual : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin n) → L.BoundedFormula α n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.roots_T_real : ∀ (n : ℕ),
  (Polynomial.Chebyshev.T ℝ ↑n).roots =
    (Finset.image (fun k => Real.cos ((2 * ↑k + 1) * Real.pi / (2 * ↑n))) (Finset.range n)).val
-- Mathlib.Data.EReal.Operations
EReal.le_of_forall_lt_iff_le : ∀ {x y : EReal}, (∀ (z : ℝ), x < ↑z → y ≤ ↑z) ↔ y ≤ x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₁.get k ⋯
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_zpow : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ) (n : ℤ), ↑(r ^ n) = ↑r ^ n
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.ext_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S T : NonUnitalSubalgebra R A}, S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T
-- Init.Data.SInt.Bitwise
ISize.not_xor : ∀ {a b : ISize}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Init.Data.Int.DivMod.Bootstrap
Int.bmod_def : ∀ (x : ℤ) (m : ℕ), x.bmod m = if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m
-- Mathlib.Algebra.Module.LinearMap.End
/-- `LinearMap.applyModule` is faithful.  -/
Module.End.apply_faithfulSMul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  FaithfulSMul (Module.End R M) M