mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isCircuit_map_iff_of_injective`. -/
SimpleGraph.Walk.IsCircuit.map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u},
  Function.Injective ⇑f → p.IsCircuit → (SimpleGraph.Walk.map f p).IsCircuit
-- Mathlib.Tactic.Linter.Style
/-- The "longLine" linter emits a warning on lines longer than
`linter.style.longLine.maxLineLength` (which defaults to 100) characters.
We allow lines containing URLs to be longer, though.  -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.longLine.longLineLinter : Lean.Linter
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.RepToAction_obj_V_carrier : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] (X : Rep.{w, u, v} k G),
  ↑((Rep.RepToAction k G).obj X).V = ↑X
-- Mathlib.Algebra.Group.Action.Defs
AddAction.ext : ∀ {G : Type u_9} {P : Type u_10} {inst : AddMonoid G} {x y : AddAction G P}, VAdd.vadd = VAdd.vadd → x = y
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeExplicitHoles : Lean.Options → Bool
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.iInf_def : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_4} (s : ι → TopologicalSpace.Closeds α),
  ⨅ i, s i = { carrier := ⋂ i, ↑(s i), isClosed' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
/-- If every finite subgraph of a graph `G` has a homomorphism to a finite graph `F`, then there is
a homomorphism from the whole of `G` to `F`.  -/
SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {F : SimpleGraph W} [Finite W]
  (h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F), Nonempty (G →g F)
-- Mathlib.Order.Hom.Lattice
InfHom.id.eq_1 : ∀ (α : Type u_2) [inst : Min α], InfHom.id α = { toFun := id, map_inf' := ⋯ }
-- Mathlib.Order.RelClasses
WellFoundedRelation.isWellFounded : ∀ {α : Type u} [h : WellFoundedRelation α], IsWellFounded α WellFoundedRelation.rel
-- Mathlib.CategoryTheory.Action.Basic
Action.instConcreteCategoryHomSubtypeV : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        {FV : V → V → Type u_3} →
          {CV : V → Type u_4} →
            [inst_2 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
              [inst_3 : CategoryTheory.ConcreteCategory V FV] →
                CategoryTheory.ConcreteCategory (Action V G) (Action.HomSubtype V G)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- A canonical splitting of the group extension associated to the semidirect product  -/
SemidirectProduct.inr_splitting : {N : Type u_1} →
  {G : Type u_3} →
    [inst : Group G] → [inst_1 : Group N] → (φ : G →* MulAut N) → (SemidirectProduct.toGroupExtension φ).Splitting
-- Mathlib.Logic.Equiv.Defs
Equiv.ord_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : Ord β] (a b : α), compare a b = compare (e a) (e b)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaEquiv_shrinkCoyoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ}
  (f : X ⟶ Y),
  CategoryTheory.shrinkCoyonedaEquiv (CategoryTheory.shrinkCoyoneda.{w, v, u}.map f) =
    CategoryTheory.shrinkCoyonedaObjObjEquiv.symm f.unop
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.symm_apply_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E), e.symm (e x) = x
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.snd : {α₁ α₂ : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.IterM m β → Std.Iterators.Types.Append α₁ α₂ m β
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_emod_sub_self : ∀ {x m : ℤ}, m ∣ x % m - x
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Pullback an additive group object along a fully faithful monoidal functor.  -/
CategoryTheory.Functor.FullyFaithful.addGrpObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.Monoidal] →
                F.FullyFaithful → (X : C) → [CategoryTheory.AddGrpObj (F.obj X)] → CategoryTheory.AddGrpObj X
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- The Cartan matrix of type E₈. See [bourbaki1968] plate VII, page 285.  -/
CartanMatrix.E₈ : Matrix (Fin 8) (Fin 8) ℤ
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
_private.Mathlib.Combinatorics.SetFamily.AhlswedeZhang.0.Finset.infs_aux : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α},
  a ∈ lowerClosure ↑(s ⊼ t) ↔ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
isAddCyclic_of_card_nsmul_eq_zero_le : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  (∀ (n : ℕ), 0 < n → {a | n • a = 0}.card ≤ n) → IsAddCyclic α
-- Mathlib.Algebra.Ring.Defs
NonAssocRing.toAddCommGroupWithOne : {α : Type u_1} → [self : NonAssocRing α] → AddCommGroupWithOne α
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- `ContDiffBump` is `𝒞ⁿ` in all its arguments.  -/
ContDiffWithinAt.contDiffBump : ∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup X]
  [inst_3 : NormedSpace ℝ X] [inst_4 : HasContDiffBump E] {n : ℕ∞} {c g : X → E} {s : Set X}
  {f : (x : X) → ContDiffBump (c x)} {x : X},
  ContDiffWithinAt ℝ (↑n) c s x →
    ContDiffWithinAt ℝ (↑n) (fun x => (f x).rIn) s x →
      ContDiffWithinAt ℝ (↑n) (fun x => (f x).rOut) s x →
        ContDiffWithinAt ℝ (↑n) g s x → ContDiffWithinAt ℝ (↑n) (fun x => ↑(f x) (g x)) s x
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.norm_apply_le_norm : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [StarOrderedRing A]
  (x : WithCStarModule A ((i : ι) → E i)) (i : ι), ‖x i‖ ≤ ‖x‖
-- Mathlib.Order.Bounded
Set.bounded_ge_inter_ge : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Bounded (fun x1 x2 => x1 ≥ x2) (s ∩ {b | b ≤ a}) ↔ Set.Bounded (fun x1 x2 => x1 ≥ x2) s
-- Mathlib.Analysis.InnerProductSpace.Subspace
DirectSum.IsInternal.collectedBasis_orthonormal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : DecidableEq ι] {V : ι → Submodule 𝕜 E},
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) →
    ∀ (hV_sum : DirectSum.IsInternal fun i => V i) {α : ι → Type u_6}
      {v_family : (i : ι) → Module.Basis (α i) 𝕜 ↥(V i)},
      (∀ (i : ι), Orthonormal 𝕜 ⇑(v_family i)) → Orthonormal 𝕜 ⇑(hV_sum.collectedBasis v_family)
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_right_injective : ∀ {x : ℕ}, Function.Injective fun x_1 => x ^^^ x_1
-- Mathlib.Algebra.Torsor.Basic
/-- Pullback of a torsor along an injective map.  -/
Function.Injective.torsor : {G : Type u_1} →
  {P : Type u_2} →
    {Q : Type u_3} →
      [inst : Group G] →
        [inst_1 : Torsor G P] →
          [inst_2 : SMul G Q] →
            [inst_3 : SDiv G Q] →
              [Nonempty Q] →
                (f : Q → P) →
                  Function.Injective f →
                    (∀ (c : G) (x : Q), f (c • x) = c • f x) → (∀ (x y : Q), x /ₛ y = f x /ₛ f y) → Torsor G Q
-- Mathlib.Topology.Order
TopologicalSpace.le_def : ∀ {α : Type u_1} {t s : TopologicalSpace α}, t ≤ s ↔ IsOpen ≤ IsOpen
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.one_mem : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), 1 ∈ A
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.hε : ∀ {D : Type u_5} [inst : CategoryTheory.Category.{v_5, u_5} D] {M : Type u_6} [inst_1 : AddCommMonoid M]
  [inst_2 : CategoryTheory.HasShift D M] (self : CategoryTheory.CommShift₂Setup D M) (m n : M),
  self.ε m n = (self.z (0, n) (m, 0))⁻¹ * self.z (m, 0) (0, n)
-- Lean.Elab.MutualInductive
/-- Finalize the inductive type, after they are all added to the environment, after auxiliary definitions are added, and after computed fields are registered.
The `levelParams`, `params`, and `replaceIndFVars` arguments of `prefinalize` are still valid here.  -/
Lean.Elab.Command.InductiveElabStep3.finalize : Lean.Elab.Command.InductiveElabStep3 → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Shift.Pullback
/-- The adjunction `adj`, seen as an adjunction between `PullbackShift.functor F φ`
and `PullbackShift.functor G φ`.
 -/
CategoryTheory.PullbackShift.adjunction : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (φ : A →+ B) →
                {D : Type u_4} →
                  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] →
                    [inst_5 : CategoryTheory.HasShift D B] →
                      {F : CategoryTheory.Functor C D} →
                        {G : CategoryTheory.Functor D C} →
                          (F ⊣ G) →
                            (CategoryTheory.PullbackShift.functor φ F ⊣ CategoryTheory.PullbackShift.functor φ G)
-- Mathlib.Analysis.Analytic.IsolatedZeros
HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (n : ℕ),
  HasFPowerSeriesAt f p z₀ →
    HasFPowerSeriesAt ((Function.swap dslope z₀)^[n] f) (FormalMultilinearSeries.fslope^[n] p) z₀
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Machine.map_step : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {Γ' : Type u_2} [inst_1 : Inhabited Γ'] {Λ : Type u_3} [inst_2 : Inhabited Λ]
  {Λ' : Type u_4} [inst_3 : Inhabited Λ'] (M : Turing.TM0.Machine Γ Λ) (f₁ : Turing.PointedMap Γ Γ')
  (f₂ : Turing.PointedMap Γ' Γ) (g₁ : Λ → Λ') (g₂ : Λ' → Λ) {S : Set Λ},
  Function.RightInverse f₁.f f₂.f →
    (∀ q ∈ S, g₂ (g₁ q) = q) →
      ∀ (c : Turing.TM0.Cfg Γ Λ),
        c.q ∈ S →
          Option.map (Turing.TM0.Cfg.map f₁ g₁) (Turing.TM0.step M c) =
            Turing.TM0.step (M.map f₁ f₂ g₁ g₂) (Turing.TM0.Cfg.map f₁ g₁ c)
-- Mathlib.CategoryTheory.Shift.CommShift
/-- Assume that we have a diagram of categories
```
C₁ ⥤ D₁
‖     ‖
v     v
C₂ ⥤ D₂
‖     ‖
v     v
C₃ ⥤ D₃
```
with functors `F₁₂ : C₁ ⥤ C₂`, `F₂₃ : C₂ ⥤ C₃` and `F₁₃ : C₁ ⥤ C₃` on the first
column that are related by a natural transformation `α : F₁₃ ⟶ F₁₂ ⋙ F₂₃`
and similarly `β : G₁₂ ⋙ G₂₃ ⟶ G₁₃` on the second column. Assume that we have
natural transformations
`e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂` (top square), `e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃` (bottom square),
and `e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃` (outer square), where the horizontal functors
are denoted `L₁`, `L₂` and `L₃`. Assume that `e₁₃` is determined by the other
natural transformations `α`, `e₂₃`, `e₁₂` and `β`. Then, if all these categories
are equipped with a shift by an additive monoid `A`, and all these functors commute with
these shifts, then the natural transformation `e₁₃` of the outer square commutes with the
shift if all `α`, `e₂₃`, `e₁₂` and `β` do.  -/
CategoryTheory.NatTrans.CommShift.verticalComposition : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [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} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₂₃ : CategoryTheory.Functor C₂ C₃} {F₁₃ : CategoryTheory.Functor C₁ C₃}
  (α : F₁₃ ⟶ F₁₂.comp F₂₃) {G₁₂ : CategoryTheory.Functor D₁ D₂} {G₂₃ : CategoryTheory.Functor D₂ D₃}
  {G₁₃ : CategoryTheory.Functor D₁ D₃} (β : G₁₂.comp G₂₃ ⟶ G₁₃) {L₁ : CategoryTheory.Functor C₁ D₁}
  {L₂ : CategoryTheory.Functor C₂ D₂} {L₃ : CategoryTheory.Functor C₃ D₃} (e₁₂ : F₁₂.comp L₂ ⟶ L₁.comp G₁₂)
  (e₂₃ : F₂₃.comp L₃ ⟶ L₂.comp G₂₃) (e₁₃ : F₁₃.comp L₃ ⟶ L₁.comp G₁₃) (A : Type u_7) [inst_6 : AddMonoid A]
  [inst_7 : CategoryTheory.HasShift C₁ A] [inst_8 : CategoryTheory.HasShift C₂ A]
  [inst_9 : CategoryTheory.HasShift C₃ A] [inst_10 : CategoryTheory.HasShift D₁ A]
  [inst_11 : CategoryTheory.HasShift D₂ A] [inst_12 : CategoryTheory.HasShift D₃ A] [inst_13 : F₁₂.CommShift A]
  [inst_14 : F₂₃.CommShift A] [inst_15 : F₁₃.CommShift A] [CategoryTheory.NatTrans.CommShift α A]
  [inst_17 : G₁₂.CommShift A] [inst_18 : G₂₃.CommShift A] [inst_19 : G₁₃.CommShift A]
  [CategoryTheory.NatTrans.CommShift β A] [inst_21 : L₁.CommShift A] [inst_22 : L₂.CommShift A]
  [inst_23 : L₃.CommShift A] [CategoryTheory.NatTrans.CommShift e₁₂ A] [CategoryTheory.NatTrans.CommShift e₂₃ A],
  e₁₃ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α L₃)
        (CategoryTheory.CategoryStruct.comp ⋯ ⋯) →
    CategoryTheory.NatTrans.CommShift e₁₃ A
-- Lean.Data.Json.Basic
Lean.Json.instCoeArrayStructured : Coe (Array Lean.Json) Lean.Json.Structured
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.map_one_fst_of_isCocycle₂ : ∀ {G : Type u_1} {A : Type u_2} [inst : Monoid G] [inst_1 : AddCommGroup A] [inst_2 : MulAction G A] {f : G × G → A},
  groupCohomology.IsCocycle₂ f → ∀ (g : G), f (1, g) = f (1, 1)
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblen (veblen … (veblen 0 0) … 0) 0 < Γ₀`  -/
Ordinal.iterate_veblen_lt_gamma_zero : ∀ (n : ℕ), (fun a => Ordinal.veblen a 0)^[n] 0 < Ordinal.gamma 0
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Equiv.Perm.OnCycleFactors.odd_of_centralizer_le_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α},
  Subgroup.centralizer {g} ≤ alternatingGroup α → ∀ i ∈ g.cycleType, Odd i
