mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.merge.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (ys : List α) (h_1 : (ys : List α) → motive [] ys)
  (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match [], ys with
    | [], ys => h_1 ys
    | xs, [] => h_2 xs
    | x :: xs, y :: ys => h_3 x xs y ys) =
    h_1 ys
-- Mathlib.Logic.Function.Conjugate
/-- We say that `f : α → β` semiconjugates `ga : α → α` to `gb : β → β` if `f ∘ ga = gb ∘ f`.
We use `∀ x, f (ga x) = gb (f x)` as the definition, so given `h : Function.Semiconj f ga gb` and
`a : α`, we have `h a : f (ga a) = gb (f a)` and `h.comp_eq : f ∘ ga = gb ∘ f`.
 -/
Function.Semiconj : {α : Type u_1} → {β : Type u_2} → (α → β) → (α → α) → (β → β) → Prop
-- Lean.Compiler.LCNF.Basic
/-- Given a scalar type `ty` and a value `fvarId : ty`, this operation returns a value of type
`tobject`. For small scalar values the result is a tagged pointer, and no memory allocation is
performed.
 -/
Lean.Compiler.LCNF.LetValue.box : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Expr →
    Lean.FVarId →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_21 →
        Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.connected_induce_union : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {s t : Set V},
  (SimpleGraph.induce s G).Preconnected →
    (SimpleGraph.induce t G).Preconnected → v ∈ s → w ∈ t → G.Adj v w → (SimpleGraph.induce (s ∪ t) G).Connected
-- Mathlib.Data.Finsupp.ToDFinsupp
Finsupp.toDFinsupp_neg : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddGroup M] (f : ι →₀ M), (-f).toDFinsupp = -f.toDFinsupp
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddGroup.addLeftReflectLE_of_addLeftMono : ∀ {N : Type u_2} [inst : AddGroup N] [inst_1 : LE N] [AddLeftMono N], AddLeftReflectLE N
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.mono_lift_of_mono_left : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.Limits.biprod.lift f g)
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
int_prod_range_pos : ∀ {m : ℤ} {n : ℕ}, Even n → m ∉ Set.Ico 0 ↑n → 0 < ∏ k ∈ Finset.range n, (m - ↑k)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- Every element of `α` has a successor.
 -/
Std.PRange.InfinitelyUpwardEnumerable.isSome_succ? : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} [self : Std.PRange.InfinitelyUpwardEnumerable α] (a : α),
  (Std.PRange.succ? a).isSome = true
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_pred_lt : ∀ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0), (a.pred ha).castSucc < a
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.existsAddOfLE : ∀ {α : Type u} [inst : LE α] [inst_1 : Add α] [ExistsAddOfLE α], ExistsAddOfLE (WithTop α)
-- Mathlib.Data.Seq.Defs
/-- Translate a sequence to a list. This function will run forever if
run on an infinite sequence.  -/
Stream'.Seq.forceToList : {α : Type u} → Stream'.Seq α → List α
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Taking representatives and then `MonoOver.exists` is isomorphic to taking `Subobject.exists`
and then taking representatives.
 -/
CategoryTheory.Subobject.existsCompRepresentativeIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasImages C] →
        (f : X ⟶ Y) →
          (CategoryTheory.Subobject.exists f).comp CategoryTheory.Subobject.representative ≅
            CategoryTheory.Subobject.representative.comp (CategoryTheory.MonoOver.exists f)
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_nnnorm_transpose : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A.transpose‖₊ = ‖A‖₊
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.codExtend'_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) {proj : Z → ↑s} (e : Bundle.Pretrivialization F proj) [inst_2 : Nonempty (B → F → Z)],
  (Bundle.Pretrivialization.codExtend' hs e).source = e.source
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.convs'Aux_stable_of_terminated : ∀ {K : Type u_1} {n m : ℕ} [inst : DivisionRing K] {s : Stream'.Seq (GenContFract.Pair K)},
  n ≤ m → s.TerminatedAt n → GenContFract.convs'Aux s m = GenContFract.convs'Aux s n
