mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
/-- An absolute left Kan lift of the identity along `u` is a left adjoint to `u`.
The unit of this adjunction is given by the unit of the Kan lift.  -/
CategoryTheory.Bicategory.LeftLift.IsAbsKan.adjunction : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {u : b ⟶ a} →
        (t : CategoryTheory.Bicategory.LeftLift u (CategoryTheory.CategoryStruct.id a)) →
          t.IsAbsKan → CategoryTheory.Bicategory.Adjunction t.lift u
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Modified version of `hasSum_int_evenKernel` omitting the constant term at `∞`.  -/
HurwitzZeta.hasSum_int_evenKernel₀ : ∀ (a : ℝ) {t : ℝ},
  0 < t →
    HasSum (fun n => if ↑n + a = 0 then 0 else Real.exp (-Real.pi * (↑n + a) ^ 2 * t))
      (HurwitzZeta.evenKernel (↑a) t - if ↑a = 0 then 1 else 0)
-- Mathlib.RingTheory.Regular.RegularSequence
AddEquiv.isRegular_congr : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {e : M ≃+ M₂}
  {as : List R} {bs : List S},
  List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs →
    (RingTheory.Sequence.IsRegular M as ↔ RingTheory.Sequence.IsRegular M₂ bs)
-- Init.Data.Nat.Bitwise.Lemmas
/-- This provides a bound on bitwise operations.  -/
Nat.bitwise_lt_two_pow : ∀ {x n y : ℕ} {f : Bool → Bool → Bool}, x < 2 ^ n → y < 2 ^ n → Nat.bitwise f x y < 2 ^ n
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropSuffix?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.toSlice.dropSuffix? pat = s.dropSuffix? pat
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_inter!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter! m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Algebra.Algebra.Hom
AlgHom.commutes' : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (self : A →ₐ[R] B) (r : R),
  (↑↑self.toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.geometrically_iff_of_commRing : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {R : Type u}
  [inst : CommRing R] {f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)},
  AlgebraicGeometry.geometrically P f ↔
    ∀ ⦃K : Type u⦄ [inst_1 : Field K] [inst_2 : Algebra R K] ⦃Y : AlgebraicGeometry.Scheme⦄ (fst : Y ⟶ X)
      (snd : Y ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)),
      CategoryTheory.IsPullback fst snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) → P Y
-- Mathlib.Logic.Denumerable
nonempty_equiv_of_countable : ∀ {α : Type u_1} {β : Type u_2} [Countable α] [Infinite α] [Countable β] [Infinite β], Nonempty (α ≃ β)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.instMonoidalProdDiag : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.Functor.diag C).Monoidal
-- Mathlib.Combinatorics.SimpleGraph.Sum
_private.Mathlib.Combinatorics.SimpleGraph.Sum.0.SimpleGraph.edgeSetSumEquiv.match_1.eq_3 : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}
  (motive : (x x_1 : V ⊕ W) → (G ⊕g H).Adj x x_1 → Sort u_3) (u : V) (v : W) (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v))
  (h_1 : (u v : V) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)) → motive (Sum.inl u) (Sum.inl v) h)
  (h_2 : (u v : W) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)) → motive (Sum.inr u) (Sum.inr v) h)
  (h_3 : (u : V) → (v : W) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)) → motive (Sum.inl u) (Sum.inr v) h)
  (h_4 : (u : W) → (v : V) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)) → motive (Sum.inr u) (Sum.inl v) h),
  (match Sum.inl u, Sum.inr v, h with
    | Sum.inl u, Sum.inl v, h => h_1 u v h
    | Sum.inr u, Sum.inr v, h => h_2 u v h
    | Sum.inl u, Sum.inr v, h => h_3 u v h
    | Sum.inr u, Sum.inl v, h => h_4 u v h) =
    h_3 u v h
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_injective : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N], Function.Injective DFunLike.coe
-- Mathlib.Order.CompleteLattice.Basic
biSup_congr : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] {f g : ι → α} {p : ι → Prop},
  (∀ (i : ι), p i → f i = g i) → ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), g i
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.OfLocalizationSpan.mk : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
        Ideal.span s = ⊤ →
          (∀ r ∈ s, P (algebraMap (Localization.Away r) (TensorProduct R (Localization.Away r) S))) →
            P (algebraMap R S)) →
      RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.prod_eq_inf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  {f₁ f₂ : CategoryTheory.Subobject A} [inst_2 : CategoryTheory.Limits.HasBinaryProduct f₁ f₂], (f₁ ⨯ f₂) = f₁ ⊓ f₂
