mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_of_cfcHom_injective : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  Function.Injective ⇑(cfcₙHom_of_cfcHom R ha)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_addZ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (P Q : Fin 3 → R),
  WeierstrassCurve.Jacobian.addZ (⇑f ∘ P) (⇑f ∘ Q) = f (WeierstrassCurve.Jacobian.addZ P Q)
-- Lean.Parser.Term
Lean.Parser.Term.letOptNondep.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] [inst_3 : Fintype β]
  {s : Finset α}, s.Nonempty → s • Finset.univ = Finset.univ
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.ofNat.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Order.Antichain
Std.Symm.compl : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Std.Symm rᶜ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryLE?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.getEntryLE? k t₁ = Std.DTreeMap.Internal.Impl.getEntryLE? k t₂
-- Mathlib.Data.ZMod.Basic
ZMod.subsingleton_ringHom : ∀ {n : ℕ} {R : Type u_1} [inst : Semiring R], Subsingleton (ZMod n →+* R)
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f: M → N` and `g: M' × N'` are immersions at `x` and `x'`, respectively,
then `f × g: M × N → M' × N'` is an immersion at `(x, x')`.  -/
Manifold.IsImmersionAtOfComplement.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u_3} {E''' : Type u_4} {E'' : Type u}
  {F : Type u_5} {F' : Type u_6} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] [inst_5 : NormedAddCommGroup E'']
  [inst_6 : NormedSpace 𝕜 E''] [inst_7 : NormedAddCommGroup E'''] [inst_8 : NormedSpace 𝕜 E''']
  [inst_9 : NormedAddCommGroup F] [inst_10 : NormedSpace 𝕜 F] [inst_11 : NormedAddCommGroup F']
  [inst_12 : NormedSpace 𝕜 F'] {H : Type u_7} [inst_13 : TopologicalSpace H] {H' : Type u_8}
  [inst_14 : TopologicalSpace H'] {G : Type u_9} [inst_15 : TopologicalSpace G] {G' : Type u_10}
  [inst_16 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} [inst_17 : TopologicalSpace M]
  [inst_18 : ChartedSpace H M] {M' : Type u_12} [inst_19 : TopologicalSpace M'] [inst_20 : ChartedSpace H' M']
  {N : Type u_13} [inst_21 : TopologicalSpace N] [inst_22 : ChartedSpace G N] {N' : Type u_14}
  [inst_23 : TopologicalSpace N'] [inst_24 : ChartedSpace G' N'] {n : WithTop ℕ∞} {x : M} {f : M → N} {g : M' → N'}
  {x' : M'} [IsManifold I n M] [⋯], ⋯
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddSemigroup : {α : Type u_1} → [AddSemigroup α] → AddSemigroup αᵐᵒᵖ
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Destructor for `Cofix F`  -/
MvQPF.Cofix.dest : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → MvQPF.Cofix F α → F (α ::: MvQPF.Cofix F α)
-- Mathlib.Algebra.Algebra.Pi
Pi.constAlgHom_eq_algebra_ofId : ∀ (R : Type u_2) [inst : CommSemiring R] (A : Type u_5), Pi.constAlgHom R A R = Algebra.ofId R (A → R)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_iSup_of_monotone : ∀ {Ω : Type u_1} {ι : Type u_2} {m' m₁ mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : SemilatticeSup ι]
  {m : ι → MeasurableSpace Ω},
  (∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm' μ) →
    (∀ (i : ι), m i ≤ mΩ) → m₁ ≤ mΩ → Monotone m → ProbabilityTheory.CondIndep m' (⨆ i, m i) m₁ hm' μ
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mk_mem_row_iff : ∀ {μ : YoungDiagram} {i j : ℕ}, (i, j) ∈ μ.row i ↔ (i, j) ∈ μ
-- Init.Classical
Classical.not_exists_not : ∀ {α : Sort u_1} {p : α → Prop}, (¬∃ x, ¬p x) ↔ ∀ (x : α), p x
-- Mathlib.Data.ENNReal.Basic
/-- Coercion from `ℝ≥0` to `ℝ≥0∞`.  -/
ENNReal.ofNNReal : NNReal → ENNReal
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.δ_naturality : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f')
  (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (n₀ n₁ : ℤ),
  autoParam (α.app 1 = β.app 0) CategoryTheory.Abelian.SpectralObject.δ_naturality._auto_1 →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_naturality._auto_3),
      CategoryTheory.CategoryStruct.comp ((X.H n₀).map β) (X.δ f' g' n₀ n₁ hn₁) =
        CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((X.H n₁).map α)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_eq_some_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.maxKey? = some (t.maxKeyD fallback)
-- Mathlib.GroupTheory.Commutator.Basic
/-- The commutator subgroup of an additive group G is the normal additive subgroup
generated by the additive commutators `[p,q] = p + q + -p + -q`.  -/
addCommutator : (G : Type u_1) → [inst : AddGroup G] → AddSubgroup G
-- Mathlib.Data.List.MinMax
List.maximum_mem : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] {l : List α} {m : α}, l.maximum = ↑m → m ∈ l
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_Iio_succ : ∀ {n : ℕ} (i : Fin n), Fin.succ ⁻¹' Set.Iio i.succ = Set.Iio i
-- Mathlib.Data.Set.Card
Set.ncard_strictMono : ∀ {α : Type u_1} [Finite α], StrictMono Set.ncard
-- Mathlib.Tactic.Peel
/-- Peel off quantifiers from an `↔` and assign the names given in `l` to the introduced
variables.  -/
Mathlib.Tactic.Peel.peelArgsIff : List Lean.Name → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The linear map corresponding to `affineCombination` is
`weightedVSub`.  -/
Finset.affineCombination_linear : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P),
  (Finset.affineCombination k s p).linear = s.weightedVSub p
-- Std.Http.Data.Headers.Value
/-- Proposition that asserts all characters in a string are valid for HTTP header values,
and that the first and last characters (if present) are `field-vchar` (not SP/HTAB).

  field-value    = *field-content
  field-content  = field-vchar
                   [ 1*( SP / HTAB / field-vchar ) field-vchar ]

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5.5
 -/
Std.Http.Header.IsValidHeaderValue : String → Prop
-- Mathlib.Analysis.Analytic.Within
AnalyticWithinAt.eventually_analyticWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {s : Set E} {x : E}, AnalyticWithinAt 𝕜 f s x → ∀ᶠ (y : E) in nhdsWithin x s, AnalyticWithinAt 𝕜 f s y
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofTacticInfo : Lean.Elab.TacticInfo → Lean.Elab.Info
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
_private.Mathlib.Combinatorics.Extremal.RuzsaSzemeredi.0.card_edgeFinset : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : CommRing α] {s : Finset α} [Fact (IsUnit 2)],
  ThreeAPFree ↑s →
    ∀ [inst_3 : DecidableEq α],
      (SimpleGraph.TripartiteFromTriangles.graph (triangleIndices✝ s)).edgeFinset.card = 3 * Fintype.card α * s.card
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.toMulEquiv_eq_coe : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S'),
  equiv.toMulEquiv = ↑equiv
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.M : Type → Type
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.unfold.sizeOf_spec : ∀ (declName unfold : Lean.Name),
  sizeOf (Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.unfold declName unfold) = 1 + sizeOf declName + sizeOf unfold
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIoc_eq_lift_Icc : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  {p a : 𝕜} [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)),
  AddCircle.liftIoc p a f = Quot.lift ((Set.Icc a (a + p)).domRestrict f) ⋯ ∘ ⇑(AddCircle.equivIccQuot p a)
-- Mathlib.Algebra.Exact.Basic
LinearMap.exact_zero_iff_injective : ∀ {R : Type u_8} [inst : Ring R] {M : Type u_12} {N : Type u_13} (P : Type u_14) [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommMonoid P] [inst_4 : Module R N] [inst_5 : Module R M] [inst_6 : Module R P]
  (f : M →ₗ[R] N), Function.Exact ⇑0 ⇑f ↔ Function.Injective ⇑f
-- Mathlib.SetTheory.Ordinal.Notation
ONote.scale_opowAux : ∀ (e a0 a : ONote) [e.NF] [a0.NF] [a.NF] (k m : ℕ),
  (e.opowAux a0 a k m).repr = Ordinal.omega0 ^ e.repr * (ONote.opowAux 0 a0 a k m).repr
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.OplaxMonoidal.whiskeringRight : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.MonoidalCategory D] →
              [inst_4 : CategoryTheory.MonoidalCategory E] →
                (L : CategoryTheory.Functor D E) →
                  [L.OplaxMonoidal] → ((CategoryTheory.Functor.whiskeringRight C D E).obj L).OplaxMonoidal
-- Lean.Meta.ReduceEval
_private.Lean.Meta.ReduceEval.0.Lean.Meta.evalName : Lean.Expr → Lean.MetaM Lean.Name
-- Lean.Setup
Lean.instReprImportArtifacts : Repr Lean.ImportArtifacts
-- Mathlib.Algebra.CharP.Defs
ringChar.eq : ∀ (R : Type u_1) [inst : NonAssocSemiring R] (p : ℕ) [C : CharP R p], ringChar R = p
-- Mathlib.LinearAlgebra.TensorProduct.Map
Equiv.tensorProductComm_def : ∀ (R : Type u_1) {A : Type u_2} {A' : Type u_3} {B : Type u_4} {B' : Type u_5} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A'] [inst_2 : AddCommMonoid B'] [inst_3 : Module R A'] [inst_4 : Module R B'] (eA : A ≃ A')
  (eB : B ≃ B'),
  TensorProduct.comm R A B =
    TensorProduct.congr (Equiv.linearEquiv R eA) (Equiv.linearEquiv R eB) ≪≫ₗ
      (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (Equiv.linearEquiv R eB).symm (Equiv.linearEquiv R eA).symm)
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_of_lt : ∀ {α : Type u} {s : Set α} [inst : Preorder α] {x y : α}, x ∈ s → y ∈ s → x < y → s.Nontrivial
-- Mathlib.Order.Bounds.Basic
upperBounds_union : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.forget₂Mon_obj_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.tryCatch.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) →
        ((ok : EStateM.Result ε σ α) → (∀ (e : ε) (s : σ), ok = EStateM.Result.error e s → False) → motive ok) →
          motive x
-- Init.Data.SInt.Lemmas
Int8.neg_add : ∀ {a b : Int8}, -(a + b) = -a - b
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Lift a family of morphisms to a limiting wide pullback cone.  -/
CategoryTheory.Limits.WidePullbackCone.IsLimit.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : C} →
        {Y : ι → C} →
          {f : (i : ι) → Y i ⟶ X} →
            {s : CategoryTheory.Limits.WidePullbackCone f} →
              CategoryTheory.Limits.IsLimit s →
                {W : C} →
                  (b : W ⟶ X) →
                    (a : (i : ι) → W ⟶ Y i) →
                      (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b) → (W ⟶ s.pt)
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.frontier_closedBall_subset_sphere : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, frontier (Metric.closedBall x ε) ⊆ Metric.sphere x ε
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHomClass.toSupBotHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Lattice α] [inst_2 : Lattice β]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [BoundedLatticeHomClass F α β], SupBotHomClass F α β
-- Lean.Syntax
Lean.Syntax.Range.start : Lean.Syntax.Range → String.Pos.Raw
-- Mathlib.Control.Monad.Cont
/-- Run a `ContT` with a provided callback.  -/
ContT.run : {r : Type u} → {m : Type u → Type v} → {α : Type w} → ContT r m α → (α → m r) → m r
-- Mathlib.Order.Filter.Basic
Filter.bot_sets_eq : ∀ {α : Type u}, ⊥.sets = Set.univ
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.min_orderTop_le_orderTop_add : ∀ {R : Type u_3} [inst : AddMonoid R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R},
  min x.orderTop y.orderTop ≤ (x + y).orderTop
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.IsPell.eq_1 : ∀ {d : ℤ} (x_1 y : ℤ), Pell.IsPell { re := x_1, im := y } = (x_1 * x_1 - d * y * y = 1)
-- Init.Data.UInt.Bitwise
USize.not_not : ∀ {a : USize}, ~~~~~~a = a
-- Init.Data.List.Basic
List.lengthTRAux.eq_1 : ∀ {α : Type u_1} (x : ℕ), [].lengthTRAux x = x
-- Mathlib.Order.SuccPred.Limit
PredOrder.prelimitRecOn_pred_of_not_isMin : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α]
  [inst_2 : WellFoundedGT α] (pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isPredPrelimit : (a : α) → Order.IsPredPrelimit a → ((b : α) → a < b → motive b) → motive a) (hb : ¬IsMin b),
  PredOrder.prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb (PredOrder.prelimitRecOn b pred isPredPrelimit)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.union_sdiff_cancel'`. -/
Set.union_diff_cancel' : ∀ {α : Type u_1} {s t u : Set α}, s ⊆ t → t ⊆ u → t ∪ u \ s = u
-- Mathlib.Topology.Order
induced_iInf : ∀ {α : Type u_1} {β : Type u_2} {g : β → α} {ι : Sort w} {t : ι → TopologicalSpace α},
  TopologicalSpace.induced g (⨅ i, t i) = ⨅ i, TopologicalSpace.induced g (t i)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_disjSum : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
  (t : Finset γ) (f : β ⊕ γ → α), (s.disjSum t).sup f = (s.sup fun x => f (Sum.inl x)) ⊔ t.sup fun x => f (Sum.inr x)
-- Lean.Elab.Tactic.Simp
/-- Position for the `[..]` child syntax in the `simp` tactic.  -/
Lean.Elab.Tactic.simpParamsPos : ℕ
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.mergeSort.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : α → α → Bool),
  x.mergeSort x_1 =
    match x, x_1 with
    | [], x => []
    | [a], x => [a]
    | a :: b :: xs, le =>
      have lr := List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩;
      have this := ⋯;
      have this := ⋯;
      ((↑lr.1).mergeSort le).merge ((↑lr.2).mergeSort le) le
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.InjectiveResolution X} {X' : C} {R' : CategoryTheory.InjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f) (n : ℤ) (m : ℕ) (h : ↑m = n) {Z : C} (h_1 : R'.cochainComplex.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (φ.hom'.f n) h_1 =
    CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n m h).hom
      (CategoryTheory.CategoryStruct.comp (φ.hom.f m)
        (CategoryTheory.CategoryStruct.comp (R'.cochainComplexXIso n m h).inv h_1))
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExceptSeries.eq_1 : ∀ (L : PeriodPair) (l₀ x : ℂ),
  L.weierstrassPExceptSeries l₀ x =
    FormalMultilinearSeries.ofScalars ℂ fun i =>
      if i = 0 then L.weierstrassPExcept l₀ x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.norm_eq_of_isometry : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  {f : NormedAddGroupHom V W}, Isometry ⇑f → ∀ (v : V), ‖f v‖ = ‖v‖
-- Mathlib.Algebra.Group.Action.Basic
MulAction.injective : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] (g : α), Function.Injective fun x => g • x
-- Mathlib.Order.Hom.Lattice
LatticeHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (g : LatticeHom β γ) (f : LatticeHom α β), LatticeHom.dual (g.comp f) = (LatticeHom.dual g).comp (LatticeHom.dual f)
-- Mathlib.Data.Finset.Union
Finset.biUnion_nonempty : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β],
  (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : Set 𝕜) (x : 𝕜),
  iteratedDerivWithin n f s x = (iteratedFDerivWithin 𝕜 n f s x) fun x => 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.instHasPushoutCompOfIsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) {X' : C} (i : X ⟶ X')
  [CategoryTheory.IsIso i] [CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp f i) g
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk_inv : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (a : G), ↑a⁻¹ = (↑a)⁻¹
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsLocalizingSequence.min : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : LinearOrder ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  {τ σ : ℕ → Ω → WithTop ι},
  ProbabilityTheory.IsLocalizingSequence 𝓕 τ P →
    ProbabilityTheory.IsLocalizingSequence 𝓕 σ P → ProbabilityTheory.IsLocalizingSequence 𝓕 (τ ⊓ σ) P
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- If `F` creates colimits of any size, it creates finite colimits.  -/
CategoryTheory.Limits.CreatesColimitsOfSize.createsFiniteColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
            CategoryTheory.Limits.CreatesFiniteColimits F
-- Mathlib.Order.Bounds.Image
StrictMono.mem_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {a : α} {s : Set α},
  StrictMono f → (f a ∈ upperBounds (f '' s) ↔ a ∈ upperBounds s)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_flip : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset β} {t : Multiset α},
  Multiset.Rel (flip r) s t ↔ Multiset.Rel r t s
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `r : R` is less than 1 if and only if `r ∈ v`.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  v.intValuation r < 1 ↔ r ∈ v.asIdeal
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.comp_apply : ∀ {R : Type u} [inst : Semiring R] {M N O : SemimoduleCat R} (f : M ⟶ N) (g : N ⟶ O) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Init.Data.Array.Bootstrap
_private.Init.Data.Array.Bootstrap.0.Array.foldlM.loop.match_1.splitter : (motive : ℕ → Sort u_1) → (i : ℕ) → (Unit → motive 0) → ((i' : ℕ) → motive i'.succ) → motive i
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getLED_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getLED k fallback = t₂.getLED k fallback
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δ_toCycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_toCycles._auto_1) {Z : C}
  (h : X.cycles f₁ f₂ n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁)
      (CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) h) =
    CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) h
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.addRight_symm : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : SeparatelyContinuousAdd G] (a : G),
  (Homeomorph.addRight a).symm = Homeomorph.addRight (-a)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Conversion to normal form on `U` changes the value only along a discrete subset
of `U`.
 -/
toMeromorphicNFOn_eqOn_codiscrete : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → f =ᶠ[Filter.codiscreteWithin U] toMeromorphicNFOn f U
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
constFormalMultilinearSeries_apply_zero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {c : F},
  constFormalMultilinearSeries 𝕜 E c 0 = ContinuousMultilinearMap.uncurry0 𝕜 E c
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.notMatcher.sizeOf_spec : sizeOf Lean.Meta.ReduceMatcherResult.notMatcher = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.inl_isoPushout_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C}
  (h_1 : CategoryTheory.Limits.pushout f g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp inl (CategoryTheory.CategoryStruct.comp h.isoPushout.hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) h_1