-- Mathlib.Algebra.Group.Units.Basic
eq_zero_of_add_right' : ∀ {α : Type u} [inst : AddCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 → a = 0
-- Mathlib.Algebra.Group.Pi.Basic
Function.extend_div : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Div γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ),
  Function.extend f (g₁ / g₂) (e₁ / e₂) = Function.extend f g₁ e₁ / Function.extend f g₂ e₂
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.getₘ : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] → (m : Std.DHashMap.Internal.Raw₀ α fun x => β) → (a : α) → m.containsₘ a = true → β
-- Lean.Meta.Tactic.Grind.Anchor
_private.Lean.Meta.Tactic.Grind.Anchor.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.mk.sizeOf_spec : ∀ {μ : YoungDiagram} (entry : ℕ → ℕ → ℕ) (row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2)
  (col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j)
  (zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0),
  sizeOf { entry := entry, row_weak' := row_weak', col_strict' := col_strict', zeros' := zeros' } = 1
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.comp_coe_cocycle₁_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0}
  (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ}
  {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0}
  (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι)),
  (CochainComplex.HomComplex.Cochain.ofHom π).comp
      ((↑(CochainComplex.Lifting.cocycle₁ sq hsq hQ hK)).comp (CochainComplex.HomComplex.Cochain.ofHom ι) ⋯) ⋯ =
    ↑(CochainComplex.Lifting.cocycle₁' sq hsq)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.symm_toStrongDual : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  WeakDual.toStrongDual.symm = StrongDual.toWeakDual
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csSup_zero : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : Zero M], sSup 0 = 0
-- Init.Data.Rat.Lemmas
Rat.divInt.eq_2 : ∀ (x : ℤ) (d : ℕ), Rat.divInt x (Int.negSucc d) = Rat.normalize (-x) d.succ ⋯
-- Init.Data.List.Basic
/-- Splits a list into the longest initial segment for which `p` returns `true`, paired with the
remainder of the list.

`O(|l|)`.

Examples:
* `[6, 8, 9, 5, 2, 9].span (· > 5) = ([6, 8, 9], [5, 2, 9])`
* `[6, 8, 9, 5, 2, 9].span (· > 10) = ([], [6, 8, 9, 5, 2, 9])`
* `[6, 8, 9, 5, 2, 9].span (· > 0) = ([6, 8, 9, 5, 2, 9], [])`
 -/
List.span : {α : Type u} → (α → Bool) → List α → List α × List α
-- Mathlib.Order.WithBotTop
WithBotTop.coe_le_coe : ∀ {ι : Type u_1} [inst : LE ι] {a b : ι}, WithBotTop.coe a ≤ WithBotTop.coe b ↔ a ≤ b
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.mapN.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι}
  (x x_1 : (SSet.Subcomplex.range (f.m j)).N), x = x_1 → f.mapN x = f.mapN x_1
-- Mathlib.Data.Sigma.Basic
Sigma.exists' : ∀ {α : Type u_1} {β : α → Type u_4} {p : (a : α) → β a → Prop}, (∃ a b, p a b) ↔ ∃ x, p x.fst x.snd
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Standard reflexive relations on types are internal reflexive relations in the category of
types.  -/
TypeCat.ReflexiveRelation.ofRefl : {X : Type w} →
  {φ : X → X → Prop} → Std.Refl φ → CategoryTheory.ReflexiveRelation (TypeCat.p₁OfRel φ) (TypeCat.p₂OfRel φ)
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.startPos_eq_endPos_iff : ∀ {s : String.Slice}, s.startPos = s.endPos ↔ s.isEmpty = true
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- If $(X, Y)$ is Gaussian, then $X$ and $Y$ are independent if they are uncorrelated.  -/
ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_strongDual : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [CompleteSpace E] [BorelSpace E]
  [SecondCountableTopology E] [inst_5 : NormedAddCommGroup F] [inst_6 : MeasurableSpace F] [CompleteSpace F]
  [BorelSpace F] [SecondCountableTopology F] [inst_10 : NormedSpace ℝ E] [inst_11 : NormedSpace ℝ F] {X : Ω → E}
  {Y : Ω → F},
  ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P →
    (∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), ProbabilityTheory.covariance (⇑L₁ ∘ X) (⇑L₂ ∘ Y) P = 0) →
      ProbabilityTheory.IndepFun X Y P
