mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.congr_eq_1 : ∀ {n : ℕ} (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1)
  (x : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c)))
  (h_2 : Unit → motive (some none)) (h_3 : Unit → motive none) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  x = some (some c) →
    (match x with
      | some (some c) => h_1 c
      | some none => h_2 ()
      | none => h_3 ()) ≍
      h_1 c
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {inst_1 : LinearOrder J} {inst_2 : OrderBot J}
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} {x y : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j},
  x.f' = y.f' → x = y
-- Mathlib.Topology.UniformSpace.Defs
Filter.HasBasis.uniformContinuous_iff : ∀ {α : Type ua} {β : Type ub} {ι : Sort u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] {ι' : Sort u_2}
  {p : ι → Prop} {s : ι → SetRel α α},
  (uniformity α).HasBasis p s →
    ∀ {q : ι' → Prop} {t : ι' → Set (β × β)},
      (uniformity β).HasBasis q t →
        ∀ {f : α → β}, UniformContinuous f ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i
-- Mathlib.Data.Rel
SetRel.comp_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (R : SetRel α β) (S : SetRel β γ) (t : SetRel γ δ),
  (R.comp S).comp t = R.comp (S.comp t)
-- Mathlib.Order.Booleanisation
Booleanisation.instSemilatticeInf : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → SemilatticeInf (Booleanisation α)
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = true ↔ ∀ (a : α), a ∉ m
-- Init.Data.Int.Linear
Int.Internal.Linear.var_eq_cert : Int.Internal.Linear.Var → ℤ → Int.Internal.Linear.Poly → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.precompFork.eq_1 : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X)
  (s : CategoryTheory.Limits.Fork f g) (c : CategoryTheory.Limits.PullbackCone s.ι h),
  CategoryTheory.Limits.precompFork h s c = CategoryTheory.Limits.Fork.ofι c.snd ⋯
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
_private.Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation.0.Orientation.termJ : Lean.ParserDescr
-- Init.Data.Nat.Coprime
/-- `m` and `n` are coprime, or relatively prime, if their `gcd` is 1.  -/
Nat.Coprime : ℕ → ℕ → Prop
-- Lean.Meta.ACLt
Lean.Meta.ACLt.ReduceMode.reduceSimpleOnly.sizeOf_spec : sizeOf Lean.Meta.ACLt.ReduceMode.reduceSimpleOnly = 1
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
/-- The determinant of the matrix obtained by replacing rows outside `s` with identity rows
equals the determinant of the principal submatrix indexed by `s`.  -/
Matrix.det_piecewise_one_eq_submatrix_det : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (s : Finset n), (Matrix.of (s.piecewise M.row (Matrix.row 1))).det = (M.submatrix Subtype.val Subtype.val).det
-- Mathlib.Data.BitVec
BitVec.toFin_nsmul : ∀ {w : ℕ} (n : ℕ) (x : BitVec w), (n • x).toFin = n • x.toFin
-- Lean.Meta.NatInstTesters
Lean.Meta.DefEq.isInstHMulNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Tactic.Widget.SelectInsertParamsClass
/-- The current tactic-mode goals.  -/
SelectInsertParamsClass.goals : {α : Type} → [self : SelectInsertParamsClass α] → α → Array Lean.Widget.InteractiveGoal
-- Lean.Data.Options
Lean.Option.set : {α : Type} → [Lean.KVMap.Value α] → Lean.Options → Lean.Option α → α → Lean.Options
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.zeta_pmul : ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : ArithmeticFunction R), (↑ArithmeticFunction.zeta).pmul f = f
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConst.mk.sizeOf_spec : ∀ (constInfo : Lean.AsyncConstantInfo) (exts? : Option (Task (Array Lean.EnvExtensionState)))
  (aconstsImpl : Task Dynamic) (isRealized : Bool),
  sizeOf { constInfo := constInfo, exts? := exts?, aconstsImpl := aconstsImpl, isRealized := isRealized } =
    1 + sizeOf constInfo + sizeOf exts? + sizeOf aconstsImpl + sizeOf isRealized
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.divRight.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
  MeasurableEquiv.divRight g = { toEquiv := Equiv.divRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_inter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (t₁ ∩ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∉ t₂
-- Mathlib.RingTheory.RootsOfUnity.Basic
Units.val_set_image_rootsOfUnity_two : ∀ {R : Type u_4} [inst : CommRing R] [NoZeroDivisors R], Units.val '' ↑(rootsOfUnity 2 R) = {1, -1}
-- Init.Data.Array.Erase
Array.set_eraseIdx : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {w : i < xs.size} {j : ℕ} {a : α} (hj : j < (xs.eraseIdx i w).size),
  (xs.eraseIdx i w).set j a hj = if h' : i ≤ j then (xs.set (j + 1) a ⋯).eraseIdx i ⋯ else (xs.set j a ⋯).eraseIdx i ⋯
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instContinuousMapClass : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q], ContinuousMapClass (P →ᴬ[R] Q) P Q
-- Lean.Parser.Do
Lean.Parser.Term.doMatchExpr : Lean.Parser.Parser
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
add_mem_lowerBounds_add : ∀ {M : Type u_3} [inst : Add M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M} {a b : M},
  a ∈ lowerBounds s → b ∈ lowerBounds t → a + b ∈ lowerBounds (s + t)
-- Mathlib.Topology.Compactness.Lindelof
mem_coLindelof' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s ∈ Filter.coLindelof X ↔ ∃ t, IsLindelof t ∧ sᶜ ⊆ t
-- Mathlib.Order.GaloisConnection.Basic
/-- Lift the infima along a Galois insertion  -/
GaloisInsertion.liftSemilatticeInf : {α : Type u} →
  {β : Type v} →
    {l : α → β} →
      {u : β → α} → [inst : PartialOrder β] → [inst_1 : SemilatticeInf α] → GaloisInsertion l u → SemilatticeInf β
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_concat : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (p₁.concat p₂) =
    Lean.Grind.CommRing.Poly.denote ctx p₁ + Lean.Grind.CommRing.Poly.denote ctx p₂
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The first period in a `PeriodPair`.  -/
PeriodPair.ω₁ : PeriodPair → ℂ
-- Mathlib.Algebra.Lie.Killing
LieAlgebra.IsKilling.mk : ∀ {R : Type u_1} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieIdeal.killingCompl R L ⊤ = ⊥ → LieAlgebra.IsKilling R L
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.nonneg_of_isRat : ∀ {A : Type u_1} {e : A} {n : ℤ} {d : ℕ} [inst : Ring A] [inst_1 : LinearOrder A],
  Mathlib.Meta.NormNum.IsRat e n d → decide (n = 0) = true → 0 ≤ e
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.opEquiv_apply_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.op.PtSimplex n (SSet.opObjEquiv.symm x)),
  (SSet.PtSimplex.opEquiv f).map = SSet.yonedaEquiv.symm (SSet.opObjEquiv (SSet.yonedaEquiv f.map))
