mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Cycle
/-- Auxiliary decidability algorithm for lists that contain at least two unique elements.
 -/
Cycle.decidableNontrivialCoe : {α : Type u_1} → [DecidableEq α] → (l : List α) → Decidable (↑l).Nontrivial
-- Mathlib.Data.List.Perm.Lattice
List.Perm.bagInter_right : ∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ : List α} (t : List α), l₁.Perm l₂ → (l₁.bagInter t).Perm (l₂.bagInter t)
-- Lean.Parser.Basic
/-- Recover from errors in `p` using `recover` to consume input until a known-good state has appeared.
If `recover` fails itself, then no recovery is performed.

`recover` is provided with information about the failing parser's effects , and it is run in the
state immediately after the failure.
 -/
Lean.Parser.recoverFn : Lean.Parser.ParserFn → (Lean.Parser.RecoveryContext → Lean.Parser.ParserFn) → Lean.Parser.ParserFn
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.mem_asIdeal : ∀ {R : Type u_1} [inst : Ring R] {I : TwoSidedIdeal R} {x : R}, x ∈ TwoSidedIdeal.asIdeal I ↔ x ∈ I
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_ne_zero : ∀ {G : Type u} [inst : Monoid G], Monoid.exponent G ≠ 0 ↔ Monoid.ExponentExists G
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.mulRight_symm : ∀ {G : Type u_5} [inst : Group G] (a : G), Equiv.symm (Equiv.mulRight a) = Equiv.mulRight a⁻¹
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.ofField_eq : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [inst_1 : Field K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K],
  Localization.subalgebra.ofField K S hS = Localization.subalgebra K S hS
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.not_le_norm : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsLinearOrder α] [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.core_cert rhs lhs p = true →
    ¬Lean.Grind.CommRing.Expr.denote ctx lhs ≤ Lean.Grind.CommRing.Expr.denote ctx rhs →
      Lean.Grind.CommRing.Poly.denote ctx p < 0
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.Discrete.essentiallySmallOfSmall : ∀ {α : Type u} [Small.{w, u} α], CategoryTheory.EssentiallySmall.{w, u, u} (CategoryTheory.Discrete α)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.toMulHom : {R : Type u_5} →
  {S : Type u_6} → [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → AbsoluteValue R S → R →ₙ* S
-- Mathlib.Order.PropInstances
sup_Prop_eq : (fun x1 x2 => max x1 x2) = fun x1 x2 => x1 ∨ x2
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.sndKernelFork_ι : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.biprod.sndKernelFork X Y) = CategoryTheory.Limits.biprod.inl
-- Batteries.Data.List.Basic
/-- `inits l` is the list of initial segments of `l`.
```
inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]
```
 -/
List.inits : {α : Type u_1} → List α → List (List α)
-- Mathlib.NumberTheory.NumberField.Norm
RingOfIntegers.coe_norm : ∀ {L : Type u_1} (K : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (x : NumberField.RingOfIntegers L), ↑((RingOfIntegers.norm K) x) = (Algebra.norm K) ↑x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_getD : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {a : α} {fallback : β},
      m.contains a = true →
        Std.DHashMap.Internal.Raw₀.Const.get? m a = some (Std.DHashMap.Internal.Raw₀.Const.getD m a fallback)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- **Alias** of `SimpleGraph.Walk.support_takeUntil_subset_support`. -/
SimpleGraph.Walk.support_takeUntil_subset : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).support ⊆ p.support
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.le.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (val : α)
  (h_1 : (val : β) → motive none (some val)) (h_2 : Unit → motive none none) (h_3 : (val : α) → motive (some val) none)
  (h_4 : (x : α) → (y : β) → motive (some x) (some y)),
  (match some val, none with
    | none, some val => h_1 val
    | none, none => h_2 ()
    | some val, none => h_3 val
    | some x, some y => h_4 x y) =
    h_3 val
-- Mathlib.Order.Interval.Finset.Basic
Finset.sup_Iic_of_monotone : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {β : Type u_3}
  [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β] {f : α → β}, Monotone f → (Finset.Iic a).sup f = f a
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flatMapAfterM.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₁', h⟩ with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => h_1 it₁' b h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it₁' h
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsCircuit.not_isColoop_of_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α}, M.IsCircuit C → e ∈ C → ¬M.IsColoop e
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Instantiate the reals as a pseudometric space.  -/
Real.pseudoMetricSpace : PseudoMetricSpace ℝ
-- Mathlib.Order.FixedPoints
OrderHom.map_gfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), f (OrderHom.gfp f) = OrderHom.gfp f
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.commute_ofSubtype_noncommPiCoprod : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α)
  (u : Equiv.Perm ↑(Function.fixedPoints ⇑f)) (v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)),
  Commute (Equiv.Perm.ofSubtype u) ((Subgroup.noncommPiCoprod ⋯) v)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symm_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃ N)
  (h : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y),
  { toEquiv := f, map_mul' := h }.symm = { toEquiv := f.symm, map_mul' := ⋯ }
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.eq_trans₃ : ∀ {α : Type u_1} {a a' b b' : α}, a = b → a = a' → b = b' → a' = b'
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.add.match_1.eq_3 : ∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)}
  (motive : Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M → Sort u_1) (a₁ : Q(«$R»)) (x₁ : Q(«$M»))
  (k₁ : ℕ) (t₁ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) (a₂ : Q(«$R»)) (x₂ : Q(«$M»)) (k₂ : ℕ)
  (t₂ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) (h_1 : (l : Mathlib.Tactic.Module.qNF R M) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.Module.qNF R M) → motive l [])
  (h_3 :
    (a₁ : Q(«$R»)) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
            (a₂ : Q(«$R»)) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) →
                  (t₂ : Mathlib.Tactic.Module.NF (Q(«$R») × Q(«$M»)) ℕ) →
                    motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (match ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ with
    | [], l => h_1 l
    | l, [] => h_2 l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
    h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.of_div_left : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, (s / t).Nonempty → s.Nonempty
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.instPreregularSmallModel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.EssentiallySmall.{u_3, v_1, u_1} C],
  CategoryTheory.Preregular (CategoryTheory.SmallModel.{u_3, v_1, u_1} C)
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.instInhabited : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → Inhabited (CategoryTheory.Functor C C)
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.testBit.match_1.splitter : (motive : PosNum → ℕ → Sort u_1) →
  (x : PosNum) →
    (x_1 : ℕ) →
      (Unit → motive PosNum.one 0) →
        ((x : ℕ) → (x = 0 → False) → motive PosNum.one x) →
          ((a : PosNum) → motive a.bit0 0) →
            ((p : PosNum) → (n : ℕ) → motive p.bit0 n.succ) →
              ((a : PosNum) → motive a.bit1 0) → ((p : PosNum) → (n : ℕ) → motive p.bit1 n.succ) → motive x x_1
