mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.codisjoint_range_inl_range_inr : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H],
  Codisjoint Monoid.Coprod.inl.range Monoid.Coprod.inr.range
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- The fork which describes the unit of the adjunction: the morphism from this fork to the
equalizer of this pair is the unit.
 -/
CategoryTheory.Comonad.ComonadicityInternal.unitFork : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              (B : C) → CategoryTheory.Limits.Fork (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_Iio : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p : ℚ≥0),
  NNRat.cast ⁻¹' Set.Iio ↑p = Set.Iio p
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.fromSubtype_π_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p] (j : J)
  {Z : C} (h : f j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) h) =
    CategoryTheory.CategoryStruct.comp
      (if h : p j then CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0) h
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Construct a bialgebra hom from an algebra hom respecting counit and comultiplication.  -/
BialgHom.ofAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Bialgebra R A] →
              [inst_4 : Bialgebra R B] →
                (f : A →ₐ[R] B) →
                  (Bialgebra.counitAlgHom R B).comp f = Bialgebra.counitAlgHom R A →
                    (Algebra.TensorProduct.map f f).comp (Bialgebra.comulAlgHom R A) =
                        (Bialgebra.comulAlgHom R B).comp f →
                      A →ₐc[R] B
-- Init.Data.Nat.Mod
Nat.mul_lt_mul_right : ∀ {a b c : ℕ}, 0 < a → (b * a < c * a ↔ b < c)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.vadd_oreSub_zero : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X] (r : R) (x : X), r +ᵥ x -ₒ 0 = (r +ᵥ x) -ₒ 0
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgEquiv.congr_simp : ∀ (σ : Type u_1) (R : Type u_3) {n : ℕ} [inst : Fintype σ] [inst_1 : CommRing R] (hn : Fintype.card σ = n),
  MvPolynomial.esymmAlgEquiv σ R hn = MvPolynomial.esymmAlgEquiv σ R hn
-- Mathlib.Topology.Category.TopCat.Basic
/-- Morphisms in `TopCat` are equivalent to continuous maps.  -/
TopCat.Hom.equivContinuousMap : (X Y : TopCat) → (X ⟶ Y) ≃ C(↑X, ↑Y)
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_le_one : ∀ {r : ℝ}, r.toNNReal ≤ 1 ↔ r ≤ 1
-- Mathlib.Algebra.BigOperators.Ring.Finset
Nat.cast_list_prod : ∀ {R : Type u_4} [inst : Semiring R] (s : List ℕ), ↑s.prod = (List.map Nat.cast s).prod
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.const_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure γ) (κ : ProbabilityTheory.Kernel α β),
  ⇑((ProbabilityTheory.Kernel.const β μ).comp κ) = fun a => (κ a) Set.univ • μ
-- Init.Data.Range.Polymorphic.UInt
UInt32.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable UInt32
-- Mathlib.Logic.Equiv.Set
Equiv.image_antitone : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {e : α ≃ β} (s : Set α),
  Antitone ⇑e → Antitone ⇑(e.image s)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.mapValueGroupWithZero.congr_simp : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : Ring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [inst_5 : ValuativeExtension A B],
  ValuativeExtension.mapValueGroupWithZero A B = ValuativeExtension.mapValueGroupWithZero A B
-- Mathlib.CategoryTheory.ConnectedComponents
/-- Given an index for a connected component, produce the actual component as a full subcategory.  -/
CategoryTheory.ConnectedComponents.Component : {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.ConnectedComponents J → Type u₁
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_sum_range_succ : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β}
  [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ℕ → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ℕ), Measurable (f i)) → ∀ (n : ℕ), ProbabilityTheory.IndepFun (∑ j ∈ Finset.range n, f j) (f n) μ
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionMain.succNthDefiningPoly_degree : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] [IsDomain k] (n : ℕ)
  (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k),
  a₁.coeff 0 ≠ 0 → a₂.coeff 0 ≠ 0 → (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).degree = ↑p
