mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Rotate
/-- The unit isomorphism of the auto-equivalence of categories `triangleRotation C` of
`Triangle C` given by the rotation of triangles.  -/
CategoryTheory.Pretriangulated.rotCompInvRot : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
          CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C) ≅
            (CategoryTheory.Pretriangulated.rotate C).comp (CategoryTheory.Pretriangulated.invRotate C)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell.match_5.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (l : Std.DTreeMap.Internal.Impl α β) → l.Balanced → Sort u_3)
  (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (h_1 : (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hl)
  (h_2 :
    (sz : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl),
  (match Std.DTreeMap.Internal.Impl.leaf, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl => h_1 hl
    | Std.DTreeMap.Internal.Impl.inner sz ky y l r, hl => h_2 sz ky y l r hl) =
    h_1 hl
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isMulLeftInvariant_smul_nnreal : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  (c : NNReal), (c • μ).IsMulLeftInvariant
-- Mathlib.CategoryTheory.Adjunction.Opposites
/-- Deprecated: prefer `(Adjunction.conjugateIsoEquiv adj1 adj2).symm`.  -/
CategoryTheory.Adjunction.natIsoOfRightAdjointNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F F' : CategoryTheory.Functor C D} →
          {G G' : CategoryTheory.Functor D C} → (F ⊣ G) → (F' ⊣ G') → (G ≅ G') → (F ≅ F')
-- Mathlib.GroupTheory.Sylow
Sylow.coe_symm_equivProdPrimeFactors_apply : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (h : p ≠ 0) (H : Sylow (p.primeFactors.prod id) G),
  ↑((Sylow.equivProdPrimeFactors h).symm H) = ↑H
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- `exp ∘ f` is analytic  -/
AnalyticAt.rexp' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  AnalyticAt ℝ f x → AnalyticAt ℝ (fun z => Real.exp (f z)) x
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.pullback_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A B : C}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Mono f],
  (CategoryTheory.Subobject.pullback f).obj (CategoryTheory.Subobject.mk f) = ⊤
-- Mathlib.Topology.Compactness.Lindelof
HereditarilyLindelofSpace.isLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] (s : Set X), IsLindelof s
-- Mathlib.Data.Vector.Mem
List.Vector.mem_cons_self : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), a ∈ (a ::ᵥ v).toList
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_sub_cos : ∀ (x y : ℝ), Real.cos x - Real.cos y = -2 * Real.sin ((x + y) / 2) * Real.sin ((x - y) / 2)
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain 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.IsCrystallographic] (i j : ι),
  RootPairing.chainBotCoeff i j = if h : LinearIndependent R ![P.root i, P.root j] then (-⋯.choose).toNat else 0
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.map_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {B : Type u_6} {M : CStarMatrix m n A} {f : A → B} {i : m} {j : n},
  M.map f i j = f (M i j)
-- Lean.Meta.Tactic.Simp.Types
/-- `Simproc` .olean entry.
 -/