-- Mathlib.Order.Atoms
GaloisCoinsertion.isAtom_of_image : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u) {a : α}, IsAtom (l a) → IsAtom a
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Kind.monoidal.sizeOf_spec : sizeOf Mathlib.Tactic.Widget.StringDiagram.Kind.monoidal = 1
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.fromBlocks₂₂ : ∀ {m : Type u_1} {n : Type u_2} {R' : Type u_4} [inst : CommRing R'] [inst_1 : PartialOrder R'] [inst_2 : StarRing R']
  [inst_3 : Fintype n] [StarOrderedRing R'] [Finite m] [inst_6 : DecidableEq n] (A : Matrix m m R') (B : Matrix m n R')
  {D : Matrix n n R'},
  D.PosDef →
    ∀ [Invertible D], (Matrix.fromBlocks A B B.conjTranspose D).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).PosSemidef
-- Lean.Meta.Tactic.Contradiction
/-- See `Simp.isEqnThmHypothesis`
 -/
_private.Lean.Meta.Tactic.Contradiction.0.Lean.Meta.isGenDiseq : Lean.Expr → Bool
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- This holds for `0 < x, y ≤ 1` due to junk values.  -/
Real.arcosh_lt_arcosh : ∀ {x y : ℝ}, 0 < x → 0 < y → (Real.arcosh x < Real.arcosh y ↔ x < y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableOn.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun x => Real.sinh (f x)) s
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inner product between a multiple of a vector and a multiple of a `π / 2` rotation of
that vector is zero.  -/
Orientation.inner_smul_rotation_pi_div_two_smul_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) (r₁ r₂ : ℝ), inner ℝ (r₂ • x) (r₁ • (o.rotation ↑(Real.pi / 2)) x) = 0
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.IsComplex.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n},
  (∀ (i : ℕ) (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.IsComplex._auto_1),
      CategoryTheory.CategoryStruct.comp (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ hi) = 0) →
    S.IsComplex
