mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- The measurable equivalence between the `realMixedSpace` and the `polarSpace`. It is actually an
homeomorphism, see `homeoRealMixedSpacePolarSpace`, but defining it in this way makes it easier
to prove that it is volume preserving, see `volume_preserving_homeoRealMixedSpacePolarSpace`.
 -/
NumberField.mixedEmbedding.measurableEquivRealMixedSpacePolarSpace : (K : Type u_1) →
  [inst : Field K] → NumberField.mixedEmbedding.realMixedSpace K ≃ᵐ NumberField.mixedEmbedding.polarSpace K
-- Mathlib.Data.Fin.SuccPred
Fin.val_sub_castLT_of_lt : ∀ {n m : ℕ} {a b : Fin m} (hb : ↑b < n) (h : a < b), ↑(a.castLT ⋯ - b.castLT hb) = ↑(a - b) + n - m
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.match_1.eq_2 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 :
    ByteArray.utf8DecodeChar?.FirstByte.done = ByteArray.utf8DecodeChar?.FirstByte.invalid →
      motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 :
    ByteArray.utf8DecodeChar?.FirstByte.done = ByteArray.utf8DecodeChar?.FirstByte.done →
      motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 :
    ByteArray.utf8DecodeChar?.FirstByte.done = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 :
    ByteArray.utf8DecodeChar?.FirstByte.done = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 :
    ByteArray.utf8DecodeChar?.FirstByte.done = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
      motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match h : ByteArray.utf8DecodeChar?.FirstByte.done with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) =
    h_2 ⋯
