mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] (d : D) {Z : D'}
  (h : F.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxLeftLinear.μₗ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d)
      (CategoryTheory.CategoryStruct.comp
        (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom) h)
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
/-- Polar form of trivial-square-zero extension.  -/
TrivSqZeroExt.eq_smul_exp_of_invertible : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [Algebra ℚ R] [Module ℚ M]
  [inst_4 : Module R M] [inst_5 : Module Rᵐᵒᵖ M] [inst_6 : IsCentralScalar R M] [inst_7 : TopologicalSpace R]
  [inst_8 : TopologicalSpace M] [inst_9 : IsTopologicalRing R] [inst_10 : IsTopologicalAddGroup M]
  [inst_11 : ContinuousSMul R M] [inst_12 : ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M)
  [inst_15 : Invertible x.fst], x = x.fst • NormedSpace.exp (⅟x.fst • TrivSqZeroExt.inr x.snd)
-- Mathlib.Algebra.Ring.Center
Set.add_mem_center : ∀ {M : Type u_1} [inst : Distrib M] {a b : M}, a ∈ Set.center M → b ∈ Set.center M → a + b ∈ Set.center M
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_univ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : ℕ}, iteratedFDerivWithin 𝕜 n f Set.univ = iteratedFDeriv 𝕜 n f
-- Init.Data.List.Lemmas
List.head?_eq_some_head : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.head? = some (l.head h)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_op : ∀ {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₂),
  Φ.HasLeftResolutions ↔ Φ.op.HasRightResolutions
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂).get? k = t₁.get? k
-- Std.Time.Date.Unit.Year
Std.Time.Year.instDecidableEqOffset : DecidableEq Std.Time.Year.Offset
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)),
  (CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence F sq sq₃).inverse =
    CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor F sq sq₃
-- Mathlib.Algebra.Notation.Indicator
Set.support_indicator_subset : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M}, Function.support (s.indicator f) ⊆ s
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.CoverByImageStructure.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {G : CategoryTheory.Functor C D} →
          {V U : D} → {f : V ⟶ U} → CategoryTheory.Presieve.CoverByImageStructure G f → C
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `declName` is the name of a `match` equation or a `match` congruence equation.
 -/
Lean.Meta.Grind.isMatchEqLikeDeclName : Lean.Name → Lean.CoreM Bool
-- Mathlib.Analysis.InnerProductSpace.MulOpposite
OrthonormalBasis.toBasis_mulOpposite : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {ι : Type u_3} {H : Type u_4} [inst_1 : NormedAddCommGroup H]
  [inst_2 : InnerProductSpace 𝕜 H] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 H),
  b.mulOpposite.toBasis = b.toBasis.mulOpposite
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.le_iff' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ : MeasureTheory.Measure α}, μ₁ ≤ μ₂ ↔ ∀ (s : Set α), μ₁ s ≤ μ₂ s
-- Mathlib.Algebra.Order.Kleene
IdemSemiring.toSemiring : {α : Type u_5} → [self : IdemSemiring α] → Semiring α
-- Init.Data.UInt.Basic
instModUInt16 : Mod UInt16
-- Mathlib.Analysis.Complex.Circle
Circle.exp_neg : ∀ (x : ℝ), Circle.exp (-x) = (Circle.exp x)⁻¹
-- Mathlib.Computability.NFA
Language.IsRegular.of_reverse : ∀ {α : Type u} {L : Language α}, L.reverse.IsRegular → L.IsRegular
-- Mathlib.Algebra.CharP.Basic
CharZero.charZero_iff_forall_prime_ne_zero : ∀ (R : Type u_1) [inst : NonAssocRing R] [NoZeroDivisors R] [Nontrivial R], CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.instMonoHomologyι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology], CategoryTheory.Mono S.homologyι
-- Init.Core
ForInStep.yield.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : α), sizeOf (ForInStep.yield a) = 1 + sizeOf a
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
DifferentiableWithinAt.comp_mdifferentiableWithinAt : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {g : F → F'}
  {f : M → F} {s : Set M} {t : Set F} {x : M},
  DifferentiableWithinAt 𝕜 g t (f x) → MDiffAt[s] f x → Set.MapsTo f s t → MDiffAt[s] (g ∘ f) x
-- Mathlib.Topology.MetricSpace.DilationEquiv
IsometryEquiv.coe_symm_toDilationEquiv : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵢ Y),
  ⇑e.toDilationEquiv.symm = ⇑e.symm
