mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.zmod.eq_1 : ∀ (n : ℕ) [inst : NeZero n] (x : ZMod n),
  AddChar.zmod n x =
    { toFun := AddCircle.toCircle, map_zero_eq_one' := AddChar.zmod._proof_1,
          map_add_eq_mul' := AddChar.zmod._proof_2 }.compAddMonoidHom
      (ZMod.toAddCircle.comp (AddMonoidHom.mulLeft x))
-- Mathlib.Logic.Equiv.Prod
Equiv.piEquivPiSubtypeProd_symm_apply : ∀ {α : Type u_9} (p : α → Prop) (β : α → Type u_10) [inst : DecidablePred p]
  (f : ((i : { x // p x }) → β ↑i) × ((i : { x // ¬p x }) → β ↑i)) (x : α),
  (Equiv.piEquivPiSubtypeProd p β).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
-- Mathlib.Tactic.Abel
/-- Interpret an integer as a coefficient to a term.  -/
Mathlib.Tactic.Abel.intToExpr : ℤ → Mathlib.Tactic.Abel.M Lean.Expr
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α ≃o β} {s : UpperSet α} {b : β},
  b ∈ (UpperSet.map f) s ↔ f.symm b ∈ s
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.span_root_support : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base),
  Submodule.span R (⇑P.root '' ↑b.support) = P.rootSpan R
-- Init.Data.Range.Polymorphic.PRange
/-- For every pair of elements `init` and `hi`, there exists a chain of successors that
  results in an element that either has no successors or is greater than `hi`.
   -/
Std.Rxc.IsAlwaysFinite.finite : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : LE α} [self : Std.Rxc.IsAlwaysFinite α] (init hi : α),
  ∃ n, (Std.PRange.succMany? n init).elim True fun x => ¬x ≤ hi
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_eq_single_one_one_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k] {a : SkewMonoidAlgebra k G},
  (a.coeff = fun₀ | 1 => 1) ↔ a = 1
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instSemilatticeSupOpenNormalSubgroup.eq_1 : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousMul G],
  OpenNormalSubgroup.instSemilatticeSupOpenNormalSubgroup =
    Function.Injective.semilatticeSup (fun H => ↑H.toOpenSubgroup) ⋯ ⋯ ⋯ ⋯
-- Init.Grind.ToInt
Lean.Grind.IntInterval.mem_ci : ∀ (lo x : ℤ), x ∈ Lean.Grind.IntInterval.ci lo ↔ lo ≤ x
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_iff_isUTF8FirstByte : ∀ {s : String.Slice} {p : String.Pos.Raw},
  String.Pos.Raw.IsValidForSlice s p ↔ p = s.rawEndPos ∨ ∃ (h : p < s.rawEndPos), (s.getUTF8Byte p h).IsUTF8FirstByte
