mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fin.Tuple.Basic
Fin.removeNth_apply : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i) (i : Fin n),
  p.removeNth f i = f (p.succAbove i)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitMulAux.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (x y : (j : J) × ↑(F.obj j)),
  MonCat.FilteredColimits.colimitMulAux F x y =
    MonCat.FilteredColimits.M.mk F
      ⟨CategoryTheory.IsFiltered.max x.fst y.fst,
        (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.IsFiltered.leftToMax x.fst y.fst))) x.snd *
          (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.IsFiltered.rightToMax x.fst y.fst))) y.snd⟩
-- Mathlib.Order.SupClosed
supClosed_preimage_ofDual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, SupClosed (⇑OrderDual.ofDual ⁻¹' s) ↔ InfClosed s
-- Mathlib.Tactic.ITauto
/-- Skip the continuation and return a failed proof if the Boolean is false.  -/
Mathlib.Tactic.ITauto.whenOk : Bool →
  Mathlib.Tactic.ITauto.IProp →
    StateM ℕ (Bool × Mathlib.Tactic.ITauto.Proof) → StateM ℕ (Bool × Mathlib.Tactic.ITauto.Proof)
-- Init.Data.List.Sublist
List.takeWhile_prefix : ∀ {α : Type u_1} {l : List α} (p : α → Bool), List.takeWhile p l <+: l
-- Mathlib.Topology.Algebra.Monoid
nhds_add_nhds_zero : ∀ {M : Type u_6} [inst : AddZeroClass M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] (a : M),
  nhds a + nhds 0 = nhds a
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₁' : CategoryTheory.MorphismProperty D₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [W₁'.RespectsIso] [W₂'.RespectsIso] [L.IsInduced]
  [L.functor.IsEquivalence] [R.IsInduced] [R.functor.IsEquivalence]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor),
  T.IsRightDerivabilityStructure ↔ B.IsRightDerivabilityStructure
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
/-- For ideals in a Dedekind domain, to divide is to contain.  -/
Ideal.dvd_iff_le : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {I J : Ideal A}, I ∣ J ↔ J ≤ I
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.support_expand : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R),
  Function.support ((PowerSeries.expand p hp) φ) = (fun x => p • x) '' Function.support φ
-- Init.Data.SInt.Basic
/-- Obtain the `BitVec` that contains the 2's complement representation of the `Int32`.
 -/
Int32.toBitVec : Int32 → BitVec 32
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.mk.sizeOf_spec : ∀ (eAssignment : Array (Option Lean.Expr)) (uAssignment : Array (Option Lean.Level))
  (ePending : Array (Lean.Expr × Lean.Expr)) (uPending : Array (Lean.Level × Lean.Level))
  (iPending : Array (Lean.Expr × Lean.Expr)) (tPending : Array ℕ) (us : List Lean.Level) (args : Array Lean.Expr),
  sizeOf
      { eAssignment := eAssignment, uAssignment := uAssignment, ePending := ePending, uPending := uPending,
        iPending := iPending, tPending := tPending, us := us, args := args } =
    1 + sizeOf eAssignment + sizeOf uAssignment + sizeOf ePending + sizeOf uPending + sizeOf iPending +
          sizeOf tPending +
        sizeOf us +
      sizeOf args