-- Mathlib.Util.DelabNonCanonical
/-- Delaborate an expression with arity `arity` into a binary notation `mkStx` iff either
argument `arg₁` or `arg₂` are non-canonical instances (are not defeq to what is synthesized for
its type, or else instance synthesis fails).  -/
Delab.Noncanonical.delabBinary : ℕ →
  ℕ →
    ℕ → (Lean.Term → Lean.Term → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term) → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- If `a < b`, then a morphism `T.obj₂ ⟶ T'.obj₂` extends to a morphism `T ⟶ T'`
of distinguished triangles when for a t-structure `T.obj₁ ≤ a` and `T'.obj₃ ≥ b`.  -/
CategoryTheory.Triangulated.TStructure.triangle_map_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {T T' : CategoryTheory.Pretriangulated.Triangle C},
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      ∀ (φ : T.obj₂ ⟶ T'.obj₂) (a b : ℤ),
        t.IsLE T.obj₁ a →
          t.IsGE T'.obj₃ b →
            autoParam (a < b) CategoryTheory.Triangulated.TStructure.triangle_map_exists._auto_1 → ∃ f, f.hom₂ = φ
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffAt_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'},
  (∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) → ContDiffAt 𝕜 n (∏ i ∈ t, f i) x
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- An orthonormal set of vectors in an `InnerProductSpace`  -/
Orthonormal : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → {ι : Type u_4} → (ι → E) → Prop
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.sum_add : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  (κ η : ι → ProbabilityTheory.Kernel α β),
  (ProbabilityTheory.Kernel.sum fun n => κ n + η n) = ProbabilityTheory.Kernel.sum κ + ProbabilityTheory.Kernel.sum η
-- Init.Data.Slice.Array.Lemmas
Subarray.foldlM_toList : ∀ {a : Type u_1} {init : a} {m : Type u_1 → Type u_2} [inst : Monad m] {α : Type u} {s : Subarray α} {f : a → α → m a}
  [LawfulMonad m], List.foldlM f init (Std.Slice.toList s) = Std.Slice.foldlM f init s
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.mk.congr_simp : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (coeff coeff_1 : Γ → R)
  (e_coeff : coeff = coeff_1) (isPWO_support' : (Function.support coeff).IsPWO),
  { coeff := coeff, isPWO_support' := isPWO_support' } = { coeff := coeff_1, isPWO_support' := ⋯ }
-- Mathlib.RingTheory.KrullDimension.Regular
ringKrullDim_quotSMulTop_succ_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] {x : R},
  IsSMulRegular R x → x ∈ IsLocalRing.maximalIdeal R → ringKrullDim (QuotSMulTop x R) + 1 = ringKrullDim R
-- Mathlib.CategoryTheory.Action.Basic
Action.instInhabitedAddCommGrpCat : (G : Type u_2) → [inst : Monoid G] → Inhabited (Action AddCommGrpCat G)
-- Mathlib.Order.Filter.Defs
Filter.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (sets : Set (Set α)) (univ_sets : Set.univ ∈ sets)
  (sets_of_superset : ∀ {x y : Set α}, x ∈ sets → x ⊆ y → y ∈ sets)
  (inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → x ∩ y ∈ sets),
  sizeOf { sets := sets, univ_sets := univ_sets, sets_of_superset := sets_of_superset, inter_sets := inter_sets } =
    1 + sizeOf univ_sets
-- Mathlib.Logic.Function.Iterate
/-- Iterate a function.  -/
«term_^[_]» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.equivSubZero_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ₁ φ₂ : S₁ ⟶ S₂) (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  (CategoryTheory.ShortComplex.Homotopy.equivSubZero φ₁ φ₂) h =
    (h.sub (CategoryTheory.ShortComplex.Homotopy.refl φ₂)).trans (CategoryTheory.ShortComplex.Homotopy.ofEq ⋯)
-- Mathlib.Algebra.Notation.Prod
Prod.instStar : {R : Type u_6} → {S : Type u_7} → [Star R] → [Star S] → Star (R × S)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.differentiableAt_cosh : ∀ {x : ℝ}, DifferentiableAt ℝ Real.cosh x
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.preimage : ∀ {R : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] {f : X → Y}
  {x : X} {s : Set Y},
  Convexity.IsAffineMap R f → Convexity.IsStarConvexSet R (f x) s → Convexity.IsStarConvexSet R x (f ⁻¹' s)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.π_leftRightHomologyComparison_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] [inst_3 : S.HasRightHomology] {Z : C}
  (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.leftHomologyπ
      (CategoryTheory.CategoryStruct.comp S.leftRightHomologyComparison
        (CategoryTheory.CategoryStruct.comp S.rightHomologyι h)) =
    CategoryTheory.CategoryStruct.comp S.iCycles (CategoryTheory.CategoryStruct.comp S.pOpcycles h)
-- Mathlib.Topology.UniformSpace.Defs
symm_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.map Prod.swap (uniformity α) ≤ uniformity α
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The second morphism in the factorization.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.π : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (K L : CochainComplex C ℤ) →
        [inst_2 : CategoryTheory.EnoughInjectives C] →
          (n₁ : ℤ) → CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.mid✝ K L n₁ ⟶ L
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_subset_Iio_union_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio b ⊆ Set.Iio a ∪ Set.Ico a b
-- Mathlib.Algebra.Group.PUnit
PUnit.instNeg_mathlib : Neg PUnit.{u_1 + 1}
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (s : Set α),
  SubAddAction.ofFixingAddSubgroup M s = { carrier := sᶜ, vadd_mem' := ⋯ }
-- Mathlib.LinearAlgebra.Prod
/-- `LinearMap.prodMap` as a `LinearMap`  -/
LinearMap.prodMapLinear : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      (M₃ : Type y) →
        (M₄ : Type z) →
          (S : Type u_3) →
            [inst : Semiring R] →
              [inst_1 : Semiring S] →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : AddCommMonoid M₃] →
                      [inst_5 : AddCommMonoid M₄] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module R M₂] →
                            [inst_8 : Module R M₃] →
                              [inst_9 : Module R M₄] →
                                [inst_10 : Module S M₃] →
                                  [inst_11 : Module S M₄] →
                                    [inst_12 : SMulCommClass R S M₃] →
                                      [inst_13 : SMulCommClass R S M₄] →
                                        (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄) →ₗ[S] M × M₂ →ₗ[R] M₃ × M₄
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.RightHomologyMapData.add_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
  (γ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₁ h₂), (γ.add γ').φH = γ.φH + γ'.φH
-- Mathlib.SetTheory.Cardinal.Free
instInfiniteFreeAddGroupOfNonempty : ∀ (α : Type u) [Nonempty α], Infinite (FreeAddGroup α)
-- Mathlib.Algebra.Group.Center
Set.addUnits_neg_mem_center : ∀ {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M}, ↑a ∈ Set.addCenter M → ↑(-a) ∈ Set.addCenter M
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.id.inj : ∀ {stx : Lean.Syntax} {id : Lean.Name} {danglingDot : Bool} {lctx : Lean.LocalContext}
  {expectedType? : Option Lean.Expr} {stx_1 : Lean.Syntax} {id_1 : Lean.Name} {danglingDot_1 : Bool}
  {lctx_1 : Lean.LocalContext} {expectedType?_1 : Option Lean.Expr},
  Lean.Elab.CompletionInfo.id stx id danglingDot lctx expectedType? =
      Lean.Elab.CompletionInfo.id stx_1 id_1 danglingDot_1 lctx_1 expectedType?_1 →
    stx = stx_1 ∧ id = id_1 ∧ danglingDot = danglingDot_1 ∧ lctx = lctx_1 ∧ expectedType? = expectedType?_1
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.LocallyOfFiniteType
-- Mathlib.Combinatorics.Additive.Convolution
Finset.op_vadd_addConvolution_eq_addConvolution_vadd : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (s : G),
  (AddOpposite.op s +ᵥ A).addConvolution B = A.addConvolution (s +ᵥ B)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.erase k).getKeyD k fallback = fallback
-- Mathlib.Dynamics.Ergodic.Conservative
MeasureTheory.Conservative.measure_inter_frequently_image_mem_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → μ (s ∩ {x | ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s}) = μ s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Complex.cos_eq_tsum' : ∀ (z : ℂ), Complex.cos z = ∑' (n : ℕ), (z * Complex.I) ^ (2 * n) / ↑(2 * n).factorial
-- Mathlib.Topology.Sober
/-- `x` is a generic point of `S` if `S` is the closure of `x`.  -/
IsGenericPoint : {α : Type u_1} → [TopologicalSpace α] → α → Set α → Prop
-- Lean.Data.Trie
Lean.Data.Trie.brecOn_2.eq : ∀ {α : Type} {motive_1 : Lean.Data.Trie α → Sort u} {motive_2 : Array (Lean.Data.Trie α) → Sort u}
  {motive_3 : List (Lean.Data.Trie α) → Sort u} (t : List (Lean.Data.Trie α))
  (F_1 : (t : Lean.Data.Trie α) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Data.Trie α)) → Lean.Data.Trie.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Data.Trie α)) → Lean.Data.Trie.below_2 t → motive_3 t),
  Lean.Data.Trie.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.Data.Trie.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.Order.Monotone.Defs
