mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.congr_simp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ μ_1 : MeasureTheory.Measure α} (e_μ : μ = μ_1)
  [inst : PseudoEMetricSpace E] {f f_1 : ℕ → α → E} (e_f : f = f_1) {g g_1 : α → E} (e_g : g = g_1)
  (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g) (a a_1 : ℕ),
  a = a_1 →
    MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg a = MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq ⋯ a_1
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.zero_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  (DoubleCentralizer.toProd 0).1 = 0
-- Mathlib.Algebra.Divisibility.Basic
rightDvd_iff_op_dvd_op : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ᵣ b ↔ MulOpposite.op a ∣ MulOpposite.op b
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.resetMaskAt : Array Bool → ℕ → Array Bool
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Complex.rightAngleRotation : ∀ (z : ℂ), Complex.orientation.rightAngleRotation z = Complex.I * z
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressOptions.workDoneProgress : Lean.Lsp.WorkDoneProgressOptions → Bool
-- Mathlib.CategoryTheory.Category.Bipointed
/-- **Alias** of `Bipointed.of`.

---

Turns a bipointing into a bipointed type.  -/
Prod.Bipointed : {X : Type u_1} → X × X → Bipointed
-- Mathlib.Analysis.Complex.CoveringMap
/-- `exp : ℂ → ℂ \ {0}` is a covering map.  -/
Complex.isCoveringMap_exp : IsCoveringMap fun z => ⟨Complex.exp z, ⋯⟩
-- Init.Data.UInt.Lemmas
UInt64.le_antisymm : ∀ {a b : UInt64}, a ≤ b → b ≤ a → a = b
-- Mathlib.Algebra.Ring.Associator
associator.eq_1 : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (x y z : R), associator x y z = x * y * z - x * (y * z)
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.has_compl_iff : ∀ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {a : Set α}, d.Has aᶜ ↔ d.Has a
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isBounded_of_image2_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] (f : α → β → γ) {K₁ : NNReal},
  (∀ (b : β), AntilipschitzWith K₁ fun a => f a b) →
    ∀ {s : Set α} {t : Set β}, Bornology.IsBounded (Set.image2 f s t) → Bornology.IsBounded s ∨ Bornology.IsBounded t
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.map_add_eq_map_conv_map : ∀ {Ω : Type u_7} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {M : Type u_10} [inst : AddMonoid M]
  [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] [MeasureTheory.IsFiniteMeasure μ] {f g : Ω → M},
  Measurable f →
    Measurable g →
      ProbabilityTheory.IndepFun f g μ →
        MeasureTheory.Measure.map (f + g) μ = (MeasureTheory.Measure.map f μ).conv (MeasureTheory.Measure.map g μ)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.of_symm_smul : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid V]
  [inst_2 : SMulZeroClass R V] (r : R) (x : HahnModule Γ R V),
  (HahnModule.of R).symm (r • x) = r • (HahnModule.of R).symm x
-- Mathlib.Algebra.Order.Sub.Defs
add_tsub_add_eq_tsub_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] [AddLeftMono α]
  [AddLeftReflectLE α] (a c b : α), a + c - (b + c) = a - b
-- Mathlib.Combinatorics.Matroid.IndepAxioms
Matroid.ofExistsFiniteIsBase_isBase : ∀ {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_finite_base : ∃ B, IsBase B ∧ B.Finite)
  (isBase_exchange : Matroid.ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).IsBase = IsBase
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
/-- Given a short exact short complex `S` in an abelian category `C` and an object `Y : C`,
this is the long exact sequence
`Ext S.X₃ Y n₀ → Ext S.X₂ Y n₀ → Ext S.X₁ Y n₀ → Ext S.X₃ Y n₁ → Ext S.X₂ Y n₁ → Ext S.X₁ Y n₁`
when `1 + n₀ = n₁`.  -/
CategoryTheory.Abelian.Ext.contravariantSequence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.HasExt C] →
        {S : CategoryTheory.ShortComplex C} →
          S.ShortExact → C → (n₀ n₁ : ℕ) → 1 + n₀ = n₁ → CategoryTheory.ComposableArrows AddCommGrpCat 5
-- Init.Data.Order.PackageFactories
Std.Packages.PartialOrderOfLEArgs.mk : {α : Type u} →
  (toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α) →
    autoParam
        (let this := toPreorderOfLEArgs.le;
        ∀ (a b : α), a ≤ b → b ≤ a → a = b)
        Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam →
      Std.Packages.PartialOrderOfLEArgs α