-- Lean.DocString.Extension
Lean.VersoModuleDocs.Snippet.mk : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) →
  Array (ℕ × Lean.DeclarationRange × Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty) →
    Lean.DeclarationRange → Lean.VersoModuleDocs.Snippet
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.isRestricted_abs_iff : ∀ {R : Type u_1} [inst : NormedRing R] {σ : Type u_2} (c : σ → ℝ) (f : MvPowerSeries σ R),
  MvPowerSeries.IsRestricted |c| f ↔ MvPowerSeries.IsRestricted c f
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_eq_self : ∀ {f : Ordinal.{u} → Ordinal.{u}} {a : Ordinal.{u}}, f a = a → Ordinal.nfp f a = a
-- Mathlib.Data.Multiset.OrderedMonoid
Multiset.instIsOrderedCancelAddMonoid : ∀ {α : Type u_1}, IsOrderedCancelAddMonoid (Multiset α)
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- If `‖pₙ‖ rⁿ` is bounded in `n`, then the radius of `p` is at least `r`.  -/
FormalMultilinearSeries.le_radius_of_bound : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (C : ℝ) {r : NNReal}, (∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C) → ↑r ≤ p.radius
-- Lean.Meta.Tactic.Grind.Types
/-- Pushes `lhs = rhs` with `proof` to `newEqs`.  -/
Lean.Meta.Grind.pushEq : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {outWidth : ℕ} {aig : Std.Sat.AIG α} {w : ℕ} (idx : ℕ)
  (x x_1 : aig.RefVec w),
  x = x_1 →
    ∀ (acc acc_1 : aig.RefVec (w * idx)),
      acc = acc_1 →
        ∀ (h : idx ≤ w) (h' : outWidth = w * w),
          Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go idx x acc h h' =
            Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go idx x_1 acc_1 h h'
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_non_aestronglyMeasurable : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {f : X → E},
  ¬MeasureTheory.AEStronglyMeasurable f μ.variation → ∫ᵛ (a : X), f a ∂[B; μ] = 0
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.CorePlotsOn.mk : {X : Type u_1} →
  (isPlotOn : {n : ℕ} → {u : Set (EuclideanSpace ℝ (Fin n))} → IsOpen u → (EuclideanSpace ℝ (Fin n) → X) → Prop) →
    (∀ {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p q : EuclideanSpace ℝ (Fin n) → X},
        Set.EqOn p q u → (isPlotOn hu p ↔ isPlotOn hu q)) →
      (isPlot : {n : ℕ} → (EuclideanSpace ℝ (Fin n) → X) → Prop) →
        autoParam (∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X}, isPlotOn ⋯ p ↔ isPlot p)
            DiffeologicalSpace.CorePlotsOn.isPlotOn_univ._autoParam →
          (∀ {n : ℕ} (x : X), isPlot fun x_1 => x) →
            (∀ {n m : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {v : Set (EuclideanSpace ℝ (Fin m))} {hu : IsOpen u}
                (hv : IsOpen v) {p : EuclideanSpace ℝ (Fin n) → X}
                {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
                Set.MapsTo f v u → isPlotOn hu p → ContDiffOn ℝ (↑⊤) f v → isPlotOn hv (p ∘ f)) →
              (∀ {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p : EuclideanSpace ℝ (Fin n) → X},
                  (∀ x ∈ u, ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ isPlotOn hv p) → isPlotOn hu p) →
                (dTopology : TopologicalSpace X) →
                  autoParam
                      (∀ {u : Set X},
                        TopologicalSpace.IsOpen u ↔
                          ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), isPlot p → IsOpen (p ⁻¹' u))
                      DiffeologicalSpace.CorePlotsOn.isOpen_iff_preimages_plots._autoParam →
                    DiffeologicalSpace.CorePlotsOn X
-- Mathlib.Order.SupClosed
infClosed_preimage_toDual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set αᵒᵈ}, InfClosed (⇑OrderDual.toDual ⁻¹' s) ↔ SupClosed s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.mk : Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof → Lean.Meta.Grind.Arith.Cutsat.LeCnstr
-- Init.Data.Iterators.ToIterator
Std.ToIterator.iterMInternal : {γ : Type u} → {m : Type w → Type w'} → {α β : outParam (Type w)} → [self : Std.ToIterator γ m α β] → γ → Std.IterM m β
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.one_add_lt_of_lt : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ b → a < b → 1 + a < b
-- Init.Data.SInt.Lemmas
Int32.le_refl : ∀ (a : Int32), a ≤ a
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv.match_1.congr_eq_1 : ∀ (motive : ℕ × ℕ → Sort u_1) (x : ℕ × ℕ) (h_1 : (e q : ℕ) → motive (e, q)) (e q : ℕ),
  x = (e, q) →
    (match x with
      | (e, q) => h_1 e q) ≍
      h_1 e q
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply : ∀ {R : Type u} [inst : CommRing R] (e : { e // IsIdempotentElem e }),
  ↑(PrimeSpectrum.isIdempotentElemEquivClopens e) = ↑(PrimeSpectrum.basicOpen ↑e)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.wellFoundedLT_of_isArtinian : ∀ (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] [IsArtinian R M], WellFoundedLT (LieSubmodule R L M)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRight_comp : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h)
        (CategoryTheory.Bicategory.associator f' g h).hom)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.ext : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β},
  (∀ (a : α), κ a = η a) → κ = η
-- Mathlib.Tactic.Linter.UnusedInstancesInType
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern.mk.inj : ∀ {fvarId : Lean.FVarId} {idx : ℕ} {fvarId_1 : Lean.FVarId} {idx_1 : ℕ},
  { fvarId := fvarId, idx := idx } = { fvarId := fvarId_1, idx := idx_1 } → fvarId = fvarId_1 ∧ idx = idx_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ENode.mk.inj : ∀ {self next root congr : Lean.Expr} {target? proof? : Option Lean.Expr} {flipped : Bool} {size : ℕ}
  {interpreted ctor hasLambdas heqProofs : Bool} {idx generation mt : ℕ} {sTerms : Lean.Meta.Grind.SolverTerms}
  {funCC : Bool} {ematchDiagSource : Lean.Meta.Grind.EMatchDiagSource} {self_1 next_1 root_1 congr_1 : Lean.Expr}
  {target?_1 proof?_1 : Option Lean.Expr} {flipped_1 : Bool} {size_1 : ℕ}
  {interpreted_1 ctor_1 hasLambdas_1 heqProofs_1 : Bool} {idx_1 generation_1 mt_1 : ℕ}
  {sTerms_1 : Lean.Meta.Grind.SolverTerms} {funCC_1 : Bool} {ematchDiagSource_1 : Lean.Meta.Grind.EMatchDiagSource},
  { self := self, next := next, root := root, congr := congr, target? := target?, proof? := proof?, flipped := flipped,
        size := size, interpreted := interpreted, ctor := ctor, hasLambdas := hasLambdas, heqProofs := heqProofs,
        idx := idx, generation := generation, mt := mt, sTerms := sTerms, funCC := funCC,
        ematchDiagSource := ematchDiagSource } =
      { self := self_1, next := next_1, root := root_1, congr := congr_1, target? := target?_1, proof? := proof?_1,
        flipped := flipped_1, size := size_1, interpreted := interpreted_1, ctor := ctor_1, hasLambdas := hasLambdas_1,
        heqProofs := heqProofs_1, idx := idx_1, generation := generation_1, mt := mt_1, sTerms := sTerms_1,
        funCC := funCC_1, ematchDiagSource := ematchDiagSource_1 } →
    self = self_1 ∧
      next = next_1 ∧
        root = root_1 ∧
          congr = congr_1 ∧
            target? = target?_1 ∧
              proof? = proof?_1 ∧
                flipped = flipped_1 ∧
                  size = size_1 ∧
                    interpreted = interpreted_1 ∧
                      ctor = ctor_1 ∧
                        hasLambdas = hasLambdas_1 ∧
                          heqProofs = heqProofs_1 ∧
                            idx = idx_1 ∧
                              generation = generation_1 ∧
                                mt = mt_1 ∧ sTerms = sTerms_1 ∧ funCC = funCC_1 ∧ ematchDiagSource = ematchDiagSource_1
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_hom : ∀ {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.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F]
  (X Y : D),
  ((CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp L W F G).μIso X Y).hom =
    ((CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost L W F G).hom.app X).app Y
-- Mathlib.Order.Concept
Concept.ext_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c = d ↔ c.extent = d.extent
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instFunLike : {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] → FunLike (P →ᴬ[R] Q) P Q
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_union_of_not_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (∀ a ∈ m₁, a ∉ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.instBEqPoly.beq.match_1.splitter : (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) →
  (x x_1 : Lean.Grind.Linarith.Poly) →
    (Unit → motive Lean.Grind.Linarith.Poly.nil Lean.Grind.Linarith.Poly.nil) →
      ((a : ℤ) →
          (a_1 : Lean.Grind.Linarith.Var) →
            (a_2 : Lean.Grind.Linarith.Poly) →
              (b : ℤ) →
                (b_1 : Lean.Grind.Linarith.Var) →
                  (b_2 : Lean.Grind.Linarith.Poly) →
                    motive (Lean.Grind.Linarith.Poly.add a a_1 a_2) (Lean.Grind.Linarith.Poly.add b b_1 b_2)) →
        ((x x_2 : Lean.Grind.Linarith.Poly) →
            (x = Lean.Grind.Linarith.Poly.nil → x_2 = Lean.Grind.Linarith.Poly.nil → False) →
              (∀ (a : ℤ) (a_1 : Lean.Grind.Linarith.Var) (a_2 : Lean.Grind.Linarith.Poly) (b : ℤ)
                  (b_1 : Lean.Grind.Linarith.Var) (b_2 : Lean.Grind.Linarith.Poly),
                  x = Lean.Grind.Linarith.Poly.add a a_1 a_2 → x_2 = Lean.Grind.Linarith.Poly.add b b_1 b_2 → False) →
                motive x x_2) →
          motive x x_1
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.indep_iff_eRk_eq_encard_of_finite : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, I.Finite → (M.Indep I ↔ M.eRk I = I.encard)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.isSome_succMany?_of_lt_size_toArray : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ}, i < r.toArray.size → (Std.PRange.succMany? i r.lower).isSome = true
-- Lean.Elab.Do.InferControlInfo
/-- When `true`, asserts that the next doElem in the enclosing sequence is semantically irrelevant
(control never falls through to it). `false` asserts nothing.
 -/
Lean.Elab.Do.ControlInfo.noFallthrough : Lean.Elab.Do.ControlInfo → Bool
-- Mathlib.LinearAlgebra.Matrix.Ideal
Ideal.matrix_bot : ∀ {R : Type u_1} [inst : Semiring R] (n : Type u_2) [inst_1 : Fintype n] [inst_2 : DecidableEq n], Ideal.matrix n ⊥ = ⊥
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {X Y : B} (a : X ⟶ Y),
  (CategoryTheory.StrictlyUnitaryPseudofunctor.mk' S).map a = S.map a
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_nnnorm_replicateCol : ∀ {n : Type u_4} {α : Type u_5} {ι : Type u_7} [inst : Fintype n] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : n → α), ‖Matrix.replicateCol ι v‖₊ = ‖WithLp.toLp 2 v‖₊
-- Mathlib.Topology.Category.Profinite.Extend
/-- Given a functor `G` from `Profinite` and `S : Profinite`, we obtain a cone on
`(StructuredArrow.proj S toProfinite ⋙ toProfinite ⋙ G)` with cone point `G.obj S`.

Whiskering this cone with `Profinite.Extend.functor c` gives `G.mapCone c` as we check in the
example below.
 -/
Profinite.Extend.cone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (G : CategoryTheory.Functor Profinite C) →
      (S : Profinite) →
        CategoryTheory.Limits.Cone
          ((CategoryTheory.StructuredArrow.proj S FintypeCat.toProfinite).comp (FintypeCat.toProfinite.comp G))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_inter_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₂.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeWhile₂_eq_takeWhile₂TR.go : ∀ (α : Type u_2) (β : Type u_1) (R : α → β → Bool) (as : List α) (bs : List β) (acca : List α) (accb : List β),
  List.takeWhile₂TR.go R as bs acca accb =
    (acca.reverse ++ (List.takeWhile₂ R as bs).1, accb.reverse ++ (List.takeWhile₂ R as bs).2)
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Embedding of a magma with zero `M`, into its magma algebra, having `M` as source.  -/
AddMonoidAlgebra.of' : (R : Type u_8) → (M : Type u_9) → [inst : Semiring R] → M → AddMonoidAlgebra R M
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.ite_zero_sum : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (p : Prop) [inst_1 : Decidable p] (s : Finset ι) (f : ι → M),
  (if p then 0 else ∑ x ∈ s, f x) = ∑ x ∈ s, if p then 0 else f x
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- The property of being separated for some presieve is preserved under isomorphisms.  -/
CategoryTheory.Presieve.isSeparatedFor_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} {P' : CategoryTheory.Functor Cᵒᵖ (Type w)} (i : P ≅ P'),
  CategoryTheory.Presieve.IsSeparatedFor P R → CategoryTheory.Presieve.IsSeparatedFor P' R
-- Mathlib.Tactic.DepRewrite
/-- Insert casts whenever necessary.  -/
Mathlib.Tactic.DepRewrite.CastMode.all : Mathlib.Tactic.DepRewrite.CastMode
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIicIoi_apply_inr : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α} (a : ↑(Set.Ioi x)), (OrderIso.sumLexIicIoi x) (toLex (Sum.inr a)) = ↑a
-- Mathlib.Combinatorics.Graph.Subgraph
/-- `H ≤i G` (`Graph.IsInducedSubgraph`) is a subgraph of `G` such that every link of `G`
involving two vertices of `H` is also a link of `H`.  -/
Graph.«term_≤i_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.toJordanDecomposition_neg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
  (-s).toJordanDecomposition = -s.toJordanDecomposition
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.addSimpCongrTheoremEntry : Lean.Meta.SimpCongrTheorems → Lean.Meta.SimpCongrTheorem → Lean.Meta.SimpCongrTheorems
-- Mathlib.Algebra.Category.MonCat.Basic
MulEquiv.toMonCatIso_inv : ∀ {X Y : Type u} [inst : Monoid X] [inst_1 : Monoid Y] (e : X ≃* Y), e.toMonCatIso.inv = MonCat.ofHom e.symm.toMonoidHom
-- Mathlib.Topology.Covering.Basic
/-- If `f : E → X` is a closed map between topological spaces with `E` Hausdorff, and `s` is
a subset of `X` on which `f` has finite fibers, such that `f` restricts to a homeomorphism on
a neighborhood of every point of `f ⁻¹' s`, then `f` is a covering map on `s`.  -/
IsClosedMap.isCoveringMapOn_of_isLocalHomeomorphOn : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X}
  [T2Space E], IsClosedMap f → (∀ x ∈ s, (f ⁻¹' {x}).Finite) → IsLocalHomeomorphOn f (f ⁻¹' s) → IsCoveringMapOn f s
-- Init.Data.Int.DivMod.Bootstrap
_private.Init.Data.Int.DivMod.Bootstrap.0.Int.ediv.match_1.eq_5 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (a : ℕ) → motive (Int.negSucc a) 0)
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc a, 0 => h_3 a
    | Int.negSucc m, Int.ofNat n.succ => h_4 m n
    | Int.negSucc m, Int.negSucc n => h_5 m n) =
    h_5 m n
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves finite products, then `F.rightOp : C ⥤ Dᵒᵖ` preserves finite
coproducts.  -/
CategoryTheory.Limits.preservesFiniteCoproducts_rightOp : ∀ {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.PreservesFiniteProducts F],
  CategoryTheory.Limits.PreservesFiniteCoproducts F.rightOp
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the first quadrant. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open first quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open first quadrant
  for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of the first quadrant.

Then `‖f z‖` is bounded from above by the same constant on the closed first quadrant.  -/
PhragmenLindelof.quadrant_I : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
  DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C) → (∀ (x : ℝ), 0 ≤ x → ‖f (↑x * Complex.I)‖ ≤ C) → 0 ≤ z.re → 0 ≤ z.im → ‖f z‖ ≤ C
-- Mathlib.Order.Directed
directed_of : ∀ {α : Type u_1} (r : α → α → Prop) [IsDirected α r] (a b : α), ∃ c, r a c ∧ r b c
-- Mathlib.Order.Comparable
/-- **Alias** of `not_incompRel_of_total`. -/
IsTotal.not_incompRel : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Total r] (a b : α), ¬IncompRel r a b
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- A def to put an `Zero` instance on a type with a `Language.ring.Structure` instance.

To be used sparingly, usually only when defining a more useful definition like,
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K`  -/
FirstOrder.Ring.zeroOfRingStructure : (R : Type u_2) → [FirstOrder.Language.ring.Structure R] → Zero R