mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Lean.MessageData.ForExprs
/-- `for (ppCtx, e) in msg.exprs do` iterates through the expressions in `MessageData` together
with their `ppCtx : PPContext`. The `ppCtx` can be used to interpret the expression in a valid
`MetaM` context via `ppCtx.runMetaM`.

The monad must support `BaseIO` in order to interpret `.ofLazy` nodes in `MessageData`.

Expressions without a valid `ppCtx` are skipped.  -/
Lean.MessageData.exprs : Lean.MessageData → Lean.MessageData.Exprs
-- Mathlib.Topology.Category.TopCat.Sphere
/-- `𝕊 n` denotes the `n`-sphere.  -/
TopCat.term𝕊_ : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- A homology map data for a morphism of short complexes induces
a homology map data in the opposite category.  -/
CategoryTheory.ShortComplex.HomologyMapData.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.HomologyData} →
            {h₂ : S₂.HomologyData} →
              CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.ShortComplex.opMap φ) h₂.op h₁.op
-- Mathlib.Data.Set.Prod
/-- **Vertical line test** for functions.

Let `f : α → β × γ` be a function to a product. Assume that `f` is surjective on the first factor
and that the image of `f` intersects every "vertical line" `{(b, c) | c : γ}` at most once.
Then the image of `f` is the graph of some monoid homomorphism `f' : β → γ`.  -/
Set.exists_range_eq_graphOn_univ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β × γ},
  Function.Surjective (Prod.fst ∘ f) →
    (∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) → ∃ f', Set.range f = Set.graphOn f' Set.univ
-- Mathlib.Tactic.Linter.Header
/-- `toSyntax s pattern` converts the two input strings into a `Syntax`, assuming that `pattern`
is a substring of `s`:
the syntax is an atom with value `pattern` whose the range is the range of `pattern` in `s`.  -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.toSyntax : String → String → optParam String.Pos.Raw 0 → Lean.Syntax
-- Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Complex.volume_preserving_equiv_pi : MeasureTheory.MeasurePreserving (⇑Complex.measurableEquivPi) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Iso.connected_iff : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (e : G ≃g H), G.Connected ↔ H.Connected
-- Init.Coe
instCoeHTC : {α : Sort u_1} → CoeHTC α α
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftComp_inv_app_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (X : CategoryTheory.Comma L₃ R),
  ((CategoryTheory.Comma.mapLeftComp R l l').inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Init.Data.List.Lemmas
List.length_filter_le : ∀ {α : Type u_1} (p : α → Bool) (l : List α), (List.filter p l).length ≤ l.length
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.tensorHom_def : ∀ (R : Type u) [inst : CommRing R] {X₁ Y₁ X₂ Y₂ : BialgCat R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    BialgCat.ofHom (Bialgebra.TensorProduct.map f.toBialgHom' g.toBialgHom')
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_3 : Inhabited α] {l : List α} {k : α},
  l.contains k = false → (Std.ExtTreeMap.unitOfList l cmp).getKey! k = default
-- Mathlib.Algebra.Group.Defs
nsmulRec'_two_add : ∀ {M : Type u_2} [inst : AddSemigroup M] [inst_1 : Zero M] (k : ℕ) (m : M), nsmulRec' (2 * k) m = nsmulRec' k (m + m)
-- Batteries.Recycling.RBTree.Basic
/-- True if `x` is an element of `t` "exactly", i.e. up to equality, not the `cmp` relation.  -/
RBTree.RBSet.EMem : {α : Type u_1} → {cmp : α → α → Ordering} → α → RBTree.RBSet α cmp → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `HasStrictFDerivAt.smul` -/
HasStrictFDerivAt.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'},
  HasStrictFDerivAt c c' x →
    HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun i => c i • f i) (c x • f' + c'.smulRight (f x)) x
-- Aesop.Saturate
Aesop.saturateMain' : Aesop.LocalRuleSet → Lean.MVarId → Aesop.SaturateM Lean.MVarId
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.setFinite_index : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] {s : Set (ι → ℝ)},
  MeasureTheory.NullMeasurableSet s MeasureTheory.volume →
    MeasureTheory.volume s ≠ ⊤ → {ν | ↑(BoxIntegral.unitPartition.box n ν) ⊆ s}.Finite