-- Init.Data.Float.Model.Unpacked.Round
/-- Shifts the mantissa and exponent and initial accuracy to the target exponent, returning
the new extended mantissa and exponent.

Important: this function will only drop bits from the mantissa and increase the exponent,
not the other way around. The result will only conform to the given specification if
the exponent was not too large to begin with. If this may be the case, you should call
`round` instead.
 -/
Float.Model.UnpackedFloat.shiftToExponent : ℕ → ℤ → Float.Model.UnpackedFloat.Accuracy → ℤ → Float.Model.UnpackedFloat.ExtendedMantissa × ℤ
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `none` if the map is empty.
 -/
Std.ExtDTreeMap.minKey? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → Option α
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.mul_scalar : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {r s : R},
  FreeAlgebra.Rel R X (FreeAlgebra.Pre.ofScalar (r * s)) (FreeAlgebra.Pre.ofScalar r * FreeAlgebra.Pre.ofScalar s)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.germ_eq_zero_of_pow_mul_eq_zero : ∀ {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↥X} (x : ↥U) {f s : ↑(X.presheaf.obj (Opposite.op U))},
  ↑x ∈ X.basicOpen s → ∀ {n : ℕ}, s ^ n * f = 0 → (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.selfEquivSigmaOrbits.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.selfEquivSigmaOrbits G α =
    (AddAction.selfEquivSigmaOrbits' G α).trans (Equiv.sigmaCongrRight fun x => Equiv.setCongr ⋯)
-- Mathlib.Algebra.Group.Center
isAddCentral_iff : ∀ {M : Type u_1} [inst : Add M] (z : M),
  IsAddCentral z ↔
    (∀ (a : M), AddCommute z a) ∧ (∀ (b c : M), z + (b + c) = z + b + c) ∧ ∀ (a b : M), a + b + z = a + (b + z)
-- Mathlib.Topology.Irreducible
/-- A set is preirreducible iff every nonempty open subset of a
preirreducible subspace is dense in the subspace.  -/
isPreirreducible_iff_subset_closure_inter_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] (S : Set X),
  IsPreirreducible S ↔ ∀ (U : Set X), IsOpen U → (S ∩ U).Nonempty → S ⊆ closure (S ∩ U)
-- Aesop.Util.Basic
/-- Remove elements for which `p` returns `false` from the given `DiscrTree`.
The removed elements are monadically folded over using `f` and `init`, so `f`
is called once for each removed element and the final state of type `σ` is
returned.
 -/
Aesop.filterDiscrTreeM : {m : Type u_1 → Type u_2} →
  {σ : Type u_1} →
    {α : Type} →
      [Monad m] →
        [Inhabited σ] →
          (α → m (ULift.{u_1, 0} Bool)) → (σ → α → m σ) → σ → Lean.Meta.DiscrTree α → m (Lean.Meta.DiscrTree α × σ)
-- Mathlib.Data.Num.Lemmas
PosNum.natSize.eq_2 : ∀ (n : PosNum), n.bit0.natSize = n.natSize.succ
-- Init.Data.Rat.Lemmas
Rat.intCast_lt_intCast : ∀ {a b : ℤ}, ↑a < ↑b ↔ a < b
-- Mathlib.Analysis.Calculus.DerivativeTest
deriv_pos_right_of_sign_deriv : ∀ {f : ℝ → ℝ} {x₀ : ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin x₀ {x₀}ᶜ, SignType.sign (deriv f x) = SignType.sign (x - x₀)) →
    ∀ᶠ (b : ℝ) in nhdsWithin x₀ (Set.Ioi x₀), deriv f b > 0
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedEMatchDiagInfo : Inhabited Lean.Meta.Grind.EMatchDiagInfo
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.isRight_congr : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ},
  Sum.LiftRel r s x y → (x.isRight = true ↔ y.isRight = true)
-- Lean.Expr
/-- Given `f a₁ a₂ ... aₙ`, returns `#[a₁, ..., aₙ]`  -/
Lean.Expr.getAppArgs : Lean.Expr → Array Lean.Expr
-- Mathlib.Algebra.Lie.Derivation.Killing
LieDerivation.IsKilling.killingForm_restrict_range_ad : ∀ (R : Type u_1) (L : Type u_2) [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Module.Finite R L],
  (killingForm R (LieDerivation R L L)).restrict (LieDerivation.ad R L).range.toSubmodule =
    killingForm R ↥(LieDerivation.ad R L).range
