mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Countable
/-- A category with countably many objects and morphisms.  -/
CategoryTheory.CountableCategory : (J : Type u_1) → [CategoryTheory.Category.{v_1, u_1} J] → Prop
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_lift_snd_f_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c}
  (α : M ⟶ K) (β : M ⟶ L) (i : ι) {Z : C} (h : L.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h) =
    CategoryTheory.CategoryStruct.comp (β.f i) h
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.not_summable_iff_tendsto_nat_atTop : ∀ {f : ℕ → NNReal}, ¬Summable f ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- This is the map from the coinvariants of `M : Rep R G` to the invariants, induced by the map
`m ↦ ∑ g : G, M.ρ g m`.  -/
Rep.tateNorm : {R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] →
      [Fintype G] →
        (M : Rep.{u, u, u} R G) →
          (groupHomology.inhomogeneousChains M).X 0 ⟶ (groupCohomology.inhomogeneousCochains M).X 0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.ker.ι_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] (f : CategoryTheory.Arrow C),
  (CategoryTheory.Limits.ker.ι C).app f = CategoryTheory.Limits.kernel.ι f.hom
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.instIsIsoτ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂) [CategoryTheory.IsIso f], CategoryTheory.IsIso f.τ₂
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.ι_comp_coequalizerComparison : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π (G.map f) (G.map g))
      (CategoryTheory.Limits.coequalizerComparison f g G) =
    G.map (CategoryTheory.Limits.coequalizer.π f g)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_edist_eq_of_L2 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x y : WithLp 2 (α × β)), edist x y = (edist x.fst y.fst ^ 2 + edist x.snd y.snd ^ 2) ^ (1 / 2)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α}, k ∈ t → t.getKey? k = some k
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.mk.sizeOf_spec : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : SizeOf k]
  [inst_4 : SizeOf K] (toIntermediateField : IntermediateField k K)
  [finiteDimensional : FiniteDimensional k ↥toIntermediateField] [isGalois : IsGalois k ↥toIntermediateField],
  sizeOf { toIntermediateField := toIntermediateField, finiteDimensional := finiteDimensional, isGalois := isGalois } =
    1 + sizeOf toIntermediateField + sizeOf finiteDimensional + sizeOf isGalois
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.PseudoMetrizableSpace.mk : ∀ {X : Type u_5} [t : TopologicalSpace X],
  (∃ u, u.toTopologicalSpace = t ∧ (uniformity X).IsCountablyGenerated) → TopologicalSpace.PseudoMetrizableSpace X
-- Mathlib.Order.Cover
AntisymmRel.trans_covBy : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → b ⋖ c → a ⋖ c
-- Aesop.Rule.Name
Aesop.PhaseName.norm.sizeOf_spec : sizeOf Aesop.PhaseName.norm = 1
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt : ∀ {𝕜 : 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] {s : Set M} {x : M} [IsManifold I 1 M]
  (V : (x : M) → TangentSpace I x),
  V =ᶠ[nhdsWithin x s]
    VectorField.mpullback I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x))
      (VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I))
-- Mathlib.Analysis.Convex.EGauge
le_egauge_pi : ∀ {𝕜 : Type u_1} [inst : NNNorm 𝕜] {ι : Type u_3} {E : ι → Type u_4} [inst_1 : (i : ι) → SMul 𝕜 (E i)] {I : Set ι}
  {i : ι}, i ∈ I → ∀ (s : (i : ι) → Set (E i)) (x : (i : ι) → E i), egauge 𝕜 (s i) (x i) ≤ egauge 𝕜 (I.pi s) x
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.noncompactSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], NoncompactSpace (TopologicalSpace.Compacts α) ↔ NoncompactSpace α
-- Batteries.Data.List.Perm
List.Perm.flatten_congr : ∀ {α : Type u_1} {l₁ l₂ : List (List α)}, List.Forall₂ (fun x1 x2 => x1.Perm x2) l₁ l₂ → l₁.flatten.Perm l₂.flatten
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, (t.getKey? a).isSome = t.contains a
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.zero_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β), ProbabilityTheory.Kernel.comp 0 κ = 0
-- Mathlib.Tactic.Ring.Common
/-- The normalized result.  -/
Mathlib.Tactic.Ring.Common.Result.expr : {u : Lean.Level} →
  {α : Q(Type u)} → {E : Q(«$α») → Type u_1} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.Common.Result E e → Q(«$α»)
