mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteLattice.Defs
sSup_le_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- The `S`-linear map on the span of coroots given by evaluating at a root.  -/
RootPairing.root'In : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_6) →
                      [inst_5 : CommRing S] →
                        [inst_6 : Algebra S R] →
                          [inst_7 : Module S N] →
                            [IsScalarTower S R N] →
                              [FaithfulSMul S R] → [P.IsValuedIn S] → ι → Module.Dual S ↥(P.corootSpan S)
-- Mathlib.Algebra.Category.GrpWithZero
/-- Typecheck a `MonoidWithZeroHom` as a morphism in `GrpWithZero`.  -/
GrpWithZero.ofHom : {X Y : Type u} →
  [inst : GroupWithZero X] →
    [inst_1 : GroupWithZero Y] → (X →*₀ Y) → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A] (k : A)
  {X Y : Cᵒᵖ} (f : X ⟶ Y),
  (Φ.skyscraperPresheafFunctor.obj k).map f =
    CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f.unop)) fun x =>
      CategoryTheory.CategoryStruct.id k
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forIn_visit_eq_bindList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {α_1 : Type u_1} {f : α → α_1 → m (ForInStep α_1)} {init : α_1}
  [inst : Monad m] [LawfulMonad m] {t : RBTree.RBNode α},
  RBTree.RBNode.forIn.visit f t init = ForInStep.bindList f t.toList (ForInStep.yield init)
-- Mathlib.Topology.Bases
/-- An open quotient of a second countable space is second countable.  -/
TopologicalSpace.Quotient.secondCountableTopology : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Setoid X} [SecondCountableTopology X],
  IsOpenMap Quotient.mk' → SecondCountableTopology (Quotient S)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.instToStringPComp : ToString Mathlib.Tactic.Linarith.PComp
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_iff : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] (s : Set E), Bornology.IsVonNBounded 𝕜 s ↔ ∀ V ∈ nhds 0, Absorbs 𝕜 V s
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric'.pre_le : ∀ {X : Type u_2} [inst : EMetricSpace X] {m : Set X → ENNReal} {r : ENNReal} {s : Set X},
  Metric.ediam s ≤ r → (MeasureTheory.OuterMeasure.mkMetric'.pre m r) s ≤ m s
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_opow_of_isPrincipal_add : ∀ {a : Ordinal.{u_1}},
  Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) a →
    ∀ (b : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) (a ^ b)
-- Init.Data.Int.Basic
/-- The absolute value of an integer is its distance from `0`.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
 * `(7 : Int).natAbs = 7`
 * `(0 : Int).natAbs = 0`
 * `(-11 : Int).natAbs = 11`
 -/