-- Lean.Data.KVMap
Lean.DataValue.str : Lean.DataValue → String
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The condition for the matrices `A`, `A'` to be an adjoint pair with respect to the square
matrices `J`, `J₃`.  -/
Matrix.IsAdjointPair : {R : Type u_1} →
  {n : Type u_11} →
    {n' : Type u_13} →
      [CommRing R] → [Fintype n] → [Fintype n'] → Matrix n n R → Matrix n' n' R → Matrix n' n R → Matrix n n' R → Prop
-- Mathlib.Data.Multiset.UnionInter
Multiset.cons_inter_of_pos : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α),
  a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zsmul_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] (a : α) (n : ℤ), n • {a} = {n • a}
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_of_not_measurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) {f : β → γ}, ¬Measurable f → κ.map f = 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RocSliceData : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Mathlib.Algebra.Opposites
AddOpposite.instMul : {α : Type u_1} → [Mul α] → Mul αᵃᵒᵖ
-- Mathlib.RingTheory.MatrixAlgebra
/-- `Matrix.kroneckerTMul` as a linear equivalence, when the two arguments are tensored.  -/
kroneckerTMulLinearEquiv : (l : Type u_1) →
  (m : Type u_2) →
    (n : Type u_3) →
      (p : Type u_4) →
        (R : Type u_5) →
          (S : Type u_6) →
            (M : Type u_9) →
              (N : Type u_10) →
                [inst : CommSemiring R] →
                  [inst_1 : Semiring S] →
                    [inst_2 : AddCommMonoid M] →
                      [inst_3 : AddCommMonoid N] →
                        [inst_4 : Algebra R S] →
                          [inst_5 : Module R M] →
                            [inst_6 : Module S M] →
                              [inst_7 : Module R N] →
                                [inst_8 : IsScalarTower R S M] →
                                  [Fintype l] →
                                    [Fintype m] →
                                      [Fintype n] →
                                        [Fintype p] →
                                          [DecidableEq l] →
                                            [DecidableEq m] →
                                              [DecidableEq n] →
                                                [DecidableEq p] →
                                                  TensorProduct R (Matrix l m M) (Matrix n p N) ≃ₗ[S]
                                                    Matrix (l × n) (m × p) (TensorProduct R M N)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdFunctorEquivUnitIso_hom_app : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (X : CategoryTheory.Functor A B × CategoryTheory.Functor A C),
  (CategoryTheory.functorProdFunctorEquivUnitIso A B C).hom.app X =
    CategoryTheory.Prod.mkHom (X.1.prod'CompFst X.2).inv (X.1.prod'CompSnd X.2).inv
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Cnstr.offset.injEq : ∀ (gen? : Option Lean.Meta.Grind.GenPatternInfo) (pat : Lean.Expr) (k : ℕ) (e : Lean.Expr)
  (gen?_1 : Option Lean.Meta.Grind.GenPatternInfo) (pat_1 : Lean.Expr) (k_1 : ℕ) (e_1 : Lean.Expr),
  (Lean.Meta.Grind.EMatch.Cnstr.offset gen? pat k e = Lean.Meta.Grind.EMatch.Cnstr.offset gen?_1 pat_1 k_1 e_1) =
    (gen? = gen?_1 ∧ pat = pat_1 ∧ k = k_1 ∧ e = e_1)
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.baireSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [BaireSpace X] (f : X ≃ₜ Y),
  BaireSpace Y
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.instNonUnitalStarRingHomClass : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B], NonUnitalStarRingHomClass (A →⋆ₙ+* B) A B
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_add_left_right_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime x (x * z + y) ↔ IsCoprime x y
-- Mathlib.Algebra.BigOperators.Expect
map_expect : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module ℚ≥0 N] {F : Type u_6} [inst_4 : FunLike F M N] [LinearMapClass F ℚ≥0 M N]
  (g : F) (f : ι → M) (s : Finset ι), g (s.expect fun i => f i) = s.expect fun i => g (f i)
