mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W Y] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Z]
  (g : W ⟶ X) (g' : Y ⟶ Z),
  CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.coprod.inr) =
    CategoryTheory.Limits.coprod.map g g'
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of the forward direction of `Matroid.indep_singleton`. -/
Matroid.Indep.isNonloop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.Indep {e} → M.IsNonloop e
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Lean.Grind.instToIntFinCoOfNatIntCast.hcongr_1 : ∀ (n n' : ℕ), n = n' → Lean.Grind.instToIntFinCoOfNatIntCast ≍ Lean.Grind.instToIntFinCoOfNatIntCast
-- Lean.Expr
/-- Similar to `getAppFn`, but skips `mdata`
 -/
Lean.Expr.getAppFn' : Lean.Expr → Lean.Expr
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.ofFn.go.eq_def : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (acc : Array α) (i : ℕ) (a : i ≤ n),
  Array.ofFn.go✝ f acc i a =
    match i, a with
    | i.succ, h =>
      have w := ⋯;
      Array.ofFn.go✝ f (acc.push (f ⟨n - i - 1, w⟩)) i ⋯
    | 0, x => acc
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
SSet.instNonemptySOfNonempty : ∀ (X : SSet) [X.Nonempty], Nonempty X.S
-- Mathlib.GroupTheory.Congruence.Hom
/-- The diagram described by the universal property for quotients of monoids, when the congruence
relation is the kernel of the homomorphism, commutes.  -/
Con.kerLift_mk : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {f : M →* P} (x : M),
  (Con.kerLift f) ↑x = f x
-- Mathlib.RingTheory.Perfection
PerfectionMap.map_eq_map : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {S : Type u₂}
  [inst_3 : CommSemiring S] [inst_4 : CharP S p] (φ : R →+* S), PerfectionMap.map p ⋯ ⋯ φ = Perfection.map p φ
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.triangle_assoc_comp_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g) =
    CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.IsIso.of_groupoid : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso f
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X : HomotopicalAlgebra.CofibrantObject C} {Y : HomotopicalAlgebra.BifibrantObject.HoCat C}
  {f g : HomotopicalAlgebra.BifibrantObject.toHoCat.obj X.bifibrantResolutionObj ⟶ Y},
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.toHoCat.map X.iBifibrantResolutionObj)
        (HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject.map f) =
      CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.toHoCat.map X.iBifibrantResolutionObj)
        (HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject.map g) →
    f = g
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.col.eq_1 : ∀ (μ : YoungDiagram) (j : ℕ), μ.col j = {c ∈ μ.cells | c.2 = j}
-- Mathlib.Topology.Perfect
/-- The closure of a preperfect set is perfect.
For a converse, see `preperfect_iff_perfect_closure`.  -/
Preperfect.perfect_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α}, Preperfect C → Perfect (closure C)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.mk.injEq : ∀ (numParams numDiscrs : ℕ) (altInfos : Array Lean.Meta.Match.AltParamInfo) (uElimPos? : Option ℕ)
  (discrInfos : Array Lean.Meta.Match.DiscrInfo) (overlaps : Lean.Meta.Match.Overlaps) (numParams_1 numDiscrs_1 : ℕ)
  (altInfos_1 : Array Lean.Meta.Match.AltParamInfo) (uElimPos?_1 : Option ℕ)
  (discrInfos_1 : Array Lean.Meta.Match.DiscrInfo) (overlaps_1 : Lean.Meta.Match.Overlaps),
  ({ numParams := numParams, numDiscrs := numDiscrs, altInfos := altInfos, uElimPos? := uElimPos?,
        discrInfos := discrInfos, overlaps := overlaps } =
      { numParams := numParams_1, numDiscrs := numDiscrs_1, altInfos := altInfos_1, uElimPos? := uElimPos?_1,
        discrInfos := discrInfos_1, overlaps := overlaps_1 }) =
    (numParams = numParams_1 ∧
      numDiscrs = numDiscrs_1 ∧
        altInfos = altInfos_1 ∧ uElimPos? = uElimPos?_1 ∧ discrInfos = discrInfos_1 ∧ overlaps = overlaps_1)
-- Mathlib.Data.Finsupp.Order
Finsupp.instCanonicallyOrderedAddOfAddLeftMono : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α]
  [inst_3 : Sub α] [OrderedSub α] [AddLeftMono α], CanonicallyOrderedAdd (ι →₀ α)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_self_eq_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), toIcoMod hp a b - b = -↑(toIcoDiv hp a b) * p