-- Mathlib.Data.List.Basic
/-- If two lists `l₁` and `l₂` are the same length and `l₁[n]! = l₂[n]!` for all `n`,
then the lists are equal.  -/
List.ext_getElem! : ∀ {α : Type u} {l₁ l₂ : List α} [inst : Inhabited α], l₁.length = l₂.length → (∀ (n : ℕ), l₁[n]! = l₂[n]!) → l₁ = l₂
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Subtype.preimage_closedEBall`. -/
Subtype.preimage_emetricClosedBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ENNReal),
  Subtype.val ⁻¹' Metric.closedEBall (↑a) r = Metric.closedEBall a r
-- Mathlib.Data.List.Sort
List.SortedGT.eq_reverse_of_mem_iff_of_sortedLT : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α},
  (∀ (a : α), a ∈ l₁ ↔ a ∈ l₂) → l₁.SortedGT → l₂.SortedLT → l₁ = l₂.reverse
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.wInner_cWeight_self : ∀ {G : Type u_1} {R : Type u_3} [inst : AddGroup G] [inst_1 : RCLike R] [inst_2 : Fintype G] (ψ : AddChar G R),
  ⟪⇑ψ, ⇑ψ⟫ₙ_[R] = 1
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_le_iff : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {a : Ordinal.{max u v}},
  o.bsup f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim_update_rev : ∀ {a b c d b' : List Turing.PartrecToTM2.Γ'},
  Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.rev b' =
    Turing.PartrecToTM2.K'.elim a b' c d
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
/-- An isometric continuous functional calculus on a unital algebra yields to a non-unital one.  -/
IsometricContinuousFunctionalCalculus.toNonUnital : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p],
  NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The morphism from the zero object determines a cone on a kernel diagram  -/
CategoryTheory.Limits.kernel.zeroKernelFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasZeroObject C] → CategoryTheory.Limits.KernelFork f
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_tsum_le_of_forall_le_of_nonneg : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {f : ι → M} {C : ℝ},
  0 ≤ C → (∀ (i : ι), ‖f i‖ ≤ C) → ‖∑' (i : ι), f i‖ ≤ C
-- Mathlib.Analysis.Normed.Group.Uniform
enorm_map' : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) (x : E), ‖f x‖ₑ = ‖x‖ₑ
-- Init.Data.List.Lemmas
List.contains_reverse : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {x : α}, l.reverse.contains x = l.contains x
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_comp_algebraMap : ∀ (K : Type u) [inst : CommRing K] [inst_1 : IsDomain K],
  RatFunc.ofFractionRing ∘ ⇑(algebraMap (Polynomial K) (FractionRing (Polynomial K))) =
    ⇑(algebraMap (Polynomial K) (RatFunc K))
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.one_apply_ne' : ∀ {n : Type u_2} {A : Type u_5} [inst : DecidableEq n] [inst_1 : Zero A] [inst_2 : One A] {i j : n}, j ≠ i → 1 i j = 0
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.snd.inj : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} {a a_1 : Std.IterM m β},
  Std.Iterators.Types.Append.snd a = Std.Iterators.Types.Append.snd a_1 → a = a_1
-- Mathlib.Topology.UrysohnsLemma
/-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological
space `X`, with `s` compact and `t` closed, then there exists a continuous
function `f : X → ℝ` such that

* `f` equals zero on `s`;
* `f` equals one on `t`;
* `0 ≤ f x ≤ 1` for all `x`.
 -/
exists_continuous_zero_one_of_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] {s t : Set X},
  IsCompact s → IsClosed t → Disjoint s t → ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
-- Mathlib.Data.Prod.Basic
Prod.snd_injective : ∀ {α : Type u_1} {β : Type u_2} [Subsingleton α], Function.Injective Prod.snd
-- Std.Async.Process
/-- Number of voluntary context switches (process yielded CPU)
 -/
Std.IO.Process.ResourceUsageStats.voluntaryContextSwitches : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Subalgebra.smul_mem_pointwise_smul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {R' : Type u_3}
  [inst_3 : Semiring R'] [inst_4 : MulSemiringAction R' A] [inst_5 : SMulCommClass R' R A] (m : R') (r : A)
  (S : Subalgebra R A), r ∈ S → m • r ∈ m • S
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.ofRepr.injEq : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (repr repr_1 : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι),
  ({ repr := repr } = { repr := repr_1 }) = (repr = repr_1)
-- Init.Data.UInt.Lemmas
UInt16.add_right_inj : ∀ {a b : UInt16} (c : UInt16), c + a = c + b ↔ a = b
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.left_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f g : a ⟶ b)
  [inst_1 : CategoryTheory.BicategoricalCoherence f g],
  CategoryTheory.BicategoricalCoherence.iso =
    CategoryTheory.Bicategory.leftUnitor f ≪≫ CategoryTheory.BicategoricalCoherence.iso
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G),
  CategoryTheory.Presheaf.IsLocallySurjective J f ↔
    CategoryTheory.Subfunctor.sheafify J
        (CategoryTheory.Subfunctor.range (CategoryTheory.Functor.whiskerRight f (CategoryTheory.forget A))) =
      ⊤
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.Basis.dual_rank_eq : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Finite ι] (b : Module.Basis ι R M), Module.rank R (Module.Dual R M) = Cardinal.lift.{uR, uM} (Module.rank R M)
-- Mathlib.Data.Num.ZNum
Num.toZNum_succ : ∀ (n : Num), n.succ.toZNum = n.toZNum.succ
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_inj : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M]
  {V₁ V₂ : Submodule R M}, Submodule.restrictScalars S V₁ = Submodule.restrictScalars S V₂ ↔ V₁ = V₂
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.c_mul_pf : ∀ {α : Type u_1} {b c : α} [inst : Mul α], b = c → ∀ (a : α), a * b = a * c
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_density_atTop_ae_of_antitone : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : ℕ → Set β),
      Antitone seq →
        ⋂ i, seq i = ∅ →
          (∀ (m : ℕ), MeasurableSet (seq m)) →
            ∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun m => κ.density ν a x (seq m)) Filter.atTop (nhds 0)
-- Mathlib.Tactic.Simproc.VecPerm
/-- Takes an expression representing a vector `Fin n → α` and returns the corresponding
array `Array α`.
 -/
_private.Mathlib.Tactic.Simproc.VecPerm.0.Mathlib.Tactic.FinVec.Matrix.matchVecConsPrefixQ : {u : Lean.Level} →
  {α : Q(Type u)} → {n : Q(ℕ)} → Q(Fin «$n» → «$α») → Lean.MetaM (Array Q(«$α») × (m : Q(ℕ)) × Q(Fin «$m» → «$α»))
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- A profinite space which is light gives rise to a light profinite space.  -/
LightProfinite.toLightDiagram : LightProfinite → LightDiagram
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- `X₁ ×[Y₁] (X₂ ×[Y₂] X₃)` is the pullback `(X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃)`.  -/
CategoryTheory.Limits.pullbackPullbackRightIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ Y₂ : C} →
      (f₁ : X₁ ⟶ Y₁) →
        (f₂ : X₂ ⟶ Y₁) →
          (f₃ : X₂ ⟶ Y₂) →
            (f₄ : X₃ ⟶ Y₂) →
              [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] →
                [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPullback f₁
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] →
                    CategoryTheory.Limits.IsLimit
                      (CategoryTheory.Limits.PullbackCone.mk
                        (CategoryTheory.Limits.pullback.lift
                          (CategoryTheory.Limits.pullback.fst f₁
                            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Limits.pullback.snd f₁
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
                            (CategoryTheory.Limits.pullback.fst f₃ f₄))
                          ⋯)
                        (CategoryTheory.Limits.pullback.snd f₁
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
                        ⋯)
-- Mathlib.Data.Nat.Log
Nat.pow_pred_clog_lt_self : ∀ {b : ℕ}, 1 < b → ∀ {x : ℕ}, 1 < x → b ^ (Nat.clog b x).pred < x
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_sub_partitions : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} (f : (ι → ℝ) → E)
  (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) {π₁ π₂ : BoxIntegral.TaggedPrepartition I},
  π₁.IsPartition →
    π₂.IsPartition →
      BoxIntegral.integralSum f vol π₁ - BoxIntegral.integralSum f vol π₂ =
        ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
          ((vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
            (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)))
-- Init.Prelude
instInhabitedUInt64 : Inhabited UInt64
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.partition_eq_of_isConj : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  IsConj σ τ ↔ σ.partition = τ.partition
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrLemma.mk : List Mathlib.Tactic.GCongr.GCongrKey →
  Lean.Name → Array Mathlib.Tactic.GCongr.GCongrHyp → ℕ → ℕ → ℕ → Bool → Mathlib.Tactic.GCongr.GCongrLemma
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.inr_ofComponents : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂)
  (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂) =
    CategoryTheory.CategoryStruct.comp f₂₁ CategoryTheory.Limits.biprod.inl +
      CategoryTheory.CategoryStruct.comp f₂₂ CategoryTheory.Limits.biprod.inr
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} {c : ℝ},
  c ≠ 0 → (c • x ∈ NumberField.mixedEmbedding.fundamentalCone K ↔ x ∈ NumberField.mixedEmbedding.fundamentalCone K)
-- Init.Data.String.Slice
/-- If `pat` matches a prefix of `s`, returns the position at the start of the remainder.
Returns `none` otherwise.

This function is generic over all currently supported patterns.
 -/
String.Slice.skipPrefix? : {ρ : Type} → (s : String.Slice) → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Option s.Pos
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.findIdxNth.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (x s : ℕ) (h_1 : (x s : ℕ) → motive [] x s)
  (h_2 : (a : α) → (xs : List α) → (s : ℕ) → motive (a :: xs) 0 s)
  (h_3 : (a : α) → (xs : List α) → (n s : ℕ) → motive (a :: xs) n.succ s),
  (match [], x, s with
    | [], x, s => h_1 x s
    | a :: xs, 0, s => h_2 a xs s
    | a :: xs, n.succ, s => h_3 a xs n s) =
    h_1 x s
-- Mathlib.Order.Hom.Basic
/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` into an actual
`OrderHom`. This is declared as the default coercion from `F` to `α →o β`.  -/
OrderHomClass.toOrderHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : FunLike F α β] → [OrderHomClass F α β] → F → α →o β
-- Init.Data.String.Lemmas.FindPos
String.posLE_lt_iff : ∀ {s : String} {p : s.Pos} {q : String.Pos.Raw}, s.posLE q < p ↔ q < p.offset
-- Lean.Data.KVMap
Lean.instCoeIntDataValue : Coe ℤ Lean.DataValue
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.IsTriangulated.instComp : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift ℤ] (G : CategoryTheory.Functor D E) [inst_7 : G.CommShift ℤ]
  [inst_8 : CategoryTheory.Limits.HasZeroObject C] [inst_9 : CategoryTheory.Limits.HasZeroObject D]
  [inst_10 : CategoryTheory.Limits.HasZeroObject E] [inst_11 : CategoryTheory.Preadditive C]
  [inst_12 : CategoryTheory.Preadditive D] [inst_13 : CategoryTheory.Preadditive E]
  [inst_14 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_15 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
  [inst_16 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [inst_17 : CategoryTheory.Pretriangulated C]
  [inst_18 : CategoryTheory.Pretriangulated D] [inst_19 : CategoryTheory.Pretriangulated E] [F.IsTriangulated]
  [G.IsTriangulated], (F.comp G).IsTriangulated
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.instPreservesLimitsOfShapeCarrierDiscreteFunctorOfNonemptyOfFinite : ∀ {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {ι : Type u_1}
  [Nonempty ι] [Finite ι], CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ι) hf.functor
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
integrally closed and Noetherian, the integral closure `C` of `A` in `L` is
Noetherian over `A`.  -/
IsIntegralClosure.isNoetherian : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] (C : Type u_4) [inst_5 : CommRing C] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
  [IsScalarTower A K L] [inst_9 : Algebra C L] [IsIntegralClosure C A L] [inst_11 : Algebra A C] [IsScalarTower A C L]
  [FiniteDimensional K L] [IsDomain A] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing A],
  IsNoetherian A C