-- Init.Data.Vector.Basic
/-- Shrinks a vector to the first `m` elements, by repeatedly popping the last element.

We immediately simplify this to the `extract` operation, so there is no verification API for this function.
 -/
Vector.shrink : {α : Type u_1} → {n : ℕ} → Vector α n → (i : ℕ) → Vector α (min i n)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.mono : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s t : Set E} {x : E},
  HasFPowerSeriesWithinAt f p s x → t ⊆ s → HasFPowerSeriesWithinAt f p t x
-- Mathlib.Algebra.Algebra.Equiv
/-- `AlgEquiv.toLinearMap` as a `MonoidHom`.  -/
AlgEquiv.toLinearMapHom : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (A ≃ₐ[R] A) →* Module.End R A
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_9 : HSub Std.Time.Millisecond.Offset Std.Time.Hour.Offset Std.Time.Millisecond.Offset
-- Mathlib.Order.WithBot
Equiv.withTopSubtypeNe_symm_apply_coe : ∀ {α : Type u_1} (x : α), ↑(Equiv.withTopSubtypeNe.symm x) = ↑x
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.id_leftLim : ∀ (x : ℝ), Function.leftLim (↑StieltjesFunction.id) x = x
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The underlying `Mor₂` term of a `WhiskerLeft` term.  -/
Mathlib.Tactic.BicategoryLike.WhiskerLeft.e : Mathlib.Tactic.BicategoryLike.WhiskerLeft → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Data.Int.Fib.Basic
_private.Mathlib.Data.Int.Fib.Basic.0.Int.fib_neg_natCast_add_neg_natCast : ∀ (m n : ℕ), Int.fib (-↑m + -↑n) = Int.fib (-↑m - 1) * Int.fib (-↑n) + Int.fib (-↑m) * Int.fib (-↑n + 1)
-- Mathlib.Topology.Path
Path.mk.inj : ∀ {X : Type u_1} {inst : TopologicalSpace X} {x y : X} {toContinuousMap : C(↑unitInterval, X)}
  {source' : toContinuousMap.toFun 0 = x} {target' : toContinuousMap.toFun 1 = y}
  {toContinuousMap_1 : C(↑unitInterval, X)} {source'_1 : toContinuousMap_1.toFun 0 = x}
  {target'_1 : toContinuousMap_1.toFun 1 = y},
  { toContinuousMap := toContinuousMap, source' := source', target' := target' } =
      { toContinuousMap := toContinuousMap_1, source' := source'_1, target' := target'_1 } →
    toContinuousMap = toContinuousMap_1
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
/-- The underlying vertices of the free groupoid  -/
Quiver.FreeGroupoid : (V : Type u_1) → [Q : Quiver V] → Type u_1
-- Init.Data.Array.Lemmas
Array.back_append_left : ∀ {α : Type u_1} {xs ys : Array α} (w : 0 < (xs ++ ys).size) (h : ys.size = 0), (xs ++ ys).back w = xs.back ⋯
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- underlying morphism between two carriers  -/
CategoryTheory.Endofunctor.Coalgebra.Hom.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} → V₀.Hom V₁ → (V₀.V ⟶ V₁.V)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ordCompare_maxKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.TreeMap.Raw α β compare},
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α}, compare ((t.modify k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.exists_ne_zero_of_setGcd_ne_zero : ∀ {s : Set ℕ}, Nat.setGcd s ≠ 0 → ∃ n ∈ s, n ≠ 0
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDeriv_succ_const : ∀ {𝕜 : 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] (n : ℕ) (c : F),
  (iteratedFDeriv 𝕜 (n + 1) fun x => c) = 0
-- Mathlib.Algebra.Algebra.Operations
Submodule.sup_mul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M N P : Submodule R A), (M ⊔ N) * P = M * P ⊔ N * P
-- Mathlib.Data.Option.Defs
Option.elim'_none_some : ∀ {α : Type u_1} {β : Type u_2} (f : Option α → β), Option.elim' (f none) (f ∘ some) = f
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mem_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : Z}, x ∈ e.source ↔ proj x ∈ e.baseSet
-- Mathlib.Order.Bounds.Lattice
isLUB_iUnion_iff_of_isLUB : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_2} {s : ι → Set α} {u : ι → α},
  (∀ (i : ι), IsLUB (s i) (u i)) → ∀ (c : α), IsLUB (Set.range u) c ↔ IsLUB (⋃ i, s i) c
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_symm_apply_val : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  {c : CategoryTheory.Limits.Multifork I} (hc : CategoryTheory.Limits.IsLimit c) (x : c.pt) (i : J.L),
  ((CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc).symm x).val i =
    (CategoryTheory.ConcreteCategory.hom (c.ι i)) x
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.instInhabitedMatchEqnsExtState.default : Lean.Meta.Match.MatchEqnsExtState
-- Mathlib.GroupTheory.OrderOfElement
exists_addOrderOf_eq_prime_pow_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)],
  (∃ k, addOrderOf x = p ^ k) ↔ ∃ m, p ^ m • x = 0
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.simpCore : Lean.Expr →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      optParam (Option Lean.Meta.Simp.Discharge) none →
        optParam Lean.Meta.Simp.State { } → Lean.MetaM (Lean.Meta.Simp.Result × Lean.Meta.Simp.State)