-- Mathlib.Order.Heyting.Basic
Pi.instHeytingAlgebra : {ι : Type u_1} → {α : ι → Type u_4} → [(i : ι) → HeytingAlgebra (α i)] → HeytingAlgebra ((i : ι) → α i)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.finsetSum_comp`. -/
ContinuousLinearMap.finset_sum_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {ι : Type u_9} {s : Finset ι}
  [inst_13 : ContinuousAdd M₃] (g : ι → M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂), (∑ i ∈ s, g i) ∘SL f = ∑ i ∈ s, g i ∘SL f
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_add_fdiv_mul : ∀ (a b : ℤ), a.fmod b + a.fdiv b * b = a
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- Note that this is not true for `Fintype.card n = 1` since `1 - 2 = 0` and not `-1`.  -/
Matrix.adjugate_adjugate : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  Fintype.card n ≠ 1 → A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_add : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {f g : α → F'},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ →
      MeasureTheory.condExpL1 hm μ (f + g) = MeasureTheory.condExpL1 hm μ f + MeasureTheory.condExpL1 hm μ g
-- Mathlib.Data.Finset.Image
Finset.erase_image_subset_image_erase : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] (f : α → β) (s : Finset α) (a : α),
  (Finset.image f s).erase (f a) ⊆ Finset.image f (s.erase a)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_add_eq_mul_omega0 : ∀ {a b : Ordinal.{u_1}}, b ≤ a * Ordinal.omega0 → Ordinal.nfp (fun x => a + x) b = a * Ordinal.omega0
-- Mathlib.Logic.Equiv.Set
Equiv.symm_image_image : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α), ⇑e.symm '' ⇑e '' s = s
-- Mathlib.Data.Int.LeastGreatest
/-- `Int.leastOfBdd` is the least integer satisfying a predicate which is false for all `z : ℤ` with
`z < b` for some fixed `b : ℤ`.  -/
Int.isLeast_coe_leastOfBdd : ∀ {P : ℤ → Prop} [inst : DecidablePred P] (b : ℤ) (Hb : ∀ (z : ℤ), P z → b ≤ z) (Hinh : ∃ z, P z),
  IsLeast {z | P z} ↑(b.leastOfBdd Hb Hinh)
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousOn_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α},
  UpperSemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≥ y) → f x ≥ y
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.HasStrictInitialObjects.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasStrictInitialObjects C]
  {I A : C} (f : A ⟶ I) (a : CategoryTheory.Limits.IsInitial I), CategoryTheory.IsIso f
-- Mathlib.Order.GaloisConnection.Defs
/-- Make a `GaloisInsertion` between `α` and `β` from a `GaloisCoinsertion` between `αᵒᵈ` and
`βᵒᵈ`.  -/
GaloisCoinsertion.ofDual : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {l : αᵒᵈ → βᵒᵈ} →
          {u : βᵒᵈ → αᵒᵈ} →
            GaloisCoinsertion l u →
              GaloisInsertion (⇑OrderDual.ofDual ∘ u ∘ ⇑OrderDual.toDual) (⇑OrderDual.ofDual ∘ l ∘ ⇑OrderDual.toDual)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F₁ F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X),
  (CategoryTheory.MorphismProperty.naturalityProperty app).StableUnderInverse
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.mono_map_iff_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) [hF₁ : F.PreservesMonomorphisms]
  [hF₂ : F.ReflectsMonomorphisms], CategoryTheory.Mono (F.map f) ↔ CategoryTheory.Mono f
-- Mathlib.Data.Set.Lattice
Set.iUnion_of_singleton : ∀ (α : Type u_12), ⋃ x, {x} = Set.univ
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_ofList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  (Std.HashMap.ofList l).isEmpty = l.isEmpty
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.closedEBall_zero`. -/
EMetric.closedBall_zero : ∀ {γ : Type w} [inst : EMetricSpace γ] (x : γ), Metric.closedEBall x 0 = {x}
-- Lean.Meta.SameCtorUtils
_private.Lean.Meta.SameCtorUtils.0.Lean.Meta.occursOrInType.go : Lean.LocalContext → Lean.Expr → Lean.Expr → Bool
-- Mathlib.Order.Disjoint
codisjoint_left_comm : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b c : α},
  Codisjoint a (b ⊔ c) ↔ Codisjoint b (a ⊔ c)
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.F_int_eq_of_mem_Icc : ∀ (k : ℕ) {a : ℝ},
  a ∈ Set.Icc 0 1 →
    ∀ {t : ℝ},
      0 < t →
        HurwitzKernelBounds.F_int k (↑a) t = HurwitzKernelBounds.F_nat k a t + HurwitzKernelBounds.F_nat k (1 - a) t
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.comp_X_sub_C : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R}, p.Monic → ∀ (r : R), (p.comp (Polynomial.X - Polynomial.C r)).Monic
-- Mathlib.Topology.Order.IntermediateValue
/-- If a preconnected set in a linear order space is unbounded below and above, then it is the whole
space.  -/
IsPreconnected.eq_univ_of_unbounded : ∀ {α : Type v} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {s : Set α},
  IsPreconnected s → ¬BddBelow s → ¬BddAbove s → s = Set.univ
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.map_sub_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G},
  IsBoundedBilinearMap 𝕜 f → ∀ {x y : E} {z : F}, f (x - y, z) = f (x, z) - f (y, z)
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.isHomogeneous_toTupleMvPolynomial : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (i : Fin 2),
  (p.toTupleMvPolynomial i).IsHomogeneous p.natDegree
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.prod_mono_left : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (t : Subsemiring S),
  Monotone fun s => s.prod t