-- Aesop.Stats.Basic
Aesop.instInhabitedStats.default : Aesop.Stats
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.proof : Lean.Meta.SimpAll.Entry → Lean.Expr
-- Mathlib.Algebra.Order.Interval.Basic
Interval.mul_eq_one_iff : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α] {s t : Interval α},
  s * t = 1 ↔ ∃ a b, s = Interval.pure a ∧ t = Interval.pure b ∧ a * b = 1
-- Mathlib.ModelTheory.LanguageMap
/-- A language equivalence maps the symbols of one language to symbols of another bijectively.  -/
FirstOrder.Language.«term_≃ᴸ_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.leftComm_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (m : M) (n : N) (p : P),
  (TensorProduct.leftComm R M N P) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) = n ⊗ₜ[R] (m ⊗ₜ[R] p)
-- Lean.MonadEnv
Lean.isInductiveCore : Lean.Environment → Lean.Name → Bool
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_eq_one_iff_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν]
  [MeasureTheory.SigmaFinite ν], μ.AbsolutelyContinuous ν → (μ.rnDeriv ν =ᵐ[ν] 1 ↔ μ = ν)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- Lift an unbundled finitely generated module to `FGModuleCat R`.  -/
FGModuleCat.of : (R : Type u) →
  [inst : Ring R] →
    (V : Type v) → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → [Module.Finite R V] → FGModuleCat R
-- Mathlib.Analysis.Convex.Integral
ConvexOn.average_mem_epigraph : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  [NeZero μ],
  ConvexOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        (∀ᵐ (x : α) ∂μ, f x ∈ s) →
          MeasureTheory.Integrable f μ →
            MeasureTheory.Integrable (g ∘ f) μ →
              (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_add_const_Ioi : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x + a) ⁻¹' Set.Ioi b = Set.Ioi (b - a)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
SpectrumRestricts.rightInvOn : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a : A} {f : S → R},
  SpectrumRestricts a f → Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Two vector spaces are isomorphic if and only if they have the same dimension.  -/
Module.nonempty_linearEquiv_iff_lift_rank_eq : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Free R M'] [StrongRankCondition R],
  Nonempty (M ≃ₗ[R] M') ↔ Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.step_filterMapWithPostcondition : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n (Option β')} [inst_1 : Monad n] [LawfulMonad n] [inst_3 : MonadLiftT m n],
  (Std.IterM.filterMapWithPostcondition f it).step = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← (f out).operation
        match __do_lift with
          | ⟨none, h'⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterMapWithPostcondition f it') ⋯))
          | ⟨some out', h'⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.filterMapWithPostcondition f it') out' ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterMapWithPostcondition f it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrpFunctor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] {X Y : C ⥤ₗ D}
  (α : X ⟶ Y), CategoryTheory.Functor.mapCommGrpFunctor.map α = CategoryTheory.Functor.mapCommGrpNatTrans α.hom
-- Mathlib.FieldTheory.FinTrdeg
FinTrdeg.trans : ∀ (K : Type u_3) (E : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field E] [inst_2 : Field L]
  [inst_3 : Algebra K E] [inst_4 : Algebra K L] [inst_5 : Algebra E L] [IsScalarTower K E L] [FinTrdeg K E]
  [FinTrdeg E L], FinTrdeg K L
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) {Z_1 : C} (h : T.left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).inv.app T))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst T.hom g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst T.hom g) h
-- Mathlib.Algebra.Group.Pi.Units
AddEquiv.val_piAddUnits_symm_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] (f : (i : ι) → AddUnits (M i)) (x : ι),
  ↑(AddEquiv.piAddUnits.symm f) x = ↑(f x)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f],
  CategoryTheory.IsIso (CategoryTheory.inv f)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.norm_compAlongOrderedFinpartition_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n)
  (f : F [×c.length]→L[𝕜] G) (p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F),
  ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i, ‖p i‖