-- Lean.Elab.DeclModifiers
Lean.Elab.ComputeKind.noncomputable : Lean.Elab.ComputeKind
-- Mathlib.Analysis.Normed.Order.UpperLower
dist_mono_right_pi : ∀ {ι : Type u_2} [inst : Fintype ι] {x : ι → ℝ}, MonotoneOn (dist x) (Set.Ici x)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (m k : ℕ),
  iteratedDeriv k (fun x => x ^ m) x = ↑(m.descFactorial k) * x ^ (m - k)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.push_rankD : ∀ {i : ℕ} (arr : Array Batteries.UFNode),
  Batteries.UnionFind.rankD (arr.push { parent := arr.size, rank := 0 }) i = Batteries.UnionFind.rankD arr i
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_real_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ},
  0 ≤ r → μ.real (Metric.closedBall x r) = r ^ Module.finrank ℝ E * μ.real (Metric.ball 0 1)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A function to 𝕜 is meromorphic in normal form at a point iff its inverse is.
 -/
meromorphicNFAt_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {f : 𝕜 → 𝕜}, MeromorphicNFAt f⁻¹ x ↔ MeromorphicNFAt f x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_abs_eq_two_mul_integral_posPart_sub_integral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → ∫ (x : α), |f x| ∂μ = 2 * ∫ (x : α), (f x)⁺ ∂μ - ∫ (x : α), f x ∂μ
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.AliasInfo.forward.injEq : ∀ (n n_1 : Lean.Name),
  (Batteries.Tactic.Alias.AliasInfo.forward n = Batteries.Tactic.Alias.AliasInfo.forward n_1) = (n = n_1)
-- Lean.Meta.Basic
/-- Throw an exception saying `fvarId` is not declared in the current local context.
 -/
Lean.FVarId.throwUnknown : {α : Type} → Lean.FVarId → Lean.CoreM α
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.toTriangle_is3Clique : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {x : α × β × γ} [inst : DecidableEq α]
  [inst_1 : DecidableEq β] [inst_2 : DecidableEq γ],
  x ∈ t → (SimpleGraph.TripartiteFromTriangles.graph t).IsNClique 3 (SimpleGraph.TripartiteFromTriangles.toTriangle x)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
/-- The object in the category of quadratic R-modules associated to a quadratic R-module.  -/
QuadraticModuleCat.of : {R : Type u} →
  [inst : CommRing R] →
    {X : Type v} → [inst_1 : AddCommGroup X] → [inst_2 : Module R X] → QuadraticForm R X → QuadraticModuleCat R
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_ground_eq_self : ∀ {α : Type u_1} (M : Matroid α), M.restrict M.E = M
-- Mathlib.Data.Nat.Find
Nat.find.congr_simp : ∀ {p p_1 : ℕ → Prop} (e_p : p = p_1) {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (H : ∃ n, p n),
  Nat.find H = Nat.find ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.summable_iff_of_support : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : γ → α} (e : ↑(Function.support f) ≃ ↑(Function.support g)),
  (∀ (x : ↑(Function.support f)), g ↑(e x) = f ↑x) → (Summable f ↔ Summable g)
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.preimage_Ioc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b a : β),
  ⇑e ⁻¹' Set.Ioc b a = Set.Ioc (e.symm b) (e.symm a)
-- Init.Data.Array.Monadic
Array.allM_pure : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → Bool} {xs : Array α},
  Array.allM (fun x => pure (p x)) xs = pure (xs.all p)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.exists_degree_lt : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : Fintype σ] (f : MvPolynomial σ R) (n : ℕ),
  f.totalDegree < n * Fintype.card σ → ∀ {d : σ →₀ ℕ}, d ∈ f.support → ∃ i, d i < n
-- Init.Data.SInt.Lemmas
ISize.le_iff_toBitVec_sle : ∀ {a b : ISize}, a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.mk.injEq : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] (toSubgroup : Subgroup G)
  (isClosed' : IsClosed toSubgroup.carrier) (toSubgroup_1 : Subgroup G) (isClosed'_1 : IsClosed toSubgroup_1.carrier),
  ({ toSubgroup := toSubgroup, isClosed' := isClosed' } = { toSubgroup := toSubgroup_1, isClosed' := isClosed'_1 }) =
    (toSubgroup = toSubgroup_1)
