mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteLatticeIntervals
/-- A nonempty `OrdConnected` set in a conditionally complete linear order is naturally a
conditionally complete linear order.  -/
ordConnectedSubsetConditionallyCompleteLinearOrder : {α : Type u_2} →
  (s : Set α) →
    [inst : ConditionallyCompleteLinearOrder α] →
      [Inhabited ↑s] → [s.OrdConnected] → ConditionallyCompleteLinearOrder ↑s
-- Mathlib.NumberTheory.LucasLehmer
one_lt_mersenne : ∀ {p : ℕ}, 1 < mersenne p ↔ 1 < p
-- Lean.LibrarySuggestions.SineQuaNon
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.sineQuaNon.go : ℕ →
  Float →
    Float →
      Lean.NameSet →
        Lean.NameSet →
          Std.TreeSet (Float × Lean.Name) compare →
            Array (Lean.Name × Float) → Std.TreeSet (Float × Lean.Name) compare → Lean.MetaM (Array (Lean.Name × Float))
-- Mathlib.Order.Monotone.Monovary
StrictAntiOn.trans_monovaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι} [inst_2 : PartialOrder ι], StrictAntiOn f s → MonovaryOn g f s → AntitoneOn g s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
/-- **Alias** of the forward direction of `Unitization.inr_nonneg_iff`. -/
Unitization.LE.le.of_inr : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A}, 0 ≤ ↑a → 0 ≤ a
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.instPreservesZeroMorphismsSingle : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι} (j : ι),
  (HomologicalComplex.single V c j).PreservesZeroMorphisms
-- Lean.Parser.Term
/-- `rightact% f a b` elaborates `f a b` as a right action using the type propagation protocol in `Lean.Elab.Extra`.
In particular, it is like a unary operation with a fixed parameter `b`, where only the left argument `a` participates in the operator coercion elaborator.  -/
Lean.Parser.Term.rightact : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (t : CategoryTheory.Limits.PullbackCone f g),
  CategoryTheory.CategoryStruct.comp t.fst f = CategoryTheory.CategoryStruct.comp t.snd g
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_zero : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.constantCoeff 0 = 0
-- Mathlib.Algebra.Ring.Basic
div_neg_eq_neg_div' : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] {b : R} (a : R), a / -b = -a / b
-- Mathlib.Combinatorics.Graph.Basic
/-- A multigraph with vertices of type `α` and edges of type `β`,
as described by vertex and edge sets `vertexSet : Set α` and `edgeSet : Set β`,
and a predicate `IsLink` describing whether an edge `e : β` has vertices `x y : α` as its ends.

The `edgeSet` structure field can be inferred from `IsLink`
via `edge_mem_iff_exists_isLink` (and this structure provides default values
for `edgeSet` and `edge_mem_iff_exists_isLink` that use `IsLink`).
While the field is not strictly necessary, when defining a graph we often
immediately know what the edge set should be,
and furthermore having `edgeSet` separate can be convenient for
definitional equality reasons.
 -/
Graph : Type u_3 → Type u_4 → Type (max u_3 u_4)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabNamedPatternErr : Lean.Elab.Term.TermElab
-- Init.Data.Int.Compare
Int.compare_eq_ite_lt : ∀ (a b : ℤ), compare a b = if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.ext_iff : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A] {ψ φ : PontryaginDual A}, ψ = φ ↔ ∀ (a : A), ψ a = φ a
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.continuousAt_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_3} [inst_1 : TopologicalSpace Y] {f : OnePoint X → Y} {x : X},
  ContinuousAt f ↑x ↔ ContinuousAt (f ∘ OnePoint.some) x
-- Mathlib.Order.Concept
Order.IsIntent.upperPolar_lowerPolar_subset : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t t' : Set β},
  Order.IsIntent r t → t' ⊆ t → upperPolar r (lowerPolar r t') ⊆ t
