mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.map_p : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).p = F.map h.p
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- This relies on `default ℕ = 0`.  -/
List.headI_le_sum : ∀ (L : List ℕ), L.headI ≤ L.sum
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.nat_mul_eq_of_eq_zero : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocSemiring α] [inst_1 : NegZeroClass β],
  Function.Antiperiodic f c → f 0 = 0 → ∀ (n : ℕ), f (↑n * c) = 0
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure_eq_of_le : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M},
  s ⊆ ↑S → S ≤ AddSubmonoid.closure s → AddSubmonoid.closure s = S
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactlyCoherentSpace.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsCoherentWith {K | IsCompact K} → CompactlyCoherentSpace X
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.multipliableLocallyUniformlyOn_eta : MultipliableLocallyUniformlyOn (fun n a => 1 - ModularForm.eta_q n a) UpperHalfPlane.upperHalfPlaneSet
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsBasis.filter.congr_simp : ∀ {α : Type u_1} {ι : Sort u_4} {p p_1 : ι → Prop} (e_p : p = p_1) {s s_1 : ι → Set α} (e_s : s = s_1)
  (h : Filter.IsBasis p s), h.filter = ⋯.filter
-- Mathlib.Data.ENNReal.BigOperators
/-- A sum is finite iff all summands are finite.  -/
ENNReal.sum_ne_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, ∑ a ∈ s, f a ≠ ⊤ ↔ ∀ a ∈ s, f a ≠ ⊤
-- Mathlib.Data.Part
Part.Mem.right_unique : ∀ {α : Type u_1}, Relator.RightUnique fun x1 x2 => x1 ∈ x2
-- Std.Data.TreeMap.Basic
/-- Check if any element satisfies the predicate, short-circuiting if a predicate fails.  -/
Std.TreeMap.any : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → (α → β → Bool) → Bool
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : PseudoEpimorphism α β),
  f.comp (PseudoEpimorphism.id α) = f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f : α → β} [inst_1 : Zero β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ),
  f =ᵐ[μ] MeasureTheory.AEFinStronglyMeasurable.mk f hf
-- Mathlib.Analysis.Convex.Segment
Pi.segment_subset : ∀ {𝕜 : Type u_1} {ι : Type u_5} {M : ι → Type u_6} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module 𝕜 (M i)] {s : Set ι} (x y : (i : ι) → M i),
  segment 𝕜 x y ⊆ s.pi fun i => segment 𝕜 (x i) (y i)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parentD_findAux_rootD : ∀ {self : Batteries.UnionFind} {x : Fin self.size},
  Batteries.UnionFind.parentD (self.findAux x).s (self.rootD ↑x) = self.rootD ↑x
-- Mathlib.Order.Zorn
zorn_le_nonempty : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α],
  (∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → BddAbove c) → ∃ m, IsMax m