-- Mathlib.Order.GaloisConnection.Basic
isLUB_image2_of_isLUB_isLUB : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {s : Set α}
  {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β},
  (∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
    (∀ (a : α), GaloisConnection (l a) (u₂ a)) → IsLUB s a₀ → IsLUB t b₀ → IsLUB (Set.image2 l s t) (l a₀ b₀)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_two_pow_sub_succ : ∀ {x n : ℕ}, x < 2 ^ n → ∀ (i : ℕ), (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
-- Mathlib.Algebra.BigOperators.Pi
/-- The canonical isomorphism between the additive monoid of homomorphisms from
a finite product of additive commutative monoids to another additive commutative monoid and
the product of the homomorphism monoids.  -/
Pi.addMonoidHomAddEquiv : {ι : Type u_7} →
  [Fintype ι] →
    [DecidableEq ι] →
      (M : ι → Type u_8) →
        [inst : (i : ι) → AddCommMonoid (M i)] →
          (M' : Type u_9) → [inst_1 : AddCommMonoid M'] → (((i : ι) → M i) →+ M') ≃+ ((i : ι) → M i →+ M')
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `(fixedBy α g)ᶜ ⊆ s`, then `g` cannot move a point of `s` outside of `s`.  -/
MulAction.set_mem_fixedBy_of_movedBy_subset : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {s : Set α} {g : G},
  (MulAction.fixedBy α g)ᶜ ⊆ s → s ∈ MulAction.fixedBy (Set α) g
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Algebra.Order.Group.Synonym
toColex_inv : ∀ {α : Type u_1} [inst : Inv α] (a : α), toColex a⁻¹ = (toColex a)⁻¹
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
IntermediateField.isAlgebraic_adjoin_iff_top : ∀ {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Ring S] [inst_4 : Algebra E S],
  Algebra.IsAlgebraic (↥(IntermediateField.adjoin F s)) S ↔ Algebra.IsAlgebraic (↥(Algebra.adjoin F s)) S
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_right_mono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] {a : α}, Monotone fun x => a * x
-- Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
CategoryTheory.MorphismProperty.monotone_ofObjectProperty_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  {Q Q' : CategoryTheory.ObjectProperty C},
  Q ≤ Q' → CategoryTheory.MorphismProperty.ofObjectProperty P Q ≤ CategoryTheory.MorphismProperty.ofObjectProperty P Q'
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.IterM.drop.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} (n : ℕ) (it : Std.IterM m β),
  Std.IterM.drop n it = { internalState := { remaining := n, inner := it } }
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.natLit : Lean.Option Bool
-- Lean.Elab.Tactic.Try
/-- Core implementation of `try?`: focus, collect info, build tactic, evaluate and suggest.
`tk` is the syntax token where "Try this:" appears. The optional `footer` is appended to the
suggestions message (only when `wrapWithBy := true`).

Public so that the `autoTry` linter (`Lean.Elab.Tactic.AutoTry`) can drive `try?` from outside
the normal `try?` syntax entry point.  -/
Lean.Elab.Tactic.Try.elabTryCore : Lean.Syntax → Lean.Try.Config → optParam Lean.MessageData Lean.MessageData.nil → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Data.ENNReal.Inv
ENNReal.sSup_mul : ∀ {s : Set ENNReal} {a : ENNReal}, sSup s * a = ⨆ b ∈ s, b * a
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Coalgebra.Repr.mul_left : ∀ {R : Type u_1} {A : Type u_2} {ι : Type u_4} {κ : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] {a b : A} (ℛ₁ : Coalgebra.Repr R a ι) (ℛ₂ : Coalgebra.Repr R b κ) (a_1 : ι × κ),
  (ℛ₁.mul ℛ₂).left a_1 = ℛ₁.left a_1.1 * ℛ₂.left a_1.2
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A copy of `⊤` gives rise to an embedding of `⊤`.  -/
SimpleGraph.Copy.topEmbedding : {V : Type u_1} → {α : Type u_4} → {G : SimpleGraph V} → ⊤.Copy G → ⊤ ↪g G
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_iSup₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → UpperSet α),
  ↑(⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
-- Mathlib.GroupTheory.QuotientGroup.Basic
Quotient.liftOn₂'.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} (q₁ q₁_1 : Quotient s₁),
  q₁ = q₁_1 →
    ∀ (q₂ q₂_1 : Quotient s₂),
      q₂ = q₂_1 →
        ∀ (f f_1 : α → β → γ) (e_f : f = f_1)
          (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), s₁ a₁ b₁ → s₂ a₂ b₂ → f a₁ a₂ = f b₁ b₂),
          q₁.liftOn₂' q₂ f h = q₁_1.liftOn₂' q₂_1 f_1 ⋯