-- Mathlib.Algebra.Group.Commute.Basic
Commute.zpow_right : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → ∀ (m : ℤ), Commute a (b ^ m)
-- Mathlib.Order.Filter.IsBounded
/-- To check that a filter is frequently bounded, it suffices to have a witness
which bounds `f` at some point for every admissible set.

This is only an implication, as the other direction is wrong for the trivial filter.  -/
Filter.IsCobounded.mk : ∀ {α : Type u_1} {r : α → α → Prop} {f : Filter α} [IsTrans α r] (a : α),
  (∀ s ∈ f, ∃ x ∈ s, r a x) → Filter.IsCobounded r f
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- The spine of the unique non-degenerate `n`-simplex in `Δ[n]`.  -/
SSet.stdSimplex.spineId : (n : ℕ) → (SSet.stdSimplex.obj { len := n }).Path n
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.Nontrivial.of_polynomial_ne : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p ≠ q → Nontrivial R
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Note that this provides `IsScalarTower F K K` which is needed by `smul_mul_assoc`.  -/
Subfield.instIsScalarTowerSubtypeMem : ∀ {K : Type u} [inst : DivisionRing K] {X : Type u_1} {Y : Type u_2} [inst_1 : SMul X Y] [inst_2 : SMul K X]
  [inst_3 : SMul K Y] [IsScalarTower K X Y] (F : Subfield K), IsScalarTower (↥F) X Y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffAt.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℂ n f x → ContDiffAt ℂ n (fun x => Complex.sin (f x)) x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  t[k]? = some v ↔ ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ t.toList