Lean.Meta.Simp.SimprocOLeanEntry : Type
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.preimage_symm_proj_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj), ↑e.symm ⁻¹' proj ⁻¹' e.baseSet ∩ e.target = e.target
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- The sheafification functor is left adjoint to the forgetful functor.  -/
CategoryTheory.plusPlusAdjunction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type w) →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {FD : D → D → Type u_1} →
            {CD : D → Type t} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [instCC : CategoryTheory.ConcreteCategory D FD] →
                  [inst_3 :
                      ∀ {X : C} (S : J.Cover X),
                        CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
                          (CategoryTheory.forget D)] →
                    [inst_4 :
                        ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                          CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
                      [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                        [inst_6 :
                            ∀ (X : C),
                              CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] →
                          [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] →
                            CategoryTheory.plusPlusSheaf J D ⊣ CategoryTheory.sheafToPresheaf J D
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_le_pi : ∀ (x : ℝ), Real.arccos x ≤ Real.pi
-- Init.Data.UInt.Lemmas
UInt64.add_left_neg : ∀ (a : UInt64), -a + a = 0
-- Lean.Expr
/-- Let-expressions.

The let-expression `let x : Nat := 2; Nat.succ x` is represented as
```
Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
```

If the `nondep` flag is `true`, then the elaborator treats this as a *non-dependent `let`* (known as a *`have` expression*).
Given an environment, a metavariable context, and a local context,
we say a let-expression `let x : t := v; e` is non-dependent when it is equivalent
to `(fun x : t => e) v`. In contrast, the dependent let-expression
`let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct,
but `(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not.

The kernel does not verify `nondep` when type checking. This is an elaborator feature.
 -/
Lean.Expr.letE : Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Expr
-- Mathlib.NumberTheory.Bernoulli
sum_bernoulli' : ∀ (n : ℕ), ∑ k ∈ Finset.range n, ↑(n.choose k) * bernoulli' k = ↑n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.gt.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {k : α → Ordering} {a : List ((a : α) × β a)} {a_1 : α}
  {a_2 : k a_1 = Ordering.gt} {a_3 : β a_1} {a_4 : List ((a : α) × β a)} {a_5 : α} {a_6 : k a_5 = Ordering.gt}
  {a_7 : β a_5},
  Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3 =
      Std.DTreeMap.Internal.Impl.ExplorationStep.gt a_4 a_5 a_6 a_7 →
    a = a_4 ∧ a_1 = a_5 ∧ a_3 ≍ a_7
-- Lean.MetavarContext
/-- Set the kind of an fvar. If the given metavariable is not declared or the
given fvar doesn't exist in its context, nothing happens.
 -/
Lean.MVarId.setFVarKind : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → Lean.FVarId → Lean.LocalDeclKind → m Unit
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.instInhabitedArg.default : Mathlib.Meta.FunProp.Mor.Arg
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_sUnion : ∀ {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {t : Set β} {f : α → β},
  Set.MapsTo f (⋃₀ S) t ↔ ∀ s ∈ S, Set.MapsTo f s t
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- The set of all complex embeddings of `L` that lie over `ψ` and are unmixed.  -/
NumberField.ComplexEmbedding.unmixedEmbeddingsOver : {K : Type u_3} → (L : Type u_4) → [inst : Field K] → [inst_1 : Field L] → (K →+* ℂ) → [Algebra K L] → Set (L →+* ℂ)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.addConjMap_comp : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {g h k : G} {a b c : α} (hg : b = g +ᵥ a)
  (hh : c = h +ᵥ b) (hk : c = k +ᵥ a) (H : k = h + g),
  (SubAddAction.ofStabilizer.conjMap hh).comp (SubAddAction.ofStabilizer.conjMap hg) =
    SubAddAction.ofStabilizer.conjMap hk
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.toIntModule : {α : Type u} → [I : Lean.Grind.Ring α] → Lean.Grind.IntModule α
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_addNat_uIcc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (fun x => x.addNat m) (Finset.uIcc i j) = Finset.uIcc (i.addNat m) (j.addNat m)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [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_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄}
  (f f_1 :
    (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶ A)),
  f = f_1 →
    CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc f =
      CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc f_1
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.mkContinue : Lean.Elab.Do.ControlStack → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- **Alias** of `WithSeminorms.continuous_iff_continuous_comp`. -/
Seminorm.continuous_iff_continuous_comp : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [inst : AddCommGroup E]
  [inst_1 : NormedField 𝕝] [inst_2 : Module 𝕝 E] [inst_3 : AddCommGroup F] [inst_4 : NormedField 𝕝₂]
  [inst_5 : Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_6 : RingHomIsometric τ₁₂] {q : SeminormFamily 𝕝₂ F ι'}
  [inst_7 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_9 : TopologicalSpace F],
  WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), Continuous ⇑f ↔ ∀ (i : ι'), Continuous ⇑((q i).comp f)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel of an arrow is natural.  -/
CategoryTheory.Limits.ker : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasKernels C] → CategoryTheory.Functor (CategoryTheory.Arrow C) C
-- Mathlib.Data.Seq.Defs
/-- The empty sequence  -/
Stream'.Seq.nil : {α : Type u} → Stream'.Seq α
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instAdd : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : AddMonoid R] → Add (HahnSeries Γ R)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- `IsConj φ σ` states that `σ : Gal(K/k)` is the conjugation under the embedding `φ : K →+* ℂ`.
 -/
NumberField.ComplexEmbedding.IsConj : {K : Type u_1} →
  [inst : Field K] → {k : Type u_2} → [inst_1 : Field k] → [inst_2 : Algebra k K] → (K →+* ℂ) → Gal(K/k) → Prop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass.mk : ∀ {α : Type u_1} {γ : Type u_3} {F : γ → Stream'.Seq α → Stream'.Seq α},
  (∀ (c : γ), Tactic.ComputeAsymptotics.Seq.FriendlyOperation (F c)) →
    Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass F
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_zpow : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α] (q : ℚ≥0) (p : ℤ), ↑(q ^ p) = ↑q ^ p
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.right_eq_zero_of_add_eq_zero : ∀ {a b : Ordinal.{u_4}}, a + b = 0 → b = 0
-- Mathlib.Data.NNReal.Basic
NNReal.range_coe : Set.range NNReal.toReal = Set.Ici 0
-- Mathlib.Algebra.Lie.Semisimple.Basic
/-- In a semisimple Lie algebra,
Lie ideals that are contained in the supremum of a finite collection of atoms
are themselves the supremum of a finite subcollection of those atoms.

By a compactness argument, this statement can be extended to arbitrary sets of atoms.
See `atomistic`.

The proof is by induction on the finite set of atoms.
 -/
_private.Mathlib.Algebra.Lie.Semisimple.Basic.0.LieAlgebra.IsSemisimple.finitelyAtomistic : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSemisimple R L] (s : Finset (LieIdeal R L)), ↑s ⊆ {I | IsAtom I} → ∀ I ≤ s.sup id, ∃ t ⊆ s, I = t.sup id
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.subRight_symm_apply : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddRightMono α] (a b : α),
  (RelIso.symm (OrderIso.subRight a)) b = b + a