-- Mathlib.Data.LawfulXor.Basic
LawfulXor.mk : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α],
  (∀ (a b c : α), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)) →
    (∀ (a : α), a ^^^ a = 0) → (∀ (a : α), a ^^^ 0 = a) → (∀ (a b : α), a ^^^ b = b ^^^ a) → LawfulXor α
-- Init.Data.Vector.Attach
Vector.countP_attach : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, Vector.countP (fun a => p ↑a) xs.attach = Vector.countP p xs
-- Mathlib.CategoryTheory.Sites.Types
/-- The discrete sieve on a type, which only includes arrows whose image is a subsingleton.  -/
CategoryTheory.discreteSieve : (α : Type u) → CategoryTheory.Sieve α
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instPartialOrder : {M : Type u_1} → [inst : Add M] → PartialOrder (AddSubsemigroup M)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
/-- This is the main result of lemma 4.1 from [Geck](Geck2017).  -/
RootPairing.GeckConstruction.trace_toEnd_eq_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CharZero R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [inst_7 : P.IsCrystallographic] [P.IsReduced] {b : P.Base} [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (x : ↥(RootPairing.GeckConstruction.lieAlgebra b)),
  (LinearMap.trace R (↥b.support ⊕ ι → R))
      ((LieModule.toEnd R (↥(RootPairing.GeckConstruction.lieAlgebra b)) (↥b.support ⊕ ι → R)) x) =
    0
-- Mathlib.GroupTheory.Index
/-- Relative version of `AddSubgroup.index_eq_two_iff_exists_notMem_and`.  -/
AddSubgroup.relIndex_eq_two_iff_exists_notMem_and : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b + a ∈ H ∨ b ∈ H
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The four stacks used by the program. `main` is used to store the input value in `trNormal`
mode and the output value in `Λ'.ret` mode, while `stack` is used to keep all the data for the
continuations. `rev` is used to store reversed lists when transferring values between stacks, and
`aux` is only used once in `cons₁`. See the section documentation.  -/
Turing.PartrecToTM2.K' : Type
-- Init.Data.Nat.Dvd
Nat.dvd_one : ∀ {n : ℕ}, n ∣ 1 ↔ n = 1
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.orthRadius_parallel_orthRadius_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  (s.orthRadius p).Parallel (s.orthRadius q) ↔ ∃ r, r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
-- Batteries.Data.List.Lemmas
List.getElem_swap_left_of_lt : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} (hj : j < xs.length) (hi : i < (xs.swap i j).length), (xs.swap i j)[i] = xs[j]
-- Mathlib.Order.Preorder.Chain
/-- By definition, a flag is a chain  -/
Flag.Chain' : ∀ {α : Type u_4} [inst : LE α] (self : Flag α), IsChain (fun x1 x2 => x1 ≤ x2) self.carrier
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.epi_iff_surjective_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    ∀ ⦃A : C⦄ (y : A ⟶ Y),
      ∃ A' π,
        ∃ (_ : CategoryTheory.Epi π),
          ∃ x, CategoryTheory.CategoryStruct.comp π y = CategoryTheory.CategoryStruct.comp x f
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.discreteTopology_of_forall_lt : ∀ {K : Type u} [inst : DivisionRing K] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [MulArchimedean Γ₀]
  [inst_3 : Valued K Γ₀] {r : Γ₀}, r ≠ 0 → (∀ (x : K), Valued.v x ≠ 0 → r < Valued.v x) → DiscreteTopology K
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.smul : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : SMul 𝕜 β] {l : Filter α} {f f' : α → 𝕜} {g g' : α → β},
  f =ᶠ[l] f' → g =ᶠ[l] g' → (fun x => f x • g x) =ᶠ[l] fun x => f' x • g' x
