mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk_X_2 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0),
  (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
/-- The single functor `C ⥤ HomotopyCategory C (ComplexShape.up ℤ)`
which sends `X` to the complex consisting of `X` in degree `n : ℤ` and zero otherwise.  -/
HomotopyCategory.singleFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasZeroObject C] → ℤ → CategoryTheory.Functor C (HomotopyCategory C (ComplexShape.up ℤ))
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.processPendingInst : Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.HasFactorization.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C},
  (∀ {X Y : C} (f : X ⟶ Y), Nonempty (W₁.MapFactorizationData W₂ f)) → W₁.HasFactorization W₂
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.of_image_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, ↑e '' (e.source ∩ s) = e.target ∩ t → e.IsImage s t
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_le_iff_le_sq : ∀ {x y : NNReal}, NNReal.sqrt x ≤ y ↔ x ≤ y ^ 2
-- Lean.PrettyPrinter.Delaborator.FieldNotation
/-- Checks that `e` is an application of a constant that equals `baseName`, taking into consideration private name mangling.
 -/
_private.Lean.PrettyPrinter.Delaborator.FieldNotation.0.Lean.PrettyPrinter.Delaborator.isAppOfBaseName : Lean.Expr → Lean.Name → Lean.MetaM Bool
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_diag : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  {A : X → Matrix n n R}, Continuous A → Continuous fun x => (A x).diag
-- Std.Do.PredTrans
/-- Any predicate transformer that is conjunctive is also monotonic.  -/
Std.Do.PredTrans.Conjunctive.mono : ∀ {ps : Std.Do.PostShape} {α : Type u} (t : Std.Do.PostCond α ps → Std.Do.Assertion ps),
  Std.Do.PredTrans.Conjunctive t → Std.Do.PredTrans.Monotonic t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).size = if t.contains k = true then t.size - 1 else t.size
-- Mathlib.Algebra.Exact.Sequence
_private.Mathlib.Algebra.Exact.Sequence.0.Module.sum_neg_one_pow_finrank_eq_zero_of_exact_six_aux : ∀ {k : Type u_1} [inst : DivisionRing k] {V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀} [inst_1 : AddCommGroup V₀] [inst_2 : Module k V₀]
  [FiniteDimensional k V₀] [inst_4 : AddCommGroup V₁] [inst_5 : Module k V₁] [FiniteDimensional k V₁]
  [inst_7 : AddCommGroup V₂] [inst_8 : Module k V₂] [FiniteDimensional k V₂] [inst_10 : AddCommGroup V₃]
  [inst_11 : Module k V₃] [FiniteDimensional k V₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [FiniteDimensional k V₄] [inst_16 : AddCommGroup V₅] [inst_17 : Module k V₅] [FiniteDimensional k V₅]
  (f₀ : V₀ →ₗ[k] V₁) (f₁ : V₁ →ₗ[k] V₂) (f₂ : V₂ →ₗ[k] V₃) (f₃ : V₃ →ₗ[k] V₄) (f₄ : V₄ →ₗ[k] V₅),
  Function.Injective ⇑f₀ →
    Function.Exact ⇑f₀ ⇑f₁ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑f₂ ⇑f₃ →
          Function.Exact ⇑f₃ ⇑f₄ →
            Function.Surjective ⇑f₄ →
              ↑(Module.finrank k V₀) - ↑(Module.finrank k V₁) + ↑(Module.finrank k V₂) - ↑(Module.finrank k V₃) +
                    ↑(Module.finrank k V₄) -
                  ↑(Module.finrank k V₅) =
                0
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- If a family is anisotropic then its components must be. The converse is not true.  -/
QuadraticMap.anisotropic_of_pi : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : AddCommMonoid P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P},
  (QuadraticMap.pi Q).Anisotropic → ∀ (i : ι), (Q i).Anisotropic
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.nonpos_intCast_of_nonpos : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R], ∀ a ≤ 0, ↑a ≤ 0
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.op.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.MorphismProperty C) (x x_1 : Cᵒᵖ)
  (f : x ⟶ x_1), P.op f = P f.unop