-- Mathlib.Data.NNRat.Defs
Mathlib.Tactic.Qify.nnratCast_le : ∀ (a b : ℚ≥0), a ≤ b ↔ ↑a ≤ ↑b
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL.match_5.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (rs : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l_1 : Std.DTreeMap.Internal.Impl α β) →
      l_1.Balanced →
        Std.DTreeMap.Internal.Impl.BalanceLPrecond l_1.size (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
          Sort u_3)
  (l_1 : Std.DTreeMap.Internal.Impl α β) (hlb : l_1.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l_1.size (Std.DTreeMap.Internal.Impl.inner rs k v l r).size)
  (h_1 :
    (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
            (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
        motive Std.DTreeMap.Internal.Impl.leaf hlb hlr)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hlb hlr)
  (hlb_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr_1 :
    Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
      (Std.DTreeMap.Internal.Impl.inner rs k v l r).size),
  l_1 = Std.DTreeMap.Internal.Impl.leaf →
    hlb ≍ hlb_1 →
      hlr ≍ hlr_1 →
        (match l_1, hlb, hlr with
          | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr => h_1 hlb hlr
          | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr, hlb, hlr => h_2 ls lk lv ll lr hlb hlr) ≍
          h_1 hlb_1 hlr_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k} {fallback : α},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKeyD fallback =
    t.minKey?.elim k fun k' => if compare k k' = Ordering.lt then k else k'
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_sup_eq_of_coprime_left : ∀ {R : Type u} [inst : Semiring R] {I J K : Ideal R} [J.IsTwoSided], I ⊔ J = ⊤ → I * K ⊔ J = K ⊔ J
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- `SemimoduleCat.Hom.hom` bundled as a linear equivalence.  -/
SemimoduleCat.homLinearEquiv : {R : Type u} →
  [inst : Semiring R] →
    {M N : SemimoduleCat R} →
      {S : Type u_1} →
        [inst_1 : Semiring S] → [inst_2 : Module S ↑N] → [inst_3 : SMulCommClass R S ↑N] → (M ⟶ N) ≃ₗ[S] ↑M →ₗ[R] ↑N
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectedSystem.natLERec.congr_simp : ∀ {L : FirstOrder.Language} {G' : ℕ → Type w} [inst : (i : ℕ) → L.Structure (G' i)]
  (f' f'_1 : (n : ℕ) → L.Embedding (G' n) (G' (n + 1))),
  f' = f'_1 →
    ∀ (m n : ℕ) (h : m ≤ n),
      FirstOrder.Language.DirectedSystem.natLERec f' m n h = FirstOrder.Language.DirectedSystem.natLERec f'_1 m n h
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  {U V : (TopologicalSpace.Opens ↑X.toTopCat)ᵒᵖ} (i : U ⟶ V) {Z : CommRingCat}
  (h :
    Y.presheaf.obj
        (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj (Opposite.unop V))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.map i)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f (Opposite.unop V)) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f (Opposite.unop U))
      (CategoryTheory.CategoryStruct.comp
        (Y.presheaf.map ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).op.map i)) h)
-- Mathlib.Topology.Order.Monotone
/-- An antitone function `f` sending `bot` to `top` and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set.  -/
AntitoneOn.map_sSup_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α},
  ContinuousWithinAt f s (sSup s) → AntitoneOn f s → f ⊥ = ⊤ → f (sSup s) = sInf (f '' s)
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.toFun_spec'' : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (g : L ≃+* L) {n : ℕ} [inst_2 : NeZero n] {t : L},
  IsPrimitiveRoot t n → g t = t ^ (modularCyclotomicCharacter.toFun n g).val
-- Mathlib.Data.Nat.Bits
_private.Mathlib.Data.Nat.Bits.0.Nat.boddDiv2.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.mk.congr_simp : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} (hom hom_1 : u.right ⟶ v.left) (e_hom : hom = hom_1)
  (comm :
    CategoryTheory.Arrow.Hom.right f - CategoryTheory.Arrow.Hom.right g = CategoryTheory.CategoryStruct.comp hom v.hom),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.y_neg : ∀ {d : ℤ} (a : Pell.Solution₁ d), (-a).y = -a.y
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instSMul.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  UpperSet.instSMul = { smul := fun a s => { carrier := (fun x => a • x) '' ↑s, upper' := ⋯ } }
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered
CategoryTheory.Limits.instHasCofilteredLimitsOfSizeFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v₁, u₁} C],
  CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, max u₂ v₁, max (max (max u₁ u₂) v₁) v₂}
    (CategoryTheory.Functor K C)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `b ≠ 0`. See `inv_mul_cancel_right`.  -/