-- Std.Data.TreeSet.Basic
/-- Monadically computes a value by folding the given function over the elements in the tree set in
ascending order.
 -/
Std.TreeSet.foldlM : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type u_1 → Type u_2} → {δ : Type u_1} → [Monad m] → (δ → α → m δ) → δ → Std.TreeSet α cmp → m δ
-- Mathlib.Data.Nat.Prime.Defs
/-- `Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  -/
Nat.prime_def : ∀ {p : ℕ}, Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearEquiv.isPositive_symm_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E ≃ₗ[𝕜] E}, (↑T.symm).IsPositive ↔ (↑T).IsPositive
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.throwNoGoalsToBeSolved : {α : Type} → Lean.Elab.Tactic.TacticM α
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiable.coordChange : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)]
  {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e']
  [inst_20 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {f : M → B} {g : M → F},
  MDiff f →
    MDiff g → (∀ (x : M), f x ∈ e.baseSet) → (∀ (x : M), f x ∈ e'.baseSet) → MDiff fun y => e.coordChange e' (f y) (g y)
-- Init.Data.String.Iterator
instToStringIterator : ToString String.Legacy.Iterator
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
algebraMap_galRestrict'_apply : ∀ (A : Type u_1) {K : Type u_2} {L : Type u_3} {L₂ : Type u_4} (B : Type u_6) (B₂ : Type u_7) [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : Algebra K L] [inst_10 : Algebra A L]
  [inst_11 : IsScalarTower A K L] [inst_12 : Algebra K L₂] [inst_13 : Algebra A L₂] [inst_14 : IsScalarTower A K L₂]
  [inst_15 : Algebra B L] [inst_16 : IsScalarTower A B L] [inst_17 : IsIntegralClosure B A L] [inst_18 : Algebra B₂ L₂]
  [inst_19 : IsScalarTower A B₂ L₂] [inst_20 : IsIntegralClosure B₂ A L₂] (σ : L →ₐ[K] L₂) (x : B),
  (algebraMap B₂ L₂) ((galRestrict' A B B₂ σ) x) = σ ((algebraMap B L) x)
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.splitter : {n : ℕ} →
  (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) →
    (step : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)) →
      (Unit → motive none) →
        ((id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints))) →
          ((id : ℕ) →
              (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
                (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints))) →
            ((id : ℕ) →
                (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
                  (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
                    (rupHints : Array ℕ) →
                      (ratHints : Array (ℕ × Array ℕ)) →
                        motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints))) →
              ((ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))) → motive step
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_union_le_size_add_size : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∪ t₂).size ≤ t₁.size + t₂.size
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the coproduct comparison morphism is an iso, its inverse is natural.  -/
CategoryTheory.Limits.coprodComparison_inv_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A' B']
  [inst_4 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B')
  [inst_6 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)]
  [inst_7 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B))
      (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g))
      (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B'))
-- Init.System.IO
/-- Moves a file or directory `old` to the new location `new`.

This function coincides with the [POSIX `rename`
function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/rename.html).
 -/
IO.FS.rename : System.FilePath → System.FilePath → IO Unit
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.mkOfOplax_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G}
  (Γ :
    (CategoryTheory.Pseudofunctor.StrongTrans.toOplax η).Modification
      (CategoryTheory.Pseudofunctor.StrongTrans.toOplax θ))
  (a : B), (CategoryTheory.Pseudofunctor.StrongTrans.Modification.mkOfOplax Γ).app a = Γ.app a
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOn.prodMk : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι} {ι' : Type u_5} {β' : Type u_6} [inst_1 : UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'}
  {p' : Filter ι'},
  TendstoUniformlyOn F f p s →
    TendstoUniformlyOn F' f' p' s →
      TendstoUniformlyOn (fun i a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ p') s
-- Mathlib.Topology.Category.Stonean.Basic
/-- The (forgetful) functor from Stonean spaces to compact Hausdorff spaces.  -/
Stonean.toCompHaus : CategoryTheory.Functor Stonean CompHaus
-- Mathlib.FieldTheory.Finite.Extension
/-- The Frobenius automorphism `x ↦ x ^ Nat.card k` that fixes `k`.  -/
FiniteField.Extension.frob : (k : Type u_1) →
  [inst : Field k] →
    [inst_1 : Finite k] →
      (p : ℕ) →
        [inst_2 : Fact (Nat.Prime p)] →
          [inst_3 : CharP k p] → (n : ℕ) → [inst_4 : NeZero n] → Gal(FiniteField.Extension k p n/k)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.OplaxTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c)
  {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (self.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))
      (CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g))
                h)))))
-- Mathlib.Algebra.BigOperators.Finprod
/-- The product of `f y` over `y ∈ Set.range g` equals the product of `f (g i)` over all `i`
provided that `g` is injective.  -/
finprod_mem_range : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {g : β → α},
  Function.Injective g → ∏ᶠ (i : α) (_ : i ∈ Set.range g), f i = ∏ᶠ (j : β), f (g j)
-- Std.Internal.Do.ExceptPost
/-- Pretty-print `EPost.Nil.mk` as `epost⟨⟩`.  -/
Std.Internal.Do.unexpandEPostNilMk : Lean.PrettyPrinter.Unexpander
-- Mathlib.RingTheory.Henselian
HenselianRing.jac : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} [self : HenselianRing R I], I ≤ ⊥.jacobson
-- Mathlib.Computability.Language
Language.sub_iSup : ∀ {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α), m - ⨆ i, l i = ⨅ i, m - l i
-- Mathlib.Data.List.ReduceOption
List.reduceOption_append : ∀ {α : Type u_1} (l l' : List (Option α)), (l ++ l').reduceOption = l.reduceOption ++ l'.reduceOption
-- Init.Data.List.Find
List.head?_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α}, (List.filterMap f l).head? = List.findSome? f l
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.lift_mk_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasImage g]
  [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)]
  (h : Y ⟶ CategoryTheory.Limits.image g)
  (H :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.Limits.image.ι g) =
      CategoryTheory.CategoryStruct.comp f g),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.image.lift
        { I := CategoryTheory.Limits.image g, m := CategoryTheory.Limits.image.ι g, m_mono := ⋯,
          e := CategoryTheory.CategoryStruct.comp f h, fac := ⋯ })
      (CategoryTheory.Limits.image.ι g) =
    CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.symmDiff : ∀ {α : Type u} {s t s' t' : Set α} {l : Filter α}, s =ᶠ[l] t → s' =ᶠ[l] t' → symmDiff s s' =ᶠ[l] symmDiff t t'
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
  IsUpperSet s → ∀ (f : α ≃o β), IsUpperSet (⇑f '' s)
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.out_dvd_iff : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (a : α) (b : Associates α),
  b.out ∣ a ↔ b ≤ Associates.mk a
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_closedEBall : ∀ (a : ℝ) (r : ENNReal), MeasureTheory.volume (Metric.closedEBall a r) = 2 * r
-- Lean.DocString.Types
Lean.Doc.Inline.bold.injEq : ∀ {i : Type u} (content content_1 : Array (Lean.Doc.Inline i)),
  (Lean.Doc.Inline.bold content = Lean.Doc.Inline.bold content_1) = (content = content_1)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Complex.rotation : ∀ (θ : Real.Angle) (z : ℂ), (Complex.orientation.rotation θ) z = ↑θ.toCircle * z
-- Mathlib.Order.Interval.Set.Defs
Set.Ici_def : ∀ {α : Type u_1} [inst : Preorder α] (b : α), {x | b ≤ x} = Set.Ici b
-- Init.Data.SInt.Basic
Int64.ofUInt64.inj : ∀ {toUInt64 toUInt64_1 : UInt64}, { toUInt64 := toUInt64 } = { toUInt64 := toUInt64_1 } → toUInt64 = toUInt64_1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.inter_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ m₄ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∩ m₂).Equiv (m₃ ∩ m₄)
-- Mathlib.RingTheory.Congruence.Basic
/-- The supremum of congruence relations `c, d` equals the smallest congruence relation containing
the binary relation '`x` is related to `y` by `c` or `d`'.  -/
RingCon.sup_eq_ringConGen : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (c d : RingCon R), c ⊔ d = ringConGen fun x y => c x y ∨ d x y
-- Mathlib.CategoryTheory.CofilteredSystem
/-- This bootstraps `nonempty_sections_of_finite_inverse_system`. In this version,
the `F` functor is between categories of the same universe, and it is an easy
corollary to `TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system`.  -/
nonempty_sections_of_finite_cofiltered_system.init : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsCofilteredOrEmpty J]
  (F : CategoryTheory.Functor J (Type u)) [hf : ∀ (j : J), Finite (F.obj j)] [hne : ∀ (j : J), Nonempty (F.obj j)],
  F.sections.Nonempty
-- Init.Data.Int.Gcd
Int.lcm_eq_right_iff_dvd : ∀ {b a : ℤ}, 0 ≤ b → (↑(a.lcm b) = b ↔ a ∣ b)
-- Mathlib.Algebra.Prime.Defs
Irreducible.not_dvd_isUnit : ∀ {M : Type u_1} [inst : CommMonoid M] {p u : M}, Irreducible p → IsUnit u → ¬p ∣ u
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instIsCancelAdd : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Add M] [IsCancelAdd M], IsCancelAdd (l.Germ M)
-- Aesop.Search.RuleSelection
Aesop.selectNormRules : Aesop.LocalRuleSet →
  Aesop.ForwardRuleMatches → Lean.MVarId → Aesop.BaseM (Array (Aesop.IndexMatchResult Aesop.NormRule))
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, ∅.sup f = ⊥
-- Mathlib.Analysis.Calculus.TaylorIntegral
DifferentiableAt.deriv_comp_add_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x y : E}
  {t : 𝕜}, DifferentiableAt 𝕜 f (x + t • y) → deriv (fun s => f (x + s • y)) t = (fderiv 𝕜 f (x + t • y)) y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensLegend.tokenTypes : Lean.Lsp.SemanticTokensLegend → Array String