-- Mathlib.Data.Finset.Insert
List.toFinset_nil : ∀ {α : Type u_1} [inst : DecidableEq α], [].toFinset = ∅
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- We call a category `NonPreadditiveAbelian` if it has a zero object, kernels, cokernels, finite
products and coproducts, and every monomorphism and every epimorphism is normal.

Notice that every such category is abelian (see `CategoryTheory.NonPreadditiveAbelian.preadditive`),
so in practice it is preferable to work directly with `Abelian`.
 -/
CategoryTheory.NonPreadditiveAbelian : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_eq_of_parseFirstByte_eq_oneMore : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
    b.toBitVec = 6#3 ++ BitVec.setWidth 5 b.toBitVec
-- Std.Data.TreeMap.Slice
Std.TreeMap.toList_roi : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.toList_roi._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap α β cmp} {bound : α},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice t bound<...*) = List.filter (fun e => (cmp e.1 bound).isGT) t.toList
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.Config.mk.sizeOf_spec : ∀ (wordSize stateSize : ℕ) (shiftSize : Fin stateSize) (maskBits : Fin wordSize) (xorMask : BitVec wordSize)
  (temperingShifts : ℕ × ℕ × ℕ × ℕ) (temperingMasks : BitVec wordSize × BitVec wordSize × BitVec wordSize)
  (initMult initSeed : BitVec wordSize),
  sizeOf
      { wordSize := wordSize, stateSize := stateSize, shiftSize := shiftSize, maskBits := maskBits, xorMask := xorMask,
        temperingShifts := temperingShifts, temperingMasks := temperingMasks, initMult := initMult,
        initSeed := initSeed } =
    1 + sizeOf wordSize + sizeOf stateSize + sizeOf shiftSize + sizeOf maskBits + sizeOf xorMask +
            sizeOf temperingShifts +
          sizeOf temperingMasks +
        sizeOf initMult +
      sizeOf initSeed
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_erase_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], (↑m).WF → ∀ {k : α}, (m.erase k).getKey! k = default
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_val : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : α → Finset β) (h : (↑s).PairwiseDisjoint t),
  (s.disjiUnion t h).val = s.val.bind fun a => (t a).val
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- An orthogonal basis with respect to a right-separating bilinear map has no self-orthogonal
elements.  -/
LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight : ∀ {n : Type u_19} {R : Type u_20} {M : Type u_21} {M₁ : Type u_22} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] {I I' : R →+* R} {B : M →ₛₗ[I] M →ₛₗ[I'] M₁}
  [Nontrivial R] {v : Module.Basis n R M}, B.IsOrthoᵢ ⇑v → B.SeparatingRight → ∀ (i : n), (B (v i)) (v i) ≠ 0
-- Mathlib.RingTheory.LocalRing.Pullback
AlgHom.surjective_pullbackSnd_of_surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : Ring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] C) (g : B →ₐ[R] C), Function.Surjective ⇑f → Function.Surjective ⇑(f.pullbackSnd g)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.homOfLE_refl : ∀ {X : SSet} (S₁ : X.Subcomplex), SSet.Subcomplex.homOfLE ⋯ = CategoryTheory.CategoryStruct.id S₁.toSSet
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_rotateL : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β} {rk : α} {rv : β rk}
  {rl rr : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.rotateL k v l rk rv rl rr).toListModel =
    l.toListModel ++ ⟨k, v⟩ :: (rl.toListModel ++ ⟨rk, rv⟩ :: rr.toListModel)
-- Mathlib.Data.Fin.Tuple.Take
/-- Alternative version of `take_eq_take_list_get` with `v : Fin n → α` instead of `l : List α`.  -/
Fin.get_take_ofFn_eq_take_comp_cast : ∀ {n : ℕ} {α : Type u_2} {m : ℕ} (v : Fin n → α) (h : m ≤ n),
  (List.take m (List.ofFn v)).get = Fin.take m h v ∘ Fin.cast ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_one_comm : ∀ {R : Type u_1} {M : Type u_4} [inst : CommSemiring R] [inst_1 : MulOneClass M] (r : R) (f : MonoidAlgebra R M),
  MonoidAlgebra.single 1 r * f = f * MonoidAlgebra.single 1 r
