mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_div_left' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] [MulRightStrictMono α] {a b : α},
  a < b → ∀ (c : α), c / b < c / a
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- Construct on a completely pseudometrizable space a pseudometric (compatible with the topology)
which is complete.  -/
TopologicalSpace.completelyPseudoMetrizableMetric : (X : Type u_3) →
  [inst : TopologicalSpace X] → [h : TopologicalSpace.IsCompletelyPseudoMetrizableSpace X] → PseudoMetricSpace X
-- Mathlib.Algebra.Order.Ring.Synonym
ofDual_ofNat : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], OrderDual.ofDual (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.pow_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x : A} {n : ℕ},
  0 < n → (IsIntegral R (x ^ n) ↔ IsIntegral R x)
-- Lean.Message
Lean.MessageData.group.inj : ∀ {a a_1 : Lean.MessageData}, a.group = a_1.group → a = a_1
-- Mathlib.RingTheory.Ideal.Maps
/-- For a prime ideal `p` of `R`, `p` extended to `S` and
restricted back to `R` is `p` if and only if `p` is the restriction of a prime in `S`.  -/
Ideal.comap_map_eq_self_iff_of_isPrime : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] {f : R →+* S} (p : Ideal R) [p.IsPrime],
  Ideal.comap f (Ideal.map f p) = p ↔ ∃ q, q.IsPrime ∧ Ideal.comap f q = p
-- Mathlib.AlgebraicGeometry.Scheme
/-- Cast a morphism of schemes into morphisms of local ringed spaces.  -/
AlgebraicGeometry.Scheme.Hom.toLRSHom : {X Y : AlgebraicGeometry.Scheme} → X.Hom Y → (X.toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_C : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R), (PowerSeries.coeff n) (PowerSeries.C a) = if n = 0 then a else 0
-- Mathlib.Dynamics.FixedPoints.Support
Function.HasCompactFixedSupport.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X ≃ X},
  Function.HasCompactFixedSupport ⇑f → Function.HasCompactFixedSupport ⇑f.symm
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodμ_functor_obj : ∀ (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] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] (X : (A × C) × D × E),
  (CategoryTheory.prod.prodμ C D E A).functor.obj X = ((X.1.1, X.2.1), X.1.2, X.2.2)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.leftUnitor_hom_app_apply : ∀ (K : SSet) {Δ : SimplexCategoryᵒᵖ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet) K).obj Δ),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (K.obj Δ)).hom) x = x.2
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn_isBase_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {E B : Set α},
  (N.comapOn E f).IsBase B ↔ N.IsBasis' (f '' B) (f '' E) ∧ Set.InjOn f B ∧ B ⊆ E
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
/-- Upgrade a Witt vector `A` whose first entry `A.coeff 0` is a unit to be, itself, a unit in `𝕎 k`.
 -/
WittVector.mkUnit : {p : ℕ} →
  [hp : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst : CommRing k] → [CharP k p] → {a : kˣ} → {A : WittVector p k} → A.coeff 0 = ↑a → (WittVector p k)ˣ
-- Mathlib.Data.Nat.Prime.Defs
/-- A copy of `not_prime_zero` stated in a way that works for `aesop`.

See https://github.com/leanprover-community/aesop/issues/197 for an explanation.  -/
Nat.prime_zero_false : Nat.Prime 0 → False
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.vanishing : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [IsTopologicalAddGroup G]
  {f : α → G}, Summable f → ∀ ⦃e : Set G⦄, e ∈ nhds 0 → ∃ s, ∀ (t : Finset α), Disjoint t s → ∑ k ∈ t, f k ∈ e