-- Mathlib.Data.List.Cycle
List.prev.eq_2 : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (x_1 : x ∈ [y]), [y].prev x x_1 = y
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- If `E` is a normed space, `Lp.simpleFunc E p μ` is a normed space. Not declared as an
instance as it is (as of writing) used only in the construction of the Bochner integral.  -/
MeasureTheory.Lp.simpleFunc.normedSpace : {α : Type u_1} →
  {E : Type u_4} →
    [inst : MeasurableSpace α] →
      [inst_1 : NormedAddCommGroup E] →
        {p : ENNReal} →
          {μ : MeasureTheory.Measure α} →
            {𝕜 : Type u_7} →
              [inst_2 : NormedField 𝕜] →
                [NormedSpace 𝕜 E] → [inst_4 : Fact (1 ≤ p)] → NormedSpace 𝕜 ↥(MeasureTheory.Lp.simpleFunc E p μ)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.toOpen_comp_comap : ∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U))))
      (CommRingCat.ofHom
        (AlgebraicGeometry.StructureSheaf.comap f U
          ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U) ⋯)) =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f)
      (CommRingCat.ofHom
        (algebraMap S
          ↑((AlgebraicGeometry.Spec.structureSheaf S).obj.obj
              (Opposite.op
                ((TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))))
-- Mathlib.Order.RelClasses
/-- **Alias** of `Prod.wellFoundedLT`. -/
Prod.wellFoundedLT' : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [WellFoundedLT α] [inst_2 : Preorder β] [WellFoundedLT β],
  WellFoundedLT (α × β)
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- Given two smooth maps into the same fibers of a Riemannian bundle,
their scalar product is smooth.  -/
ContMDiffOn.inner_bundle : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (x : B) → NormedAddCommGroup (E x)] [inst_9 : (x : B) → InnerProductSpace ℝ (E x)]
  [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E] {EM : Type u_6} [inst_12 : NormedAddCommGroup EM]
  [inst_13 : NormedSpace ℝ EM] {HM : Type u_7} [inst_14 : TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM}
  {M : Type u_8} [inst_15 : TopologicalSpace M] [inst_16 : ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB n F E]
  {b : M → B} {v w : (x : M) → E (b x)} {s : Set M},
  ContMDiffOn IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun m => ⟨b m, v m⟩) s →
    ContMDiffOn IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun m => ⟨b m, w m⟩) s →
      ContMDiffOn IM (modelWithCornersSelf ℝ ℝ) n (fun b_1 => inner ℝ (v b_1) (w b_1)) s