-- Mathlib.Algebra.Group.Int.Defs
Int.instCommSemigroup : CommSemigroup ℤ
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient_fun_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (x : F) (c : 𝕜), gradient (fun x => c) x = 0
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFinset_map : ∀ {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) [inst : Fintype α] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {n : ℕ} [inst_3 : Fintype β] [inst_4 : DecidableEq β] (f : α ↪ β),
  n ≠ 1 → (SimpleGraph.map (⇑f) G).cliqueFinset n = Finset.map { toFun := Finset.map f, inj' := ⋯ } (G.cliqueFinset n)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instToExprProof.toExpr : Mathlib.Tactic.ITauto.Proof → Lean.Expr
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanHom_id : ∀ {α : Type u_2} [inst : CommMonoid α] {A₁ A₂ : Set α} {n : ℕ}, A₁ ⊆ A₂ → IsMulFreimanHom n A₁ A₂ id
-- Lean.Data.Lsp.Ipc
_private.Lean.Data.Lsp.Ipc.0.Lean.Lsp.Ipc.collectDiagnostics.loop : Lean.JsonRpc.RequestID →
  Option Lean.Lsp.PublishDiagnosticsParams →
    Lean.Lsp.Ipc.IpcM (Option (Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams))
-- Lean.Elab.App
Lean.Elab.Term.elabExplicitUnivs : Array Lean.Syntax → Lean.Elab.TermElabM (List Lean.Level)
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.instAddActionSubtypeAEEqFunMemAddAddSubgroupLp : {M : Type u_1} →
  {α : Type u_3} →
    {E : Type u_4} →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {μ : MeasureTheory.Measure α} →
            {p : ENNReal} →
              [inst_2 : AddMonoid M] →
                [inst_3 : AddAction M α] →
                  [MeasureTheory.VAddInvariantMeasure M α μ] →
                    [MeasurableConstVAdd M α] → AddAction Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Algebra.Star.SelfAdjoint
/-- A normal element of a star monoid commutes with its adjoint.  -/
IsStarNormal.star_comm_self : ∀ {R : Type u_1} {inst : Mul R} {inst_1 : Star R} {x : R} [self : IsStarNormal x], Commute (star x) x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          aig.RefVec w → aig.RefVec w → (curr : ℕ) → curr ≤ w → aig.Ref → aig.RefVec curr → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Topology.Order
tendsto_nhds_Prop : ∀ {α : Type u_1} {l : Filter α} {p : α → Prop} {q : Prop}, Filter.Tendsto p l (nhds q) ↔ q → ∀ᶠ (x : α) in l, p x
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.restrict_isCircuit_iff : ∀ {α : Type u_1} {M : Matroid α} {C R : Set α},
  autoParam (R ⊆ M.E) Matroid.restrict_isCircuit_iff._auto_1 → ((M.restrict R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R)
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.below.rfind : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n →. ℕ) → Nat.Partrec' a → Prop} {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ}
  (a : Nat.Partrec' ↑f), Nat.Partrec'.below a → motive (↑f) a → Nat.Partrec'.below ⋯
-- Init.Data.String.Basic
String.Slice.Pos.le_ofSliceFrom : ∀ {s : String.Slice} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos}, p₀ ≤ String.Slice.Pos.ofSliceFrom pos
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.of_symm_image_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, ↑e.symm '' (e.target ∩ t) = e.source ∩ s → e.IsImage s t
-- Std.Http.Data.Request
/-- Creates a new HTTP DELETE Request builder with the specified URI.
 -/
Std.Http.Request.delete : Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.NumberTheory.Modular
ModularGroup.im_T_zpow_smul : ∀ (z : UpperHalfPlane) (n : ℤ), (ModularGroup.T ^ n • z).im = z.im
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.natCast_mul_eq_nsmul : ∀ (x : ℝ) (n : ℕ), ↑(↑n * x) = n • ↑x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_iff_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α},
  a ∈ m ↔ (m.get? a).isSome = true
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- The underlying submonoid of a `NonUnitalSubring`.  -/
NonUnitalSubring.toSubsemigroup : {R : Type u} → [inst : NonUnitalNonAssocRing R] → NonUnitalSubring R → Subsemigroup R
-- Aesop.Stats.Basic
Aesop.instInhabitedRuleStats.default : Aesop.RuleStats
-- Mathlib.CategoryTheory.Elements
/-- Constructor for isomorphisms in the category of elements of a functor to types.  -/
CategoryTheory.CategoryOfElements.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} →
      (x y : F.Elements) →
        (e : x.fst ≅ y.fst) → (CategoryTheory.ConcreteCategory.hom (F.map e.hom)) x.snd = y.snd → (x ≅ y)
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instCommutativeMeet : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l], Std.Commutative fun x1 x2 => Lean.Order.meet x1 x2
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHSubOffset_1 : HSub Std.Time.PlainDateTime Std.Time.Week.Offset Std.Time.PlainDateTime
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Sort u_1} {U : ι → Y.Opens},
  iSup U = ⊤ → ⨆ i, (TopologicalSpace.Opens.map f.base).obj (U i) = ⊤
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- The isomorphism of `S`-modules between `I ⧸ I ^ 2` and `σ → S` given
by `P.relation i ↦ ∂ⱼ (P.relation i)`.  -/
Algebra.SubmersivePresentation.cotangentEquiv : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] → (P : Algebra.SubmersivePresentation R S ι σ) → P.toExtension.Cotangent ≃ₗ[S] σ → S
-- Mathlib.Algebra.Order.Group.Basic
zsmul_lt_zsmul_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α},
  0 < a → (m • a < n • a ↔ m < n)