-- Mathlib.Data.Sign.Defs
SignType.coe_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Neg α], ↑0 = 0
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.coproducts_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{w, v, u} W],
  CategoryTheory.MorphismProperty.coproducts.{w, v, u} W ≤ W
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_eq_zero_iff : ∀ {n : ISize}, n.toNatClampNeg = 0 ↔ n ≤ 0
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_C : ∀ {R : Type u_1} [inst : Semiring R] {a : R}, a ≠ 0 → (LaurentPolynomial.C a).degree = 0
-- Lean.DocString.Extension
Lean.VersoDocString.subsections : Lean.VersoDocString → Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasProd.nat_mul_neg : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m : M} [ContinuousMul M] {f : ℤ → M},
  HasProd f m → HasProd (fun n => f ↑n * f (-↑n)) (m * f 0)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- the degree of a multivariate polynomial with respect to a monomial ordering, where polynomial
`0` has degree `⊥`, which is not equal to `0`. `MonomialOrder.withBotDegree` is to
`MonomialOrder.degree` as `Polynomial.degree` is to `Polynomial.natDegree`.  -/
MonomialOrder.withBotDegree : {σ : Type u_1} → MonomialOrder σ → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R → WithBot (σ →₀ ℕ)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
Equiv.Perm.cycleType_eq_two_two_subset_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], {g | g.cycleType = {2, 2}} ⊆ ↑(alternatingGroup α)
-- Mathlib.Algebra.Polynomial.Bivariate
AdjoinRoot.evalEval_apply : ∀ {R : Type u_1} [inst : CommRing R] {x y : R} {p : Polynomial (Polynomial R)} (h : Polynomial.evalEval x y p = 0)
  (a : Polynomial (Polynomial R) ⧸ Submodule.toAddSubgroup (Ideal.span {p})),
  (AdjoinRoot.evalEval h) a =
    (QuotientAddGroup.lift (Submodule.toAddSubgroup (Ideal.span {p}))
        ↑(Polynomial.eval₂RingHom (Polynomial.evalRingHom x) y) ⋯)
      a
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_closure_iff : ∀ {K : Type u} [inst : Field K] {s : Set K} {x : K},
  x ∈ Subfield.closure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instPartialOrder : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → PartialOrder (NonUnitalStarSubalgebra R A)
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.getKey!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] (m : Std.DHashMap.Raw α β)
  (a : α), m.getKey! a = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.getKey! ⟨m, h⟩ a else default
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.hasCoeToLieModuleHom : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → Coe (M ≃ₗ⁅R,L⁆ N) (M →ₗ⁅R,L⁆ N)
-- Init.Data.UInt.Lemmas
BitVec.ofFin_uInt16ToFin : ∀ (n : UInt16), { toFin := n.toFin } = n.toBitVec
-- Mathlib.SetTheory.Ordinal.Notation
ONote.add.eq_1 : ∀ (x : ONote), ONote.zero.add x = x
-- Mathlib.Algebra.Lie.Ideal
LieHom.isIdealMorphism_def : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'),
  f.IsIdealMorphism ↔ LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.simpAllOrSimpAtStar : Bool → Lean.MVarId → Option Lean.Term → Lean.Meta.Simp.UsedSimps → Aesop.Script.TacticBuilder
-- Mathlib.CategoryTheory.Linear.LinearFunctor
/-- the functor induces a linear map on morphisms  -/
CategoryTheory.Functor.Linear.map_smul : ∀ {R : Type u_1} {inst : Semiring R} {C : Type u_2} {D : Type u_3} {inst_1 : CategoryTheory.Category.{v_1, u_2} C}
  {inst_2 : CategoryTheory.Category.{v_2, u_3} D} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : CategoryTheory.Preadditive D} {inst_5 : CategoryTheory.Linear R C} {inst_6 : CategoryTheory.Linear R D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Functor.Linear R F] {X Y : C} (f : X ⟶ Y) (r : R),
  F.map (r • f) = r • F.map f
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.isBipartiteWith_sum_degrees_eq_twice_card_edges : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V], G.IsBipartiteWith ↑s ↑t → ∑ v ∈ s ∪ t, G.degree v = 2 * G.edgeFinset.card
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {he : t.isEmpty = false}, t.getKey! (t.maxKey he) = t.maxKey he
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.differentiable_fourierIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V]
  {μ : MeasureTheory.Measure V},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) μ →
      Differentiable ℝ (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.nextCoeff_X_sub_C : ∀ {S : Type v} [inst : Ring S] (c : S), (Polynomial.X - Polynomial.C c).nextCoeff = -c
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instReprSolverTerms.repr : Lean.Meta.Grind.SolverTerms → ℕ → Std.Format
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.decreaseKnownSize : Option Std.Http.Body.Length → Std.Http.Chunk → Option Std.Http.Body.Length
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.eq_1 : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g),
  MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg 0 = MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqAux hfg 0
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.evalDSimp : Lean.Elab.Tactic.Tactic
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.range_comap_fst : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S],
  Set.range (PrimeSpectrum.comap (RingHom.fst R S)) = PrimeSpectrum.zeroLocus ↑(RingHom.ker (RingHom.fst R S))