-- Mathlib.LinearAlgebra.Matrix.Ideal
RingCon.ofMatrix_matrix : ∀ {R : Type u_1} {n : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [Nonempty n] (c : RingCon R), (RingCon.matrix n c).ofMatrix = c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_map_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k k' : α},
  t.getKey? k = some k' →
    Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.map f t) k = Option.map (f k') (Std.ExtDTreeMap.Const.get? t k)
-- Mathlib.MeasureTheory.OuterMeasure.Basic
/-- A version of `MeasureTheory.OuterMeasure.ext` that assumes `μ₁ s = μ₂ s` on all *nonempty*
sets `s`, and gets `μ₁ ∅ = μ₂ ∅` from `MeasureTheory.OuterMeasure.empty'`.  -/
MeasureTheory.OuterMeasure.ext_nonempty : ∀ {α : Type u_1} {μ₁ μ₂ : MeasureTheory.OuterMeasure α}, (∀ (s : Set α), s.Nonempty → μ₁ s = μ₂ s) → μ₁ = μ₂
-- Mathlib.Data.Int.Init
/-- **Alias** of `Int.leInductionDown`.

---

See `Int.inductionOn'` for an induction in both directions.  -/
Int.le_induction_down : {m : ℤ} →
  {motive : (n : ℤ) → n ≤ m → Sort u_1} →
    motive m ⋯ → ((n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯) → (n : ℤ) → (hnm : n ≤ m) → motive n hnm
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k a : α}, (t.erase k)[a]! = if cmp k a = Ordering.eq then default else t[a]!
-- Mathlib.Order.Disjointed
disjointed_eq_inter_compl : ∀ {α : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] (f : ι → Set α) (i : ι),
  disjointed f i = f i ∩ ⋂ j, ⋂ (_ : j < i), (f j)ᶜ
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.ι_mapBifunctorRightUnitor_hom_apply_assoc : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D)
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  (j : J) {Z : D} (h : X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom j)
        h) =
    CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
      (CategoryTheory.CategoryStruct.comp (e.hom.app (X j)) h)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.instNormalSubgroup : ∀ {G : Type u_1} [inst : Group G] (c : Con G), c.subgroup.Normal
-- Std.Sat.CNF.Basic
Std.Sat.CNF.emptyWithCapacity : {α : Type u_1} → ℕ → Std.Sat.CNF α
-- Mathlib.Algebra.Algebra.Subalgebra.Prod
Subalgebra.prod_mono : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B},
  S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_7 : ∀ (a : Lean.Grind.CommRing.Expr), a.neg.toPoly = Lean.Grind.CommRing.Poly.mulConst (-1) a.toPoly
-- Init.Data.String.Lemmas.Splits
/-- Given a string `s` such that `s = t₁ ++ t₂`, obtain the position sitting between `t₁` and `t₂`.
 -/
String.Pos.ofEqAppend : {s t₁ t₂ : String} → s = t₁ ++ t₂ → s.Pos
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.comp_hom_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X},
  CategoryTheory.CategoryStruct.comp f α.hom = CategoryTheory.CategoryStruct.id Y ↔ f = α.inv
-- Std.Time.Duration
/-- Adds two durations together, handling any carry-over in nanoseconds.
 -/
Std.Time.Duration.add : Std.Time.Duration → Std.Time.Duration → Std.Time.Duration
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_eq_true_iff_forall_mem_getKey_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {p : α → β → Bool},
  m.WF → (m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = true)