Int.natAbs : ℤ → ℕ
-- Mathlib.Data.Finset.Functor
Finset.pure_def : ∀ {α : Type u_1}, pure = singleton
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.map.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3) →
      (X Y : CategoryTheory.WithInitial C) →
        (f : X ⟶ Y) →
          ((a a_1 : C) →
              (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
                motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) f) →
            ((a : C) →
                (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
                  motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x) →
              ((x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
                  motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x) →
                motive X Y f
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The generators of the free Lie algebra from which we construct the Lie algebra of a Cartan
matrix as a quotient.  -/
CartanMatrix.Generators : Type v → Type v
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.EvalConfigItem.mk.inj : ∀ {α : Type} {set set_1 : α → Lean.Elab.ConfigEval.ConfigItem → Lean.Elab.TermElabM α},
  { set := set } = { set := set_1 } → set = set_1
-- Mathlib.Topology.Maps.Strict.Basic
/-- **Alias** of `IsHomeomorph.isStrictMap`.

---

A homeomorphism is a strict map.  -/
Topology.IsHomeomorph.isStrictMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Topology.IsStrictMap f
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
IsBaseChange.map_smul_top_ne_top_iff_of_faithfullyFlat : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u_1}
  {N : Type u_2} [inst_3 : CommRing S] [inst_4 : Algebra R S] [Module.FaithfullyFlat R S] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] [inst_8 : Module S N] [inst_9 : IsScalarTower R S N] {f : M →ₗ[R] N},
  IsBaseChange S f → ∀ (I : Ideal R), Ideal.map (algebraMap R S) I • ⊤ ≠ ⊤ ↔ I • ⊤ ≠ ⊤
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : Preorder β] [OrderClosedTopology β] [TopologicalSpace.PseudoMetrizableSpace β] {f g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.NullMeasurableSet {a | f a < g a} μ
-- Mathlib.Algebra.Group.Translate
comp_translate : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_5} [inst : AddCommGroup G] (a : G) (f : G → α) (g : α → β),
  g ∘ translate a f = translate a (g ∘ f)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_sub : ∀ {R : Type u_1} {a b : R} [inst : Sub R] (z w : QuadraticAlgebra R a b), (z - w).im = z.im - w.im
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isUltrametricDist_of_forall_nnnorm_add_le_max_nnnorm : ∀ {S' : Type u_2} [inst : SeminormedAddGroup S'], (∀ (x y : S'), ‖x + y‖₊ ≤ max ‖x‖₊ ‖y‖₊) → IsUltrametricDist S'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  k ∈ t.alter k f ↔ (f (t.get? k)).isSome = true
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.iSup_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M),
  ↑(⨆ i, p i) = ⨆ i, ↑(p i)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Every acyclic subgraph `H ≤ G` is contained in a maximal such subgraph.  -/
SimpleGraph.exists_maximal_isAcyclic_of_le_isAcyclic : ∀ {V : Type u_1} {G H : SimpleGraph V}, H ≤ G → H.IsAcyclic → ∃ H', H ≤ H' ∧ Maximal (fun H => H ≤ G ∧ H.IsAcyclic) H'
-- Lean.Meta.Tactic.Grind.Arith.EvalNum
Lean.Meta.Grind.Arith.evalNat? : Lean.Expr → Lean.Meta.Grind.GrindM (Option ℕ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_eraseKey_le : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α},
  (Std.Internal.List.eraseKey k l).length ≤ l.length
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBy_torsionBy_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Submodule.torsionBy R (↥(Submodule.torsionBy R M a)) a = ⊤
-- Mathlib.Analysis.InnerProductSpace.Calculus
HasDerivWithinAt.norm_sq : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {f : ℝ → F} {f' : F} {s : Set ℝ}
  {x : ℝ}, HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => ‖f x‖ ^ 2) (2 * inner ℝ (f x) f') s x
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instOne : {α : Type u_1} → [One α] → One (Lex α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey_modifyKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    ∀ (h : Std.Internal.List.containsKey k (Std.Internal.List.Const.modifyKey k f l) = true),
      Std.Internal.List.getKey k (Std.Internal.List.Const.modifyKey k f l) h = k
-- Batteries.Data.AssocList
/-- `O(n)`. Remove the first entry in the list with key equal to `a`.  -/
Batteries.AssocList.erase : {α : Type u_1} → {β : Type u_2} → [BEq α] → α → Batteries.AssocList α β → Batteries.AssocList α β
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapComp_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.Under.mapComp f g).hom = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.top_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat} (x : C), ⊤.obj x = ⊤
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabel_imp : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ}
  (φ ψ : L.BoundedFormula α k),
  FirstOrder.Language.BoundedFormula.relabel g (φ.imp ψ) =
    (FirstOrder.Language.BoundedFormula.relabel g φ).imp (FirstOrder.Language.BoundedFormula.relabel g ψ)
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Filter.Tendsto.dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {f g : β → α} {x : Filter β} {a b : α},
  Filter.Tendsto f x (nhds a) →
    Filter.Tendsto g x (nhds b) → Filter.Tendsto (fun x => dist (f x) (g x)) x (nhds (dist a b))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_maxKey?_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.associator_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (P Q R : C),
  (CategoryTheory.Limits.prod.associator P Q R).inv =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.sl2SubalgebraOfRoot.eq_1 : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero),
  LieAlgebra.IsKilling.sl2SubalgebraOfRoot hα =
    (fun h x => (fun e x => (fun f x => IsSl2Triple.toLieSubalgebra K ⋯) (Classical.choose x) ⋯) (Classical.choose x) ⋯)
      (Classical.choose ⋯) ⋯
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_succ : ∀ (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr q.succ =
    Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main
      (Turing.TM2.Stmt.branch (fun s => decide (s = some Turing.PartrecToTM2.Γ'.bit1))
        (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.rev (fun x => Turing.PartrecToTM2.Γ'.bit0)
          (Turing.TM2.Stmt.goto fun x => q.succ))
        (Turing.TM2.Stmt.branch (fun s => decide (s = some Turing.PartrecToTM2.Γ'.cons))
          (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun x => Turing.PartrecToTM2.Γ'.cons)
            (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun x => Turing.PartrecToTM2.Γ'.bit1)
              (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q)))
          (Turing.TM2.Stmt.push Turing.PartrecToTM2.K'.main (fun x => Turing.PartrecToTM2.Γ'.bit1)
            (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.unrev q))))
-- Init.Data.Iterators.Combinators.Monadic.Take
/-- The internal state of the `IterM.take` iterator combinator.
 -/
Std.Iterators.Types.Take : (α : Type w) → (m : Type w → Type w') → {β : Type w} → [Std.Iterator α m β] → Type w
-- Mathlib.Order.Filter.CountableInter
countable_iInter_mem : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s : ι → Set α},
  ⋂ i, s i ∈ l ↔ ∀ (i : ι), s i ∈ l
-- Mathlib.Algebra.Polynomial.DenomsClearable
DenomsClearable.add : ∀ {R : Type u_1} {K : Type u_2} [inst : Semiring R] [inst_1 : CommSemiring K] {i : R →+* K} {a b : R} {N : ℕ}
  {f g : Polynomial R}, DenomsClearable a b N f i → DenomsClearable a b N g i → DenomsClearable a b N (f + g) i
-- Init.Data.Int.Bitwise.Lemmas
Int.natCast_shiftLeft : ∀ (n s : ℕ), ↑(n <<< s) = ↑n <<< s
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
/-- The absolute discriminant of a number field.  -/
NumberField.discr : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℤ
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.subset_compl_iff_disjoint_right : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α], s ⊆ tᶜ ↔ Disjoint s t
-- Mathlib.LinearAlgebra.Pi
LinearMap.proj_comp_single_same : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i : ι),
  LinearMap.proj i ∘ₗ LinearMap.single R φ i = LinearMap.id
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.rank_bot' : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  Module.rank (↥⊥) E = Module.rank F E
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_injective : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F],
  Function.Injective ContinuousLinearMapWOT.ofCLM
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracket_swap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {x : E}, VectorField.lieBracket 𝕜 V W x = -VectorField.lieBracket 𝕜 W V x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  F.mapComp f (CategoryTheory.CategoryStruct.id b) =
    F.map₂Iso (CategoryTheory.Bicategory.rightUnitor f) ≪≫
      (CategoryTheory.Bicategory.rightUnitor (F.map f)).symm ≪≫
        (CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId b)).symm
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabSeq : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.conj_eqToHom_assoc : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y x' y' : X} {p : Path.Homotopic.Quotient x y} (hx : x' = x)
  (hy : y' = y) {Z : FundamentalGroupoid X} (h : { as := y' } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)) =
    CategoryTheory.CategoryStruct.comp (p.cast hx hy) h
