mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.limit_ext : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u})
  (x y : ↑(ProfiniteAddGrp.limit F).toProfinite.toTop), (∀ (j : J), ↑x j = ↑y j) → x = y
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromTarget.instMin : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P P' : CategoryTheory.ObjectProperty C)
  (Q : CategoryTheory.MorphismProperty C) [P.InheritedFromTarget Q] [P'.InheritedFromTarget Q],
  (P ⊓ P').InheritedFromTarget Q
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomWhiskerRight.eq_1 : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X X' : C}
  (f : X ⟶ X') (Y : C),
  CategoryTheory.eHomWhiskerRight V f Y =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X' ⟶[V] Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.eHomEquiv V) f) (X' ⟶[V] Y))
        (CategoryTheory.eComp V X X' Y))
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAtFilter.scomp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F} {y : 𝕜'}
  {L : Filter 𝕜} {L' : Filter 𝕜'},
  HasDerivAtFilter g₁ g₁' (L' ×ˢ pure y) →
    HasDerivAtFilter h h' (L ×ˢ pure x) →
      y = h x → Filter.Tendsto h L L' → HasDerivAtFilter (g₁ ∘ h) (h' • g₁') (L ×ˢ pure x)
-- Lean.Meta.Tactic.Grind.Types
/-- Case-split source. That is, where it came from.
We store the current source in the `grind` context.
 -/
Lean.Meta.Grind.SplitSource : Type
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_constVAdd : ∀ {G : Type u_1} (P : Type u_2) [inst : AddGroup G] [inst_1 : AddTorsor G P] (v : G),
  ⇑(Equiv.constVAdd P v) = fun x => v +ᵥ x
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul : ∀ (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : Algebra A B] [inst_15 : IsScalarTower A B M] (m : M)
  (n : N) (a : A),
  (TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N) (m ⊗ₜ[A] (a ⊗ₜ[R] n)) = (a • m) ⊗ₜ[R] n
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (p : ι → Prop) [inst_1 : DecidablePred p] (i : ι)
  (f : Π₀ (i : ι), β i), (DFinsupp.filter p f) i = if p i then f i else 0
-- Init.Data.Int.DivMod.Basic
_private.Init.Data.Int.DivMod.Basic.0.Int.fdiv.match_1.eq_6 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.negSucc n with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_6 m n
-- Init.Data.BitVec.Lemmas
BitVec.allOnes_shiftLeft_and_shiftLeft : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, BitVec.allOnes w <<< n &&& x <<< n = x <<< n
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual_of_not_memLp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E],
  ¬MeasureTheory.MemLp id 2 μ → ∀ (L₁ L₂ : StrongDual ℝ E), ((ProbabilityTheory.covarianceBilinDual μ) L₁) L₂ = 0