-- Mathlib.Topology.Bornology.Constructions
Pi.instBornology : {ι : Type u_3} → {X : ι → Type u_4} → [(i : ι) → Bornology (X i)] → Bornology ((i : ι) → X i)
-- Init.Data.Array.FinRange
Array.finRange_succ_last : ∀ {n : ℕ}, Array.finRange (n + 1) = Array.map Fin.castSucc (Array.finRange n) ++ #[Fin.last n]
-- Mathlib.Order.Interval.Set.UnorderedInterval
/-- Same as `Ioo_subset_uIoo` but with `Ioo a b` replaced by `Ioo b a`.  -/
Set.Ioo_subset_uIoo' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioo b a ⊆ Set.uIoo a b
-- Mathlib.Order.Defs.Unbundled
IsPreorder.toRefl : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsPreorder α r], Std.Refl r
-- Mathlib.Algebra.Ring.SumsOfSquares
IsSumSq.one : ∀ {R : Type u_1} [inst : AddZeroClass R] [inst_1 : MulOneClass R], IsSumSq 1
-- Mathlib.Order.UpperLower.Prod
lowerClosure_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : Set α) (t : Set β),
  lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t
-- Mathlib.Tactic.ITauto
/-- `(p: A ∨ B → C) ⊢ A → C`  -/
Mathlib.Tactic.ITauto.Proof.orImpL : Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Analysis.Normed.Group.Bounded
NormedCommGroup.cauchySeq_iff : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedGroup E] [Nonempty α] [inst_2 : SemilatticeSup α] {u : α → E},
  CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖(u m)⁻¹ * u n‖ < ε
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_mod_65536 : ∀ (n : UInt16), n.toUInt32 % 65536 = n.toUInt32
-- Mathlib.Condensed.Light.Functors
instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet : CategoryTheory.Limits.PreservesFiniteCoproducts lightProfiniteToLightCondSet
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.inv'_apply : ∀ (G : Type u_3) [inst : DivisionMonoid G], ⇑(MulEquiv.inv' G) = MulOpposite.op ∘ Inv.inv
-- Mathlib.Data.Set.Card
Set.ncard_sdiff_singleton_add_one : ∀ {α : Type u_1} {s : Set α} {a : α},
  a ∈ s → autoParam s.Finite Set.ncard_sdiff_singleton_add_one._auto_1 → (s \ {a}).ncard + 1 = s.ncard
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.div_add_mod : ∀ {R : Type u} [inst : EuclideanDomain R] (a b : R), b * (a / b) + a % b = a
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.isMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α], Order.IsSuccPrelimit (Order.succ a) → IsMax a
-- Mathlib.Order.Filter.Finite
Filter.mem_iInf_finite : ∀ {α : Type u} {ι : Type u_2} {f : ι → Filter α} (s : Set α), s ∈ iInf f ↔ ∃ t, s ∈ ⨅ i ∈ t, f i
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.AltParamInfo.mk.injEq : ∀ (numFields numOverlaps : ℕ) (hasUnitThunk : Bool) (numFields_1 numOverlaps_1 : ℕ) (hasUnitThunk_1 : Bool),
  ({ numFields := numFields, numOverlaps := numOverlaps, hasUnitThunk := hasUnitThunk } =
      { numFields := numFields_1, numOverlaps := numOverlaps_1, hasUnitThunk := hasUnitThunk_1 }) =
    (numFields = numFields_1 ∧ numOverlaps = numOverlaps_1 ∧ hasUnitThunk = hasUnitThunk_1)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertMany_list_singleton : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, m.insertMany [(k, v)] = m.insert k v