-- Mathlib.Order.Hom.CompleteLattice
instCoeTCSSupHomOfSSupHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : SupSet α] → [inst_2 : SupSet β] → [sSupHomClass F α β] → CoeTC F (sSupHom α β)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, ∅.size = 0
-- Init.System.FilePath
/-- A path on the file system.

Paths consist of a sequence of directories followed by the name of a file or directory. They are
delimited by a platform-dependent separator character (see `System.FilePath.pathSeparator`).
 -/
System.FilePath : Type
-- Std.Data.DTreeMap.Internal.Operations
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.interSmallerFn : {α : Type u} →
  {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → { t // t.Balanced } → α → { res // res.Balanced }
-- Init.Data.Nat.Fold
Nat.fold_succ : ∀ {α : Type u} (n : ℕ) (f : (i : ℕ) → i < n + 1 → α → α) (init : α),
  (n + 1).fold f init = f n ⋯ (n.fold (fun i h => f i ⋯) init)
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
SSet.range_eq_iSup_of_isColimit : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type u)]
  {F : CategoryTheory.Functor J SSet} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  {X : SSet} (φ : c.pt ⟶ X),
  SSet.Subcomplex.range φ = ⨆ j, SSet.Subcomplex.range (CategoryTheory.CategoryStruct.comp (c.ι.app j) φ)
-- Init.Data.Dyadic.Basic
Int.trailingZeros.aux.congr_simp : ∀ (k k_1 : ℕ) (e_k : k = k_1) (i i_1 : ℤ) (e_i : i = i_1) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc acc_1 : ℕ),
  acc = acc_1 → Int.trailingZeros.aux k i hi hk acc = Int.trailingZeros.aux k_1 i_1 ⋯ ⋯ acc_1
