mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Basic
/-- `mkNatTrans` respects vertical composition.  -/
CategoryTheory.Join.mkNatTransComp : ∀ {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 F' F'' : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (αₗ : (CategoryTheory.Join.inclLeft C D).comp F ⟶ (CategoryTheory.Join.inclLeft C D).comp F')
  (αᵣ : (CategoryTheory.Join.inclRight C D).comp F ⟶ (CategoryTheory.Join.inclRight C D).comp F')
  (βₗ : (CategoryTheory.Join.inclLeft C D).comp F' ⟶ (CategoryTheory.Join.inclLeft C D).comp F'')
  (βᵣ : (CategoryTheory.Join.inclRight C D).comp F' ⟶ (CategoryTheory.Join.inclRight C D).comp F'')
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
          ((CategoryTheory.Prod.snd C D).whiskerLeft αᵣ) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).whiskerLeft αₗ)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F'))
      CategoryTheory.Join.mkNatTransComp._auto_1)
  (h' :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F')
          ((CategoryTheory.Prod.snd C D).whiskerLeft βᵣ) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).whiskerLeft βₗ)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F''))
      CategoryTheory.Join.mkNatTransComp._auto_3),
  CategoryTheory.Join.mkNatTrans (CategoryTheory.CategoryStruct.comp αₗ βₗ) (CategoryTheory.CategoryStruct.comp αᵣ βᵣ)
      ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mkNatTrans αₗ αᵣ h)
      (CategoryTheory.Join.mkNatTrans βₗ βᵣ h')
-- Lean.Expr
Lean.Nat.mkInstHMul : Lean.Expr
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.cg_iff_structure_cg : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.Substructure M),
  S.CG ↔ FirstOrder.Language.Structure.CG L ↥S
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.embDomain_single : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ ↪o Γ'} {g : Γ} {r : R}, HahnSeries.embDomain f ((HahnSeries.single g) r) = (HahnSeries.single (f g)) r
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Refl.ne_imp_iff`.

---

If a reflexive relation `r : α → α → Prop` holds over `x y : α`,
then it holds whether or not `x ≠ y`.  -/
reflexive_ne_imp_iff : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {x y : α}, x ≠ y → r x y ↔ r x y
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.count_eq_fold : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] [inst_4 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id]
  {it : Std.Iter β}, it.length = Std.Iter.fold (fun acc x => acc + 1) 0 it
-- Init.Data.Vector.Lemmas
Vector.forall_mem_flatten : ∀ {α : Type u_1} {n m : ℕ} {p : α → Prop} {xss : Vector (Vector α n) m},
  (∀ x ∈ xss.flatten, p x) ↔ ∀ xs ∈ xss, ∀ x ∈ xs, p x
-- Mathlib.Algebra.QuadraticDiscriminant
discrim_le_zero_of_nonpos : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a b c : K},
  (∀ (x : K), a * (x * x) + b * x + c ≤ 0) → discrim a b c ≤ 0
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.SimpTheorems.foldSimpEntriesM.processTheorem : {m : Type u_1 → Type u_2} →
  {σ : Type u_1} →
    [Monad m] → (σ → Lean.Meta.SimpEntry → m σ) → Lean.Meta.SimpTheorems → σ → Lean.Meta.SimpTheorem → m σ
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instOfIsClosedImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f], AlgebraicGeometry.IsFinite f
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.instLinearEquivClass : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂}, LinearEquivClass (B₁.IsometryEquiv B₂) R M₁ M₂
-- Mathlib.Algebra.Module.Bimodule
/-- If `A` and `B` are also `Algebra`s over yet another set of scalars `S` then we may "base change"
from `R` to `S`.  -/
Subbimodule.baseChange : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {M : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : Semiring A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Module A M] →
                    [inst_6 : Module B M] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] →
                          [inst_9 : IsScalarTower R A M] →
                            [inst_10 : IsScalarTower R B M] →
                              [inst_11 : SMulCommClass A B M] →
                                (S : Type u_5) →
                                  [inst_12 : CommSemiring S] →
                                    [inst_13 : Module S M] →
                                      [inst_14 : Algebra S A] →
                                        [inst_15 : Algebra S B] →
                                          [inst_16 : IsScalarTower S A M] →
                                            [inst_17 : IsScalarTower S B M] →
                                              Submodule (TensorProduct R A B) M → Submodule (TensorProduct S A B) M
-- Lean.Parser.Types
Lean.Parser.ParserContextCore.toParserModuleContext : Lean.Parser.ParserContextCore → Lean.Parser.ParserModuleContext
-- Mathlib.Algebra.Polynomial.RingDivision
_private.Mathlib.Algebra.Polynomial.RingDivision.0.Polynomial.rootMultiplicity_comp_C_mul_X_add_C_le : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R) (a b c : R),
  IsUnit a →
    Polynomial.rootMultiplicity c (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)) ≤
      Polynomial.rootMultiplicity (a * c + b) p
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measure_preimage_mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulRightInvariant] (g : G) (A : Set G), μ ((fun h => h * g) ⁻¹' A) = μ A
-- Mathlib.NumberTheory.LSeries.SumCoeff
_private.Mathlib.NumberTheory.LSeries.SumCoeff.0.LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ : ∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => (∑ k ∈ Finset.Icc 1 n, f k) / ↑n) Filter.atTop (nhds l) →
    (∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s) →
      ∀ {ε : ℝ},
        ε > 0 →
          ∃ C ≥ 0,
            (fun s => ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖) ≤ᶠ[nhdsWithin 1 (Set.Ioi 1)] fun s => (s - 1) * s * C + s * ε
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.instInhabited : {X : Type u_3} → [Inhabited X] → Inhabited (FundamentalGroupoid X)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.leftUnitor_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor G).hom.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).hom
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- By forgetting the inverse to `mapComp`, a `StrictlyUnitaryPseudofunctor`
is a `StrictlyUnitaryLaxFunctor`.  -/
CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictlyUnitaryPseudofunctor B C → CategoryTheory.StrictlyUnitaryLaxFunctor B C
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.Hom.hom_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X],
  CategoryTheory.InducedCategory.Hom.hom 1 = 1
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The pushout-product is commutative: `X₁ □ X₂ ≅ X₂ □ X₁`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.braiding : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        [CategoryTheory.BraidedCategory C] → (X₁ X₂ : CategoryTheory.Arrow C) → (X₁ □ X₂) ≅ X₂ □ X₁
-- Mathlib.Topology.CantorBendixson
/-- The transfinite iteration of the relative derived-set operator on a set.  -/
CantorBendixson.iteratedDerivedSet : {X : Type u} → [TopologicalSpace X] → Set X → Ordinal.{u} → Set X
-- Mathlib.Order.Preorder.Chain
Set.Subsingleton.isChain : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, s.Subsingleton → IsChain r s
-- Mathlib.Logic.Equiv.Multiset
_private.Mathlib.Logic.Equiv.Multiset.0.Denumerable.lower.match_1.eq_2 : ∀ (motive : List ℕ → ℕ → Sort u_1) (m : ℕ) (l : List ℕ) (n : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (m : ℕ) → (l : List ℕ) → (n : ℕ) → motive (m :: l) n),
  (match m :: l, n with
    | [], x => h_1 x
    | m :: l, n => h_2 m l n) =
    h_2 m l n
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_mul_of_le_two`. -/
Ordinal.principal_mul_of_le_two : ∀ {o : Ordinal.{u}}, o ≤ 2 → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o
-- Init.Internal.Order.Basic
Lean.Order.iterates.below.sup : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {f : α → α} {motive : (a : α) → Lean.Order.iterates f a → Prop} {c : α → Prop}
  (hc : Lean.Order.chain c) (hi : ∀ (x : α), c x → Lean.Order.iterates f x),
  (∀ (x : α) (a : c x), Lean.Order.iterates.below ⋯) → (∀ (x : α) (a : c x), motive x ⋯) → Lean.Order.iterates.below ⋯
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.GammaIntegral_ofReal : ∀ (s : ℝ), (↑s).GammaIntegral = ↑(∫ (x : ℝ) in Set.Ioi 0, Real.exp (-x) * x ^ (s - 1))
-- Init.Data.String.Lemmas.Iterate
String.forIn_eq_forIn_toList : ∀ {β : Type u} {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {s : String} {b : β}
  {f : Char → β → m (ForInStep β)}, forIn s b f = forIn s.toList b f
-- Mathlib.Analysis.Meromorphic.Order
/-- If a function is meromorphic on a set `U`, then for each point in `U`, it is analytic at nearby
points in `U`. When the target space is complete, this can be strengthened to analyticity at all
nearby points, see `MeromorphicAt.eventually_analyticAt`.  -/
MeromorphicOn.eventually_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜},
  MeromorphicOn f U → x ∈ U → ∀ᶠ (y : 𝕜) in nhdsWithin x (U \ {x}), AnalyticAt 𝕜 f y
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.universal_property' : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsStronglyCocartesian f φ]
  {b' : 𝒳} (g : S ⟶ p.obj b') (φ' : a ⟶ b') [p.IsHomLift (CategoryTheory.CategoryStruct.comp f g) φ'],
  ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ'
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan_inj : ∀ {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 C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D) (j : J),
  CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
      (e.hom.app (Y j))
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ} (α : F ≅ G),
  CategoryTheory.NatIso.unop (CategoryTheory.Functor.isoWhiskerRight α H) =
    G.unopComp H ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.NatIso.unop α) H.unop ≪≫ (F.unopComp H).symm
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ x : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ →
    ∀ {s t : Set Ω}, MeasurableSet s → MeasurableSet t → ProbabilityTheory.Kernel.IndepSet s t κ μ