-- Lean.Meta.Sym.SymM
/-- Returns the internalized `Bool.true`.   -/
Lean.Meta.Sym.getBoolTrueExpr : Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Data.List.Indexes
_private.Mathlib.Data.List.Indexes.0.List.mapIdxMAux'.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (x : ℕ) (h_1 : (x : ℕ) → motive x [])
  (h_2 : (i : ℕ) → (a : α) → (as : List α) → motive i (a :: as)),
  (match x, [] with
    | x, [] => h_1 x
    | i, a :: as => h_2 i a as) =
    h_1 x
-- Mathlib.Order.DirSupClosed
DirSupClosedOn.univ : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α], DirSupClosedOn D Set.univ
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instDiv.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  UpperSet.instDiv = { div := fun s t => { carrier := Set.image2 (fun x1 x2 => x1 / x2) ↑s ↑t, upper' := ⋯ } }
-- Init.Data.Float.Model.Unpacked.Sign
/-- Constructs a sign from a bitvector, with positive sign denoted by `0`.
 -/
Float.Model.UnpackedFloat.Sign.ofBitVec : BitVec 1 → Float.Model.UnpackedFloat.Sign
-- Mathlib.RingTheory.PowerSeries.Substitution
_private.Mathlib.RingTheory.PowerSeries.Substitution.0.PowerSeries.substInvFun.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ),
  (n = 0 → False) →
    (match n.succ with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | n.succ => h_3 n) =
      h_3 n
-- Mathlib.Topology.Compactification.StoneCech
stoneCechExtend.eq_1 : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [inst_2 : T2Space β] {g : α → β}
  (hg : Continuous g) [inst_3 : CompactSpace β], stoneCechExtend hg = T2Quotient.lift ⋯
-- Aesop.Index
_private.Aesop.Index.0.Aesop.Index.applicableUnindexedRules : {α : Type} → Aesop.Index α → (Aesop.Rule α → Bool) → Array (Aesop.Rule α × Array Aesop.IndexMatchLocation)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_iSup : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Sort u_4}
  (S : ι → Submodule R M), -⨆ i, S i = ⨆ i, -S i
-- Batteries.Data.Fin.Coding
Fin.encodeProd.eq_1 : ∀ {m n : ℕ} (i : Fin m) (j : Fin n), Fin.encodeProd (i, j) = i.mkDivMod j
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getResultingTypeCore?.finalize' : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.of.injEq : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (carrier : Type v)
  [str : TopologicalSpace carrier] (carrier_1 : Type v) (str_1 : TopologicalSpace carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.hom_inv_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.hom h)
      (CategoryTheory.Bicategory.whiskerRight η.inv h) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
Matrix.row_ne_zero_iff_exists_isLeadingEntry : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [inst : Zero R] [inst_1 : LT n] [WellFoundedLT n]
  {i : m}, A i ≠ 0 ↔ ∃ c, A.IsLeadingEntry i c
-- Mathlib.Data.Holor
Holor.CPRankMax.below : {α : Type} →
  [inst : Mul α] →
    [inst_1 : AddMonoid α] →
      {motive : (a : ℕ) → {ds : List ℕ} → (a_1 : Holor α ds) → Holor.CPRankMax a a_1 → Prop} →
        {a : ℕ} → {ds : List ℕ} → {a_1 : Holor α ds} → Holor.CPRankMax a a_1 → Prop