-- Init.Data.Nat.Lemmas
Nat.mul_self_le_mul_self_iff : ∀ {m n : ℕ}, m * m ≤ n * n ↔ m ≤ n
-- Mathlib.Algebra.GroupWithZero.Action.Defs
AddGroup.int_smulCommClass : ∀ {M : Type u_1} {A : Type u_7} [inst : AddGroup A] [inst_1 : DistribSMul M A], SMulCommClass ℤ M A
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.subsingleton_liftStruct_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : X ⟶ A} {i : B ⟶ A} {p : Y ⟶ X}
  {g : Y ⟶ B} (sq : CategoryTheory.CommSq g p i f) [CategoryTheory.Mono i], Subsingleton sq.LiftStruct
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.subst.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_4} (motive : L.Term α → (α → L.Term β) → Sort u_5) (a : α)
  (tf : α → L.Term β) (h_1 : (a : α) → (tf : α → L.Term β) → motive (FirstOrder.Language.var a) tf)
  (h_2 :
    (l : ℕ) →
      (f : L.Functions l) → (ts : Fin l → L.Term α) → (tf : α → L.Term β) → motive (FirstOrder.Language.func f ts) tf),
  (match FirstOrder.Language.var a, tf with
    | FirstOrder.Language.var a, tf => h_1 a tf
    | FirstOrder.Language.func f ts, tf => h_2 l f ts tf) =
    h_1 a tf
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addCommMagma.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : AddCommMagma M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Injective.addCommMagma f hf mul = { toAdd := inst, add_comm := ⋯ }
-- Init.Meta.Defs
/-- Valid identifier names  -/
Lean.isGreek : Char → Bool
-- Mathlib.RepresentationTheory.Irreducible
Representation.IsIrreducible.instSubsingletonIntertwiningMapOfIsEmptyEquiv : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {σ : Representation k G W} [ρ.IsIrreducible] [σ.IsIrreducible] [IsEmpty (ρ.Equiv σ)],
  Subsingleton (ρ.IntertwiningMap σ)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.instInhabited : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → Inhabited (CategoryTheory.MonoOver X)
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.instCoeConvexCone : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] → [inst_4 : Module R E] → Coe (PointedCone R E) (ConvexCone R E)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `L/E/K` is a tower of fields and `x = algebraMap E L g`, then the spectral norm
of `g : E` when regarded as an element of the normal closure of `E` equals the spectral norm
of `x : L`.  -/
spectralNorm.eq_of_normalClosure : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  {E : IntermediateField K L} {x : L} (g : ↥E),
  (algebraMap (↥E) L) g = x →
    spectralNorm K (↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E)))
        ((algebraMap ↥E ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) g) =
      spectralNorm K L x
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The center of a (not necessarily associative) semiring
is isomorphic to the center of its opposite.  -/
Subsemiring.centerToMulOpposite : {R : Type u} → [inst : NonAssocSemiring R] → ↥(Subsemiring.center R) ≃+* ↥(Subsemiring.center Rᵐᵒᵖ)
-- Init.Data.Array.MapIdx
Array.mapFinIdx_congr : ∀ {α : Type u_1} {β : Type u_2} {xs ys : Array α} (w : xs = ys) (f : (i : ℕ) → α → i < xs.size → β),
  xs.mapFinIdx f = ys.mapFinIdx fun i a h => f i a ⋯
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.exists_mul_add_sub_mem_of_mem_jacobson : ∀ {R : Type u} [inst : Ring R] {I : Ideal R}, ∀ r ∈ I.jacobson, ∃ s, s * (r + 1) - 1 ∈ I
-- Mathlib.Order.Hom.Basic
OrderHom.prod_coe : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α →o β) (g : α →o γ) (x : α), (f.prod g) x = (f x, g x)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.op_hom_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C), (β_ X Y).hom.op = (β_ (Opposite.op Y) (Opposite.op X)).hom
-- Mathlib.Data.List.Map2
List.map₂Right_eq_map₂Right' : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) (bs : List β),
  List.map₂Right f as bs = (List.map₂Right' f as bs).1
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
CategoryTheory.FunctorToTypes.monoidalClosed : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MonoidalClosed (CategoryTheory.Functor C (Type (max w v u)))
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.leSupr_apply_mk : ∀ {X : TopCat} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X) (i : ι) (x : ↑X) (m : x ∈ U i),
  (TopologicalSpace.Opens.leSupr U i) ⟨x, m⟩ = ⟨x, ⋯⟩