-- Init.Data.String.Basic
String.Pos.Raw.IsValid.append_right : ∀ {s : String} {p : String.Pos.Raw}, String.Pos.Raw.IsValid s p → ∀ (t : String), String.Pos.Raw.IsValid (s ++ t) p
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzOnWith.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {K : NNReal} {s : Set α} {f : α → β} {g : β → γ} {t : Set β} {Kg : NNReal},
  LipschitzOnWith Kg g t → LipschitzOnWith K f s → Set.MapsTo f s t → LipschitzOnWith (Kg * K) (g ∘ f) s
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_ofFromSpecStalk : ∀ {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [inst : IrreducibleSpace ↥X]
  [inst_1 : AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↥X} [inst_2 : X.IsGermInjectiveAt x]
  (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y)
  (h : CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX),
  (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).fromSpecStalkOfMem ⋯ = φ
-- Lean.Elab.ConfigEval.Commands
/-- `declare_term_config_elab f struct binders* [where ...]` defines a configuration elaborator
```lean
f binders* (cfg : Syntax) (init : struct := {}) (logExceptions : Bool := true) : TermElabM struct
```
that evaluates the `cfg` configuration items to update `init`.
Acceptable configuration syntax is documented in `Lean.Elab.ConfigEval.foldConfigM`,
which includes anything that looks like `Lean.Parser.Term.optConfig`, possibly wrapped
in null nodes.

When `logExceptions` is true, it uses the current `errToSorry` state to decide whether or not to
recover by logging errors and skipping invalid options.

The command will transitively derive any necessary `ConfigEval.EvalTerm`/`ConfigEval.EvalExpr`
instances to support evaluation of configuration options for structure fields.
These instances will be `private local`.

See `ConfigEval.defEvalConfigItemCmd` for further documentation.

See also `declare_core_config_elab`, `declare_config_elab`, and `declare_command_config_elab`.
 -/
Lean.Elab.ConfigEval.declareTermConfigElab : Lean.ParserDescr
-- Batteries.Data.List.Lemmas
List.diff_nil : ∀ {α : Type u_1} [inst : BEq α] (l : List α), l.diff [] = l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t : Std.DTreeMap.Internal.Impl α β) (k : α)
  (v : β k) (ht : t.Balanced),
  t.getThenInsertIfNew? k v ht =
    match t.get? k with
    | none => (none, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ht).impl)
    | some b => (some b, t)
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inverseAssociator_map_inr_inr : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : E} (f : X ⟶ Y),
  (CategoryTheory.sum.inverseAssociator C D E).map
      ((CategoryTheory.Sum.inr_ C (D ⊕ E)).map ((CategoryTheory.Sum.inr_ D E).map f)) =
    (CategoryTheory.Sum.inr_ (C ⊕ D) E).map f
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_rightInverse : ∀ {n : ℕ} [NeZero n], Function.RightInverse ZMod.val Nat.cast
-- Mathlib.Algebra.GCDMonoid.Basic
/-- `normalize` in a `StrongNormalizationMonoid` as a `MonoidWithZeroHom`.  -/
normalizeHom : {α : Type u_1} → [inst : CommMonoidWithZero α] → [StrongNormalizationMonoid α] → α →*₀ α
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.extThms : Lean.Meta.Grind.ExtensionState → Lean.Meta.Grind.ExtTheorems
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.State.mk.injEq : ∀ (numSteps : ℕ) (cache : Lean.Meta.Sym.DSimp.Cache) (numSteps_1 : ℕ) (cache_1 : Lean.Meta.Sym.DSimp.Cache),
  ({ numSteps := numSteps, cache := cache } = { numSteps := numSteps_1, cache := cache_1 }) =
    (numSteps = numSteps_1 ∧ cache = cache_1)
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.rightFun_implicitFunctionDataOfProdDomain : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {f'u : E₁ × E₂ →L[𝕜] F}
  (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  (dfu.implicitFunctionDataOfProdDomain if₂u).rightFun = Prod.fst
-- Init.Data.UInt.Lemmas
USize.zero_mod : ∀ {a : USize}, 0 % a = 0
-- Mathlib.Algebra.MvPolynomial.Coeff
MvPolynomial.coeff_sum_X_pow_of_fintype : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype σ] (d : σ →₀ ℕ) (n : ℕ),
  MvPolynomial.coeff d ((∑ i, MvPolynomial.X i) ^ n) = ↑(if (d.sum fun x m => m) = n then d.multinomial else 0)
-- Mathlib.Computability.Encoding
_private.Mathlib.Computability.Encoding.0.Computability.encodePosNum.match_1.eq_3 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match n.bit1 with
    | PosNum.one => h_1 ()
    | n.bit0 => h_2 n
    | n.bit1 => h_3 n) =
    h_3 n
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : M) (n : ℕ), ↑((AdicCompletion.of I M) x) n = (I ^ n • ⊤).mkQ x
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
Polynomial.isCompact_image_comap_of_monic : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R),
  g.Monic → IsCompact (PrimeSpectrum.comap Polynomial.C '' (PrimeSpectrum.zeroLocus {g} \ PrimeSpectrum.zeroLocus {f}))
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.den : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          {𝒜 : ι → σ} → {x : Submonoid A} → (self : HomogeneousLocalization.NumDenSameDeg 𝒜 x) → ↥(𝒜 self.deg)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateRow_smul : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R)
  (j : n) (s : R) (u : n → R), (M.updateRow j (s • u)).det = s * (M.updateRow j u).det
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
/-- The Zariski precoverage on the category of schemes is the precoverage defined by
jointly surjective families of open immersions.  -/
AlgebraicGeometry.Scheme.zariskiPrecoverage : CategoryTheory.Precoverage AlgebraicGeometry.Scheme
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Given a coalgebra morphism whose carrier part is an epimorphism, we get an algebra epimorphism.
 -/