inv_mul_right_le : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b : G₀}, 0 ≤ a → a * b⁻¹ * b ≤ a
-- Mathlib.ModelTheory.Satisfiability
/-- A theory models a (bounded) formula when any of its nonempty models realizes that formula on all
inputs.  -/
FirstOrder.Language.Theory.«term_⊨ᵇ_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Group.Prod
MeasurableEquiv.shearSubRight.eq_1 : ∀ (G : Type u_1) [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
  [inst_3 : MeasurableNeg G],
  MeasurableEquiv.shearSubRight G =
    { toEquiv := (Equiv.refl G).prodShear Equiv.subRight, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_eq_right : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ⊢ₛ Q ↔ P ⊣⊢ₛ Q ∧ P
-- Batteries.Data.Array.Scan
Array.scanr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (as : Array α) (start stop : ℕ),
  Array.scanr f init as start stop = (Array.scanrM (fun x1 x2 => pure (f x1 x2)) init as start stop).run
-- Mathlib.Analysis.Complex.Norm
Complex.edist_of_im_eq : ∀ {z w : ℂ}, z.im = w.im → edist z w = edist z.re w.re
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N)
  (a : AdicCompletion.AdicCauchySequence I M),
  (AdicCompletion.map I f) ((AdicCompletion.mk I M) a) =
    (AdicCompletion.mk I N) ((AdicCompletion.AdicCauchySequence.map I f) a)
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.hasBasis_open_twoSidedIdeal : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [ContinuousAdd R] [IsLinearTopology R R]
  [IsLinearTopology Rᵐᵒᵖ R], (nhds 0).HasBasis (fun I => IsOpen ↑I) fun I => ↑I
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.mem_finsuppAntidiag_insert : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] {a : ι} {s : Finset ι},
  a ∉ s →
    ∀ (n : μ) {f : ι →₀ μ},
      f ∈ (insert a s).finsuppAntidiag n ↔
        ∃ m ∈ Finset.HasAntidiagonal.antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piFinTwo_symm_apply : ∀ (X : Fin 2 → Type u) [inst : (i : Fin 2) → TopologicalSpace (X i)],
  ⇑(Homeomorph.piFinTwo X).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a monoid are inhabited because `1` is a unit.  -/
Units.instInhabited : {α : Type u} → [inst : Monoid α] → Inhabited αˣ
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.monoLM.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n₁ n₂ : ℕ∞} {K₁ K₂ : TopologicalSpace.Compacts E},
  ContDiffMapSupportedIn.monoLM 𝕜 =
    { toFun := fun f => if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0,
      map_add' := ⋯, map_smul' := ⋯ }
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withInductiveLocalDecls.match_4.eq_1 : ∀ (motive : Option (Lean.Expr × Subarray Lean.Expr) → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : (origParam : Lean.Expr) → (s' : Subarray Lean.Expr) → motive (some (origParam, s'))),
  (match none with
    | none => h_1 ()
    | some (origParam, s') => h_2 origParam s') =
    h_1 ()
-- Mathlib.Topology.EMetricSpace.Defs
instEMetricSpaceMulOpposite.eq_1 : ∀ {α : Type u_2} [inst : EMetricSpace α], instEMetricSpaceMulOpposite = EMetricSpace.induced MulOpposite.unop ⋯ inst
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- For any circle integrable function `f`, the power series `cauchyPowerSeries f c R`, `R > 0`,
converges to the Cauchy integral `(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z` on the open
disc `Metric.ball c R`.  -/
sum_cauchyPowerSeries_eq_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ},
  CircleIntegrable f c R →
    ‖w‖ < R →
      (cauchyPowerSeries f c R).sum w = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.Std.Iter.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Algebra.Group.Submonoid.Operations
AddEquiv.coe_addSubmonoidMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M)
  (g : ↥S), ↑((e.addSubmonoidMap S) g) = e ↑g
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {G : Type u_3} [inst_5 : SMul G β]
  [inst_6 : IsScalarTower G β β] (a : G) (x : β), CauSeq.const abv (a • x) = a • CauSeq.const abv x
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.apply_le_norm : ∀ {α : Type u} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) (x : α), f x ≤ ‖f‖
-- Mathlib.Order.Interval.Finset.Basic
Finset.notMem_uIcc_of_lt : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}, c < a → c < b → c ∉ Finset.uIcc a b
-- Lean.Meta.Sym.Canon
/-- `true` if we are visiting a type.  -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.Context.insideType : Lean.Meta.Sym.Canon.Context✝ → Bool
-- Init.Data.Vector.Lemmas
Vector.push_pop_back : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α (n + 1)), xs.pop.push xs.back = xs
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The zero acts trivially.  -/
CategoryTheory.AddModObj.zero_vadd : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {M : C} {inst_4 : CategoryTheory.AddMonObj M} (X : D) [self : CategoryTheory.AddModObj M X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.zero X)
      CategoryTheory.AddModObj.vadd =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
-- Init.Data.Option.Lemmas
Option.merge_lt_iff : ∀ {α : Type u_1} [inst : LT α] {f : α → α → α} {o₁ o₂ o₃ : Option α},
  (∀ (a b c : α), f a b < c ↔ a < c ∧ b < c) → (Option.merge f o₁ o₂ < o₃ ↔ o₁ < o₃ ∧ o₂ < o₃)
