mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.liftKaehlerDifferential_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (D : Derivation R S M) (x : ↥(KaehlerDifferential.ideal R S)),
  D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent x) = D.tensorProductTo ↑x
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_nonneg : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}, 0 ≤ a⁻¹ ↔ 0 ≤ a
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- The one-vertex subgraph.  -/
SimpleGraph.singletonSubgraph : {V : Type u} → (G : SimpleGraph V) → V → G.Subgraph
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.mod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] → (self : CategoryTheory.Mod D A) → CategoryTheory.ModObj A self.X
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_union : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t₁ t₂ : Finset β},
  s +ᵥ t₁ ∪ t₂ = (s +ᵥ t₁) ∪ (s +ᵥ t₂)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_add : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Add α] (A B : Matrix m n α),
  (A + B).submatrix = A.submatrix + B.submatrix
-- Mathlib.Topology.Order.MonotoneConvergence
LinearOrder.supConvergenceClass : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α], SupConvergenceClass α
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.transvection_mem_commutator₁ : ∀ {F : Type u_1} [inst : Field F] {a : F},
  a ≠ 0 →
    a ^ 2 ≠ 1 → ∀ (c : F), Matrix.SpecialLinearGroup.transvection ⋯ c ∈ commutator (Matrix.SpecialLinearGroup (Fin 2) F)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isClosedEmbedding_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsClosedEmbedding ⇑DomAddAct.mk.symm
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_inf : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (K K' : LieSubalgebra R L), ↑(K ⊓ K') = ↑K ∩ ↑K'
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofArrows_le_ofObjects : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {X : C} (f : (i : I) → Y i ⟶ X),
  CategoryTheory.Sieve.ofArrows Y f ≤ CategoryTheory.Sieve.ofObjects Y X
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.denseAt.congr_simp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsDense] (Y : D), F.denseAt Y = F.denseAt Y
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toList_mapWithPostcondition_mapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} {n : Type w → Type w''}
  {δ : Type w} [inst_1 : Monad m] [LawfulMonad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m γ}
  {g : γ → Std.Iterators.PostconditionT n δ},
  (Std.IterM.mapWithPostcondition g (Std.Iter.mapWithPostcondition f it)).toList =
    (Std.Iter.mapWithPostcondition (fun b => liftM (f b) >>= g) it).toList
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotation_def : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)),
  o.rightAngleRotation = LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯
-- Aesop.RuleSet
Aesop.BaseRuleSet.empty : Aesop.BaseRuleSet
-- Init.Data.ToString.Basic
/-- Converts a value into a string.  -/
ToString.toString : {α : Type u} → [self : ToString α] → α → String
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.uIoo a b = Set.Ioo a b
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfLax'_mapId_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] (a : B),
  ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapId a).hom = CategoryTheory.inv (F.mapId a)
-- Mathlib.Tactic.CancelDenoms.Core
_private.Mathlib.Tactic.CancelDenoms.Core.0.Mathlib.Tactic.cancelDenominators : Lean.Elab.Tactic.Location → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precompose_obj_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : G ⟶ F) (c : CategoryTheory.Limits.Cocone F),
  ((CategoryTheory.Limits.Cocone.precompose α).obj c).pt = c.pt
-- Mathlib.Order.Filter.Finite
Set.Finite.eventuallyEq_iUnion : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
  s.Finite → ∀ {f g : ι → Set α}, (∀ i ∈ s, f i =ᶠ[l] g i) → ⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i
-- Mathlib.Order.Sublattice
Sublattice.instSetLike : {α : Type u_2} → [inst : Lattice α] → SetLike (Sublattice α) α
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.adj_unit : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  GeneratedByTopCat.adj.unit = GeneratedByTopCat.adjUnitIso.hom
-- Lean.Compiler.IR.CompilerM
Lean.IR.getDecl' : Lean.Name → Array Lean.IR.Decl → Lean.IR.CompilerM Lean.IR.Decl
-- Mathlib.Algebra.Lie.Submodule
/-- Given a Lie subalgebra `K ⊆ L`, if we view `L` as a `K`-module by restriction, it contains
a distinguished Lie submodule for the action of `K`, namely `K` itself.  -/
LieSubalgebra.toLieSubmodule : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (K : LieSubalgebra R L) → LieSubmodule R (↥K) L
-- Mathlib.Order.Monotone.Defs
Antitone.prodMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Preorder δ] {f : α → γ} {g : β → δ}, Antitone f → Antitone g → Antitone (Prod.map f g)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_sum : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ι : Type u_4}
  (μ : ι → MeasureTheory.Measure (α × β)),
  (MeasureTheory.Measure.sum μ).snd = MeasureTheory.Measure.sum fun n => (μ n).snd
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.IsDPMorphism.dpow_comp : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} {f : A →+* B},
  hI.IsDPMorphism hJ f → ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a topological space, `𝔖` a covering of `X` by compact subsets, and