-- Mathlib.Order.Category.OmegaCompletePartialOrder
/-- A construction of the equalizer fork.  -/
ωCPO.HasEqualizers.equalizer : {X Y : ωCPO} → (f g : X ⟶ Y) → CategoryTheory.Limits.Fork f g
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.ExactAt.of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {i : ι},
  K.ExactAt i → ∀ {L : HomologicalComplex C c} (e : K ≅ L), L.ExactAt i
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.coe_mul : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (x y : ↑(Set.Ioc 0 1)),
  ↑(x * y) = ↑x * ↑y
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.tsum_mul_right : ∀ {α : Type u_2} {L : SummationFilter α} (f : α → NNReal) (a : NNReal),
  ∑'[L] (x : α), f x * a = (∑'[L] (x : α), f x) * a
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A function which can be uniformly approximated by continuous functions is continuous.  -/
continuous_of_uniform_approx_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : α → β},
  (∀ u ∈ uniformity β, ∃ F, Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u) → Continuous f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_hom_app : ∀ (X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair),
  CategoryTheory.Limits.walkingCospanOpEquiv.counitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_eq_singleton_iff_isTop : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α}, Set.Ici x = {x} ↔ IsTop x
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.mem_inv : ∀ {G : Type u_2} [inst : Group G] {g : G} {S : Submonoid G}, g ∈ S⁻¹ ↔ g⁻¹ ∈ S
-- Mathlib.Algebra.Field.MinimalAxioms
/-- Define a `Field` structure on a Type by proving a minimal set of axioms.
Note that this uses the default definitions for `npow`, `nsmul`, `zsmul`, `div` and `sub`.
See note [reducible non-instances].  -/
Field.ofMinimalAxioms : (K : Type u) →
  [inst : Add K] →
    [inst_1 : Mul K] →
      [inst_2 : Neg K] →
        [inst_3 : Inv K] →
          [inst_4 : Zero K] →
            [inst_5 : One K] →
              (∀ (a b c : K), a + b + c = a + (b + c)) →
                (∀ (a : K), 0 + a = a) →
                  (∀ (a : K), -a + a = 0) →
                    (∀ (a b c : K), a * b * c = a * (b * c)) →
                      (∀ (a b : K), a * b = b * a) →
                        (∀ (a : K), 1 * a = a) →
                          (∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) →
                            0⁻¹ = 0 → (∀ (a b c : K), a * (b + c) = a * b + a * c) → (∃ x y, x ≠ y) → Field K