-- Mathlib.Logic.Equiv.Fin.Rotate
finCycle_apply : ∀ {n : ℕ} (k i : Fin n), (finCycle k) i = i + k
-- Mathlib.CategoryTheory.Bicategory.Product
/-- `fst` is the strict pseudofunctor given by projection to the first factor.  -/
CategoryTheory.Bicategory.Prod.fst : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] →
    (C : Type u₂) → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.StrictPseudofunctor (B × C) B
-- Lean.Parser.Tactic
/-- Introduces one or more hypotheses, optionally naming and/or pattern-matching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a `let` or function type.

* `intro` by itself introduces one anonymous hypothesis, which can be accessed
  by e.g. `assumption`. It is equivalent to `intro _`.
* `intro x y` introduces two hypotheses and names them. Individual hypotheses
  can be anonymized via `_`, given a type ascription, or matched against a pattern:
  ```lean
  -- ... ⊢ α × β → ...
  intro (a, b)
  -- ..., a : α, b : β ⊢ ...
  ```
* `intro rfl` is short for `intro h; subst h`, if `h` is an equality where the left-hand or right-hand side
  is a variable.
* Alternatively, `intro` can be combined with pattern matching much like `fun`:
  ```lean
  intro
  | n + 1, 0 => tac
  | ...
  ```
 -/
Lean.Parser.Tactic.introMatch : Lean.Parser.Parser
-- Std.Http.Protocol.H1.Reader
/-- Number of body bytes read for the current message.
 -/
Std.Http.Protocol.H1.Reader.bodyBytesRead : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → ℕ
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- If two vector fields are `C^n` with `n ≥ m + 1`, then their Lie bracket is `C^m`.  -/
ContMDiffAt.mlieBracket_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (minSmoothness 𝕜 2) M]
  [CompleteSpace E] {m n : ℕ∞} [IsManifold I (↑n + 1) M] {U V : (x : M) → TangentSpace I x} {x : M},
  ContMDiffAt I I.tangent (↑n) (fun x => ⟨x, U x⟩) x →
    ContMDiffAt I I.tangent (↑n) (fun x => ⟨x, V x⟩) x →
      minSmoothness 𝕜 (↑m + 1) ≤ ↑n → ContMDiffAt I I.tangent (↑m) (fun x₀ => ⟨x₀, VectorField.mlieBracket I U V x₀⟩) x
-- Mathlib.Condensed.Discrete.Characterization
/-- A light condensed object is *discrete* if it is constant as a sheaf, i.e. isomorphic to a constant
sheaf.
 -/