-- Mathlib.Data.Int.Cast.Lemmas
Int.cast_commute : ∀ {α : Type u_3} [inst : NonAssocRing α] (n : ℤ) (a : α), Commute (↑n) a
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftBindFunction.mk : ∀ {m : Type u → Type v} {n : Type w → Type x} [inst : Monad m] [inst_1 : Monad n]
  {liftBind : (γ : Type u) → (δ : Type w) → (γ → n δ) → m γ → n δ},
  (∀ {γ : Type u} {δ : Type w} (f : γ → n δ) (a : γ), liftBind γ δ f (pure a) = f a) →
    (∀ {β γ : Type u} {δ : Type w} (f : γ → n δ) (x : m β) (g : β → m γ),
        liftBind γ δ f (x >>= g) = liftBind β δ (fun b => liftBind γ δ f (g b)) x) →
      Std.Internal.LawfulMonadLiftBindFunction liftBind
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  P.pairing i j = (P.root' i) (P.coroot j)
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.Equiv.exists_step_of_step : ∀ {α₁ : Type u_1} {m : Type u_1 → Type u_2} {β α₂ : Type u_1} [inst : Std.Iterator α₁ m β]
  [inst_1 : Std.Iterator α₂ m β] [inst_2 : Monad m] [inst_3 : LawfulMonad m] {ita : Std.IterM m β}
  {itb : Std.IterM m β}, ita.Equiv itb → ∀ (s : ita.Step), ∃ s', (↑s).bundledQuotient = (↑s').bundledQuotient
-- Mathlib.Data.Set.Restrict
Set.domRestrict_ite_compl : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [inst : (x : α) → Decidable (x ∈ s)],
  (sᶜ.domRestrict fun a => if a ∈ s then f a else g a) = sᶜ.domRestrict g
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_bijOn : Set.BijOn Real.artanh (Set.Ioo (-1) 1) Set.univ
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₂Toπ₃_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.π₂Toπ₃.app S = S.g
-- Mathlib.Algebra.Group.Basic
add_right_surjective : ∀ {G : Type u_3} [inst : AddGroup G] (a : G), Function.Surjective fun x => x + a
-- Init.Data.Range.Polymorphic.SInt
Int32.le.eq_1 : ∀ (a b : Int32), a.le b = (a.toBitVec.sle b.toBitVec = true)
-- Mathlib.Data.Fin.Tuple.Basic
/-- Splitting a dependent finite sequence v into an initial part and a final part,
and then concatenating these components, produces an identical sequence.  -/
Fin.addCases_castAdd_natAdd : ∀ {m n : ℕ} {γ : Fin (m + n) → Sort u_2} (v : (i : Fin (m + n)) → γ i) (i : Fin (m + n)),
  Fin.addCases (fun i => v (Fin.castAdd n i)) (fun j => v (Fin.natAdd m j)) i = v i
