mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Relrank
Subfield.lift_rank_comap : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A : Subfield E) (f : L →+* E),
  Cardinal.lift.{v, w} (Module.rank (↥(Subfield.comap f A)) L) = Cardinal.lift.{w, v} (A.relrank f.fieldRange)
-- Mathlib.Geometry.Manifold.Complex
/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
complex normed space. Let `f : E → F` be a function that is complex differentiable on `U`. Suppose
that `‖f x‖` takes its maximum value on `U` at `c ∈ U`. Then `‖f x‖ = ‖f c‖` for all `x ∈ U`.  -/
MDifferentiableOn.norm_eqOn_of_isPreconnected_of_isMaxOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {H : Type u_3} [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
  {M : Type u_4} [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I 1 M] {f : M → F} {U : Set M}
  {c : M},
  MDiff[U] f →
    IsPreconnected U → IsOpen U → c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn (norm ∘ f) (Function.const M ‖f c‖) U
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Finsupp.sConvexComb_apply : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {ι : Type u_3}
  {X : Type u_4} [inst_3 : Zero X] [inst_4 : Convexity.ConvexSpace R X] (w : Convexity.StdSimplex R (ι →₀ X)) (i : ι),
  (Convexity.sConvexComb w) i = Convexity.iConvexComb w fun x => x i
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
/-- the left map  -/
CategoryTheory.Span.l : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} → {c c' : C} → (self : CategoryTheory.Span Wₗ Wᵣ c c') → self.apex ⟶ c
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instStarAddMonoid : {R : Type u_1} →
  {A : Type u_2} →
    [inst : AddMonoid R] →
      [inst_1 : AddMonoid A] → [StarAddMonoid R] → [StarAddMonoid A] → StarAddMonoid (Unitization R A)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hV2 : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → (self : Rep.{w, u, v} k G) → Module k ↑self
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.hasFPowerSeriesAt_exp_zero_of_radius_pos : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] [CharZero 𝕂],
  0 < (NormedSpace.expSeries 𝕂 𝔸).radius → HasFPowerSeriesAt NormedSpace.exp (NormedSpace.expSeries 𝕂 𝔸) 0
-- Mathlib.Tactic.NormNum.Ineq
/-- Helper function to synthesize typed `Field α` `LinearOrder α` `IsStrictOrderedRing α`
expressions.  -/
Mathlib.Meta.NormNum.inferLinearOrderedField : {u : Lean.Level} →
  (α : Q(Type u)) → Lean.MetaM ((x : Q(Field «$α»)) × (x_1 : Q(LinearOrder «$α»)) × Q(IsStrictOrderedRing «$α»))
-- Plausible.Testable
/-- `DecorationsOf p` is used as a hint to `mk_decorations` to specify
that the goal should be satisfied with a proposition equivalent to `p`
with added annotations.  -/
Plausible.Decorations.DecorationsOf : Prop → Type
-- Mathlib.Logic.Function.Basic
Function.swap_gt : ∀ {α : Type u_4} [inst : LT α], (Function.swap fun x1 x2 => x1 > x2) = fun x1 x2 => x1 < x2
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The ring equivalence between `ContinuousLinearMapWOT` and `ContinuousLinearMap`.  -/
ContinuousLinearMapWOT.ringEquiv : {𝕜₁ : Type u_1} →
  [inst : NormedField 𝕜₁] →
    {E : Type u_3} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace E] →
          [inst_3 : Module 𝕜₁ E] → [inst_4 : IsTopologicalAddGroup E] → (E →WOT[𝕜₁] E) ≃+* (E →L[𝕜₁] E)
-- Mathlib.Order.Partition.Basic
Partition.mem_iff_exists : ∀ {α : Type u_1} {x : α} {u : Set α} {P : Partition u}, x ∈ u ↔ ∃ t ∈ P, x ∈ t
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_mulLeft : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : InvolutiveStar R] {E : Type u_6} [inst_2 : NonUnitalNonAssocSemiring E]
  [inst_3 : StarRing E] [inst_4 : Module R E] [inst_5 : StarModule R E] [inst_6 : SMulCommClass R E E]
  [inst_7 : IsScalarTower R E E] (x : E),
  star (WithConv.toConv (LinearMap.mulLeft R x)) = WithConv.toConv (LinearMap.mulRight R (star x))