-- Mathlib.Topology.Compactness.Lindelof
nonLindelofSpace_of_neBot : ∀ {X : Type u} [inst : TopologicalSpace X], (Filter.coLindelof X).NeBot → NonLindelofSpace X
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the forward direction of `uniqueMDiffWithinAt_iff_uniqueDiffWithinAt`. -/
UniqueMDiffWithinAt.uniqueDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E}, UniqueMDiffAt[s] x → UniqueDiffWithinAt 𝕜 s x
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.TensorProduct.quotIdealMapEquivTensorQuot_symm_tmul : ∀ {A : Type u_1} (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (I : Ideal A) (b : B)
  (a : A),
  (Algebra.TensorProduct.quotIdealMapEquivTensorQuot B I).symm (b ⊗ₜ[A] (Ideal.Quotient.mk I) a) =
    Submodule.Quotient.mk (a • b)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instSemigroupWithZero : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [SemigroupWithZero Y] → SemigroupWithZero (LocallyConstant X Y)
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- The identity map is a coalgebra equivalence.  -/
CoalgEquiv.refl : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [inst_3 : CoalgebraStruct R A] → A ≃ₗc[R] A
-- Batteries.Tactic.GeneralizeProofs
/-- Computes expected types for each argument to `f`,
given that the type of `mkAppN f args` is supposed to be `ty?`
(where if `ty?` is none, there's no type to propagate inwards).
 -/
Batteries.Tactic.GeneralizeProofs.appArgExpectedTypes : Lean.Expr → Array Lean.Expr → Option Lean.Expr → Lean.MetaM (Array (Option Lean.Expr))
-- Mathlib.Analysis.Normed.Module.Basic
/-- A linear map from a `Module` to a `NormedSpace` induces a `NormedSpace` structure on the
domain, using the `SeminormedAddCommGroup.induced` norm.

See note [reducible non-instances]  -/
NormedSpace.induced : {F : Type u_6} →
  (𝕜 : Type u_7) →
    (E : Type u_8) →
      (G : Type u_9) →
        [inst : NormedField 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  [inst_5 : FunLike F E G] → [inst_6 : LinearMapClass F 𝕜 E G] → (f : F) → NormedSpace 𝕜 E
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R), W'.neg P = ![P 0, W'.negY P, P 2]
-- Lean.Expr
Lean.instInhabitedData_1 : Inhabited Lean.Expr.Data
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchAltViews.throwEx : {α : Type} → Lean.Elab.Term.SavedState × Lean.Exception → Lean.Elab.TermElabM α
-- Mathlib.Data.List.Lookmap
List.lookmap_nil : ∀ {α : Type u_1} (f : α → Option α), List.lookmap f [] = []
-- Mathlib.Analysis.Normed.Group.Basic
/-- Extension for the `positivity` tactic: multiplicative norms are always nonnegative, and positive
on non-one inputs.  -/
Mathlib.Meta.Positivity.evalMulNorm : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.mk.injEq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (adj₁ : F ⊣ G) (adj₂ : G ⊣ H) (adj₁_1 : F ⊣ G) (adj₂_1 : G ⊣ H),
  ({ adj₁ := adj₁, adj₂ := adj₂ } = { adj₁ := adj₁_1, adj₂ := adj₂_1 }) = (adj₁ = adj₁_1 ∧ adj₂ = adj₂_1)
-- LeanSearchClient.Syntax
LeanSearchClient.leanSearchTacticImpl : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one_nonempty : ∀ {α : Type u_2} [inst : One α], Finset.Nonempty 1
-- Mathlib.Tactic.Linter.AuxLemma
/-- Returns `true` if `s` is an auto-generated auxiliary name component,
such as `_proof_1`, `match_2`, or `_sizeOf_3`.  -/
_private.Mathlib.Tactic.Linter.AuxLemma.0.Mathlib.Linter.AuxLemma.isAuxName : String → Bool
-- Mathlib.Order.SemiconjSup
isOrderRightAdjoint_csSup : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : Preorder β] (f : α → β),
  (∀ (y : β), ∃ x, f x ≤ y) → (∀ (y : β), BddAbove {x | f x ≤ y}) → IsOrderRightAdjoint f fun y => sSup {x | f x ≤ y}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.termZ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.commGroupTopologicalClosure.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] [inst_3 : T2Space G]
  (s : Subgroup G) (hs : ∀ (x y : ↥s), x * y = y * x),
  s.commGroupTopologicalClosure hs = { toGroup := s.topologicalClosure.toGroup, mul_comm := ⋯ }
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- `equiv.subLeft` as a `MeasurableEquiv`  -/
MeasurableEquiv.subLeft : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : MeasurableSpace G] → [MeasurableAdd G] → [MeasurableNeg G] → G → G ≃ᵐ G
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.coinfNatTrans_app : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G) [inst_2 : S.Normal] (n : ℕ)
  (A : Rep.{u, u, u} k G),
  (groupHomology.coinfNatTrans k S n).app A = groupHomology.map (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S) n