-- Mathlib.Order.Heyting.Basic
Disjoint.sdiff_eq_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → a \ b = a
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Zero G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G],
  ⇑0 = 0
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.Embedding.instFullEmbedding : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C],
  (CategoryTheory.Mat_.embedding C).Full
-- Mathlib.Analysis.Convex.Exposed
IsExposed.subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A B : Set E}, IsExposed 𝕜 A B → B ⊆ A
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.coe_withLpProdUnique : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : Unique β], ⇑(IsometryEquiv.withLpProdUnique p α β) = WithLp.fst
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- A division function (denoted `/`) on `R`.
This satisfies the property `b * (a / b) + a % b = a`, where `%` denotes `remainder`.  -/
EuclideanDomain.quotient : {R : Type u} → [self : EuclideanDomain R] → R → R → R
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : CancelMonoid α],
  MulOpposite.instCancelMonoid = { toLeftCancelMonoid := MulOpposite.instLeftCancelMonoid, toIsRightCancelMul := ⋯ }
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.Monadic.step_eq_step : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] {it : Std.IterM Id α},
  Std.Iterator.step it = pure (Std.Shrink.deflate ⟨Std.Rxo.Iterator.Monadic.step it, ⋯⟩)
-- Mathlib.Data.Finset.Preimage
Finset.preimage_subset_of_subset_image : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {f : α → β} {s : Finset β} {t : Finset α},
  s ⊆ Finset.image f t → ∀ {hf : Set.InjOn f (f ⁻¹' ↑s)}, s.preimage f hf ⊆ t
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_restrictScalars : ∀ (R : Type u_1) {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {S : Type u_5}
  [inst_6 : CommSemiring S] [inst_7 : Algebra S A] [inst_8 : Module S M] [inst_9 : LinearMap.CompatibleSMul A M R S]
  (d : Derivation S A M), ⇑(Derivation.restrictScalars R d) = ⇑d
-- Mathlib.Order.Interval.Set.Disjoint
IsGLB.iUnion_Ioi_eq : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {a : α} {f : ι → α},
  IsGLB (Set.range f) a → ⋃ x, Set.Ioi (f x) = Set.Ioi a
-- Mathlib.MeasureTheory.Integral.Average
/-- If `s` is a connected set of finite, nonzero `μ`-measure and `f : α → ℝ` is continuous on `s`
and integrable on `s` w.r.t. `μ`, then `f` attains its `μ`-average on `s`.  -/
MeasureTheory.exists_eq_setAverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [inst : TopologicalSpace α]
  {f : α → ℝ},
  IsConnected s →
    ContinuousOn f s → MeasureTheory.IntegrableOn f s μ → μ s ≠ ⊤ → μ s ≠ 0 → ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The relation itself.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {I₁ I₂ : S.Arrow} (self : I₁.Relation I₂),
  CategoryTheory.CategoryStruct.comp self.g₁ I₁.f = CategoryTheory.CategoryStruct.comp self.g₂ I₂.f
-- Mathlib.Topology.MetricSpace.Closeds
/-- In an emetric space, the type of non-empty compact subsets is an emetric space,
where the edistance is the Hausdorff edistance  -/
TopologicalSpace.NonemptyCompacts.instEMetricSpace : {α : Type u_1} → [inst : EMetricSpace α] → EMetricSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Tactic.Translate.Core
/-- An optional flag for not giving the new declaration a user-facing name.
This is achieved by appending e.g. `_to_dual_1` to the name of the original declaration.  -/
Mathlib.Tactic.Translate.Config.none : Mathlib.Tactic.Translate.Config → Bool
-- Mathlib.Data.List.Rotate
List.cyclicPermutations_ne_nil : ∀ {α : Type u} (l : List α), l.cyclicPermutations ≠ []
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.top_lie_le_iff_le_normalizer : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (N N' : LieSubmodule R L M), ⁅⊤, N⁆ ≤ N' ↔ N ≤ N'.normalizer
-- Init.Data.Int.Order
Int.le_toNat : ∀ {n : ℕ} {z : ℤ}, 0 ≤ z → (n ≤ z.toNat ↔ ↑n ≤ z)