-- Mathlib.RingTheory.WittVector.Domain
WittVector.shift.eq_1 : ∀ {p : ℕ} {R : Type u_1} (x : WittVector p R) (n : ℕ), x.shift n = { coeff := fun i => x.coeff (n + i) }
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_inv_fac_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesRightKanExtension F L] [inst_5 : L.HasRightKanExtension F]
  {Z : CategoryTheory.Functor A D} (h : F.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).inv)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.rightKanExtension F) G).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.rightKanExtensionCounit F) G) h)) =
    CategoryTheory.CategoryStruct.comp (L.rightKanExtensionCounit (F.comp G)) h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_mem_Ioc : ∀ (θ : Real.Angle), θ.toReal ∈ Set.Ioc (-Real.pi) Real.pi
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).isColimit₂ =
    CategoryTheory.Limits.coproductIsCoproduct fun i => B i.i
-- Mathlib.Data.Finset.Sups
Finset.compls_subset_compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s₁ s₂ : Finset α}, s₁.compls ⊆ s₂.compls ↔ s₁ ⊆ s₂
-- Mathlib.Order.Interval.Set.Defs
/-- `Ioi a` is the left-open right-infinite interval $(a, ∞)$.  -/
Set.Ioi : {α : Type u_1} → [Preorder α] → α → Set α
-- Mathlib.ModelTheory.Complexity
/-- An existential formula is a formula defined by applying only existential quantifiers to a
quantifier-free formula.  -/
FirstOrder.Language.BoundedFormula.IsExistential : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → Prop
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.isOpenEmbedding : ∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom U.inclusion')
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.finset_inf'_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {t : Set X} {x : X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousWithinAt (f i) t x) → ContinuousWithinAt (fun a => s.inf' hne fun x => f x a) t x
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.isBasis_union_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis I X → M.Indep J → I ⊆ J → M.IsBasis J (J ∪ X)
-- Mathlib.RingTheory.Bialgebra.Hom
CoalgHom.copy.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f f_1 : A →ₗc[R] B) (e_f : f = f_1) (f' f'_1 : A → B) (e_f' : f' = f'_1) (h : f' = ⇑f), f.copy f' h = f_1.copy f'_1 ⋯
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_hom_app_comp_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n m mn : M) (hnm : m + n = mn) (a a' a'' : M)
  (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) {Z : A} (h : (F.shift a'').obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X))
      (CategoryTheory.CategoryStruct.comp ((F.shiftIso m a' a'' ha'').hom.app X) h) =
    CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X))
      (CategoryTheory.CategoryStruct.comp ((F.shiftIso mn a a'' ⋯).hom.app X) h)
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
/-- A prime `p` does not divide `discr K` if and only if `p` (as the ideal `span {p}`) is
unramified in the ring of integers `𝒪`.

Also see `not_dvd_discr_iff_forall_liesOver` and `not_dvd_discr_iff_forall_mem` for variants
whose RHS does not use `Algebra.IsUnramifiedIn`.  -/
NumberField.not_dvd_discr_iff_isUnramifiedIn : ∀ (K : Type u_1) (𝒪 : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsIntegralClosure 𝒪 ℤ K] {p : ℤ}, Prime p → (¬p ∣ NumberField.discr K ↔ Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p}))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_add_of_le_add_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] {a b c d : α}, a ≤ b + c → c ≤ d → a ≤ b + d
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Std.Do.PredTrans.pushOption.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Given a (full, resolvable) declaration name `foo` and an array of parameters
`#[p₁, p₂, ..., pₙ]`, constructs the message:
```null
`{foo}` does not use the following hypothes(is/es) in its type{ outside of proofs}:
  • {p₁}
  • {p₂}
  ⋮
  • {pₙ}
```
where the bracketed "outside of proofs" is only included if some parameter appears in a proof in
the type.
 -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Lean.Name.unusedInstancesMsg : Lean.Name → Array Mathlib.Linter.UnusedInstancesInType.Parameter✝ → Lean.MessageData
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Context.mk.inj : ∀ {sharedExprs : Lean.Meta.Sym.SharedExprs} {config : Lean.Meta.Sym.Config} {sharedExprs_1 : Lean.Meta.Sym.SharedExprs}
  {config_1 : Lean.Meta.Sym.Config},
  { sharedExprs := sharedExprs, config := config } = { sharedExprs := sharedExprs_1, config := config_1 } →
    sharedExprs = sharedExprs_1 ∧ config = config_1
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.symm_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1},
  Metric.Snowflaking.toSnowflaking.symm = Metric.Snowflaking.ofSnowflaking
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_translate : ∀ (x : ℝ), (↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x))).translationNumber = x