-- Init.Data.Vector.Perm
Vector.perm_mk : ∀ {α : Type u_1} {n : ℕ} (as bs : Array α) (ha : as.size = n) (hb : bs.size = n),
  (Vector.mk as ha).Perm (Vector.mk bs hb) ↔ as.Perm bs
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t_fst_fst_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X j ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
          (𝒰.f i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j))
      h
-- Lean.Data.Lsp.Internal
/-- Range of this parent decl.  -/
Lean.Lsp.DeclInfo.range : Lean.Lsp.DeclInfo → Lean.Lsp.Range
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotate_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.rotate C).obj T = T.rotate
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_apply : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal) (x : v.Completion),
  ↑((NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv) x) =
    (NumberField.InfinitePlace.Completion.extensionEmbedding v) x
-- Init.Data.List.Basic
List.instLawfulBEq : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α], LawfulBEq (List α)
-- Aesop.Forward.Match.Types
/-- An entry in the forward state queues. Represents a complete match.  -/
Aesop.ForwardRuleMatch : Type
-- Mathlib.Analysis.InnerProductSpace.Projection.Minimal
/-- Characterization of minimizers for the projection on a convex set in a real inner product
space.  -/
norm_eq_iInf_iff_real_inner_le_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {K : Set F},
  Convex ℝ K → ∀ {u v : F}, v ∈ K → (‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, inner ℝ (u - v) (w - v) ≤ 0)
-- Mathlib.FieldTheory.CardinalEmb
IntermediateField.equivOfEq.congr_simp : ∀ {F : Type u_4} [inst : Field F] {E : Type u_5} [inst_1 : Field E] [inst_2 : Algebra F E] {S T : IntermediateField F E}
  (h : S = T), IntermediateField.equivOfEq h = IntermediateField.equivOfEq h
-- Mathlib.Order.Category.Frm
Frm.ofHom_id : ∀ {X : Type u} [inst : Order.Frame X],
  Frm.ofHom (FrameHom.id X) = CategoryTheory.CategoryStruct.id { carrier := X, str := inst }
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseAction : Std.Internal.Parsec.ByteArray.Parser Std.Tactic.BVDecide.LRAT.IntAction
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.congr_mono : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s s₁ : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → Set.EqOn f₁ f s₁ → s₁ ⊆ s → f₁ x = f x → ContDiffWithinAt 𝕜 n f₁ s₁ x
-- Mathlib.CategoryTheory.Elements
/-- The equivalence `(-.Elements)ᵒᵖ ≅ (yoneda, -)` of is actually a natural isomorphism of functors.
 -/
CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ (Type v)} (α : F₁ ⟶ F₂),
  (CategoryTheory.CategoryOfElements.map α).op.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F₂) =
    (CategoryTheory.CategoryOfElements.toCostructuredArrow F₁).comp (CategoryTheory.CostructuredArrow.map α)
-- Init.Data.UInt.Lemmas
USize.toBitVec_ofNatTruncate_of_le : ∀ {n : ℕ}, USize.size ≤ n → (USize.ofNatClamp n).toBitVec = (USize.size - 1)#'USize.toBitVec_ofNatClamp_of_le._proof_1
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.rotateL.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → Sort u_2) (l : Ordnode α) (x : α) (size : ℕ) (m : Ordnode α)
  (y : α) (r : Ordnode α)
  (h_1 :
    (l : Ordnode α) →
      (x : α) → (size : ℕ) → (m : Ordnode α) → (y : α) → (r : Ordnode α) → motive l x (Ordnode.node size m y r))
  (h_2 : (l : Ordnode α) → (x : α) → motive l x Ordnode.nil),
  (match l, x, Ordnode.node size m y r with
    | l, x, Ordnode.node size m y r => h_1 l x size m y r
    | l, x, Ordnode.nil => h_2 l x) =
    h_1 l x size m y r