-- Mathlib.NumberTheory.Primorial
primorial_le_four_pow : ∀ (n : ℕ), primorial n ≤ 4 ^ n
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
/-- The morphism on cochain complexes indexed by `ℤ` that is induced by
a (heterogeneous) morphism of projective resolutions.  -/
CategoryTheory.ProjectiveResolution.Hom.hom' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X : C} →
        {R : CategoryTheory.ProjectiveResolution X} →
          {X' : C} →
            {R' : CategoryTheory.ProjectiveResolution X'} →
              {f : X ⟶ X'} → R.Hom R' f → (R.cochainComplex ⟶ R'.cochainComplex)
-- Lean.DocString.Markdown
Lean.Doc.instMarkdownBlockEmpty : {i : Type u_1} → Lean.Doc.MarkdownBlock i Empty
-- Mathlib.CategoryTheory.Subobject.Limits
/-- Given a commutative square between morphisms `f` and `g`,
we have a morphism in the category from `imageSubobject f` to `imageSubobject g`.  -/
CategoryTheory.Limits.imageSubobjectMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      {f : W ⟶ X} →
        [inst_1 : CategoryTheory.Limits.HasImage f] →
          {g : Y ⟶ Z} →
            [inst_2 : CategoryTheory.Limits.HasImage g] →
              (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) →
                [CategoryTheory.Limits.HasImageMap sq] →
                  CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶
                    CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject g)
-- Mathlib.GroupTheory.Coprod.Basic
/-- Lift two additive monoid
equivalences `e : M ≃+ N` and `e' : M' ≃+ N'` to an additive monoid equivalence
`(AddMonoid.Coprod M M') ≃+ (AddMonoid.Coprod N N')`.  -/
AddEquiv.coprodCongr : {M : Type u_1} →
  {N : Type u_2} →
    {M' : Type u_3} →
      {N' : Type u_4} →
        [inst : AddZeroClass M] →
          [inst_1 : AddZeroClass N] →
            [inst_2 : AddZeroClass M'] →
              [inst_3 : AddZeroClass N'] → M ≃+ N → M' ≃+ N' → AddMonoid.Coprod M M' ≃+ AddMonoid.Coprod N N'
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.directLimitRight_symm_of_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M] {i : ι}
  (m : M) (g : G i),
  (TensorProduct.directLimitRight f M).symm
      ((Module.DirectLimit.of R ι (fun x => TensorProduct R M (G x)) (fun i j h => LinearMap.lTensor M (f i j h)) i)
        (m ⊗ₜ[R] g)) =
    m ⊗ₜ[R] (Module.DirectLimit.of R ι G f i) g
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Lower hemicontinuity along a countably generated filter** (subsequence form):
if `f : α → Set β` is lower hemicontinuous at `x₀`, `y₀ ∈ f x₀`, `𝓝 y₀` is countably generated and
`x : ι → α` tends to `x₀` along a nontrivial countably generated filter `l`, then some sequence
`u : ℕ → ι` converging to `l` admits a companion `y : ℕ → β` tending to `y₀` with
`y k ∈ f (x (u k))` eventually.

For a general filter one must pass to the subsequence `u`: the "same-index" conclusion already
fails for `l = pure i₀` (which is `NeBot` and countably generated). When `l = atTop` one may take
`u = id`, recovering `LowerHemicontinuousAt.exists_seq_tendsto`.  -/
LowerHemicontinuousAt.exists_subseq_tendsto : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {ι : Type u_5}
  {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] {x₀ : α},
  LowerHemicontinuousAt f x₀ →
    ∀ {x : ι → α},
      Filter.Tendsto x l (nhds x₀) →
        ∀ {y₀ : β},
          y₀ ∈ f x₀ →
            ∀ [(nhds y₀).IsCountablyGenerated],
              ∃ u y,
                Filter.Tendsto u Filter.atTop l ∧
                  (∀ᶠ (k : ℕ) in Filter.atTop, y k ∈ f (x (u k))) ∧ Filter.Tendsto y Filter.atTop (nhds y₀)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKeyD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β},
  Std.ExtDTreeMap.Const.modify t k f ≠ ∅ →
    ∀ {fallback : α},
      (Std.ExtDTreeMap.Const.modify t k f).maxKeyD fallback =
        if cmp (t.maxKeyD fallback) k = Ordering.eq then k else t.maxKeyD fallback
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimits.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.HasLimits C = CategoryTheory.Limits.HasLimitsOfSize.{v, v, v, u} C
-- Batteries.Data.UnionFind.Basic
/-- Size requirement  -/
Batteries.UnionFind.FindAux.size_eq : ∀ {n : ℕ} (self : Batteries.UnionFind.FindAux n), self.s.size = n
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.iInf_natCast_ne_top`. -/
ENat.iInf_coe_ne_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨅ i, ↑(f i) ≠ ⊤ ↔ Nonempty ι
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- Given a short complex `S` of modules, this is the isomorphism between
the abstract `S.homology` of the homology API and the more explicit
quotient of `LinearMap.ker S.g` by the image of
`S.moduleCatToCycles : S.X₁ →ₗ[R] LinearMap.ker S.g`.  -/
CategoryTheory.ShortComplex.moduleCatHomologyIso : {R : Type u} →
  [inst : Ring R] → (S : CategoryTheory.ShortComplex (ModuleCat R)) → S.homology ≅ S.moduleCatLeftHomologyData.H
-- Mathlib.GroupTheory.GroupAction.Primitive
AddAction.IsQuasiPreprimitive.isPretransitive_of_normal : ∀ {G : Type u_1} {X : Type u_2} {inst : AddGroup G} {inst_1 : AddAction G X} [self : AddAction.IsQuasiPreprimitive G X]
  {N : AddSubgroup G} [N.Normal], AddAction.fixedPoints (↥N) X ≠ Set.univ → AddAction.IsPretransitive (↥N) X
-- Mathlib.Data.Fin.Tuple.Basic
Fin.get_find?_eq_find_of_eq_true : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool} (h : p i = true), (Fin.find? p).get ⋯ = Fin.find (fun x => p x = true) ⋯
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- additive version of `MeasureTheory.Measure.haar.clPrehaar`  -/
MeasureTheory.Measure.haar.clAddPrehaar : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] → Set G → TopologicalSpace.OpenNhdsOf 0 → Set (TopologicalSpace.Compacts G → ℝ)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.findExistsOneDivLT_spec : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i →
    MeasureTheory.SignedMeasure.ExistsOneDivLT✝ s i (MeasureTheory.SignedMeasure.findExistsOneDivLT✝ s i)
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
CategoryTheory.LocalizerMorphism.functorialRightResolutions.W₁_ι_app : ∀ {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₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  {ρ : CategoryTheory.Functor C₂ C₁} {i : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor},
  (∀ (X₂ : C₂), W₂ (i.app X₂)) →
    W₁ = W₂.inverseImage Φ.functor →
      ∀ [inst_2 : Φ.functor.Full] [inst_3 : Φ.functor.Faithful] (X₁ : C₁),
        W₁ ((CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι i).app X₁)
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_insert : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {x : α} {s : Set α},
  (insert x s).einfsep = min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.pullbackShiftFunctorAdd'_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) (X : CategoryTheory.PullbackShift C φ)
  (a₁ a₂ a₃ : A) (h : a₁ + a₂ = a₃) (b₁ b₂ b₃ : B) (h₁ : b₁ = φ a₁) (h₂ : b₂ = φ a₂) (h₃ : b₃ = φ a₃),
  (CategoryTheory.shiftFunctorAdd' (CategoryTheory.PullbackShift C φ) a₁ a₂ a₃ h).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ a₃ b₃ h₃).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((CategoryTheory.shiftFunctor C b₁).obj X))
          ((CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a₂).map
            ((CategoryTheory.pullbackShiftIso C φ a₁ b₁ h₁).inv.app X))))
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instAddCommMonoidWithOne : {R : Type u_1} → [AddCommMonoidWithOne R] → AddCommMonoidWithOne (Lex R)
-- Mathlib.Order.FixedPoints
/-- Greatest fixed point of a monotone function  -/
OrderHom.gfp : {α : Type u} → [inst : CompleteLattice α] → (α →o α) →o α
-- Mathlib.Topology.Category.LightProfinite.Basic
lightDiagramToLightProfinite_map : ∀ {X Y : LightDiagram} (f : X ⟶ Y), lightDiagramToLightProfinite.map f = CategoryTheory.InducedCategory.homMk f.hom.hom
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mclosure_preimage_le : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) (s : Set N),
  Submonoid.closure (⇑f ⁻¹' s) ≤ Submonoid.comap f (Submonoid.closure s)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.ext : ∀ {G : Type u_1} {inst : Group G} {x y : FiniteIndexNormalSubgroup G}, x.carrier = y.carrier → x = y
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.support_sum_eq_biUnion : ∀ {α : Type u_16} {ι : Type u_17} {M : Type u_18} [inst : DecidableEq α] [inst_1 : AddCommMonoid M] {g : ι → α →₀ M}
  (s : Finset ι),
  (∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support) →
    (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {toStrictlyUnitaryPseudofunctor : CategoryTheory.StrictlyUnitaryPseudofunctor B C}
  {map_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toStrictlyUnitaryPseudofunctor.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toStrictlyUnitaryPseudofunctor.map f)
            (toStrictlyUnitaryPseudofunctor.map g))
      CategoryTheory.StrictPseudofunctor.map_comp._autoParam}
  {mapComp_eq_eqToIso :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), toStrictlyUnitaryPseudofunctor.mapComp f g = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso._autoParam}
  {toStrictlyUnitaryPseudofunctor_1 : CategoryTheory.StrictlyUnitaryPseudofunctor B C}
  {map_comp_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toStrictlyUnitaryPseudofunctor_1.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toStrictlyUnitaryPseudofunctor_1.map f)
            (toStrictlyUnitaryPseudofunctor_1.map g))
      CategoryTheory.StrictPseudofunctor.map_comp._autoParam}
  {mapComp_eq_eqToIso_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), toStrictlyUnitaryPseudofunctor_1.mapComp f g = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso._autoParam},
  { toStrictlyUnitaryPseudofunctor := toStrictlyUnitaryPseudofunctor, map_comp := map_comp,
        mapComp_eq_eqToIso := mapComp_eq_eqToIso } =
      { toStrictlyUnitaryPseudofunctor := toStrictlyUnitaryPseudofunctor_1, map_comp := map_comp_1,
        mapComp_eq_eqToIso := mapComp_eq_eqToIso_1 } →
    toStrictlyUnitaryPseudofunctor = toStrictlyUnitaryPseudofunctor_1
-- Mathlib.Data.Finset.Sups
Finset.sups_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s : Finset α}, s ⊻ ∅ = ∅
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.discrInfos : Lean.Meta.Match.MkMatcherInput → Array Lean.Meta.Match.DiscrInfo
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.GHSpace.toGHSpace_rep : ∀ (p : GromovHausdorff.GHSpace), GromovHausdorff.toGHSpace p.Rep = p
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.mapId_hom_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition]
  [inst_3 : P.IsMultiplicative] [inst_4 : Q.RespectsIso] (X : T)
  (f : optParam (X ⟶ X) (CategoryTheory.CategoryStruct.id X))
  (hf : autoParam (f = CategoryTheory.CategoryStruct.id X) CategoryTheory.MorphismProperty.Over.mapId._auto_1)
  (X_1 : P.Over Q X),
  ((CategoryTheory.MorphismProperty.Over.mapId Q X f hf).hom.app X_1).left = CategoryTheory.CategoryStruct.id X_1.left
-- Mathlib.Algebra.Order.Round
round_ofNat_add : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (n : ℕ)
  [inst_4 : n.AtLeastTwo] (x : α), round (OfNat.ofNat n + x) = OfNat.ofNat n + round x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonMonoidHom.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : MulOneClass α],
  Finset.singletonMonoidHom = { toFun := Finset.singletonMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.pathComposition_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.Paths C),
  (CategoryTheory.pathComposition C).obj X = X
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- The canonical algebra map from the adic completion to `R ⧸ I ^ n`.

This is `AdicCompletion.eval` postcomposed with the algebra isomorphism
`R ⧸ (I ^ n • ⊤) ≃ₐ[R] R ⧸ I ^ n`.  -/
AdicCompletion.evalₐ : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → (n : ℕ) → AdicCompletion I R →ₐ[R] R ⧸ I ^ n
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_range_succ_sub_top : ∀ {M : Type u_4} (f : ℕ → M) {n : ℕ} [inst : AddCommGroup M],
  ∑ i ∈ Finset.range (n + 1), f i - f n = ∑ i ∈ Finset.range n, f i
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.mem_sup_left : ∀ {M : Type u_2} [inst : Add M] {S T : AddSubsemigroup M} {x : M}, x ∈ S → x ∈ S ⊔ T
-- Mathlib.Order.Heyting.Basic
hnot_le_iff_codisjoint_left : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, ￢b ≤ a ↔ Codisjoint a b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_eq_getLastD_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.maxKeyD fallback = t.keys.getLastD fallback
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.lhom_ext'_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] {N : Type u_7} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R N] [inst_4 : Module R S] {f g : AddMonoidAlgebra S M →ₗ[R] N},
  f = g ↔ ∀ (x : M), f ∘ₗ AddMonoidAlgebra.lsingle x = g ∘ₗ AddMonoidAlgebra.lsingle x
-- Init.Data.List.Lemmas
List.filter_eq_cons_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {a : α} {as : List α},
  List.filter p l = a :: as ↔ ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ x ∈ l₁, ¬p x = true) ∧ p a = true ∧ List.filter p l₂ = as
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.D_two : CartanMatrix.D 2 = !![2, 0; 0, 2]
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.apply_symm_apply' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B} {x : F},
  b ∈ e.baseSet → ↑e (↑e.symm (b, x)) = (b, x)
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.isImmersionAtOfComplement_complement : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x), Manifold.IsImmersionAtOfComplement h.complement I J n f x
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Reinterpret an `IntermediateField` as a `Subalgebra`.  -/
IntermediateField.toSubalgebra : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → IntermediateField K L → Subalgebra K L
-- Mathlib.Order.SuccPred.CompleteLinearOrder
IsLUB.mem_of_nonempty_of_not_isSuccPrelimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {x : α},
  IsLUB s x → s.Nonempty → ¬Order.IsSuccPrelimit x → x ∈ s
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The associator as a natural isomorphism between trifunctors `C ⥤ C ⥤ C ⥤ C`.  -/
CategoryTheory.MonoidalCategory.curriedAssociatorNatIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.bifunctorComp₁₂ (CategoryTheory.MonoidalCategory.curriedTensor C)
          (CategoryTheory.MonoidalCategory.curriedTensor C) ≅
        CategoryTheory.bifunctorComp₂₃ (CategoryTheory.MonoidalCategory.curriedTensor C)
          (CategoryTheory.MonoidalCategory.curriedTensor C)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.coe_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X Y : LeftInvariantDerivation I G), ⇑(X + Y) = ⇑X + ⇑Y
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
instSetLikeHomogeneousSubmodule : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {σA : Type u_3} →
      {σM : Type u_4} →
        {A : Type u_5} →
          {M : Type u_6} →
            [inst : Semiring A] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module A M] →
                  (𝒜 : ιA → σA) →
                    (ℳ : ιM → σM) →
                      [inst_3 : DecidableEq ιA] →
                        [inst_4 : AddMonoid ιA] →
                          [inst_5 : SetLike σA A] →
                            [inst_6 : AddSubmonoidClass σA A] →
                              [inst_7 : GradedRing 𝒜] →
                                [inst_8 : DecidableEq ιM] →
                                  [inst_9 : SetLike σM M] →
                                    [inst_10 : AddSubmonoidClass σM M] →
                                      [inst_11 : DirectSum.Decomposition ℳ] →
                                        [inst_12 : VAdd ιA ιM] →
                                          [inst_13 : SetLike.GradedSMul 𝒜 ℳ] → SetLike (HomogeneousSubmodule 𝒜 ℳ) M