-- Mathlib.Analysis.Normed.Group.Basic
enorm_add_le : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedAddMonoid E] (a b : E), ‖a + b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Scheme.Hom.mem_smoothLocus : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [inst : AlgebraicGeometry.LocallyOfFinitePresentation f] {x : ↥X},
  x ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus f ↔
    (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).FormallySmooth
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_exp_mul_I : ∀ (θ : ℝ), (Complex.exp (↑θ * Complex.I)).arg = toIocMod Real.two_pi_pos (-Real.pi) θ
-- Init.Data.Array.Lemmas
Array.isEmpty_toList : ∀ {α : Type u_1} {xs : Array α}, xs.toList.isEmpty = xs.isEmpty
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- `spanCone` is a limit cone.  -/
Profinite.NobelingProof.spanCone_isLimit : {I : Type u} →
  {C : Set (I → Bool)} →
    [inst : (s : Finset I) → (i : I) → Decidable (i ∈ s)] →
      (hC : IsCompact C) → CategoryTheory.Limits.IsLimit (Profinite.NobelingProof.spanCone hC)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Given a continuous `R`-multilinear map `f` taking values in `R`, `f.smulRight z` is the
continuous multilinear map sending `m` to `f m • z`.  -/
ContinuousMultilinearMap.smulRight : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : TopologicalSpace R] →
                    [inst_6 : (i : ι) → TopologicalSpace (M₁ i)] →
                      [inst_7 : TopologicalSpace M₂] →
                        [ContinuousSMul R M₂] → ContinuousMultilinearMap R M₁ R → M₂ → ContinuousMultilinearMap R M₁ M₂
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_add : ∀ {a b : USize} (h : System.Platform.numBits = 32), (a + b).toBitVec32 h = a.toBitVec32 h + b.toBitVec32 h
-- Lean.Meta.DiscrTree.Basic
_private.Lean.Meta.DiscrTree.Basic.0.Lean.Meta.DiscrTree.keysAsPattern.mkApp : Lean.MessageData → Array Lean.MessageData → Bool → Lean.CoreM Lean.MessageData
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.smul_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (t : R) (x : K ⋊⁅ψ⁆ L),
  t • x = { left := t • x.left, right := t • x.right }