-- Mathlib.Algebra.BigOperators.Finprod
Nat.cast_finsum : ∀ {ι : Type u_3} [Finite ι] {M : Type u_7} [inst : AddCommMonoidWithOne M] (f : ι → ℕ),
  ↑(∑ᶠ (x : ι), f x) = ∑ᶠ (x : ι), ↑(f x)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.topEquiv_symm_apply_coe : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A),
  ↑(Subalgebra.topEquiv.symm a) = a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_op_nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s : Finset α) (n : ℕ),
  Finset.image AddOpposite.op (n • s) = n • Finset.image AddOpposite.op s
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.congr_of_eventuallyEq_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x → f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → MDiffAt[s] f₁ x
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The sieve of `pullback (E.f i₁) (E.f i₂)` given by `E : PreOneHypercover S`.  -/
CategoryTheory.PreOneHypercover.sieve₁' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        (i₁ i₂ : E.I₀) →
          [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] →
            CategoryTheory.Sieve (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.instFintype : {Δ : SimplexCategoryᵒᵖ} → Fintype (CategoryTheory.SimplicialObject.Splitting.IndexSet Δ)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.addOrderOf_div_of_gcd_eq_one' : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {m : ℤ}
  {n : ℕ}, 0 < n → m.natAbs.gcd n = 1 → addOrderOf ↑(↑m / ↑n * p) = n
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RiiSliceData.range : {α : Type u} → Std.DTreeMap.Internal.Unit.RiiSliceData α → Std.Rii α
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_two_pow_mul_add : ∀ (a : ℕ) {b i : ℕ}, b < 2 ^ i → ∀ (j : ℕ), (2 ^ i * a + b).testBit j = if j < i then b.testBit j else a.testBit (j - i)
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
MulAction.IsMultiplyPreprimitive.of_bijective_map : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {N : Type u_3} {β : Type u_4}
  [inst_2 : Group N] [inst_3 : MulAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Bijective ⇑f → ∀ {n : ℕ}, MulAction.IsMultiplyPreprimitive M α n → MulAction.IsMultiplyPreprimitive N β n
-- Mathlib.Order.Sublocale
Sublocale.instSetLike : {X : Type u_1} → [inst : Order.Frame X] → SetLike (Sublocale X) X
-- Mathlib.Data.Nat.ChineseRemainder
_private.Mathlib.Data.Nat.ChineseRemainder.0.Nat.chineseRemainderOfList.match_1.eq_2 : ∀ {ι : Type u_1} (s : ι → ℕ) (motive : (x : List ι) → List.Pairwise (Function.onFun Nat.Coprime s) x → Sort u_2) (i : ι)
  (l : List ι) (co : List.Pairwise (Function.onFun Nat.Coprime s) (i :: l))
  (h_1 : (x : List.Pairwise (Function.onFun Nat.Coprime s) []) → motive [] x)
  (h_2 : (i : ι) → (l : List ι) → (co : List.Pairwise (Function.onFun Nat.Coprime s) (i :: l)) → motive (i :: l) co),
  (match i :: l, co with
    | [], x => h_1 x
    | i :: l, co => h_2 i l co) =
    h_2 i l co
-- Mathlib.RingTheory.LocalRing.Pullback
/-- The subalgebra of pairs `(a, b) : A × B` such that `f a = g b`, i.e.,
the pullback of f and g as a subalgebra of A × B.  -/
AlgHom.pullback : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : Semiring C] → [inst_6 : Algebra R C] → (A →ₐ[R] C) → (B →ₐ[R] C) → Subalgebra R (A × B)
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict_precomp_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K K' : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (α : K' ⟶ K) (ψ : K ⟶ L.extend e) {Z : HomologicalComplex C c} (h : L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.homRestrict (CategoryTheory.CategoryStruct.comp α ψ)) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap α e)
      (CategoryTheory.CategoryStruct.comp (e.homRestrict ψ) h)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The unit of the chosen left Kan extension `leftKanExtension L F`.  -/
CategoryTheory.Functor.leftKanExtensionUnit : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) → [inst_3 : L.HasLeftKanExtension F] → F ⟶ L.comp (L.leftKanExtension F)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instSetLike.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M],
  SubAddAction.instSetLike = { coe := SubAddAction.carrier, coe_injective := ⋯ }
-- Mathlib.Tactic.Linter.Whitespace
/-- If the `linter.style.whitespace.verbose` option is `true`, the `whitespace` linter
reports some helpful diagnostic information.  -/
Mathlib.Linter.linter.style.whitespace.verbose : Lean.Option Bool
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.left_le : ∀ {J : Type u_1} [inst : LinearOrder J] {i j : J} (self : CategoryTheory.SimplicialThickening.Path i j),
  ∀ k ∈ self.I, i ≤ k
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.mem_of_mem_roo : ∀ {α : Type u} [inst : LT α] {lo hi a : α}, (a ∈ lo<...hi) → a ∈ *...hi
-- Init.Data.String.Basic
/-- Returns `true` if a specified byte position is greater than or equal to the position which points to
the end of a string. Otherwise, returns `false`.