-- Init.Data.SInt.IntToBitVec
Int32.toBitVec64_toISize : ∀ (n : Int32) (h : System.Platform.numBits = 64), n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec
-- Mathlib.SetTheory.Cardinal.NatCard
List.Nodup.length_le_enatCard : ∀ {α : Type u_1} {l : List α}, l.Nodup → ↑l.length ≤ ENat.card α
-- Mathlib.Data.Fin.Tuple.Basic
Set.insert.eq_1 : ∀ {α : Type u} (a : α) (s : Set α), Set.insert a s = {b | b = a ∨ b ∈ s}
-- Mathlib.Data.Finset.Image
/-- If a `Finset` is a subset of the image of a `Set` under `f`,
then it is equal to the `Finset.image` of a `Finset` subset of that `Set`.  -/
Finset.subset_set_image_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Set α} {t : Finset β} {f : α → β},
  ↑t ⊆ f '' s ↔ ∃ s', ↑s' ⊆ s ∧ Finset.image f s' = t
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_add : ∀ {α : Type u_1} (xs ys : FreeAddMonoid α),
  FreeAddMonoid.toList (xs + ys) = FreeAddMonoid.toList xs ++ FreeAddMonoid.toList ys
-- Mathlib.Data.Fintype.EquivFin
Fintype.card_le_one_iff_subsingleton : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α ≤ 1 ↔ Subsingleton α
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph.isPath_tail_cycle : ∀ {n : ℕ}, (SimpleGraph.cycleGraph.cycle n).tail.IsPath
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α], 1⁻ᵐ = 1
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.smulRightₗ_apply : ∀ {R : Type u_1} {M : Type u_4} {M₂ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M₂ →ₗ[R] R) (x : M),
  (LinearMap.smulRightₗ f) x = f.smulRight x
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion g]
  [AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)], AlgebraicGeometry.IsOpenImmersion f
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by erasing elements from `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.IteratedEntryErasureFrom : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Type (max 0 u v)
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_succ_of_lt : ∀ {n : ℕ} (p i : Fin n), p < i → p.succ.succAbove i = i.succ
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.descHomotopyZeroZero.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z}
  (f f_1 : I.cocomplex ⟶ J.cocomplex) (e_f : f = f_1) (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0),
  CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm =
    CategoryTheory.InjectiveResolution.descHomotopyZeroZero f_1 ⋯
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_map : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {N : Type u_5} [inst_1 : AddGroup N] {P : Type u_6}
  [inst_2 : AddGroup P] (g : N →+ P) (f : G →+ N),
  AddSubgroup.map g (AddSubgroup.map f K) = AddSubgroup.map (g.comp f) K
-- Mathlib.RingTheory.Etale.Finite
/-- The category of finite étale `R`-algebras.  -/
CommAlgCat.FiniteEtale : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.one_eq_closure : ∀ {R : Type u_2} [inst : AddMonoidWithOne R], 1 = AddSubmonoid.closure {1}
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- An alternative to `biproduct.map` constructed via colimits.
This construction only exists in order to show it is equal to `biproduct.map`.  -/
CategoryTheory.Limits.biproduct.map' : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {f g : J → C} →
          [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
            [inst_3 : CategoryTheory.Limits.HasBiproduct g] → ((b : J) → f b ⟶ g b) → (⨁ f ⟶ ⨁ g)
-- Mathlib.Data.Finsupp.Sigma
/-- `embSigma` is a left inverse to `split` at the same index.  -/
Finsupp.split_embSigma_self : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k : κ} (f : ι k →₀ M), f.embSigma.split k = f
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- `N`-conjugacy is transitive.  -/
AddGroupExtension.IsAddConj.trans : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  (S : AddGroupExtension N E G) {s₁ s₂ s₃ : S.Splitting}, S.IsAddConj s₁ s₂ → S.IsAddConj s₂ s₃ → S.IsAddConj s₁ s₃
-- Init.Data.Iterators.Consumers.Monadic.Access
Std.IterM.IsPlausibleNthOutputStep.below.skip : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β]
  {motive :
    (a : ℕ) →
      (a_1 : Std.IterM m β) →
        (a_2 : Std.IterStep (Std.IterM m β) β) → Std.IterM.IsPlausibleNthOutputStep a a_1 a_2 → Prop}
  {n : ℕ} {it it' : Std.IterM m β} {step : Std.IterStep (Std.IterM m β) β}
  (a : it.IsPlausibleStep (Std.IterStep.skip it')) (a_1 : Std.IterM.IsPlausibleNthOutputStep n it' step),
  Std.IterM.IsPlausibleNthOutputStep.below a_1 → motive n it' step a_1 → Std.IterM.IsPlausibleNthOutputStep.below ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A natural isomorphism between the functor `map (𝟭 C)` and `𝟭 (WithTerminal C)`.  -/
CategoryTheory.WithTerminal.mapId : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.WithTerminal.map (CategoryTheory.Functor.id C) ≅
      CategoryTheory.Functor.id (CategoryTheory.WithTerminal C)
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.toPrefunctor_symm_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Quiver.SingleObj α ⥤q Quiver.SingleObj β)
  (g : Quiver.SingleObj β ⥤q Quiver.SingleObj γ),
  Quiver.SingleObj.toPrefunctor.symm (f ⋙q g) =
    Quiver.SingleObj.toPrefunctor.symm g ∘ Quiver.SingleObj.toPrefunctor.symm f
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.toMatrix_smul : ∀ {R : Type u_3} {N : Type u_5} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : Invertible 2] [inst_4 : AddCommGroup N] [inst_5 : Module R N] (b : Module.Basis n R N) (a : R)
  (Q : QuadraticForm R N), QuadraticForm.toMatrix b (a • Q) = a • QuadraticForm.toMatrix b Q
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_fun_abs : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ (p : ENNReal), MeasureTheory.lpNorm (fun x => |f x|) p μ = MeasureTheory.lpNorm f p μ
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.LimitCone.mk : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          (cone : CategoryTheory.Limits.Cone F) → CategoryTheory.Limits.IsLimit cone → CategoryTheory.Limits.LimitCone F
-- Lean.Elab.Tactic.Omega.Frontend
/-- Helpful error message when omega cannot find a solution
 -/
Lean.Elab.Tactic.Omega.formatErrorMessage : Lean.Elab.Tactic.Omega.Problem → Lean.Elab.Tactic.Omega.OmegaM Lean.MessageData
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.hom_ofHom : ∀ {X Y : Type u} [inst : UniformSpace X] [inst_1 : UniformSpace Y] (f : { f // UniformContinuous f }),
  UniformSpaceCat.Hom.hom (UniformSpaceCat.ofHom f) = f
-- Std.Async.Basic
/-- Runs two computations concurrently and returns both results as a pair.
 -/
Std.Async.EAsync.concurrently : {ε α β : Type} →
  Std.Async.EAsync ε α →
    Std.Async.EAsync ε β → optParam Task.Priority Task.Priority.default → Std.Async.EAsync ε (α × β)
-- Lean.Data.SMap
/-- Monadic fold over a staged map.  -/
Lean.SMap.foldM : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        {σ : Type w} → {m : Type w → Type w'} → [Monad m] → (σ → α → β → m σ) → σ → Lean.SMap α β → m σ
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- Define a `Kernel α γ` from a `Kernel (α × β) γ` by taking the comap of `fun a ↦ (a, b)` for
a given `b : β`.  -/
ProbabilityTheory.Kernel.sectL : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          {mγ : MeasurableSpace γ} → ProbabilityTheory.Kernel (α × β) γ → β → ProbabilityTheory.Kernel α γ
-- Mathlib.Order.WellFoundedSet
Set.Subsingleton.partiallyWellOrderedOn : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [Std.Refl r], s.Subsingleton → s.PartiallyWellOrderedOn r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.get!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {k : α} [inst_1 : Inhabited (β k)], t₁.get! k = t₂.get! k
-- Std.Data.DHashMap.Basic
/-- Support for the `for` loop construct in `do` blocks.  -/
Std.DHashMap.Const.forInUncurried : {α : Type u} →
  {δ : Type w} →
    {m : Type w → Type w'} →
      [Monad m] →
        {x : BEq α} →
          {x_1 : Hashable α} → {β : Type v} → (α × β → δ → m (ForInStep δ)) → δ → (Std.DHashMap α fun x => β) → m δ
-- Std.Data.DTreeMap.DecidableEquiv
Std.DTreeMap.instDecidableEquivOfTransCmpOfLawfulEqCmpOfLawfulBEq : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        [Std.LawfulEqCmp cmp] →
          [inst : (k : α) → BEq (β k)] →
            [∀ (k : α), LawfulBEq (β k)] → {t₁ t₂ : Std.DTreeMap α β cmp} → Decidable (t₁.Equiv t₂)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.obj_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n)
  (X : C), CategoryTheory.ComposableArrows.Precomp.obj F X 0 = X
-- Mathlib.Order.Hom.Lattice
SupHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Max α] [inst_1 : Max β] [inst_2 : Max γ]
  [inst_3 : Max δ] (f : SupHom γ δ) (g : SupHom β γ) (h : SupHom α β), (f.comp g).comp h = f.comp (g.comp h)