-- Mathlib.Data.Rel
SetRel.isRefl_univ : ∀ {α : Type u_1}, SetRel.IsRefl Set.univ
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation scales the diameter by `ratio f` in pseudometric spaces.  -/
Dilation.diam_image : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (s : Set α),
  Metric.diam (⇑f '' s) = ↑(Dilation.ratio f) * Metric.diam s
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.integrable_cexp_mul_of_re_mem_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  AEMeasurable X μ →
    z.re ∈ ProbabilityTheory.integrableExpSet X μ → MeasureTheory.Integrable (fun ω => Complex.exp (z * ↑(X ω))) μ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] (s : Finset α), s + ∅ = ∅
-- Mathlib.Combinatorics.SimpleGraph.Trails
/-- The edge set of an Eulerian graph is finite.  -/
SimpleGraph.Walk.IsEulerian.fintypeEdgeSet : {V : Type u_1} →
  {G : SimpleGraph V} → [inst : DecidableEq V] → {u v : V} → {p : G.Walk u v} → p.IsEulerian → Fintype ↑G.edgeSet
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
/-- Assume that the processes $((X^t_s)_{s \in S_t})_{t \in T}$ are jointly Gaussian. Then they are
independent if for all $t_1, t_2 \in T$ with $t_1 \ne t_2$ and
$s_1 \in S_{t_1}$, $s_2 \in S_{t_2}$, $X^{t_1}_{s_1}$ and $X^{t_2}_{s_2}$ are uncorrelated.  -/
ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_strongDual : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [CompleteSpace E] {S : T → Type u_4} {X : (t : T) → S t → Ω → E} [inst_5 : NormedSpace ℝ E],
  ProbabilityTheory.IsGaussianProcess (fun p ω => X p.fst p.snd ω) P →
    (∀ (t : T) (s : S t), AEMeasurable (X t s) P) →
      (∀ (t₁ t₂ : T),
          t₁ ≠ t₂ →
            ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E),
              ProbabilityTheory.covariance (⇑L₁ ∘ X t₁ s₁) (⇑L₂ ∘ X t₂ s₂) P = 0) →
        ProbabilityTheory.iIndepFun (fun t ω s => X t s ω) P
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.instIsScalarTower : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : FaithfulSMul R K] {R₀ : Type u_6} [inst_4 : SMul R₀ R] [inst_5 : IsScalarTower R₀ R R] [inst_6 : SMul R₀ K]
  [IsScalarTower R₀ R K], IsScalarTower R₀ (FractionRing R) K
-- Init.Data.BitVec.Bitblast
BitVec.slt_eq_not_carry : ∀ {w : ℕ} {x y : BitVec w}, x.slt y = (x.msb == y.msb ^^ BitVec.carry w x (~~~y) true)
-- Mathlib.Tactic.Positivity.Core
/-- Attempts to prove that `e ≥ 0` using `zero_le` in a `CanonicallyOrderedAdd` monoid.  -/
Mathlib.Meta.Positivity.positivityCanon : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      (pα : Q(PartialOrder «$α»)) → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e (some pα))
-- Mathlib.Order.PiLex
Pi.toColex_apply : ∀ {ι : Type u_1} {β : ι → Type u_2} (x : (i : ι) → β i) (i : ι), toColex x i = x i
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.closure_empty : ∀ {M : Type u_1} [inst : Add M], AddSubsemigroup.closure ∅ = ⊥
-- Mathlib.Order.Filter.Pointwise
Filter.le_div_iff : ∀ {α : Type u_2} [inst : Div α] {f g h : Filter α}, h ≤ f / g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set α⦄, t ∈ g → s / t ∈ h
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.hom = 0
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_pow : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], Polynomial.C (a ^ n) = Polynomial.C a ^ n
-- Mathlib.Topology.ContinuousOn
Topology.IsInducing.continuousOn_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {g : β → γ},
  Topology.IsInducing g → ∀ {s : Set α}, ContinuousOn f s ↔ ContinuousOn (g ∘ f) s
-- Mathlib.LinearAlgebra.Lagrange
/-- `nodal s v` is the unique monic polynomial whose roots are the nodes defined by `v` and `s`.

That is, the roots of `nodal s v` are exactly the image of `v` on `s`,
with appropriate multiplicity.

We can use `nodal` to define the barycentric forms of the evaluated interpolant.
 -/