MonotoneOn.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, MonotoneOn g t → MonotoneOn f s → Set.MapsTo f s t → MonotoneOn (g ∘ f) s
-- Mathlib.Data.Finset.Sups
Finset.disjSups_left_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DistribLattice α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] (s t u : Finset α), s.disjSups (t.disjSups u) = t.disjSups (s.disjSups u)
-- Mathlib.Data.Setoid.Partition
/-- Two equivalence relations are equal iff their equivalence classes are equal.  -/
Setoid.classes_inj : ∀ {α : Type u_1} {r₁ r₂ : Setoid α}, r₁ = r₂ ↔ r₁.classes = r₂.classes
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- Composing the lift of a functor through a full subcategory with the inclusion yields the
original functor. This is actually true definitionally.  -/
CategoryTheory.ObjectProperty.liftCompιIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        (P : CategoryTheory.ObjectProperty D) →
          (F : CategoryTheory.Functor C D) → (hF : ∀ (X : C), P (F.obj X)) → (P.lift F hF).comp P.ι ≅ F
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
ContinuousWithinAt.clog : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {s : Set α} {x : α},
  ContinuousWithinAt f s x → f x ∈ Complex.slitPlane → ContinuousWithinAt (fun t => Complex.log (f t)) s x
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The right homotopy relation is reflexive.
 -/
SSet.Truncated.HomotopicR.refl : ∀ {X : SSet.Truncated 2}
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f : SSet.Truncated.Edge x y}, SSet.Truncated.HomotopicR f f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is an `AddCommSemigroup` under pointwise operations if `α` is.  -/
Set.addCommSemigroup : {α : Type u_2} → [AddCommSemigroup α] → AddCommSemigroup (Set α)
-- Mathlib.Topology.ClusterPt
/-- A point `a` is a cluster point of the sequence `x` if and only if `a` belongs to the closure
of every tail `x '' {n | i ≤ n}`.  -/
mapClusterPt_atTop_iff_forall_mem_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type u_3} [inst_1 : Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {x : ι → X} {a : X}, MapClusterPt a Filter.atTop x ↔ ∀ (i : ι), a ∈ closure (x '' Set.Ici i)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.d : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → ℤ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase_eq_erase! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced},
  (Std.DTreeMap.Internal.Impl.erase k t h).impl = Std.DTreeMap.Internal.Impl.erase! k t