-- Mathlib.Data.PNat.Basic
PNat.dvd_one_iff : ∀ (n : ℕ+), n ∣ 1 ↔ n = 1
-- Mathlib.Data.Rat.Lemmas
Rat.inv_ofNat_num : ∀ (a : ℕ) [a.AtLeastTwo], (OfNat.ofNat a)⁻¹.num = 1
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instSub : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddGroup Y] → Sub (Function.locallyFinsuppWithin U Y)
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.IsHomological.toPreservesZeroMorphisms : ∀ {C : Type u_1} {A : Type u_3} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.HasShift C ℤ}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} A} {F : CategoryTheory.Functor C A}
  {inst_3 : CategoryTheory.Limits.HasZeroObject C} {inst_4 : CategoryTheory.Preadditive C}
  {inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_6 : CategoryTheory.Pretriangulated C}
  {inst_7 : CategoryTheory.Abelian A} [self : F.IsHomological], F.PreservesZeroMorphisms
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.lt_sup_edge : ∀ {V : Type u_1} (G : SimpleGraph V) (s t : V), s ≠ t → ¬G.Adj s t → G < G ⊔ SimpleGraph.edge s t
-- Init.Control.Lawful.Instances
ReaderT.run.eq_1 : ∀ {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ), x.run r = x r
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- If `P` lies over `p`, then `R / p` has a canonical map to `A / P`.  -/
Ideal.Quotient.algebraQuotientOfLEComap : {A : Type u_3} →
  [inst : Ring A] →
    {R : Type u_5} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R A] →
          {p : Ideal R} →
            {P : Ideal A} → [inst_3 : P.IsTwoSided] → p ≤ Ideal.comap (algebraMap R A) P → Algebra (R ⧸ p) (A ⧸ P)
-- Mathlib.Analysis.Calculus.MeanValue
/-- If two differentiable functions on `[a, b]` have the same derivative within `[a, b]` everywhere
on `[a, b)` and are equal at `a`, then they are equal everywhere on `[a, b]`.  -/
eq_of_derivWithin_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {g : ℝ → E},
  DifferentiableOn ℝ f (Set.Icc a b) →
    DifferentiableOn ℝ g (Set.Icc a b) →
      Set.EqOn (derivWithin f (Set.Icc a b)) (derivWithin g (Set.Icc a b)) (Set.Ico a b) →
        f a = g a → ∀ y ∈ Set.Icc a b, f y = g y
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.leftUnitor_hom_app : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B),
  (CategoryTheory.Bicategory.leftUnitor F).hom.toNatTrans.app X = CategoryTheory.eqToHom ⋯
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportFailure.mk.inj : ∀ {module const : Lean.Name} {exception : Lean.Exception} {module_1 const_1 : Lean.Name} {exception_1 : Lean.Exception},
  { module := module, const := const, exception := exception } =
      { module := module_1, const := const_1, exception := exception_1 } →
    module = module_1 ∧ const = const_1 ∧ exception = exception_1
-- Mathlib.GroupTheory.Index
Subgroup.index_range : ∀ {G : Type u_1} [inst : Group G] {f : G →* G} [hf : f.ker.FiniteIndex], f.range.index = Nat.card ↥f.ker
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_finsetProd : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R),
  (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree
-- Mathlib.GroupTheory.OrderOfElement
/-- **Alias** of the reverse direction of `isMulTorsionFree_iff_not_isOfFinOrder`. -/
IsMulTorsionFree.of_not_isOfFinOrder : ∀ {G : Type u_1} [inst : CommGroup G], (∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a) → IsMulTorsionFree G
-- Mathlib.Data.Sym.Sym2
/-- A predicate for testing whether an element of `Sym2 α` is on the diagonal.
 -/
Sym2.IsDiag : {α : Type u_1} → Sym2 α → Prop
-- Mathlib.Analysis.Complex.RealDeriv
Differentiable.real_of_complex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
  Differentiable ℂ f → Differentiable ℝ f
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- A measure `μ` on the `AddQuotient` of `α` mod `G` satisfies
`AddQuotientMeasureEqMeasurePreimage` if: for any fundamental domain `t`, and any measurable
subset `U` of the quotient, `μ U = volume ((π ⁻¹' U) ∩ t)`.  -/
MeasureTheory.AddQuotientMeasureEqMeasurePreimage : {G : Type u_1} →
  {α : Type u_3} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] →
        [inst_2 : MeasurableSpace α] →
          autoParam (MeasureTheory.Measure α) MeasureTheory.AddQuotientMeasureEqMeasurePreimage._auto_1 →
            MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)) → Prop