-- Init.Data.List.Nat.TakeDrop
List.rotateLeft_replicate : ∀ {α : Type u_1} {m n : ℕ} {a : α}, (List.replicate m a).rotateLeft n = List.replicate m a
-- Mathlib.Tactic.GRewrite.Core
/-- The type  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.type : Mathlib.Tactic.GRewrite.GRewriteLemma✝ → Lean.Expr
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.opEquiv_symm_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R Aᵐᵒᵖ), (RelIso.symm Subalgebra.opEquiv) S = S.unop
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₂'_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₂'.X₂ = S.L₃.X₁
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.pow_eq_zero : ∀ {z : Complex.UnitDisc} {n : ℕ+}, z ^ n = 0 ↔ z = 0
-- Mathlib.Topology.Order.IsLUB
exists_seq_tendsto_sInf : ∀ {α : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [FirstCountableTopology α] {S : Set α},
  S.Nonempty → BddBelow S → ∃ u, Antitone u ∧ Filter.Tendsto u Filter.atTop (nhds (sInf S)) ∧ ∀ (n : ℕ), u n ∈ S
-- Mathlib.Data.PNat.Prime
/-- Two pnats are coprime if their gcd is 1.  -/
PNat.Coprime : ℕ+ → ℕ+ → Prop
-- Mathlib.Data.NNRat.Defs
NNRat.divNat_inj : ∀ {n₁ n₂ d₁ d₂ : ℕ}, d₁ ≠ 0 → d₂ ≠ 0 → (NNRat.divNat n₁ d₁ = NNRat.divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁)
-- Mathlib.Order.Antichain
IsMaxAntichain.isEmpty_iff : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsMaxAntichain r s → (IsEmpty α ↔ s = ∅)
-- Mathlib.GroupTheory.Commutator.Basic
commutatorSet_def : ∀ (G : Type u_1) [inst : Group G], commutatorSet G = {g | ∃ g₁ g₂, ⁅g₁, g₂⁆ = g}
-- Lean.Parser.Basic
Lean.Parser.symbolFnAux : String → String → Lean.Parser.ParserFn
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors.  -/
Orientation.cos_oangle_sub_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).cos = ‖x‖ / ‖x - y‖
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.not_prime_pow : ∀ {x n : ℕ}, 2 ≤ n → ¬Nat.Prime (x ^ n)
-- Mathlib.Algebra.DirectSum.Basic
/-- `⨁ i, f i` is notation for `DirectSum _ f` and equals the direct sum of `fun i ↦ f i`.
Taking the direct sum over multiple arguments is possible, e.g. `⨁ (i) (j), f i j`.  -/
DirectSum.«term⨁_,_» : Lean.ParserDescr
-- Mathlib.Order.Filter.CountableInter
countableInterFilter_bot : ∀ {α : Type u_2}, CountableInterFilter ⊥
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_roc : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.toList (Std.Roc.Sliceable.mkSlice xs lo<...=hi) =
    List.drop (lo + 1) (List.take (hi + 1) (Std.Slice.toList xs))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.radical_top : ∀ {X : AlgebraicGeometry.Scheme}, ⊤.radical = ⊤