-- Mathlib.Algebra.Homology.LeftResolution.Transport
/-- Transport `LeftResolution` via equivalences of categories.  -/
CategoryTheory.Abelian.LeftResolution.transport : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {A' : Type u_3} →
          {C' : Type u_4} →
            [inst_2 : CategoryTheory.Category.{v_3, u_4} C'] →
              [inst_3 : CategoryTheory.Category.{v_4, u_3} A'] →
                {ι : CategoryTheory.Functor C A} →
                  CategoryTheory.Abelian.LeftResolution ι →
                    {ι' : CategoryTheory.Functor C' A'} →
                      (eA : A' ≌ A) →
                        (eC : C' ≌ C) →
                          (ι'.comp eA.functor ≅ eC.functor.comp ι) → CategoryTheory.Abelian.LeftResolution ι'
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.eq_1 : ∀ {α : Type u} (s : Set α), s.Finite = Finite ↑s
-- Init.Data.Vector.Extract
Vector.extract_succ_right : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (w : i < j + 1) (h : j < n),
  xs.extract i (j + 1) = Vector.cast ⋯ ((xs.extract i j).push xs[j])
-- Lean.Compiler.IR.Basic
Lean.IR.Param : Type
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A uniform limit on a set of functions which are continuous on this set is itself continuous
on this set.  -/
TendstoUniformlyOn.continuousOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι},
  TendstoUniformlyOn F f p s → (∃ᶠ (n : ι) in p, ContinuousOn (F n) s) → ContinuousOn f s
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.Λ'.Supports.match_1.eq_3 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.read q with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k s q => h_2 k s q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret k => h_8 k) =
    h_3 q
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_neg_fun : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E] (f : k → E),
  slope (-f) = -slope f
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- Given a finite monoid `M` with unit group `Mˣ` cyclic of order `n` and an `n`th root of
unity `ζ` in `R`, there is a multiplicative character `M → R` that sends a given generator
of `Mˣ` to `ζ`.  -/
MulChar.ofRootOfUnity : {M : Type u_1} →
  [inst : CommMonoid M] →
    [inst_1 : Fintype M] →
      [inst_2 : DecidableEq M] →
        {R : Type u_2} →
          [inst_3 : CommMonoidWithZero R] →
            {ζ : Rˣ} →
              ζ ∈ rootsOfUnity (Fintype.card Mˣ) R → {g : Mˣ} → (∀ (x : Mˣ), x ∈ Subgroup.zpowers g) → MulChar M R
-- Mathlib.Topology.UniformSpace.CompareReals
CompareReals.compare_uc : UniformContinuous ⇑CompareReals.compareEquiv
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.opEquivOpUnder_unitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T),
  (CategoryTheory.Over.opEquivOpUnder X).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Over (Opposite.op X)))
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
IsLUB.csSup_eq : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, IsLUB s a → s.Nonempty → sSup s = a
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn_ι : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c) (f.filtration j).ι =
    CategoryTheory.CategoryStruct.comp c.horn.ι c.map
-- Mathlib.GroupTheory.Torsion
/-- The free rank of a finitely generated abelian group is the rank of its free part.  -/
CommGroup.freeRank : (G : Type u_1) → [inst : CommGroup G] → [Group.FG G] → ℕ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If `f` is an integrable periodic function with period `T`, and `n` is an integer, then its
integral over `[t, t + n • T]` is `n` times its integral over `[t, t + T]`.  -/
Function.Periodic.intervalIntegral_add_zsmul_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
  Function.Periodic f T →
    ∀ (n : ℤ) (t : ℝ),
      (∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.volume t₁ t₂) →
        ∫ (x : ℝ) in t..t + n • T, f x = n • ∫ (x : ℝ) in t..t + T, f x
-- Init.Data.String.Subslice
String.Slice.Subslice.endExclusive_ofSliceFrom : ∀ {s : String.Slice} {p : s.Pos} {sl : (s.sliceFrom p).Subslice},
  sl.ofSliceFrom.endExclusive = String.Slice.Pos.ofSliceFrom sl.endExclusive
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- Coinduction principle for proving that an operation is friendly.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.coind : ∀ {α : Type u_1} (motive : (Stream'.Seq α → Stream'.Seq α) → Prop) {op : Stream'.Seq α → Stream'.Seq α},
  motive op →
    (∀ (op : Stream'.Seq α → Stream'.Seq α),
        motive op →
          ∃ T,
            ∀ (s : Stream'.Seq α),
              (op s).destruct =
                Option.map
                  (fun x =>
                    match x with
                    | (hd, op') => (hd, ↑op' s.tail))
                  (T s.head)) →
      Tactic.ComputeAsymptotics.Seq.FriendlyOperation op
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.rankTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.HeapNode α → ℕ → Sort u_2) (a : α)
  (child s : Batteries.BinomialHeap.Imp.HeapNode α) (r : ℕ)
  (h_1 : (r : ℕ) → motive Batteries.BinomialHeap.Imp.HeapNode.nil r)
  (h_2 :
    (a : α) →
      (child s : Batteries.BinomialHeap.Imp.HeapNode α) →
        (r : ℕ) → motive (Batteries.BinomialHeap.Imp.HeapNode.node a child s) r),
  (match Batteries.BinomialHeap.Imp.HeapNode.node a child s, r with
    | Batteries.BinomialHeap.Imp.HeapNode.nil, r => h_1 r
    | Batteries.BinomialHeap.Imp.HeapNode.node a child s, r => h_2 a child s r) =
    h_2 a child s r
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.add_mem_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x y : AddUnits M},
  x ∈ S.addUnits → y ∈ S.addUnits → x + y ∈ S.addUnits
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.isReservedName : Lean.Environment → Lean.Name → Bool
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.instInhabitedExpr : Inhabited Nat.Internal.SOM.Expr
-- Mathlib.Data.Fin.Init
Fin.xor_comm : ∀ {k : ℕ} (a b : Fin k), a ^^^ b = b ^^^ a
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.instIsStableUnderShiftTriangEnvelopeInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.triangEnvelope.IsStableUnderShift ℤ
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.algHom_ext : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (I : Ideal S) [IsAdicComplete I S] [inst_4 : CommRing A] [inst_5 : Algebra R A] {f g : A →ₐ[R] S},
  (∀ (n : ℕ), (Ideal.Quotient.mkₐ R (I ^ n)).comp f = (Ideal.Quotient.mkₐ R (I ^ n)).comp g) → f = g
-- Lean.Data.Lsp.InitShutdown
/-- Not used by the language server. We use the cwd of the server process instead.  -/
Lean.Lsp.InitializeParams.rootUri? : Lean.Lsp.InitializeParams → Option String
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.lt_arcsin_iff_sin_lt : ∀ {x y : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → y ∈ Set.Icc (-1) 1 → (x < Real.arcsin y ↔ Real.sin x < y)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_const_iff : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {l : Filter α} {c : F''},
  (f'' =O[l] fun _x => c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖
-- Mathlib.Topology.Sets.VietorisTopology
Topology.IsInducing.compacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsInducing f), Topology.IsInducing (TopologicalSpace.Compacts.map f ⋯)
-- Mathlib.Data.Set.Image
Set.image_preimage_eq_range_inter : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set β}, f '' f ⁻¹' t = Set.range f ∩ t
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.absolutelyContinuous_comp_of_countable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [Countable α] [MeasurableSingletonClass α],
  ∀ᵐ (ω : α) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- Help the typechecker by converting a path in a topological space to an arrow in the
fundamental groupoid of that space.  -/
FundamentalGroupoid.fromPath : {X : Type u_1} →
  [inst : TopologicalSpace X] → {x₀ x₁ : X} → Path.Homotopic.Quotient x₀ x₁ → ({ as := x₀ } ⟶ { as := x₁ })
-- Mathlib.Algebra.BigOperators.Finprod
finsum_of_not_hasFiniteSupport : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M}, ¬Function.HasFiniteSupport f → ∑ᶠ (i : α), f i = 0
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMonoid.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → Monoid (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instMonoid =
    { toSemigroup := DirectLimit.instSemigroupOfMulHomClass, toOne := DirectLimit.instMulOneClassOfMonoidHomClass.toOne,
      one_mul := ⋯, mul_one := ⋯, npow := fun n => DirectLimit.map f f (fun x x_1 => x_1 ^ n) ⋯, npow_zero := ⋯,
      npow_succ := ⋯ }
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_const_enorm : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {c : ε},
  ‖c‖ₑ ≠ ⊤ → MeasureTheory.LocallyIntegrable (fun x => c) μ
-- Mathlib.NumberTheory.WellApproximable
mem_add_wellApproximable_iff : ∀ {A : Type u_1} [inst : SeminormedAddGroup A] {δ : ℕ → ℝ} {a : A},
  a ∈ addWellApproximable A δ ↔ a ∈ Filter.blimsup (fun n => approxAddOrderOf A n (δ n)) Filter.atTop fun n => 0 < n
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.propagateDiseqs.go.match_1.eq_3 : ∀ (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1) (id₁ : ℕ) (lhs : Lean.Expr)
  (lhsTerms : Lean.Meta.Grind.SolverTerms) (id₂ : ℕ) (rhs : Lean.Expr) (rhsTerms : Lean.Meta.Grind.SolverTerms)
  (h_1 : (x : Lean.Meta.Grind.SolverTerms) → motive Lean.Meta.Grind.SolverTerms.nil x)
  (h_2 : (x : Lean.Meta.Grind.SolverTerms) → motive x Lean.Meta.Grind.SolverTerms.nil)
  (h_3 :
    (id₁ : ℕ) →
      (lhs : Lean.Expr) →
        (lhsTerms : Lean.Meta.Grind.SolverTerms) →
          (id₂ : ℕ) →
            (rhs : Lean.Expr) →
              (rhsTerms : Lean.Meta.Grind.SolverTerms) →
                motive (Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms)
                  (Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms)),
  (match Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms with
    | Lean.Meta.Grind.SolverTerms.nil, x => h_1 x
    | x, Lean.Meta.Grind.SolverTerms.nil => h_2 x
    | Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms =>
      h_3 id₁ lhs lhsTerms id₂ rhs rhsTerms) =
    h_3 id₁ lhs lhsTerms id₂ rhs rhsTerms
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.StrictOrLazy.lazy.inj : ∀ {α β : Type} {a a_1 : β}, Lean.Widget.StrictOrLazy.lazy a = Lean.Widget.StrictOrLazy.lazy a_1 → a = a_1
-- Mathlib.Topology.Algebra.Ring.Basic
Pi.instIsSemitopologicalRing : ∀ {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (R i)]
  [inst_1 : (i : ι) → NonUnitalNonAssocRing (R i)] [∀ (i : ι), IsSemitopologicalRing (R i)],
  IsSemitopologicalRing ((i : ι) → R i)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_congr : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {φ₁ φ₂ : Prop},
  (φ₁ ↔ φ₂) → Lean.Order.CompleteLattice.ofProp φ₁ = Lean.Order.CompleteLattice.ofProp φ₂
-- Init.Data.Vector.Nat
Vector.sum_eq_foldl_nat : ∀ {n : ℕ} {xs : Vector ℕ n}, xs.sum = Vector.foldl (fun x1 x2 => x1 + x2) 0 xs
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_singleton : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  [hE : CompleteSpace E] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure α} (f : α → E) (a : α),
  ∫ (a : α) in {a}, f a ∂μ = μ.real {a} • f a
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.mrange_nontrivial : ∀ {G : Type u_1} {H : Type u_2} [inst : MulZeroOneClass G] [inst_1 : MulZeroOneClass H] [Nontrivial H] (f : G →*₀ H),
  Nontrivial ↥(MonoidHom.mrange f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- To construct an isomorphism of pullback cones, it suffices to construct an isomorphism
of the cone points and check it commutes with `fst` and `snd`.  -/
CategoryTheory.Limits.PullbackCone.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {s t : CategoryTheory.Limits.PullbackCone f g} →
            (i : s.pt ≅ t.pt) →
              autoParam (s.fst = CategoryTheory.CategoryStruct.comp i.hom t.fst)
                  CategoryTheory.Limits.PullbackCone.ext._auto_1 →
                autoParam (s.snd = CategoryTheory.CategoryStruct.comp i.hom t.snd)
                    CategoryTheory.Limits.PullbackCone.ext._auto_3 →
                  (s ≅ t)
-- Mathlib.Order.Hom.Bounded
TopHom.instSemilatticeInf : {α : Type u_2} →
  {β : Type u_3} → [inst : Top α] → [inst_1 : SemilatticeInf β] → [inst_2 : OrderTop β] → SemilatticeInf (TopHom α β)
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- If `f` has a local min on `s` at `a` and both `y` and `-y` belong to the positive tangent cone
of `s` at `a`, then `f' y = 0`.  -/
IsLocalMinOn.fderivWithin_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {a y : E},
  IsLocalMinOn f s a → y ∈ posTangentConeAt s a → -y ∈ posTangentConeAt s a → (fderivWithin ℝ f s a) y = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits, then `F : C ⥤ D` reflects limits.  -/
CategoryTheory.Limits.reflectsLimits_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimits F.op], CategoryTheory.Limits.ReflectsLimits F
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
CommGrpCat.tensorObj_eq : ∀ (G H : CommGrpCat), CategoryTheory.MonoidalCategoryStruct.tensorObj G H = CommGrpCat.of (↑G × ↑H)
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- Given a sequence of `GenContFract.Pair`s `s = [(a₀, b₀), (a₁, b₁), ...]`, `squashSeq s n`
combines `⟨aₙ, bₙ⟩` and `⟨aₙ₊₁, bₙ₊₁⟩` at position `n` to `⟨aₙ, bₙ + aₙ₊₁ / bₙ₊₁⟩`. For example,
`squashSeq s 0 = [(a₀, b₀ + a₁ / b₁), (a₁, b₁),...]`.
If `s.TerminatedAt (n + 1)`, then `squashSeq s n = s`.
 -/