-- Mathlib.RingTheory.Norm.Transitivity
/-- A matrix with X added to the corner.  -/
Algebra.Norm.Transitivity.cornerAddX : {S : Type u_2} → {m : Type u_5} → [inst : CommRing S] → Matrix m m S → [DecidableEq m] → m → Matrix m m (Polynomial S)
-- Mathlib.Order.Directed
IsCodirectedOrder.eq_1 : ∀ (α : Type u_5) [inst : LE α], IsCodirectedOrder α = IsDirected α fun x1 x2 => x2 ≤ x1
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.differentiableAt_arcosh : ∀ {x : ℝ}, x ∈ Set.Ioi 1 → DifferentiableAt ℝ Real.arcosh x
-- Mathlib.Order.Filter.Defs
/-- If two sets belong to a filter, then their intersection belongs to the filter as well.  -/
Filter.inter_sets : ∀ {α : Type u_1} (self : Filter α) {x y : Set α}, x ∈ self.sets → y ∈ self.sets → x ∩ y ∈ self.sets
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The algebra isomorphism of monoid algebras induced by an isomorphism of the base algebras.  -/
MonoidAlgebra.mapAlgEquiv : (R : Type u_1) →
  {A : Type u_4} →
    {B : Type u_5} →
      (M : Type u_7) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] → [inst_5 : Monoid M] → (A ≃ₐ[R] B) → MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra B M
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.functorCategory_inverseImage_isomorphisms_unit : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  [F.Full] [F.Faithful] (adj : G ⊣ F),
  ((CategoryTheory.MorphismProperty.isomorphisms C₂).inverseImage G).functorCategory C₁ adj.unit
-- Mathlib.Analysis.Convex.Between
Wbtw.right_mem_affineSpan_of_left_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z → x ≠ y → z ∈ line[R, x, y]
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- the induced map on opcycles  -/
CategoryTheory.ShortComplex.RightHomologyMapData.φQ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.RightHomologyData} →
            {h₂ : S₂.RightHomologyData} → CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂ → (h₁.Q ⟶ h₂.Q)
-- Aesop.RuleTac.Basic
Aesop.CasesTarget.patterns.injEq : ∀ (patterns patterns_1 : Array Aesop.CasesPattern),
  (Aesop.CasesTarget.patterns patterns = Aesop.CasesTarget.patterns patterns_1) = (patterns = patterns_1)
-- Mathlib.Probability.Distributions.Gaussian.Real
Equiv.mulLeft₀.congr_simp : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a a_1 : G₀) (e_a : a = a_1) (ha : a ≠ 0),
  Equiv.mulLeft₀ a ha = Equiv.mulLeft₀ a_1 ⋯
-- Std.Data.TreeMap.Basic
Std.TreeMap.instForMProdOfMonad : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForM m (Std.TreeMap α β cmp) (α × β)
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_top_bot : ∀ {G : Type u_1} [inst : Group G], ⊤.IsComplement' ⊥
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forIn_eq_forIn_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ},
  forIn t init f = forIn t.toList init f
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The composition of the algebra homomorphisms `A → (A / I)` and `(A / I) → (A / I) / J'`,
where `J'` is the projection `J` in `A / I`.  -/
DoubleQuot.quotQuotMkₐ : (R : Type u) →
  {A : Type u_1} →
    [inst : CommSemiring R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] → (I J : Ideal A) → A →ₐ[R] (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁_X_left : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R],
  MvPolynomial.bind₁ MvPolynomial.X = AlgHom.id R (MvPolynomial σ R)
-- Init.Data.Fin.Lemmas
Fin.ge_of_eq : ∀ {n : ℕ} {a b : Fin n}, a = b → b ≤ a
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_induction : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {s : Set E}
  {p : (x : E) → x ∈ IntermediateField.adjoin F s → Prop},
  (∀ (x : E) (hx : x ∈ s), p x ⋯) →
    (∀ (x : F), p ((algebraMap F E) x) ⋯) →
      (∀ (x y : E) (hx : x ∈ IntermediateField.adjoin F s) (hy : y ∈ IntermediateField.adjoin F s),
          p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x : E) (hx : x ∈ IntermediateField.adjoin F s), p x hx → p x⁻¹ ⋯) →
          (∀ (x y : E) (hx : x ∈ IntermediateField.adjoin F s) (hy : y ∈ IntermediateField.adjoin F s),
              p x hx → p y hy → p (x * y) ⋯) →
            ∀ {x : E} (h : x ∈ IntermediateField.adjoin F s), p x h
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.algebraMap_isUnit : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [IsLocalization.Away x S], IsUnit ((algebraMap R S) x)
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_one_const_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] (a : 𝕜) (f : ι → 𝕜),
  ⟪Function.const ι a, f⟫_[𝕜] = (∑ i, f i) * (starRingEnd 𝕜) a
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.desc.multicofork_pt : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃),
  (SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt = X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_union!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true →
          Std.DTreeMap.Internal.Impl.contains k m₂ = false → Std.DTreeMap.Internal.Impl.contains k m₁ = true
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconcaveOn.antitone_comp : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_4 : LinearOrder β] [inst_5 : Preorder γ] {s : Set E}
  {f : E → β} {g : β → γ}, Antitone g → QuasiconcaveOn 𝕜 s f → QuasiconvexOn 𝕜 s (g ∘ f)