CategoryTheory.Comonad.algebra_epi_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X Y : G.Coalgebra}
  (f : X ⟶ Y) [h : CategoryTheory.Epi f.f], CategoryTheory.Epi f
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.addBuiltin : {γ : Type} → Lean.KeyedDeclsAttribute γ → Lean.KeyedDeclsAttribute.Key → Lean.Name → γ → IO Unit
-- Mathlib.Algebra.Group.Action.Defs
VAddAssocClass.mk : ∀ {M : Type u_9} {N : Type u_10} {α : Type u_11} [inst : VAdd M N] [inst_1 : VAdd N α] [inst_2 : VAdd M α],
  (∀ (x : M) (y : N) (z : α), (x +ᵥ y) +ᵥ z = x +ᵥ y +ᵥ z) → VAddAssocClass M N α
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Helper structure for the return type of the `test` function in `terminalReplacement`.  -/
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome : Type
-- Mathlib.Order.Hom.BoundedLattice
/-- `id` as a `BoundedLatticeHom`.  -/
BoundedLatticeHom.id : (α : Type u_2) → [inst : Lattice α] → [inst_1 : BoundedOrder α] → BoundedLatticeHom α α
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.add_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.toGL_mul : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A B : ↥(Matrix.unitaryGroup n α)),
  Matrix.UnitaryGroup.toGL (A * B) = Matrix.UnitaryGroup.toGL A * Matrix.UnitaryGroup.toGL B
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.linearDisjoint_iff : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E)
  (L : Type w) [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L ↔ A.LinearDisjoint (IsScalarTower.toAlgHom F L E).range
-- Mathlib.Topology.Order.Compact
/-- A continuous function with compact support has a global minimum.  -/
Continuous.exists_forall_le_of_hasCompactMulSupport : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] [Nonempty β] [inst_5 : One α] {f : β → α},
  Continuous f → HasCompactMulSupport f → ∃ x, ∀ (y : β), f x ≤ f y
-- Mathlib.Algebra.Ring.Action.Pointwise.Set
Set.neg_smul_set : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β] (a : α) (t : Set β),
  -a • t = -(a • t)
-- Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.Config.mk.sizeOf_spec : ∀ (toConfig : Lean.Meta.Rewrite.Config) (useRewrite implicationHyp useKAbstract : Bool),
  sizeOf
      { toConfig := toConfig, useRewrite := useRewrite, implicationHyp := implicationHyp,
        useKAbstract := useKAbstract } =
    1 + sizeOf toConfig + sizeOf useRewrite + sizeOf implicationHyp + sizeOf useKAbstract
-- Mathlib.Data.Sum.Order
Sum.Lex.inl_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : OrderBot α] [inst_2 : LE β], toLex (Sum.inl ⊥) = ⊥
-- Mathlib.Data.List.Iterate
Nat.iterate.eq_def : ∀ {α : Sort u} (op : α → α) (x : ℕ) (x_1 : α),
  op^[x] x_1 =
    match x, x_1 with
    | 0, a => a
    | k.succ, a => op^[k] (op a)
-- Mathlib.Combinatorics.SimpleGraph.Tutte
/-- **Tutte's theorem**

A graph has a perfect matching if and only if: For every subset `u` of vertices, removing this
subset induces at most `u.ncard` components of odd size. This is formally stated using the
predicate `IsTutteViolator`, which is satisfied exactly when this condition does not hold.  -/
SimpleGraph.tutte : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V], (∃ M, M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.sinhHomeomorph_apply : ⇑Real.sinhHomeomorph = Real.sinh
-- Mathlib.Algebra.Algebra.Unitization
NonUnitalAlgHom.toAlgHom_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {C : Type u_5} [inst_5 : Semiring C]
  [inst_6 : Algebra R C] (φ : A →ₙₐ[R] C) (x : Unitization R A),
  φ.toAlgHom x = (algebraMap R C) x.toProd.1 + φ x.toProd.2
-- Mathlib.Analysis.SpecificLimits.Normed
not_summable_of_ratio_test_tendsto_gt_one : ∀ {α : Type u_4} [inst : SeminormedAddCommGroup α] {f : ℕ → α} {l : ℝ},
  1 < l → Filter.Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) Filter.atTop (nhds l) → ¬Summable f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, t.WF → k ∈ Std.TreeMap.Raw.map f t → k ∈ t
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α},
  UpperSemicontinuousAt f x ↔ ∀ (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≥ y) → f x ≥ y
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- The image of a finitely presented additive group under a surjective additive
homomorphism whose kernel is finitely generated as a normal subgroup is finitely presented.  -/
AddGroup.IsFinitelyPresented.of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] [hG : AddGroup.IsFinitelyPresented G]
  (f : G →+ H), Function.Surjective ⇑f → f.ker.IsFinitelyNormallyGenerated → AddGroup.IsFinitelyPresented H
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.tmul_coe_mul_algebraMap_tmul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {j₁ : ι} (a₁ : A) (b₁ : ↥(ℬ j₁)) (r : R) (b₂ : B),
  a₁ ᵍ⊗ₜ[R] ↑b₁ * (algebraMap R A) r ᵍ⊗ₜ[R] b₂ = (a₁ * (algebraMap R A) r) ᵍ⊗ₜ[R] (↑b₁ * b₂)