-- Mathlib.Logic.Function.DependsOn
dependsOn_univ : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (f : ((i : ι) → α i) → β), DependsOn f Set.univ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.ext_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f g : S.LocalizationMap N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasLimit_inverse_equivalence_comp_iff : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (e : J ≌ K),
  CategoryTheory.Limits.HasLimit (e.inverse.comp F) ↔ CategoryTheory.Limits.HasLimit F
-- Std.Internal.Do.Order.PreservesSup
/-- Counit (modus ponens), from join preservation: `f (upperAdjoint f b) ⊑ b`.  -/
Lean.Order.PreservesSup.upperAdjoint_le : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (f : α → α) [Lean.Order.PreservesSup f] (b : α),
  Lean.Order.PartialOrder.rel (f (Lean.Order.PreservesSup.upperAdjoint f b)) b
-- Init.Data.Slice.Array.Lemmas
Array.size_mkSlice_rii : ∀ {α : Type u_1} {xs : Array α}, Std.Slice.size (Std.Rii.Sliceable.mkSlice xs *...*) = xs.size
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
map_div₀ : ∀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero G₀']
  [inst_2 : FunLike F G₀ G₀'] [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a b : G₀), f (a / b) = f a / f b
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.rfl : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, G.Reachable u u
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- To construct an isomorphism between forks,
it suffices to give an isomorphism between the cone points
and check that it commutes with the `ι` morphisms.
 -/
CategoryTheory.Limits.Fork.ext : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {s t : CategoryTheory.Limits.Fork f g} →
          (i : s.pt ≅ t.pt) →
            autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) CategoryTheory.Limits.Fork.ext._auto_1 →
              (s ≅ t)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- This is the counit of the tilde-Gamma adjunction.  -/