-- Mathlib.Algebra.Group.Units.Defs
/-- An additive unit can be interpreted as a term in the base `AddMonoid`.  -/
AddUnits.instCoeHead : {α : Type u} → [inst : AddMonoid α] → CoeHead (AddUnits α) α
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop : ∀ {M : Type u_4} [inst : CommMonoid M] (l l' : List M),
  l.prod * l'.prod =
    (List.zipWith (fun x1 x2 => x1 * x2) l l').prod * (List.drop l'.length l).prod * (List.drop l.length l').prod
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_add_erase : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ),
  (SkewPolynomial.monomial n) (p.coeff n) + SkewPolynomial.erase n p = p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₂_p_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₁₂ (CategoryTheory.CategoryStruct.comp h₁₂.p h_1) =
    CategoryTheory.CategoryStruct.comp h.p h_1
-- Init.Data.Order.Classes
Std.LawfulOrderMin.mk : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α] [toMinEqOr : Std.MinEqOr α] [toLawfulOrderInf : Std.LawfulOrderInf α],
  Std.LawfulOrderMin α
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
ClassGroup.extendedHom_comp_apply : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDedekindDomain A] (C : Type u_3) [inst_5 : CommRing C]
  [inst_6 : Algebra B C] [inst_7 : Algebra A C] [IsScalarTower A B C] [inst_9 : Module.IsTorsionFree B C]
  [inst_10 : Module.IsTorsionFree A C] [inst_11 : IsDedekindDomain C] [inst_12 : IsDedekindDomain B] (x : ClassGroup A),
  (ClassGroup.extendedHom B C) ((ClassGroup.extendedHom A B) x) = (ClassGroup.extendedHom A C) x
-- Init.Data.Array.Perm
Array.Perm.pairwise : ∀ {α : Type u_1} {R : α → α → Prop} {xs ys : Array α},
  xs.Perm ys → List.Pairwise R xs.toList → (∀ {x y : α}, R x y → R y x) → List.Pairwise R ys.toList
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (s : AddSubgroup (Additive (NumberField.RingOfIntegers K)ˣ)),
  AddSubgroup.map (NumberField.Units.logEmbedding K) (s ⊔ Subgroup.toAddSubgroup (NumberField.Units.torsion K)) =
    AddSubgroup.map (NumberField.Units.logEmbedding K) s