Examples:
* `(0 |> "abc".next |> "abc".next |> "abc".atEnd) = false`
* `(0 |> "abc".next |> "abc".next |> "abc".next |> "abc".next |> "abc".atEnd) = true`
* `(0 |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".atEnd) = false`
* `(0 |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".atEnd) = true`
* `"abc".atEnd ⟨4⟩ = true`
* `"L∃∀N".atEnd ⟨7⟩ = false`
* `"L∃∀N".atEnd ⟨8⟩ = true`
 -/
String.Pos.Raw.atEnd : String → String.Pos.Raw → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- If `j` is terminal in the index category, then the map `colimit.ι F j` is an isomorphism.
 -/
CategoryTheory.Limits.isIso_ι_of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {j : J} (I : CategoryTheory.Limits.IsTerminal j) (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasColimit F], CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F j)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isEmpty_inter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∩ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∉ m₂
-- Mathlib.Analysis.Calculus.FDeriv.Comp
Differentiable.fun_comp : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {g : F → G},
  Differentiable 𝕜 g → Differentiable 𝕜 f → Differentiable 𝕜 fun x => g (f x)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.firstDart_toProd : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil), (p.firstDart hp).toProd = (v, p.snd)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_symm_addEquivProd : ∀ {R : Type u_3} [inst : Add R] (c₁ c₂ c₃ : R),
  ⇑(QuaternionAlgebra.addEquivProd c₁ c₂ c₃).symm = ⇑(QuaternionAlgebra.equivProd c₁ c₂ c₃).symm
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.eq_of_not_disjoint_openCell`.

---

The contrapositive of `disjoint_openCell_of_ne`.  -/
Topology.CWComplex.eq_of_not_disjoint_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] {n : ℕ}
  {j : Topology.RelCWComplex.cell C n} {m : ℕ} {i : Topology.RelCWComplex.cell C m},
  ¬Disjoint (Topology.RelCWComplex.openCell n j) (Topology.RelCWComplex.openCell m i) → ⟨n, j⟩ = ⟨m, i⟩
-- Mathlib.MeasureTheory.Measure.Comap
MeasurableEquiv.comap_symm : ∀ {α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {mb : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  (e : α ≃ᵐ β), MeasureTheory.Measure.comap (⇑e.symm) μ = MeasureTheory.Measure.map (⇑e) μ
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The cosine of the angle between two vectors is -1 if and only if the angle is π.  -/
InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  Real.cos (InnerProductGeometry.angle x y) = -1 ↔ InnerProductGeometry.angle x y = Real.pi
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_le_choose : ∀ {a b : ℕ} (c : ℕ), a ≤ b → a.choose c ≤ b.choose c
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentIdentifier : Lean.ToJson Lean.Lsp.TextDocumentIdentifier
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Inhabited α] [inst_3 : BEq α]
  [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km : α}, Std.Internal.List.minKey? l = some km → Std.Internal.List.getKey! km l = km
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.trStmts₁.match_1.eq_4 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (f : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k f q))
  (h_2 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k f q))
  (h_3 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k f q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (x : Turing.TM2.Stmt Γ Λ σ) → motive x),
  (match Turing.TM2.Stmt.load a q with
    | Turing.TM2.Stmt.push k f q => h_1 k f q
    | Turing.TM2.Stmt.peek k f q => h_2 k f q
    | Turing.TM2.Stmt.pop k f q => h_3 k f q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | x => h_6 x) =
    h_4 a q
-- Std.Data.ByteSlice
instSliceableByteSliceNat : Std.Rcc.Sliceable ByteSlice ℕ ByteSlice
-- ProofWidgets.Util
/-- A copy of `Delaborator.annotateTermInfo` for other syntactic categories.  -/
Lean.PrettyPrinter.Delaborator.annotateTermLikeInfo : {n : Lean.SyntaxNodeKinds} → Lean.TSyntax n → Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax n)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_pushoutRightPushoutInlIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout f' (CategoryTheory.Limits.pushout.inl f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp f f') g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f' (CategoryTheory.Limits.pushout.inl f g))
        h)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.addLocalEntry : {α β σ : Type} → Lean.ScopedEnvExtension α β σ → Lean.Environment → β → Lean.Environment
-- Mathlib.Algebra.Free
FreeAddSemigroup.add_seq : ∀ {α β : Type u} {f g : FreeAddSemigroup (α → β)} {x : FreeAddSemigroup α}, f + g <*> x = (f <*> x) + (g <*> x)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The third projection functor `ShortComplex C ⥤ C`.  -/
CategoryTheory.ShortComplex.π₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_symm : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ∨ Q ⊢ₛ Q ∨ P
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.strictMap_obj : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) {X : C}, P X → P.strictMap F (F.obj X)
-- Mathlib.RingTheory.LaurentSeries
/-- The support of `Cauchy.coeff` is bounded below  -/
LaurentSeries.Cauchy.coeff_support_bddBelow : ∀ {K : Type u_2} [inst : Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ),
  BddBelow (Function.support (LaurentSeries.Cauchy.coeff hℱ))
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_comp_two_mul_X : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  (Polynomial.Chebyshev.C R n).comp (2 * Polynomial.X) = 2 * Polynomial.Chebyshev.T R n
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.edges_cycleBypass_subset_edges : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (w : G.Walk v v), w.cycleBypass.edges ⊆ w.edges
-- Mathlib.Data.Sym.Sym2
Sym2.sound : ∀ {α : Type u_1} {a b c d : α}, Sym2.Rel α (a, b) (c, d) → s(a, b) = s(c, d)
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.leftInverse_symm : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (e : A ≃⋆+* B), Function.LeftInverse ⇑e.symm ⇑e
-- Mathlib.Order.CompleteBooleanAlgebra
compl_iSup : ∀ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ι → α}, (iSup f)ᶜ = ⨅ i, (f i)ᶜ
-- Mathlib.Algebra.Quaternion
/-- The imaginary part of a quaternion.

Note that unless `c₂ = 0`, this definition is not particularly well-behaved;
for instance, `QuaternionAlgebra.star_im` only says that the star of an imaginary quaternion
is imaginary under this condition.  -/
QuaternionAlgebra.im : {R : Type u_3} → {c₁ c₂ c₃ : R} → [Zero R] → QuaternionAlgebra R c₁ c₂ c₃ → QuaternionAlgebra R c₁ c₂ c₃
-- Mathlib.Order.SupClosed
/-- The semilattice generated by a finite set is finite.  -/
Set.Finite.infClosure : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α}, s.Finite → (infClosure s).Finite
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.coe_toOrderHom : ∀ (f : CircleDeg1Lift), ⇑f.toOrderHom = ⇑f
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
/-- The category of `R`-Hopf algebras.  -/
HopfAlgCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Mathlib.Order.SuccPred.Limit
SuccOrder.prelimitRecOn_succ_of_not_isMax : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α]
  [inst_2 : WellFoundedLT α] (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a) (hb : ¬IsMax b),
  SuccOrder.prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb (SuccOrder.prelimitRecOn b succ isSuccPrelimit)
-- Mathlib.Topology.UniformSpace.Defs
UniformContinuous.comp : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {g : β → γ} {f : α → β}, UniformContinuous g → UniformContinuous f → UniformContinuous (g ∘ f)
-- Mathlib.Algebra.Ring.Action.End
RingAut.apply_faithfulSMul : ∀ {R : Type u_2} [inst : Semiring R], FaithfulSMul (RingAut R) R
-- Mathlib.Order.Atoms
GaloisCoinsertion.isCoatom_iff' : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α]
  [inst_3 : OrderTop β] [IsCoatomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u),
  l ⊤ = ⊤ → (∀ (b : β), IsCoatom b → l (u b) = b) → ∀ (a : α), IsCoatom (l a) ↔ IsCoatom a
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesMap_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K L : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], HomologicalComplex.cyclesMap 0 i = 0
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Sheaf.interUnionPullbackCone_pt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Sheaf C X)
  (U V : TopologicalSpace.Opens ↑X), (F.interUnionPullbackCone U V).pt = F.obj.obj (Opposite.op (U ⊔ V))
-- Lean.Elab.Import
Lean.Elab.processHeaderCore : String.Pos.Raw →
  Array Lean.Import →
    Bool →
      Lean.Options →
        Lean.MessageLog →
          Lean.Parser.InputContext →
            optParam UInt32 0 →
              optParam (Array Lean.Plugin) #[] →
                optParam Bool false →
                  optParam Lean.Name Lean.Name.anonymous →
                    optParam (Option Lean.PkgId) none →
                      optParam (Lean.NameMap Lean.ImportArtifacts) ∅ →
                        optParam (Option Lean.Elab.HeaderSyntax) none →
                          optParam (Option Lean.Elab.HeaderSyntax) none → IO (Lean.Environment × Lean.MessageLog)
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- `∃ᵐ a ∂μ, p a` means that `p` holds `∂μ`-frequently,
i.e. `p` holds on a set of positive measure.

This is notation for `Filter.Frequently p (MeasureTheory.ae μ)`.  -/
MeasureTheory.«term∃ᵐ_∂_,_» : Lean.ParserDescr
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Remaining terms to match  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.PartialMatch.keys : Lean.Meta.RefinedDiscrTree.PartialMatch✝ → List Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.instNormOneClassOfNontrivial : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] [Nontrivial E], NormOneClass E
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.cons_nil_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).append p = SimpleGraph.Walk.cons h p
-- Lean.Structure
Lean.StructureResolutionState : Type
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rco_eq_none : ∀ {m n : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m...n).toArray[i]? = none