-- Mathlib.Data.Set.Notation
/-- If the `Set.Notation` namespace is open, sets of a subtype coerced to the ambient type are
represented with `↑`.
 -/
Set.Notation.delabSetImageSubtype : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Order.Heyting.Basic
sdiff_le_sdiff_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, b ≤ a → c \ a ≤ c \ b
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The `finrank` of `M × M'` is `(finrank R M) + (finrank R M')`.  -/
Module.finrank_prod : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [StrongRankCondition R] [Module.Free R M] [Module.Free R M']
  [Module.Finite R M] [Module.Finite R M'], Module.finrank R (M × M') = Module.finrank R M + Module.finrank R M'
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.hom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → {f g : C ⟶ D} → Homotopy f g → (i j : ι) → C.X i ⟶ D.X j
-- Mathlib.Algebra.Star.Basic
isLeftRegular_star_iff : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x : R}, IsLeftRegular (star x) ↔ IsRightRegular x
-- Mathlib.Algebra.Free
FreeSemigroup.length_map : ∀ {α : Type u} {β : Type v} (f : α → β) (x : FreeSemigroup α), ((FreeSemigroup.map f) x).length = x.length
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.sumIDeriv_map : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) (f : R →+* S),
  Polynomial.sumIDeriv (Polynomial.map f p) = Polynomial.map f (Polynomial.sumIDeriv p)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instIsScalarTowerHahnSeries_1 : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [IsOrderedCancelAddMonoid Γ] [inst_3 : PartialOrder Γ'] [inst_4 : AddAction Γ Γ'] [inst_5 : IsOrderedCancelVAdd Γ Γ']
  [inst_6 : AddCommMonoid V] [inst_7 : Semiring R] [inst_8 : Module R V],
  IsScalarTower R (HahnSeries Γ R) (HahnModule Γ' R V)
-- Init.Data.Nat.Lemmas
Nat.add_eq_zero_iff : ∀ {n m : ℕ}, n + m = 0 ↔ n = 0 ∧ m = 0
-- Mathlib.CategoryTheory.EqToHom
/-- A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`.  -/
CategoryTheory.eqToHom_iso_inv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b)
  {j j' : β} (w : j = j'),
  CategoryTheory.CategoryStruct.comp (z j).inv (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').inv
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- `ContMDiff I I' n f` indicates that the function `f : M → M'` between manifolds
is `n` times continuously differentiable.

`f` is `n` times continuously differentiable if it is continuous and, for any pair of points,
it is `n` times continuously differentiable in the charts around these points.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions.  -/
ContMDiff : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                ModelWithCorners 𝕜 E' H' →
                                  {M' : Type u_7} →
                                    [inst : TopologicalSpace M'] → [ChartedSpace H' M'] → WithTop ℕ∞ → (M → M') → Prop
-- Mathlib.Algebra.Module.Torsion.Basic
/-- An `S`-torsion module is a module where every element is `a`-torsion for some `a` in `S`.  -/
Module.IsTorsion' : (M : Type u_2) → [AddCommMonoid M] → (S : Type u_3) → [SMul S M] → Prop
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.sup_eq_top_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p p' : Submodule R M), p ⊔ p' = ⊤ ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v
-- Mathlib.Data.List.Cycle
List.pmap_prev_eq_rotate_length_sub_one : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → List.pmap l.prev l ⋯ = l.rotate (l.length - 1)
-- Mathlib.Data.ENNReal.Action
ENNReal.smul_top : ∀ {R : Type u_1} [inst : Semiring R] [IsDomain R] [inst_2 : Module R ENNReal] [IsScalarTower R ENNReal ENNReal]
  [Module.IsTorsionFree R ENNReal] [inst_5 : DecidableEq R] (c : R), c • ⊤ = if c = 0 then 0 else ⊤
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_union_Icc_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ b → b ≤ c → Set.Icc a b ∪ Set.Icc b c = Set.Icc a c
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.unfold.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.Seq1 α) → Sort u_2) →
    (x : Option (Stream'.Seq1 α)) →
      (Unit → motive none) → ((t_hd : α) → (t_tl : Stream'.Seq α) → motive (some (t_hd, t_tl))) → motive x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_one_iff : ∀ {x y : ℝ}, 0 ≤ x → (x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y)
-- Mathlib.CategoryTheory.Grothendieck
/-- The identity morphism in the Grothendieck category.
 -/
CategoryTheory.Grothendieck.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} → (X : CategoryTheory.Grothendieck F) → X.Hom X
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.instPartialOrder : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → PartialOrder (L.ElementarySubstructure M)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (X_1 : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso α β X).hom.app X_1).right.right =
    CategoryTheory.CategoryStruct.id X_1.right.right