`α` a uniform space. An equicontinuous subset of `X → α` is closed in the topology of uniform
convergence on all `K ∈ 𝔖` iff it is closed in the topology of pointwise convergence.

This is a specialization of `EquicontinuousOn.isClosed_range_pi_of_uniformOnFun'` to the case where
`𝔖` covers `X`.  -/
EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    ⋃₀ 𝔖 = Set.univ →
      (∀ K ∈ 𝔖, EquicontinuousOn F K) → (IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) ↔ IsClosed (Set.range F))
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.root_chainTopIdx : ∀ {ι : 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 : ι},
  P.root (RootPairing.chainTopIdx i j) = P.root j + RootPairing.chainTopCoeff i j • P.root i
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.cgf_neg : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  ProbabilityTheory.cgf (-X) μ t = ProbabilityTheory.cgf X μ (-t)
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.add.match_1.eq_2 : ∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)}
  (motive : Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M → Sort u_1)
  (l : Mathlib.Tactic.Module.qNF R M) (h_1 : (l : Mathlib.Tactic.Module.qNF R M) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.Module.qNF R M) → motive l [])
  (h_3 :
    (a₁ : Q(«$R»)) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
            (a₂ : Q(«$R»)) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) →
                  (t₂ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
                    motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (l = [] → False) →
    (match l, [] with
      | [], l => h_1 l
      | l, [] => h_2 l
      | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
      h_2 l
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.Hom.mk.congr_simp : ∀ {X Y : SFinKer} (hom hom_1 : ProbabilityTheory.Kernel X.carrier Y.carrier) (e_hom : hom = hom_1)
  (property : ProbabilityTheory.IsSFiniteKernel hom),
  { hom := hom, property := property } = { hom := hom_1, property := ⋯ }
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.vle_refl`. -/
ValuativeRel.vle.refl : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R), x ≤ᵥ x
-- Mathlib.RingTheory.Localization.Module
LinearEquiv.extendScalarsOfIsLocalization_symm_apply : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (f : M ≃ₗ[R] N) (a : N),
  (LinearEquiv.extendScalarsOfIsLocalization S A f).symm a = f.symm a
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {E : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} E] {X Y : C}
  (f f_1 : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y),
  f = f_1 → ∀ (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F), f.map F hF = f_1.map F hF
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.liftOfRightInverse.congr_simp : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f : G₁ →* G₂) (f_inv f_inv_1 : G₂ → G₁) (e_f_inv : f_inv = f_inv_1) (hf : Function.RightInverse f_inv ⇑f),
  f.liftOfRightInverse f_inv hf = f.liftOfRightInverse f_inv_1 ⋯
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.mul_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 ≤ f₁ i) → (∀ i ∈ s, 0 ≤ f₂ i) → MonovaryOn f₁ g s → MonovaryOn f₂ g s → MonovaryOn (f₁ * f₂) g s
-- Mathlib.Analysis.Calculus.FDeriv.Const
support_fderiv_subset : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F}, Function.support (fderiv 𝕜 f) ⊆ tsupport f
-- Mathlib.NumberTheory.WellApproximable
addWellApproximable.eq_1 : ∀ (A : Type u_1) [inst : SeminormedAddGroup A] (δ : ℕ → ℝ),
  addWellApproximable A δ = Filter.blimsup (fun n => approxAddOrderOf A n (δ n)) Filter.atTop fun n => 0 < n
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Fintype J] (f : J → C) (X : C),
  (CategoryTheory.rightDistributor f X).inv =
    ∑ j,
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j)
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The composition of the unit and the counit is equal to the identity up to unitors.  -/
CategoryTheory.Bicategory.Adjunction.right_triangle : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (self : CategoryTheory.Bicategory.Adjunction f g),
  CategoryTheory.Bicategory.rightZigzag self.unit self.counit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom
      (CategoryTheory.Bicategory.leftUnitor g).inv
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- Coercing a `Matrix.SpecialLinearGroup` via `GL_pos` and `GL` is the same as coercing straight to
a matrix.  -/
Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] (g : Matrix.SpecialLinearGroup n R), ↑↑(Matrix.SpecialLinearGroup.toGLPos g) = ↑g
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_neg_le_of_le : ∀ {R : Type u} {m : ℕ} [inst : Ring R] {p : Polynomial R}, p.natDegree ≤ m → (-p).natDegree ≤ m
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.of_findIdx?_eq_some.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Std.Time.Time.PlainTime
Std.Time.instInhabitedPlainTime : Inhabited Std.Time.PlainTime
-- Mathlib.NumberTheory.Bernoulli
/-- The Bernoulli numbers:
the $n$-th Bernoulli number $B_n$ is defined recursively via
$$B_n = 1 - \sum_{k < n} \binom{n}{k}\frac{B_k}{n+1-k}$$  -/
bernoulli' : ℕ → ℚ
-- Mathlib.LinearAlgebra.Ray
/-- The ray given by a positive multiple of a nonzero vector.  -/
ray_pos_smul : ∀ {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] {v : M} (h : v ≠ 0) {r : R},
  0 < r → ∀ (hrv : r • v ≠ 0), rayOfNeZero R (r • v) hrv = rayOfNeZero R v h
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- `Matrix.kronecker` as a bilinear map.  -/
Matrix.kroneckerBilinear : {R : Type u_1} →
  {α : Type u_3} →
    {l : Type u_9} →
      {m : Type u_10} →
        {n : Type u_11} →
          {p : Type u_12} →
            [inst : CommSemiring R] →
              [inst_1 : Semiring α] →
                [inst_2 : Algebra R α] → Matrix l m α →ₗ[R] Matrix n p α →ₗ[R] Matrix (l × n) (m × p) α
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousComp_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (A : Type u) [inst_3 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (L : CategoryTheory.GrothendieckTopology E) [inst_4 : F.IsContinuous J K] [inst_5 : G.IsContinuous K L]
  (X : CategoryTheory.Sheaf L A) (X_1 : Cᵒᵖ),
  ((F.sheafPushforwardContinuousComp G A J K L).hom.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj (Opposite.op (G.obj (F.obj (Opposite.unop X_1)))))
-- Mathlib.Order.CompleteLattice.Basic
iInf_split : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (p : β → Prop),
  ⨅ i, f i = (⨅ i, ⨅ (_ : p i), f i) ⊓ ⨅ i, ⨅ (_ : ¬p i), f i
-- Mathlib.Data.Analysis.Topology
Ctop.top_mem : ∀ {α : Type u_1} {σ : Type u_2} (self : Ctop α σ) (x : α), x ∈ self.f (self.top x)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Ideal.minimalPrimes_eq_comap : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R},
  I.minimalPrimes = Ideal.comap (Ideal.Quotient.mk I) '' minimalPrimes (R ⧸ I)
-- Mathlib.Topology.ExtremallyDisconnected
/-- Lemma 2.4 in [Gleason, *Projective topological spaces*][gleason1958]:
a continuous surjection $\pi$ from a compact space $D$ to a Fréchet space $A$ restricts to
a compact subset $E$ of $D$, such that $\pi$ maps $E$ onto $A$ and satisfies the
"Zorn subset condition", where $\pi(E_0) \ne A$ for any proper closed subset $E_0 \subsetneq E$.  -/
exists_compact_surjective_zorn_subset : ∀ {A D : Type u} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace D] [T1Space A] [CompactSpace D] {X : D → A},
  Continuous X →
    Function.Surjective X →
      ∃ E,
        CompactSpace ↑E ∧
          X '' E = Set.univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ Set.univ → IsClosed E₀ → E.domRestrict X '' E₀ ≠ Set.univ
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflection in the `Submodule.map` of a subspace.  -/
Submodule.reflection_map_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup E'] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E')
  (K : Submodule 𝕜 E) [inst_5 : K.HasOrthogonalProjection] (x : E'),
  (Submodule.map (↑f.toLinearEquiv) K).reflection x = f (K.reflection (f.symm x))
-- Mathlib.Dynamics.Minimal
MulAction.isMinimal_of_pretransitive : ∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [MulAction.IsPretransitive M α], MulAction.IsMinimal M α
-- Mathlib.Analysis.Complex.Basic
Complex.equivRealProdCLM_symm_apply : ∀ (p : ℝ × ℝ), Complex.equivRealProdCLM.symm p = ↑p.1 + ↑p.2 * Complex.I
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : C}
  {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : Opposite.unop Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYoneda.{w, v, u}.obj X).map g))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm f) =
    CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g.unop f)
-- Mathlib.Tactic.DeriveTraversable
/-- Derive the `cls` instance for the inductive type constructor `n` using the `tac` tactic.  -/
Mathlib.Deriving.Traversable.mkOneInstance : Lean.Name →
  Lean.Name →
    (Lean.MVarId → Lean.Elab.TermElabM Unit) →
      (optParam (Lean.Name → Lean.Expr → Lean.Elab.TermElabM Lean.Expr) fun n arg =>
          liftM (Lean.Meta.mkAppM n #[arg])) →
        Lean.Elab.TermElabM Unit
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N), Function.Surjective ⇑e
-- Init.Prelude
/-- `Or.inl` is "left injection" into an `Or`. If `h : a` then `Or.inl h : a ∨ b`.  -/
Or.inl : ∀ {a b : Prop}, a → a ∨ b
-- Mathlib.Topology.GDelta.MetrizableSpace
instNormalSpaceOfPseudoMetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X], NormalSpace X
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- The restriction of a `MorphismProperty Scheme` to morphisms with affine target.  -/
AlgebraicGeometry.AffineTargetMorphismProperty.of : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → AlgebraicGeometry.AffineTargetMorphismProperty
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_diff_le_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp], (t₁ \ t₂).size ≤ t₁.size
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableDiv₂ : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Div α] [DiscreteMeasurableSpace (α × α)], MeasurableDiv₂ α
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The extended distance between two vertices is the length of the shortest walk between them.
It is `⊤` if no such walk exists.
 -/
SimpleGraph.edist : {V : Type u_1} → SimpleGraph V → V → V → ℕ∞
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.iso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)],
  CategoryTheory.Limits.PreservesPushout.iso G f g =
    (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.span (G.map f) (G.map g))).coconePointUniqueUpToIso
      (CategoryTheory.Limits.isColimitOfHasPushoutOfPreservesColimit G f g)
-- Mathlib.Algebra.Module.Torsion.Basic
Module.IsTorsionBySet.isScalarTower : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (hM : Module.IsTorsionBySet R M ↑I) {S : Type u_3} [inst_3 : SMul S R] [inst_4 : SMul S M] [IsScalarTower S R M]
  [inst_6 : IsScalarTower S R R], IsScalarTower S (R ⧸ I) M
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.mkHom_apply : ∀ {M N : Type u} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N] (f : NormedAddGroupHom M N)
  (i : f.NormNoninc) (x : { carrier := M, str := inst }.carrier),
  ↑(SemiNormedGrp₁.Hom.hom (SemiNormedGrp₁.mkHom f i)) x = f x
-- Init.Data.Iterators.Consumers.Monadic.Access
Std.IterM.IsPlausibleNthOutputStep.below.done : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β]
  {motive :
    (a : ℕ) →
      (a_1 : Std.IterM m β) →
        (a_2 : Std.IterStep (Std.IterM m β) β) → Std.IterM.IsPlausibleNthOutputStep a a_1 a_2 → Prop}
  {n : ℕ} {it : Std.IterM m β} (a : it.IsPlausibleStep Std.IterStep.done), Std.IterM.IsPlausibleNthOutputStep.below ⋯
-- Lean.Elab.PreDefinition.WF.Preprocess
_private.Lean.Elab.PreDefinition.WF.Preprocess.0.Lean.Elab.WF.anyLetValueIsWfParam : Lean.Expr → Bool
-- Mathlib.Algebra.FreeMonoid.Basic
/-- The length of an additive free monoid element: 1.length = 0 and (a + b).length =
a.length + b.length  -/
FreeAddMonoid.length : {α : Type u_1} → FreeAddMonoid α → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A subgraph of a connected graph is maximal acyclic iff it is a tree.  -/
SimpleGraph.Connected.maximal_le_isAcyclic_iff_isTree : ∀ {V : Type u_1} {G T : SimpleGraph V}, G.Connected → T ≤ G → (Maximal (fun H => H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The map `embedding ∘ orderMonoidIso (valuation R))` is identity.  -/
ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R],
  Function.LeftInverse ⇑MonoidWithZeroHom.ValueGroup₀.embedding
    ⇑(ValuativeRel.ValueGroupWithZero.orderMonoidIso (ValuativeRel.valuation R))