LightCondensed.IsDiscrete : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology LightProfinite) C] → LightCondensed C → Prop
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.Pos.find?_prop_eq_some_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos pos' : s.Pos},
  pos.find? p = some pos' ↔
    pos ≤ pos' ∧
      (∃ (h : pos' ≠ s.endPos), p (pos'.get h)) ∧
        ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), ¬p (pos''.get ⋯)
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.empty_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), ∅ ∪ s = s
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.numericTypes : Lean.Option Bool
-- Mathlib.Data.Bool.Basic
Bool.toNat_beq_one : ∀ (b : Bool), (b.toNat == 1) = b
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_right_pure_floor_add_one : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [OrderClosedTopology α] (x : α), Filter.Tendsto Int.ceil (nhdsWithin x (Set.Ioi x)) (pure (⌊x⌋ + 1))
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.leftUnitor_inv_apply : ∀ {X : Type u} {x : X},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) x = (PUnit.unit, x)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atTop_neBot : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α], Filter.atTop.NeBot
-- Mathlib.Algebra.Algebra.Unitization
NonUnitalAlgHom.mk.congr_simp : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (toDistribMulActionHom toDistribMulActionHom_1 : A →ₑ+[φ] B)
  (e_toDistribMulActionHom : toDistribMulActionHom = toDistribMulActionHom_1)
  (map_mul' :
    ∀ (x y : A), toDistribMulActionHom.toFun (x * y) = toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y),
  { toDistribMulActionHom := toDistribMulActionHom, map_mul' := map_mul' } =
    { toDistribMulActionHom := toDistribMulActionHom_1, map_mul' := ⋯ }
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.iff_of_ladder_mulEquiv : ∀ {X₁ : Type u_8} {X₂ : Type u_9} {X₃ : Type u_10} {Y₁ : Type u_11} {Y₂ : Type u_12} {Y₃ : Type u_13}
  [inst : CommMonoid X₁] [inst_1 : CommMonoid X₂] [inst_2 : CommMonoid X₃] [inst_3 : CommMonoid Y₁]
  [inst_4 : CommMonoid Y₂] [inst_5 : CommMonoid Y₃] (e₁ : X₁ ≃* Y₁) (e₂ : X₂ ≃* Y₂) (e₃ : X₃ ≃* Y₃) {f₁₂ : X₁ →* X₂}
  {f₂₃ : X₂ →* X₃} {g₁₂ : Y₁ →* Y₂} {g₂₃ : Y₂ →* Y₃},
  g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂ →
    g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃ → (Function.MulExact ⇑g₁₂ ⇑g₂₃ ↔ Function.MulExact ⇑f₁₂ ⇑f₂₃)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.trans_i₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P P' : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasPushout P.i₁ P'.i₀],
  (P.trans P').i₁ = CategoryTheory.CategoryStruct.comp P'.i₁ (CategoryTheory.Limits.pushout.inr P.i₁ P'.i₀)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : PartialOrder ι] {τ : Ω → WithTop ι}
  {f : MeasureTheory.Filtration ι m} [Countable ι],
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
-- Mathlib.Control.Functor.Multivariate
/-- `map` preserved identities, i.e., maps identity on `α` to identity on `F α`  -/
LawfulMvFunctor.id_map : ∀ {n : ℕ} {F : TypeVec.{u_2} n → Type u_1} {inst : MvFunctor F} [self : LawfulMvFunctor F] {α : TypeVec.{u_2} n}
  (x : F α), MvFunctor.map TypeVec.id x = x
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_comm : ∀ {α : Type u_1} [inst : Lattice α] (a b : α), Set.uIcc a b = Set.uIcc b a
-- Init.Data.AC
Lean.Data.AC.ContextInformation.isNeutral : {α : Sort u} → [self : Lean.Data.AC.ContextInformation α] → α → ℕ → Bool
-- Mathlib.NumberTheory.Cyclotomic.Discriminant
/-- If `p` is a prime and `IsCyclotomicExtension {p ^ k} K L`, then there are `u : ℤˣ` and
`n : ℕ` such that the discriminant of `hζ.powerBasis K` is `u * p ^ n`. Often this is enough and
less cumbersome to use than `IsCyclotomicExtension.discr_prime_pow`.  -/
IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow : ∀ {p k : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ (p ^ k)),
  Irreducible (Polynomial.cyclotomic (p ^ k) K) →
    ∃ u n, Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑↑u * ↑p ^ n
-- Mathlib.Order.LiminfLimsup
/-- Writing a limsup as an infimum of supremum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the supremum of sets which are
not bounded below.  -/
Filter.HasBasis.limsup_eq_ite : ∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι} [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)],
  v.HasBasis p s →
    ∀ (f : ι → α),
      Filter.limsup f v =
        if ∃ j, s ↑j = ∅ then sInf Set.univ
        else if ∀ (j : Subtype p), ¬BddAbove (Set.range fun i => f ↑i) then sInf ∅ else ⨅ j, ⨆ i, f ↑i