-- Aesop.Forward.State
Aesop.instInhabitedRawHyp : Inhabited Aesop.RawHyp
-- Init.PropLemmas
eq_mp_eq_cast : ∀ {α β : Sort u_1} (h : α = β), h.mp = cast h
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.wp_econs : ∀ {Pred : Type u_2} {EPred : Type u_1} {Prog : Type u} {Value : Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog)
  (post : Value → Pred) (epost epost' : EPred),
  Lean.Order.PartialOrder.rel epost epost' →
    Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x post epost) (Std.Internal.Do.wp x post epost')
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.precomp_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) {X_1 Y : Fin (n + 1 + 1)} (g : X_1 ⟶ Y),
  (F.precomp f).map g = CategoryTheory.ComposableArrows.Precomp.map F f X_1 Y ⋯
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocal K] {X : C} (𝒰 : K.ZeroHypercover X), (∀ (i : 𝒰.I₀), P (𝒰.X i)) → P X
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.getMatcherInfoCore? : Lean.Environment → Lean.Name → Option Lean.Meta.MatcherInfo
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {k fallback : α}, (cmp (t.maxKeyD fallback) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_def : ∀ (a b : ℤ), a.tmod b = a - b * a.tdiv b
-- Mathlib.Data.Finset.Grade
Finset.covBy_iff_exists_erase : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s ⋖ t ↔ ∃ a ∈ t, t.erase a = s
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_natCast : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : SeminormedRing R] (n : ℕ), ⇑↑n = ↑n
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_div_comm : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, a ≤ b / c ↔ c ≤ b / a
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invUnitsSub_mul_sub : ∀ {R : Type u_1} [inst : Ring R] (u : Rˣ), PowerSeries.invUnitsSub u * (PowerSeries.C ↑u - PowerSeries.X) = 1
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- **Alias** of `not_integrableOn_Ici_inv`.

---

The function `fun x ↦ x⁻¹` is not integrable on any interval `[a, +∞)`.  -/
not_IntegrableOn_Ici_inv : ∀ {a : ℝ}, ¬MeasureTheory.IntegrableOn (fun x => x⁻¹) (Set.Ici a) MeasureTheory.volume
-- Mathlib.Topology.Spectral.Hom
/-- Copy of a `SpectralMap` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
SpectralMap.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → (f : SpectralMap α β) → (f' : α → β) → f' = ⇑f → SpectralMap α β
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_mono : Monotone ENat.toENNReal
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
CategoryTheory.instExtensiveOfArrowsι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C]
  {α : Type} [inst_2 : Finite α] (Z : α → C),
  (CategoryTheory.Presieve.ofArrows Z fun i => CategoryTheory.Limits.Sigma.ι Z i).Extensive
-- Mathlib.Algebra.Group.Action.Basic
/-- Pullback a multiplicative distributive multiplicative action along an injective monoid
homomorphism.  -/
Function.Injective.mulDistribMulAction : {M : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : Monoid M] →
        [inst_1 : Monoid A] →
          [inst_2 : MulDistribMulAction M A] →
            [inst_3 : Monoid B] →
              [inst_4 : SMul M B] →
                (f : B →* A) →
                  Function.Injective ⇑f → (∀ (c : M) (x : B), f (c • x) = c • f x) → MulDistribMulAction M B
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.insertIfNew₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size} {a : α}
  {b : β a} (a_1 : m.WF), Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.Algebra.Order.Ring.Abs
/-- If `a` is even, then `n` is odd iff `n % a` is odd.  -/
Odd.mod_even_iff : ∀ {n a : ℕ}, Even a → (Odd (n % a) ↔ Odd n)
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.or_elim : ∀ (a b : Bool), (a || b) = !(!a && !b)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- Specialized version of `isParabolic_iff_of_upperTriangular` intended for use with
discrete subgroups of `GL(2, ℝ)`.  -/
Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det : ∀ {K : Type u_2} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {g : GL (Fin 2) K},
  Matrix.GeneralLinearGroup.det g = 1 ∨ Matrix.GeneralLinearGroup.det g = -1 →
    ↑g 1 0 = 0 →
      (g.IsParabolic ↔
        (∃ x, x ≠ 0 ∧ g = Matrix.GeneralLinearGroup.upperRightHom x) ∨
          ∃ x, x ≠ 0 ∧ g = -Matrix.GeneralLinearGroup.upperRightHom x)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.AlgHom.«term↑ₐ_1» : Lean.ParserDescr
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.support_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R),
  ((MvPolynomial.finSuccEquiv R n) f).support = Finset.image (fun m => m 0) f.support
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.exists_eRk_insert_eq_add_one_of_lt : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.eRk X < M.eRk Y → ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1
-- Init.Data.List.Basic
List.concat_eq_append : ∀ {α : Type u} {as : List α} {a : α}, as.concat a = as ++ [a]