-- Init.Data.Option.Lemmas
Option.map_eq_map : ∀ {α α_1 : Type u_1} {f : α → α_1}, Functor.map f = Option.map f
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.Limits.prod.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X X_1 : C) (e_X : X = X_1) (Y Y_1 : C) (e_Y : Y = Y_1)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y], (X ⨯ Y) = (X_1 ⨯ Y_1)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Iio_cast : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n),
  ∏ i < Fin.cast h a, f i = ∏ i < a, f (Fin.cast h i)
-- Mathlib.Algebra.Free
FreeAddSemigroup.head_add : ∀ {α : Type u} (x y : FreeAddSemigroup α), (x + y).head = x.head
-- Mathlib.Order.RelIso.Basic
/-- A relation embedding with respect to a given pair of relations `r` and `s`
is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`.  -/
RelEmbedding : {α : Type u_5} → {β : Type u_6} → (α → α → Prop) → (β → β → Prop) → Type (max u_5 u_6)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.map_id : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Algebra.Extension.CotangentSpace.map (Algebra.Extension.Hom.id P) = LinearMap.id
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup : ∀ {R : Type u} [inst : CommRing R] (s₁ s₂ : TopologicalSpace.Clopens (PrimeSpectrum R)),
  PrimeSpectrum.isIdempotentElemEquivClopens.symm (s₁ ⊔ s₂) =
    ⟨↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₁) + ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₂) -
        ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₁) * ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₂),
      ⋯⟩
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.mk.injEq : ∀ {C : Type u₁} (of of_1 : C), ({ of := of } = { of := of_1 }) = (of = of_1)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalClosure_closure_eq_normalClosure : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, Subgroup.normalClosure ↑(Subgroup.closure s) = Subgroup.normalClosure s
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.id_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrictHom_symm_algebraMap_apply : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L]
  (σ : B →ₐ[A] B) (x : B), ((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)
-- Mathlib.Analysis.Convex.Star
StarConvex.mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E} [ZeroLEOneClass 𝕜], StarConvex 𝕜 x s → s.Nonempty → x ∈ s
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toList_head? : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (w : Monoid.CoprodI.NeWord M i j),
  w.toList.head? = some ⟨i, w.head⟩
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_modify_eq_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {f : β → β} {fallback : α}, (t.modify k f).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- Enable `a ^ y` notation for `CFC.nnrpow`. This is a low-priority instance to make sure it does
not take priority over other instances when they are available.  -/
CFC.instPowNNReal : {A : Type u_1} →
  [inst : PartialOrder A] →
    [inst_1 : NonUnitalRing A] →
      [inst_2 : TopologicalSpace A] →
        [inst_3 : StarRing A] →
          [inst_4 : Module ℝ A] →
            [inst_5 : SMulCommClass ℝ A A] →
              [inst_6 : IsScalarTower ℝ A A] →
                [StarOrderedRing A] →
                  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] → [NonnegSpectrumClass ℝ A] → Pow A NNReal
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_def' : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ),
  κ.rnDeriv η = fun a x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)
-- Mathlib.Dynamics.Ergodic.AddCircleAdd
AddCircle.ergodic_add_right : ∀ {p : ℝ} [inst : Fact (0 < p)] {a : AddCircle p}, Ergodic (fun x => x + a) MeasureTheory.volume ↔ addOrderOf a = 0