-- Mathlib.Data.FP.Basic
FP.Float.finite.sizeOf_spec : ∀ [C : FP.FloatCfg] (a : Bool) (e : ℤ) (m : ℕ) (a_1 : FP.ValidFinite e m),
  sizeOf (FP.Float.finite a e m a_1) = 1 + sizeOf a + sizeOf e + sizeOf m + sizeOf a_1
-- Aesop.Forward.Match
/-- Create a one-element match. `subst` is the substitution that results from
matching a hypothesis against slot 0, or from a pattern substitution.
`isPatSubst` is `true` if the substitution resulted from a rule pattern.
`forwardDeps` are the forward dependencies of slot 0. `conclusionDeps` are the
conclusion dependencies of the rule to which this match belongs.  -/
Aesop.Match.initial : Aesop.Substitution → Bool → Array Aesop.PremiseIndex → Array Aesop.PremiseIndex → Aesop.Match
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.card_le : ∀ {α : Type u_1} [inst : BooleanAlgebra α] [inst_1 : Fintype α] {s : Finset α},
  (↑s).Intersecting → 2 * s.card ≤ Fintype.card α
-- Mathlib.Algebra.Quandle
/-- A *rack* is an automorphic set (a set with an action on itself by
bijections) that is self-distributive.  It is a shelf such that each
element's action is invertible.

The notations `x ◃ y` and `x ◃⁻¹ y` denote the action and the
inverse action, respectively, and they are right associative.
 -/
Rack : Type u → Type u
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.zero_lt_finrank_genWeightSpace : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] [IsDomain R]
  [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] [inst_11 : LieRing.IsNilpotent L] {χ : L → R},
  LieModule.genWeightSpace M χ ≠ ⊥ → 0 < Module.finrank R ↥(LieModule.genWeightSpace M χ)
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_symm_some : ∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), (finSuccEquiv' i).symm (some j) = i.succAbove j
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeSyntheticMVars.loop : Lean.Elab.Term.PostponeBehavior → Bool → Unit → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_add : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α]
  (s t : NonemptyInterval α), (s + t).toProd.1 = s.toProd.1 + t.toProd.1
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.evalAddHom.eq_1 : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → Add (f i)] (i : I),
  Pi.evalAddHom f i = { toFun := fun g => g i, map_add' := ⋯ }
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.instLocallySmallSmallModel : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.EssentiallySmall.{w, v, u} C]
  [CategoryTheory.LocallySmall.{w', v, u} C],
  CategoryTheory.LocallySmall.{w', w, w} (CategoryTheory.SmallModel.{w, v, u} C)
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- Construct a `RingHomInvPair` from both directions of a ring equiv.

This is not an instance, as for equivalences that are involutions, a better instance
would be `RingHomInvPair e e`.
 -/
RingHomInvPair.of_ringEquiv : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (e : R₁ ≃+* R₂), RingHomInvPair ↑e ↑e.symm
-- Mathlib.Analysis.Normed.Group.Defs
/-- An e-seminormed commutative monoid is a commutative monoid endowed with a continuous enorm.  -/
ESeminormedCommMonoid : (E : Type u_8) → [TopologicalSpace E] → Type u_8
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.mem_zmultiples_iff : ∀ {G : Type u_1} [inst : AddGroup G] {g h : G}, h ∈ AddSubgroup.zmultiples g ↔ ∃ k, k • g = h
-- Lean.Environment
/-- Adds given declaration to the environment, type checking it unless `doCheck` is false.

This is a plumbing function for the implementation of `Lean.addDecl`, most users should use it
instead.
 -/
Lean.Environment.addDeclCore : Lean.Environment →
  USize →
    USize →
      Lean.Declaration → Option IO.CancelToken → optParam Bool true → Except Lean.Kernel.Exception Lean.Environment
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.center_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  Subsemiring.center (R × S) = (Subsemiring.center R).prod (Subsemiring.center S)
-- Init.Data.List.MapIdx
List.mapIdx_cons : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {l : List α} {a : α},
  List.mapIdx f (a :: l) = f 0 a :: List.mapIdx (fun i => f (i + 1)) l
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.instIsStableUnderBaseChangePrecoverageOfIsStableUnderBaseChange : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange], P.precoverage.IsStableUnderBaseChange
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfLeftIso_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).inl = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.matrix.eq_1 : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k),
  CategoryTheory.Limits.biproduct.matrix m =
    CategoryTheory.Limits.biproduct.desc fun j => CategoryTheory.Limits.biproduct.lift fun k => m j k
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.center_eq_univ_of_subsingleton : ∀ {α : Type u_1} {G : SimpleGraph α} [Subsingleton α], G.center = Set.univ