-- Init.Data.Array.Lemmas
Array.some_getElem_eq_getElem?_iff : ∀ {α : Type u_1} (xs : Array α) (i : ℕ) (h : i < xs.size), some xs[i] = xs[i]? ↔ True
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates colimits of `K.leftOp : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : Cᵒᵖ ⥤ D`
creates limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.createsLimitOfRightOp : {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] →
            (K : CategoryTheory.Functor J Cᵒᵖ) →
              (F : CategoryTheory.Functor Cᵒᵖ D) →
                [CategoryTheory.CreatesColimit K.leftOp F.rightOp] → CategoryTheory.CreatesLimit K F
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) → [addGrp : CategoryTheory.AddGrpObj X] → CategoryTheory.AddGrp C
-- Mathlib.Analysis.InnerProductSpace.l2Space
Submodule.isHilbertSumOrthogonal : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (K : Submodule 𝕜 E) [hK : CompleteSpace ↥K],
  IsHilbertSum 𝕜 (fun b => ↥(bif b then K else Kᗮ)) fun b => (bif b then K else Kᗮ).subtypeₗᵢ
-- Init.Data.List.Basic
/-- Returns the smallest element of a non-empty list.

Examples:
* `[4].min (by decide) = 4`
* `[1, 4, 2, 10, 6].min (by decide) = 1`
 -/