GenContFract.squashSeq : {K : Type u_1} → [DivisionRing K] → Stream'.Seq (GenContFract.Pair K) → ℕ → Stream'.Seq (GenContFract.Pair K)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.norm_integral_le_lintegral_norm : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (f : α → G), ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- The `essSup` of a function `g` on the quotient space `G ⧸ Γ` with respect to the pushforward
of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental domain `𝓕`, is the
same as the `essSup` of `g`'s lift to the universal cover `G` with respect to `μ`.  -/
essSup_comp_quotientGroup_mk : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : Subgroup G} {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [μ.IsMulRightInvariant]
      {g : G ⧸ Γ → ENNReal},
      AEMeasurable g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) →
        essSup g (MeasureTheory.Measure.map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.instIsIsoHomOfMapForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Comon C} (f : A ⟶ B) [e : CategoryTheory.IsIso ((CategoryTheory.Comon.forget C).map f)],
  CategoryTheory.IsIso f.hom
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.one_le_iff : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R], v.IsEquiv w → ∀ {x : R}, 1 ≤ v x ↔ 1 ≤ w x
-- Init.Prelude
/-- Computes a hash for strings.
 -/
String.hash : String → UInt64
-- Mathlib.Algebra.BigOperators.ModEq
Nat.sum_modEq_single : ∀ {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α} {a : α},
  (a ∉ s → f a ≡ 0 [MOD n]) → (∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]) → ∑ x ∈ s, f x ≡ f a [MOD n]
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ext_iff : ∀ {𝕜₁ : 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] {A B : E →SWOT[σ] F},
  A = B ↔ ∀ (x : E), A x = B x