-- Mathlib.Analysis.Normed.Field.Basic
NormedDivisionRing.toNorm : {α : Type u_5} → [self : NormedDivisionRing α] → Norm α
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_nonneg : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] {s : Multiset α} [AddLeftMono α],
  (∀ x ∈ s, 0 ≤ x) → 0 ≤ s.sum
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.eval₂_coe : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] (φ : R →+* S) (a : σ → S) (f : MvPolynomial σ R),
  MvPowerSeries.eval₂ φ a ↑f = MvPolynomial.eval₂ φ a f
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_anti₀` for the implication from right-to-left with one fewer assumption.  -/
inv_le_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → 0 < b → (a⁻¹ ≤ b⁻¹ ↔ b ≤ a)
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_left : ∀ {α : Type u_1} {s t : Multiset α}, Disjoint s t ↔ ∀ {a : α}, a ∈ s → a ∉ t
-- Mathlib.Order.Bounds.Basic
isLUB_congr_of_antisymmRel : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α},
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (IsLUB s a ↔ IsLUB s b)
-- Mathlib.Algebra.Module.Defs
/-- A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  -/
Module : (R : Type u) → (M : Type v) → [Semiring R] → [AddCommMonoid M] → Type (max u v)
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- The canonical projection from the `I`-adic completion of `S` to `S ⧸ I`. Defined
in terms of a surjective map `S →ₐ[R] A`.  -/
AdicCompletion.kerProj : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        {A : Type u_4} →
          [inst_2 : CommRing A] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R S] →
                {f : S →ₐ[R] A} → Function.Surjective ⇑f → AdicCompletion (RingHom.ker f) S →ₐ[R] A
-- Mathlib.Order.Hom.Lattice
/-- `SupHomClass F α β` states that `F` is a type of `⊔`-preserving morphisms.

You should extend this class when you extend `SupHom`.  -/
SupHomClass : (F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [Max α] → [Max β] → [FunLike F α β] → Prop
-- Mathlib.Algebra.Star.SelfAdjoint
CommMonoid.isStarNormal : ∀ {R : Type u_1} [inst : CommMonoid R] [inst_1 : StarMul R] {x : R}, IsStarNormal x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldl_eq_foldl_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {f : δ → α → β → δ}
  {init : δ}, Std.TreeMap.Raw.foldl f init t = List.foldl (fun a b => f a b.1 b.2) init t.toList
-- Mathlib.Order.RelIso.Basic
RelHom.coe_toMap : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α → β), ⇑(RelHom.toMap r f) = f
-- Mathlib.Topology.UniformSpace.Defs
/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is transitive.  -/
Filter.Tendsto.uniformity_trans : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {l : Filter β} {f₁ f₂ f₃ : β → α},
  Filter.Tendsto (fun x => (f₁ x, f₂ x)) l (uniformity α) →
    Filter.Tendsto (fun x => (f₂ x, f₃ x)) l (uniformity α) → Filter.Tendsto (fun x => (f₁ x, f₃ x)) l (uniformity α)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_add : ∀ {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] {n : ℕ} (m : Fin n → V) [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup E] [LineDerivAdd V E E] (x y : E),
  LineDeriv.iteratedLineDerivOp m (x + y) = LineDeriv.iteratedLineDerivOp m x + LineDeriv.iteratedLineDerivOp m y
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoX₂_inv_hom_id_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.HasLeftHomology] (hg : S.g = 0) {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.cyclesIsoX₂ hg).inv (CategoryTheory.CategoryStruct.comp S.iCycles h) = h
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.isAdmissible_singleton_iff : ∀ {m a : ℕ}, SimplexCategoryGenRel.IsAdmissible m [a] ↔ a ≤ m
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.isEqv.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → (α → α → Bool) → Sort u_2) (x x_1 : List α) (x_2 : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] [] x)
  (h_2 : (a : α) → (as : List α) → (b : α) → (bs : List α) → (eqv : α → α → Bool) → motive (a :: as) (b :: bs) eqv)
  (h_3 : (x x_3 : List α) → (x_4 : α → α → Bool) → motive x x_3 x_4),
  (x = [] → x_1 = [] → False) →
    (∀ (a : α) (as : List α) (b : α) (bs : List α), x = a :: as → x_1 = b :: bs → False) →
      (match x, x_1, x_2 with
        | [], [], x => h_1 x
        | a :: as, b :: bs, eqv => h_2 a as b bs eqv
        | x, x_5, x_6 => h_3 x x_5 x_6) =
        h_3 x x_1 x_2
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mem_disjUnion : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I}
  (h : Disjoint π₁.iUnion π₂.iUnion), J ∈ π₁.disjUnion π₂ h ↔ J ∈ π₁ ∨ J ∈ π₂
-- Lean.Data.Lsp.Client
Lean.Lsp.RegistrationParams.mk.injEq : ∀ (registrations registrations_1 : Array Lean.Lsp.Registration),
  ({ registrations := registrations } = { registrations := registrations_1 }) = (registrations = registrations_1)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- Given a predicate on `β` and `Set α` where both `α` and `β` are measurable spaces, if the
predicate holds for almost every `x : β` and
- `∅ : Set α`
- a family of sets generating the σ-algebra of `α`

Moreover, if for almost every `x : β`, the predicate is closed under complements and countable
disjoint unions, then the predicate holds for almost every `x : β` and all measurable sets of `α`.

This is an AE version of `MeasurableSpace.induction_on_inter` where the condition is dependent
on a measurable space `β`.  -/
MeasurableSpace.ae_induction_on_inter : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure β} {C : β → Set α → Prop}
  {s : Set (Set α)} [m : MeasurableSpace α],
  m = MeasurableSpace.generateFrom s →
    IsPiSystem s →
      (∀ᵐ (x : β) ∂μ, C x ∅) →
        (∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t) →
          (∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ) →
            (∀ᵐ (x : β) ∂μ,
                ∀ (f : ℕ → Set α),
                  Pairwise (Function.onFun Disjoint f) →
                    (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)) →
              ∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t
-- Mathlib.Data.Fintype.Quotient
Quotient.listChoice_mk : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)} {l : List ι}
  (a : (i : ι) → i ∈ l → α i), (Quotient.listChoice fun x1 x2 => ⟦a x1 x2⟧) = ⟦a⟧
-- Init.Data.Dyadic.Basic
Dyadic.ble_iff_toRat : ∀ {x y : Dyadic}, x.ble y = true ↔ x.toRat ≤ y.toRat
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.pow_NonnegCoeffs : ∀ {p : Lean.Grind.CommRing.Poly} (k : ℕ), p.NonnegCoeffs → (p.pow k).NonnegCoeffs
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
/-- **Alias** of `CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_hom`. -/
CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  {X Y W : CategoryTheory.Sheaf J A} (f : W ⟶ X) (g : W ⟶ Y),
  (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_3.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.Topology.Instances.Matrix
instContinuousNegMatrix : ∀ {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : Neg R] [ContinuousNeg R],
  ContinuousNeg (Matrix m n R)
-- Mathlib.Order.Lattice
/-- The infimum is a lower bound on the second argument  -/
Lattice.inf_le_right : ∀ {α : Type u} [self : Lattice α] (a b : α), Lattice.inf a b ≤ b
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_wcovBy : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ}
  (b : Module.Basis (Fin n) K V) (i : Fin n), b.flag i.castSucc ⩿ b.flag i.succ
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.normalize.eq_1 : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω),
  μ.normalize = if zero : μ.mass = 0 then ⟨MeasureTheory.Measure.dirac inst.some, ⋯⟩ else ⟨μ.mass⁻¹ • ↑μ, ⋯⟩
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_iff : ∀ (c : Cardinal.{u_1}), c.IsRegular ↔ Cardinal.aleph0 ≤ c ∧ c ≤ c.ord.cof
-- Mathlib.GroupTheory.Schreier
Subgroup.closure_mul_image_mul_eq_top : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {R S : Set G} (hR : Subgroup.IsComplement (↑H) R),
  1 ∈ R → Subgroup.closure S = ⊤ → ↑(Subgroup.closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S))) * R = ⊤
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The polar `polar 𝕜 s` of a set `s : E` is a closed subset when the weak star topology
is used.  -/
WeakDual.isClosed_polar : ∀ (𝕜 : Type u_1) {M : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module 𝕜 M] (s : Set M), IsClosed (WeakDual.polar 𝕜 s)
-- Mathlib.Order.Category.PartOrd
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe : ∀ (X : Preord) (a : ↑((preordToPartOrd.comp PartOrd.dual).obj X)),
  (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X)) a =
    (OrderIso.dualAntisymmetrization ↑X) a
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_prevAuxGo : ∀ {s : String.Slice} (off : ℕ) (h₁ : off < s.utf8ByteSize),
  String.Pos.Raw.IsValidForSlice s (String.Slice.Pos.prevAux.go off h₁)