List.min : {α : Type u} → [Min α] → (l : List α) → l ≠ [] → α
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.pushforwardToOfIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C Y}
  {𝒢 : TopCat.Presheaf C X} (H₂ : ℱ ⟶ (TopCat.Presheaf.pushforward C H₁.hom).obj 𝒢),
  TopCat.Presheaf.pushforwardToOfIso H₁ H₂ =
    ((TopCat.Presheaf.presheafEquivOfIso C H₁.symm).toAdjunction.homEquiv ℱ 𝒢).symm H₂
-- Init.Data.Order.Ord
Std.TransCmp.mk : ∀ {α : Type u} {cmp : α → α → Ordering} [toOrientedCmp : Std.OrientedCmp cmp],
  (∀ {a b c : α}, (cmp a b).isLE = true → (cmp b c).isLE = true → (cmp a c).isLE = true) → Std.TransCmp cmp
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instModule : {m : Type u_1} →
  {n : Type u_2} →
    {R : Type u_3} →
      {A : Type u_5} → [inst : Semiring R] → [inst_1 : AddCommMonoid A] → [Module R A] → Module R (CStarMatrix m n A)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.monomorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderBaseChange
-- Mathlib.Order.Filter.Basic
Filter.empty_notMem : ∀ {α : Type u} (f : Filter α) [f.NeBot], ∅ ∉ f
-- Mathlib.Tactic.Positivity.Core
ne_of_ne_of_eq' : ∀ {α : Sort u_1} {a c b : α}, a ≠ c → a = b → b ≠ c
-- Init.Data.UInt.Lemmas
UInt8.lt_of_lt_of_le : ∀ {a b c : UInt8}, a < b → b ≤ c → a < c
-- Mathlib.Topology.Separation.Regular
/-- The `SeparationQuotient` of a normal space is a normal space.  -/
SeparationQuotient.instNormalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X], NormalSpace (SeparationQuotient X)
-- Lean.DocString.Extension
Lean.VersoModuleDocs.Snippet.addBlock : Lean.VersoModuleDocs.Snippet → Lean.Doc.Block Lean.ElabInline Lean.ElabBlock → Lean.VersoModuleDocs.Snippet
-- Std.Do.PostCond
/-- Implication of exception assertions is defined as pointwise implication of the assertion for each
exception.

Unlike entailment (`ExceptConds.entails`), which is an ordinary proposition of type `Prop`,
implication of exception assertions is itself an exception assertion.
 -/