Lagrange.nodal : {R : Type u_1} → [inst : CommRing R] → {ι : Type u_2} → Finset ι → (ι → R) → Polynomial R
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_of_subsingleton`. -/
Ideal.inertiaDeg_of_subsingleton : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [hp : p.IsMaximal] [hQ : Subsingleton (S ⧸ P)], p.inertiaDeg' P = 0
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatch.le_of_isRevMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos → String.Slice.Pattern.Model.IsRevMatch pat pos' → pos ≤ pos'
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.get? t.max! = some t.max!
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β),
  ((HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V).hom.app X).f i =
    CategoryTheory.CategoryStruct.id (X.obj i)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_pow : ∀ {M : Type u_1} [inst : CommMonoid M] (a : M) (n : ℕ), Associates.mk (a ^ n) = Associates.mk a ^ n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
min_lt_max_of_add_lt_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] {a b c d : α} [AddLeftMono α] [AddRightMono α],
  a + b < c + d → min a b < max c d
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- Category structure on the strong transformations between pseudofunctors.

Note that this a scoped instance in the `Pseudofunctor.StrongTrans` namespace.  -/
CategoryTheory.Pseudofunctor.StrongTrans.homCategory : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          CategoryTheory.Category.{max u₁ w₂, max (max (max u₁ v₁) v₂) w₂} (F ⟶ G)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyι_comp_fromOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {Z : C} (h : S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.rightHomologyι (CategoryTheory.CategoryStruct.comp S.fromOpcycles h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Http.Server
/-- Waits for the server to shut down. Blocks until another task or async operation calls the `shutdown` function.
 -/
Std.Http.Server.waitShutdown : Std.Http.Server → Std.Async.Async Unit
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (g : A₂ ⟶ B) [inst_2 : CategoryTheory.Mono g] (X : CategoryTheory.Subobject B)
  (h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g) (h₂ : CategoryTheory.Subobject.mk g ≤ X),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h₁)
      (CategoryTheory.Subobject.ofMkLE g X h₂) =
    CategoryTheory.Subobject.ofMkLE f X ⋯
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_eq_zero_iff : ∀ {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}}, o.blsub f = 0 ↔ o = 0
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.not_isUnit_X : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], ¬IsUnit Polynomial.X
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `PComp.assump c n` creates a `PComp` whose comparison is `c` and whose source is
`CompSource.assump n`, that is, `c` is derived from the `n`th hypothesis.
The history is the singleton set `{n}`.
No variables have been eliminated (effectively or implicitly).
 -/
Mathlib.Tactic.Linarith.PComp.assump : Mathlib.Tactic.Linarith.Comp → ℕ → Mathlib.Tactic.Linarith.PComp
-- Init.Data.Option.Lemmas
Option.max_pfilter_left : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] {o : Option α} {p : (a : α) → o = some a → Bool},
  o.pfilter p ⊔ o = o
-- Std.Time.Format.Modifier
Std.Time.instInhabitedOffsetO : Inhabited Std.Time.OffsetO
-- Mathlib.Order.Heyting.Regular
/-- The Galois insertion between `Regular.toRegular` and `coe`.  -/
Heyting.Regular.gi : {α : Type u_1} → [inst : HeytingAlgebra α] → GaloisInsertion (⇑Heyting.Regular.toRegular) Heyting.Regular.val
-- Mathlib.Data.Set.Finite.Basic
Set.card_fintypeInsertOfNotMem : ∀ {α : Type u} {a : α} (s : Set α) [inst : Fintype ↑s] (h : a ∉ s), Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂ : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [inst_4 : F₁.CommShift ℤ]
  [inst_5 : F₂.CommShift ℤ] [inst_6 : CategoryTheory.NatTrans.CommShift e.hom ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIso e).inv.app X).hom₂ = e.inv.app X.obj₂
-- Mathlib.Tactic.Replace
/-- `replace h := e` is like `have h := e`, but it removes a previous hypothesis
of the same name as this one if possible. For example, if the state is:

```lean
f : α → β
h : α
⊢ goal
```

Then after `replace h := f h` the state will be:

```lean
f : α → β
h : β
⊢ goal
```

whereas `have h := f h` would result in:

```lean
f : α → β
h† : α
h : β
⊢ goal
```

The tactic `specialize h a₁ ... aₙ` is a way to write `replace h := h a₁ ... aₙ`,
automatically inferring which hypothesis should be replaced.

The `replace` tactic can be used to simulate Rocq's `apply at` tactic.


Extensions:

 * `replace h : t`, without a subsequent proof, creates a new main goal `case h : ... ⊢ t`.
   This form is considered deprecated in Mathlib: use `replace h : t := _` instead. -/
Mathlib.Tactic.replace' : Lean.ParserDescr
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsPrimitiveRoot.norm_of_cyclotomic_irreducible : ∀ {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [inst : CommRing L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L],
  IsPrimitiveRoot ζ n →
    ∀ [IsDomain L] [IsCyclotomicExtension {n} K L],
      Irreducible (Polynomial.cyclotomic n K) → (Algebra.norm K) ζ = if n = 2 then -1 else 1
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- The induced map on the first homology of the (naive) cotangent complex of `S` over `R`.  -/
Algebra.H1Cotangent.map : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (S' : Type u_2) →
            [inst_3 : CommRing S'] →
              [inst_4 : Algebra R S'] →
                (T : Type w) →
                  [inst_5 : CommRing T] →
                    [inst_6 : Algebra R T] →
                      [inst_7 : Algebra S T] →
                        [IsScalarTower R S T] →
                          [inst_9 : Algebra S' T] →
                            [IsScalarTower R S' T] → Algebra.H1Cotangent R S' →ₗ[S'] Algebra.H1Cotangent S T
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).ContainsIdentities] (X : C),
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.star_right_conjugate_le_norm_smul : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  autoParam (IsSelfAdjoint b) CStarAlgebra.star_right_conjugate_le_norm_smul._auto_1 →
    a * b * star a ≤ ‖b‖ • (a * star a)
-- Mathlib.Algebra.Ring.ULift
RingHom.comp_ulift_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  ULift.ringEquiv.toRingHom.comp ((RingHom.ulift.{u₁, u₂, u_1, u_2} f).comp ULift.ringEquiv.symm.toRingHom) = f
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.casesOn : ∀
  {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → ms.Approximates → Prop}
  {basis : Tactic.ComputeAsymptotics.Basis} {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion basis}
  (t : ms.Approximates),
  (∀ (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion []), motive ms ⋯) →
    (∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ} (hf : f =ᶠ[Filter.atTop] 0),
        motive
          (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
            Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil f)
          ⋯) →
      (∀ {basis_hd f : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
          {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
          {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
          (h_coef : coef.Approximates) (h_maj : Tactic.ComputeAsymptotics.Majorized f basis_hd exp)
          (h_tl :
            (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates),
          motive
            (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
              (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f)
            ⋯) →
        motive ms t
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] {i j k : J}
  (x :
    ↥(CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.IsLocallyDirected.V F i j).ι
        (AlgebraicGeometry.Scheme.IsLocallyDirected.V F i k).ι)),
  ∃ l fi fj fk α z,
    AlgebraicGeometry.IsOpenImmersion α ∧
      CategoryTheory.CategoryStruct.comp α
            (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.IsLocallyDirected.V F i j).ι
              (AlgebraicGeometry.Scheme.IsLocallyDirected.V F i k).ι) =
          CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map fi)).hom
            ((F.obj i).homOfLE ⋯) ∧
        CategoryTheory.CategoryStruct.comp α
              (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.IsLocallyDirected.V F i j).ι
                (AlgebraicGeometry.Scheme.IsLocallyDirected.V F i k).ι) =
            CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map fi)).hom
              ((F.obj i).homOfLE ⋯) ∧
          α z = x
-- Aesop.Script.Step
Aesop.Script.LazyStep.preState : Aesop.Script.LazyStep → Lean.Meta.SavedState
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.prop_of_retract : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts]
  {X Y : C} (h : CategoryTheory.Retract X Y), P Y → P X
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ioo (f (Order.succ n)) (f n)` are pairwise disjoint.  -/
Antitone.pairwise_disjoint_on_Ioo_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Function.onFun Disjoint fun n => Set.Ioo (f (Order.succ n)) (f n))
-- Mathlib.Algebra.Module.LinearMap.Basic
Sum.elimZeroRight_apply : ∀ {ι : Type u_6} {κ : Type u_7} {R : Type u_8} [inst : Semiring R] (f : ι → R) (a : ι ⊕ κ),
  Sum.elimZeroRight f a = Sum.elim f 0 a
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.tendsto_verticalIntegral : ∀ {b : ℂ}, 0 < b.re → ∀ (c : ℝ), Filter.Tendsto (GaussianFourier.verticalIntegral b c) Filter.atTop (nhds 0)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfZeroLE.eq_1 : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (i : Set α) (hi₁ : MeasurableSet i)
  (hi₂ : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i),
  s.toMeasureOfZeroLE i hi₁ hi₂ = MeasureTheory.Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi₂) ⋯ ⋯
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.all.inj : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {f f_1 : L.BoundedFormula α (n + 1)}, f.all = f_1.all → f = f_1
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
CategoryTheory.Functor.ReflectsIsomorphisms.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D},
  (∀ {A B : C} (f : A ⟶ B) [CategoryTheory.IsIso (F.map f)], CategoryTheory.IsIso f) → F.ReflectsIsomorphisms