-- Mathlib.Algebra.Group.Action.Faithful
/-- Let `Q / P / N / M` be a tower. If `Q / N / M`, `Q / P / M` and `Q / P / N` are
scalar towers, then `P / N / M` is also a scalar tower.
 -/
IsScalarTower.to₁₂₃ : ∀ (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [inst : SMul M N] [inst_1 : SMul M P] [inst_2 : SMul M Q]
  [inst_3 : SMul N P] [inst_4 : SMul N Q] [inst_5 : SMul P Q] [FaithfulSMul P Q] [IsScalarTower M N Q]
  [IsScalarTower M P Q] [IsScalarTower N P Q], IsScalarTower M N P
-- Init.Data.Float.Model.Unpacked.Operations.Sub
/-- Computes the difference of two floating point numbers and rounds the result according to
the given specification.
 -/
Float.Model.UnpackedFloat.sub : Float.Model.Format → Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Float.Model.UnpackedFloat
-- Mathlib.Order.Fin.Tuple
Fin.insertNthOrderIso_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)] (p : Fin (n + 1))
  (f : α p × ((i : Fin n) → α (p.succAbove i))) (j : Fin (n + 1)),
  (Fin.insertNthOrderIso α p) f j = p.insertNth f.1 f.2 j
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.X_dvd_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} {j : σ →₀ ℕ} {r : R},
  MvPolynomial.X i ∣ (MvPolynomial.monomial j) r ↔ r = 0 ∨ j i ≠ 0
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.con_le_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N M : AddSubgroup G} [inst_1 : N.Normal] [inst_2 : M.Normal],
  QuotientAddGroup.con N ≤ QuotientAddGroup.con M ↔ N ≤ M
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_interval_sub_interval_comm' : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c d : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b →
    IntervalIntegrable f μ c d →
      IntervalIntegrable f μ a c →
        ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in c..d, f x ∂μ = ∫ (x : ℝ) in d..b, f x ∂μ - ∫ (x : ℝ) in c..a, f x ∂μ
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram : ∀ (D : AlgebraicGeometry.Scheme.GlueData), CategoryTheory.Limits.HasMulticoequalizer D.diagram
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.sub_const_eq_X_mul_shift : ∀ {R : Type u_1} [inst : Ring R] (φ : PowerSeries R),
  φ - PowerSeries.C (PowerSeries.constantCoeff φ) =
    PowerSeries.X * PowerSeries.mk fun p => (PowerSeries.coeff (p + 1)) φ
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.r_w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g) {Z_1 : C} (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left h.r) (CategoryTheory.CategoryStruct.comp f h_1) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right h.r) h_1)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.bounds_bddBelow : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  {f : ContinuousMultilinearMap 𝕜 E G}, BddBelow {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i, ‖m i‖}
-- Init.PropLemmas
Decidable.iff_congr_left : ∀ {P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R], ((P ↔ R) ↔ (Q ↔ R)) ↔ (P ↔ Q)
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorem.mk.sizeOf_spec : ∀ (theoremName funName : Lean.Name) (hypothesesPos : Array ℕ) (priority : ℕ),
  sizeOf { theoremName := theoremName, funName := funName, hypothesesPos := hypothesesPos, priority := priority } =
    1 + sizeOf theoremName + sizeOf funName + sizeOf hypothesesPos + sizeOf priority
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.instFreeCotangentSpaceToExtension : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  (P : Algebra.Generators R S ι), Module.Free S P.toExtension.CotangentSpace
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.instInv : {M : Type u_1} → [inst : CommMonoid M] → Inv (Algebra.GrothendieckGroup M)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIic_self : ∀ {α : Type u_1} [inst : LinearOrder α] (b : α), Set.projIic b b = ⟨b, ⋯⟩