-- Mathlib.Data.List.OfFn
Fin.repeat.eq_1 : ∀ {n : ℕ} {α : Sort u_1} (m : ℕ) (a : Fin n → α) (x : Fin (m * n)), Fin.repeat m a x = a x.modNat
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_sphere' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.sphere x ε ↔ dist x y = ε
-- Mathlib.Algebra.Group.ForwardDiff
/-- Forward difference operator, `fwdDiff h f n = f (n + h) - f n`. The notation `Δ_[h]` for this
operator is available in the `fwdDiff` namespace.
 -/
fwdDiff.«termΔ_[_]» : Lean.ParserDescr
-- Lean.Meta.CtorRecognizer
_private.Lean.Meta.CtorRecognizer.0.Lean.Meta.getConstructorVal? : Lean.Environment → Lean.Name → Option Lean.ConstructorVal
-- Mathlib.Algebra.Group.Int.Even
Int.even_add : ∀ {m n : ℤ}, Even (m + n) ↔ (Even m ↔ Even n)
-- Mathlib.SetTheory.Cardinal.Free
Cardinal.mk_freeAddMonoid : ∀ (α : Type u) [Nonempty α], Cardinal.mk (FreeAddMonoid α) = max (Cardinal.mk α) Cardinal.aleph0
-- Mathlib.Algebra.Ring.Subring.Basic
/-- If two ring homomorphisms are equal on a set, then they are equal on its subring closure.  -/
RingHom.eqOn_set_closure : ∀ {R : Type u} [inst : NonAssocRing R] {S : Type v} [inst_1 : Semiring S] {f g : R →+* S} {s : Set R},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subring.closure s)
-- Batteries.Data.Array.Scan
Array.getElem?_scanr : ∀ {α : Type u_1} {β : Type u_2} {b : β} {as : Array α} {i : ℕ} {f : α → β → β},
  (Array.scanr f b as)[i]? = if i < as.size + 1 then some (Array.foldr f b (as.drop i)) else none
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_transpose_eq_transpose_conjTranspose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Star α] (M : Matrix m n α),
  M.transpose.conjTranspose = M.conjTranspose.transpose
-- Mathlib.Analysis.LocallyConvex.WeakDual
LinearMap.mem_span_iff_bound : ∀ {ι : Type u_4} {𝕜 : Type u_5} {E : Type u_6} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜),
  φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ s c, φ.toSeminorm ≤ c • s.sup fun i => (f i).toSeminorm