AlgebraicGeometry.Scheme.Modules.fromTildeΓ : {R : CommRingCat} →
  (M : (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Modules) →
    AlgebraicGeometry.tilde ((AlgebraicGeometry.modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)) ⟶ M
-- Mathlib.GroupTheory.SpecificGroups.Alternating
Equiv.Perm.finRotate_bit1_mem_alternatingGroup : ∀ {n : ℕ}, finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1))
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_neg_add_nhds_zero : ∀ (Gₗ : Type u_2) [inst : UniformSpace Gₗ] [inst_1 : AddGroup Gₗ] [IsLeftUniformAddGroup Gₗ],
  uniformity Gₗ = Filter.comap (fun x => -x.1 + x.2) (nhds 0)
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.orthogonalProjection_apply_mem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p x : P},
  x ∈ s → ↑((EuclideanGeometry.orthogonalProjection s) p) = ↑(s.direction.orthogonalProjectionOnto (p -ᵥ x)) +ᵥ x
-- Mathlib.Algebra.Order.Group.Abs
min_mabs_mabs_le_mabs_max : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] {a b : G}, min |a|ₘ |b|ₘ ≤ |max a b|ₘ
-- Init.MetaTypes
Lean.Meta.LiftLetsConfig.mk.injEq : ∀ (toExtractLetsConfig toExtractLetsConfig_1 : Lean.Meta.ExtractLetsConfig),
  ({ toExtractLetsConfig := toExtractLetsConfig } = { toExtractLetsConfig := toExtractLetsConfig_1 }) =
    (toExtractLetsConfig = toExtractLetsConfig_1)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
map_mabs : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {β : Type u_2} {F : Type u_3} [inst_2 : Group β]
  [inst_3 : LinearOrder β] [inst_4 : FunLike F α β] [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) (a : α),
  f |a|ₘ = |f a|ₘ
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.continuous_coe : ∀ (α : Type u_1) [inst : UniformSpace α], Continuous UniformSpace.Completion.coe'
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
RealRMK.rieszMeasure.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (Λ Λ_1 : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ),
  Λ = Λ_1 → ∀ [inst_4 : LocallyCompactSpace X], RealRMK.rieszMeasure Λ = RealRMK.rieszMeasure Λ_1
-- Mathlib.Data.Finset.Image
/-- **Alias** of the forward direction of `Finset.surjOn_iff_subset_image`. -/
Set.SurjOn.subset_finsetImage : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  Set.SurjOn f ↑s ↑t → t ⊆ Finset.image f s
-- Mathlib.Algebra.Lie.BaseChange
_private.Mathlib.Algebra.Lie.BaseChange.0.LieAlgebra.ExtendScalars.bracket'.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M],
  LieAlgebra.ExtendScalars.bracket'✝ R A L M = LieAlgebra.ExtendScalars.bracket'✝ R A L M
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.mul : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {z : M} {F' : Type u_21} [inst_6 : NormedRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'}, MDiffAt p z → MDiffAt q z → MDiffAt (p * q) z
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.lift_lift_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddMonObj B] (f g h : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
          CategoryTheory.AddMonObj.add)
        h)
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h)
          CategoryTheory.AddMonObj.add))
      CategoryTheory.AddMonObj.add
-- Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
_private.Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ.0.WeierstrassCurve.exists_variableChange_of_char_three_of_j_eq_zero : ∀ {F : Type u_1} [inst : Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [E.IsElliptic] [E'.IsElliptic] [CharP F 3]
  [E.IsShortNF] [E'.IsShortNF], ∃ C, C • E = E'
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_tprod_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] (f : ι → M),
  ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.coe_refl : ∀ {M : Type u_4} [inst : Mul M], ⇑(MulEquiv.refl M) = id
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.sub_congr : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Sub α] [Lean.Grind.ToInt.Sub α i]
  {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a - b) = i.wrap (a' - b')