-- Lean.Data.Json.Basic
Lean.JsonNumber.fromNat : ℕ → Lean.JsonNumber
-- Mathlib.RingTheory.Valuation.Quotient
Valuation.comap_onQuot_eq : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (J : Ideal R)
  (v : Valuation (R ⧸ J) Γ₀), (Valuation.comap (Ideal.Quotient.mk J) v).onQuot ⋯ = v
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.instMonoι : ∀ {n : ℕ} (i : Fin (n + 2)), CategoryTheory.Mono (SSet.boundary.ι i)
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.dual_id : ∀ {α : Type u_2} [inst : SupSet α], sSupHom.dual (sSupHom.id α) = sInfHom.id αᵒᵈ
-- Mathlib.Order.Disjointed
disjointed_eq_self : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι] {f : ι → α} {i : ι}, (∀ j < i, Disjoint (f j) (f i)) → disjointed f i = f i
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.vaddAssocClass : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass M'] [inst_1 : VAdd α β] [inst_2 : VAdd M' α]
  [inst_3 : VAdd M' β] [VAddAssocClass M' α β] (S : AddSubmonoid M'), VAddAssocClass (↥S) α β
-- Mathlib.Computability.Reduce
ManyOneReducible.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → β} (q : β → Prop),
  Computable f → (fun a => q (f a)) ≤₀ q
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_addHom_mk : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₙ+ M₃) (h : ∀ (m : R) (x : M), f.toFun (m • x) = σ m • f.toFun x), ↑{ toAddHom := f, map_smul' := h } = f
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.induction_on : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] {x y : A} (hy : y ∈ StarAlgebra.elemental R x)
  {P : (u : A) → u ∈ StarAlgebra.elemental R x → Prop},
  P x ⋯ →
    P (star x) ⋯ →
      (∀ (r : R), P ((algebraMap R A) r) ⋯) →
        (∀ (u : A) (hu : u ∈ StarAlgebra.elemental R x) (v : A) (hv : v ∈ StarAlgebra.elemental R x),
            P u hu → P v hv → P (u + v) ⋯) →
          (∀ (u : A) (hu : u ∈ StarAlgebra.elemental R x) (v : A) (hv : v ∈ StarAlgebra.elemental R x),
              P u hu → P v hv → P (u * v) ⋯) →
            (∀ (s : Set A) (hs : s ⊆ ↑(StarAlgebra.elemental R x)),
                (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure s), P v ⋯) →
              P y hy
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff : ∀ {θ : ℝ} {k : ℤ}, (↑θ).toReal = θ - 2 * ↑k * Real.pi ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * Real.pi) ((2 * ↑k + 1) * Real.pi)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIdIso C).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
-- Mathlib.Topology.Compactness.LocallyFinite
/-- If `X` is a compact space, then a locally finite family of sets of `X` can have only finitely
many nonempty elements.  -/
LocallyFinite.finite_nonempty_of_compact : ∀ {X : Type u_1} {ι : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] {f : ι → Set X},
  LocallyFinite f → {i | (f i).Nonempty}.Finite