Std.Do.ExceptConds.imp : {ps : Std.Do.PostShape} → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps
-- Mathlib.Topology.Separation.Regular
/-- A T₅ space is a completely normal T₁ space.  -/
T5Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.Analysis.Normed.Group.Defs
Norm.mk : {E : Type u_8} → (E → ℝ) → Norm E
-- Init.Notation
/-- `Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.


Conventions for notations in identifiers:

 * The recommended spelling of `∨` in identifiers is `or`. -/
«term_∨_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Floor.Div
ceilDiv_le_iff_le_mul : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : CeilDiv α α] {a b c : α},
  0 < a → (b ⌈/⌉ a ≤ c ↔ b ≤ a * c)
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.dual_apply_toOrderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : BoundedOrder α] [inst_2 : Preorder β]
  [inst_3 : BoundedOrder β] (f : BoundedOrderHom α β), (BoundedOrderHom.dual f).toOrderHom = OrderHom.dual f.toOrderHom
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.tendsto_nhds : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {f : Filter β} {u : β → α} {a : α},
  Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, edist (u x) a < ε
-- Mathlib.Topology.IsClosedRestrict
/-- The restriction of a compact closed set in a product space to a set of coordinates is closed.  -/
IsCompact.isClosed_image_restrict : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} [inst : (i : ι) → TopologicalSpace (α i)] (S : Set ι),
  IsCompact s → IsClosed s → IsClosed (S.domRestrict '' s)
-- Mathlib.Topology.Algebra.Algebra.Rat
/-- The action induced by `DivisionRing.toRatAlgebra` is continuous.  -/
DivisionRing.continuousConstSMul_rat : ∀ {A : Type u_1} [inst : DivisionRing A] [inst_1 : TopologicalSpace A] [SeparatelyContinuousMul A]
  [inst_3 : CharZero A], ContinuousConstSMul ℚ A
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_div_dvd : ∀ {K : Type u} [inst : Field K] (p q : Polynomial K),
  ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).denom ∣ q
-- Mathlib.Data.Sym.Sym2
Sym2.diagElemEquiv_apply : ∀ {α : Type u_1} (x : { a // a.IsDiag }), Sym2.diagElemEquiv x = (↑x).diagElem ⋯
-- Batteries.Data.Fin.Lemmas
Fin.map_rev_findRev? : ∀ {n : ℕ} {p : Fin n → Bool}, Option.map Fin.rev (Fin.findRev? fun x => p x.rev) = Fin.find? p
-- Mathlib.Topology.Compactness.Compact
/-- For every open directed cover of a compact set, there exists a single element of the
cover which itself includes the set.  -/
IsCompact.elim_directed_cover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v} [hι : Nonempty ι],
  IsCompact s →
    ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → Directed (fun x1 x2 => x1 ⊆ x2) U → ∃ i, s ⊆ U i
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (s : UpperSet α),
  ((UpperSet.map f) s).compl = (LowerSet.map f) s.compl
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.integrable_cauchyPDFReal : ∀ (x₀ : ℝ) {γ : NNReal}, MeasureTheory.Integrable (ProbabilityTheory.cauchyPDFReal x₀ γ) MeasureTheory.volume
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_map_iff_of_nontrivial : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Set β},
  t.Nontrivial → ((SimpleGraph.map (⇑f) G).IsClique t ↔ ∃ s, G.IsClique s ∧ ⇑f '' s = t)
-- Mathlib.Data.List.Induction
List.bidirectionalRec.eq_2 : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a])
  (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (a : α),
  List.bidirectionalRec nil singleton cons_append [a] = singleton a
-- Mathlib.Analysis.Normed.Order.UpperLower
dist_le_dist_of_le_pi : ∀ {ι : Type u_2} [inst : Fintype ι] {a₁ a₂ b₁ b₂ : ι → ℝ}, a₂ ≤ a₁ → a₁ ≤ b₁ → b₁ ≤ b₂ → dist a₁ b₁ ≤ dist a₂ b₂
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.subset_mapRange_neLocus : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N]
  [inst_3 : DecidableEq M] [inst_4 : Zero M] (f g : α →₀ N) {F : N → M} (F0 : F 0 = 0),
  (Finsupp.mapRange F F0 f).neLocus (Finsupp.mapRange F F0 g) ⊆ f.neLocus g
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.mk.sizeOf_spec : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SizeOf G] (toAddSubgroup : AddSubgroup G)
  (isClosed' : IsClosed toAddSubgroup.carrier),
  sizeOf { toAddSubgroup := toAddSubgroup, isClosed' := isClosed' } = 1 + sizeOf toAddSubgroup + sizeOf isClosed'
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.ShortComplex.ShortExact.injective_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C],
  S.ShortExact → Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.f))
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The canonical map from `List (α × Bool)` to the free additive group on `α`.  -/
FreeAddGroup.mk : {α : Type u} → List (α × Bool) → FreeAddGroup α
-- Std.Http.Test.Helpers
/-- POST with a fixed Content-Length body. `extra` is appended before the blank line.
 -/
Std.Http.Internal.Test.mkPost : String → String → optParam String "" → String
-- Mathlib.FieldTheory.Perfect
PerfectRing.pow : ∀ (M : Type u_1) (p : ℕ) [inst : CommMonoid M] [PerfectRing M p] (n : ℕ), PerfectRing M (p ^ n)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_natCast : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  (n : ℕ), ⌊↑n⌋₊ = n