-- Init.Data.List.Lemmas
List.getElem!_eq_getElem?_getD : ∀ {α : Type u_1} [inst : Inhabited α] {l : List α} {i : ℕ}, l[i]! = l[i]?.getD default
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.modify_eq_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (f : β a → β a), m.modify a f = m.alter a fun x => Option.map f x
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.finset_sup_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [inst_3 : OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {t : Set X}
  {x : X}, (∀ i ∈ s, ContinuousWithinAt (f i) t x) → ContinuousWithinAt (fun a => s.sup fun x => f x a) t x
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimitCore.mk.sizeOf_spec : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  [inst_1 : SizeOf J] (desc : (c' : F.CoconeTypes) → c.pt → c'.pt)
  (fac :
    autoParam (∀ (c' : F.CoconeTypes) (j : J), desc c' ∘ c.ι j = c'.ι j)
      CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac._autoParam)
  (funext : ∀ {T : Type w₂} {f g : c.pt → T}, (∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) → f = g),
  sizeOf { desc := desc, fac := fac, funext := funext } = 1
-- Mathlib.Data.List.Basic
List.getLastI.eq_2 : ∀ {α : Type u_1} [inst : Inhabited α] (a : α), [a].getLastI = a
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.fromOpcycles_d_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) [inst_2 : K.HasHomology i] {Z : C}
  (h : K.X k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) (CategoryTheory.CategoryStruct.comp (K.d j k) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.IsFundamentalGroup.continuous_smul : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {F : CategoryTheory.Functor C FintypeCat}
  {inst_1 : CategoryTheory.GaloisCategory C} {G : Type u_1} {inst_2 : Group G}
  {inst_3 : (X : C) → MulAction G (F.obj X).obj} {inst_4 : TopologicalSpace G} {inst_5 : IsTopologicalGroup G}
  {inst_6 : CompactSpace G} [self : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (X : C),
  ContinuousSMul G (F.obj X).obj
-- Init.Data.List.Lemmas
List.filterMap.eq_2 : ∀ {α : Type u} {β : Type v} (f : α → Option β) (a : α) (as : List α),
  List.filterMap f (a :: as) =
    match f a with
    | none => List.filterMap f as
    | some b => b :: List.filterMap f as
-- Mathlib.Algebra.Group.Units.Equiv
toUnits_val_apply : ∀ {G : Type u_6} [inst : Group G] (x : Gˣ), toUnits ↑x = x
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.instNeg : {K : Type u_1} →
  {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → Neg (ConjRootClass K L)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∉ t₂ → (t₁ \ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.isLittleO_pow_logb_id_atTop : ∀ {b : ℝ} {n : ℕ}, (fun x => Real.logb b x ^ n) =o[Filter.atTop] id
-- Mathlib.Data.List.Cycle
List.next_reverse_eq_prev : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ (x : α) (hx : x ∈ l), l.reverse.next x ⋯ = l.prev x hx
-- Init.Data.BitVec.Lemmas
BitVec.or_zero : ∀ {w : ℕ} {x : BitVec w}, x ||| 0#w = x
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- The isomorphism from the restriction to the top subspace.
 -/
AlgebraicGeometry.PresheafedSpace.restrictTopIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (X : AlgebraicGeometry.PresheafedSpace C) → X.restrict ⋯ ≅ X
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonpos_of_mul_nonneg_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R], 0 ≤ a * b → b < 0 → a ≤ 0