mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_gt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.gt →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.filter (fun x => k x.fst == Ordering.gt) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        l.toListModel ++ ⟨k', v'⟩ :: List.filter (fun x => k x.fst == Ordering.gt) r.toListModel
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.posRootForm.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : LinearOrder S] [inst_7 : IsStrictOrderedRing S] [inst_8 : Algebra S R]
  [inst_9 : FaithfulSMul S R] [inst_10 : P.IsValuedIn S] [inst_11 : Fintype ι],
  P.posRootForm S = { form := P.RootForm, symm := ⋯, isOrthogonal_reflection := ⋯, exists_eq := ⋯, exists_pos_eq := ⋯ }
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.instMulOneClass : {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → MulOneClass (Monoid.Coprod M N)
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.funCC.sizeOf_spec : sizeOf Lean.Meta.Grind.AttrKind.funCC = 1
-- Init.Data.String.Substring
/-- Returns the substring-relative position of the first occurrence of `c` in `s`, or `s.bsize` if `c`
doesn't occur.
 -/
Substring.Raw.posOf : Substring.Raw → Char → String.Pos.Raw
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `η ▷ f`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight.mkEvalWhiskerRightAuxOf : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m] →
    Mathlib.Tactic.BicategoryLike.WhiskerRight → Mathlib.Tactic.BicategoryLike.Atom₁ → m Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The map between edge sets induced by a homomorphism.
The underlying map on edges is given by `Sym2.map`.  -/
SimpleGraph.Hom.mapEdgeSet : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G →g G' → ↑G.edgeSet → ↑G'.edgeSet
-- Mathlib.Tactic.Translate.Core
/-- Rename binder names in pi type.  -/
Mathlib.Tactic.Translate.renameBinderNames : Mathlib.Tactic.GuessName.GuessNameData → Lean.NameMap Lean.Name → Lean.Expr → Lean.Expr
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.eq_single_iff_length : ∀ {n : ℕ} (h : 0 < n) {c : Composition n}, c = Composition.single n h ↔ c.length = 1
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.mk.sizeOf_spec : ∀ (Functions : ℕ → Type u) (Relations : ℕ → Type v), sizeOf { Functions := Functions, Relations := Relations } = 1
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.norm_holderL_le : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G)
  [inst_7 : Fact (1 ≤ p)] [inst_8 : Fact (1 ≤ q)] [inst_9 : Fact (1 ≤ r)], ‖ContinuousLinearMap.holderL μ p q r B‖ ≤ ‖B‖
-- Mathlib.Combinatorics.Enumerative.Bell
_private.Mathlib.Combinatorics.Enumerative.Bell.0.Nat.bell.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_mapRingEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (e : R ≃+* S) (x : AddMonoidAlgebra R M) (m : M), ((AddMonoidAlgebra.mapRingEquiv M e) x).coeff m = e (x.coeff m)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.colimit_topology : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat)
  [inst_1 : CategoryTheory.Limits.HasColimit F],
  (CategoryTheory.Limits.colimit F).str =
    ⨆ j,
      TopologicalSpace.coinduced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)))
        (F.obj j).str
-- Mathlib.FieldTheory.Galois.Basic
/-- If `K/F` is a finite Galois extension, then for any extension `L/F`, the extension `KL/L`
is also Galois.
 -/
IsGalois.sup_right : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K L : IntermediateField F E)
  [IsGalois F ↥K] [FiniteDimensional F ↥K], K ⊔ L = ⊤ → IsGalois (↥L) E
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.comp_range : ∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂)
  (g : NormedAddGroupHom V₂ V₃), (g.comp f).range = AddSubgroup.map g.toAddMonoidHom f.range
-- Mathlib.Topology.CompactOpen
/-- If `g : C(Y, Z)` is a topology inducing map,
then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is a topology inducing map too.  -/
ContinuousMap.isInducing_postcomp : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (g : C(Y, Z)), Topology.IsInducing ⇑g → Topology.IsInducing g.comp
-- Mathlib.Algebra.Module.Lattice
/-- Any `R`-lattice is finite.  -/
Submodule.IsLattice.finite : ∀ {R : Type u_1} [inst : CommRing R] (A : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : Module A V] [inst_6 : IsScalarTower R A V]
  (M : Submodule R V) [Submodule.IsLattice A M], Module.Finite R ↥M
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.WeakRankFunction.mk.injEq : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] (rank : ↑P.II → α)
  (lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank x < rank y) (rank_1 : ↑P.II → α)
  (lt_1 : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank_1 x < rank_1 y),
  ({ rank := rank, lt := lt } = { rank := rank_1, lt := lt_1 }) = (rank = rank_1)
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.isT0 : ∀ (self : CpltSepUniformSpace), T0Space self.α
-- Init.Tactics
/-- Auxiliary macro for lifting have/suffices/let/...
It makes sure the "continuation" `?_` is the main goal after refining.
 -/
Lean.Parser.Tactic.tacticRefine_lift_ : Lean.ParserDescr
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instInter : {α : Type u} → {cmp : α → α → Ordering} → Inter (Std.TreeSet.Raw α cmp)
-- Mathlib.CategoryTheory.Elements
/-- The initial object in `F.Elements` if `F` is representable.  -/
CategoryTheory.Functor.Elements.initialOfRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} → {X : C} → F.RepresentableBy X → F.Elements
-- Qq.SortLocalDecls
Qq.SortLocalDecls.State.mk.injEq : ∀ (visited : Lean.NameSet) (result : Array Lean.LocalDecl) (visited_1 : Lean.NameSet) (result_1 : Array Lean.LocalDecl),
  ({ visited := visited, result := result } = { visited := visited_1, result := result_1 }) =
    (visited = visited_1 ∧ result = result_1)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.extendDomain : ∀ {α : Type u_2} {β : Type u_3} {g : Equiv.Perm α} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
  g.IsCycle → (g.extendDomain f).IsCycle
-- Mathlib.Data.Num.Lemmas
PosNum.to_nat_inj : ∀ {m n : PosNum}, ↑m = ↑n ↔ m = n
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instInhabited.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E], AddGroupSeminorm.instInhabited = { default := 0 }
-- Mathlib.SetTheory.Cardinal.NatCard
Finite.card_le_one_iff_subsingleton : ∀ {α : Type u_1} [Finite α], Nat.card α ≤ 1 ↔ Subsingleton α
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_sub_measure : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} {f : α → E} {ν : MeasureTheory.Measure α}
  (hTμ : MeasureTheory.DominatedFinMeasAdditive μ T C) (hTν : MeasureTheory.DominatedFinMeasAdditive ν T' C'),
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable f ν →
      MeasureTheory.setToFun (μ + ν) (T - T') ⋯ f = MeasureTheory.setToFun μ T hTμ f - MeasureTheory.setToFun ν T' hTν f
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.prop_shiftClosure_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (X : C), P.shiftClosure A X ↔ ∃ Y a x, P Y
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.mk.congr_simp : ∀ {A : Type u_9} {B : Type u_10} [inst : Add A] [inst_1 : Add B] (toEquiv toEquiv_1 : A ≃ B)
  (e_toEquiv : toEquiv = toEquiv_1) (map_add' : ∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y),
  { toEquiv := toEquiv, map_add' := map_add' } = { toEquiv := toEquiv_1, map_add' := ⋯ }
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addCovolume.eq_1 : ∀ (G : Type u_6) (α : Type u_7) [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α]
  (ν : MeasureTheory.Measure α),
  MeasureTheory.addCovolume G α ν = if funDom : MeasureTheory.HasAddFundamentalDomain G α ν then ν ⋯.choose else 0
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.instIsProbabilityMeasureSetSetBernoulli : ∀ {ι : Type u_1} {u : Set ι} {p : ↑unitInterval},
  MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.setBernoulli u p)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.eq_inv_of_hom_inv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [inst_1 : CategoryTheory.IsIso f]
  {g : Y ⟶ X}, CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X → g = CategoryTheory.inv f
-- Mathlib.Algebra.Ring.Commute
Ring.instBracket : {R : Type u} → [NonUnitalNonAssocRing R] → Bracket R R
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- Given a morphism `φ : K ⟶ L` of cochain complexes, this is the triangle
`mappingCocone φ ⟶ K ⟶ L ⟶ ...`.  -/
CochainComplex.mappingCocone.triangle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (K ⟶ L) →
          [CategoryTheory.Limits.HasBinaryBiproducts C] → CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- Curried `C^n` functions are `C^n` in the second coordinate.  -/
ContMDiffOn.curry_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {s : Set (M × M')},
  ContMDiffOn (I.prod I') J n (Function.uncurry f) s → ContMDiffOn I' J n (fun y => f x y) {y | (x, y) ∈ s}
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.comp_of_degree_le_one_of_monic : ∀ {R : Type u_1} [inst : CommSemiring R] {f g : Polynomial R}, f.Splits → g.degree ≤ 1 → g.Monic → (f.comp g).Splits
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_inter_inter_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u v : Finset α), s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from above (a.e. version):
the measure of the intersection of a family of sets that is almost everywhere monotone
is equal to the infimum of the measures.  -/
MeasureTheory.measure_iInter_of_ae_monotone : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [IsCodirectedOrder ι] [Filter.atBot.IsCountablyGenerated] {s : ι → Set α},
  (∀ᵐ (ω : α) ∂μ, Monotone fun x => ω ∈ s x) →
    (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) → (∃ i, μ (s i) ≠ ⊤) → μ (⋂ i, s i) = ⨅ i, μ (s i)
-- Batteries.Data.Array.Scan
Array.size_scanl : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} (init : β) (as : Array α), (Array.scanl f init as).size = as.size + 1
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.dropSuffix_char_eq_dropSuffix_beq : ∀ {c : Char} {s : String.Slice}, s.dropSuffix c = s.dropSuffix fun x => x == c
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.allM_pure : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {p : β → ULift.{w, 0} Bool}, Std.IterM.allM (fun x => pure (p x)) it = Std.IterM.all (fun x => (p x).down) it
-- Aesop.Util.EqualUpToIds
_private.Aesop.Util.EqualUpToIds.0.Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃.normalizeMVar : Lean.MetavarContext → Lean.MVarId → Lean.MetaM Aesop.EqualUpToIds.MVarValue
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_σ_succ'_apply : ∀ {S : SSet} {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.succ →
    ∀ (x : S.obj (Opposite.op { len := n })),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S j))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S i)) x) =
        x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.instLawfulVecOperatorShiftConcatInputBlastShiftConcat : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat
-- Mathlib.GroupTheory.Complement
/-- A right transversal is finite iff the subgroup has finite index.  -/
Subgroup.IsComplement.finite_right_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G},
  Subgroup.IsComplement (↑H) T → (Finite ↑T ↔ H.FiniteIndex)
-- Mathlib.Data.Matrix.Basic
/-- The `RingEquiv` between spaces of square matrices induced by a `RingEquiv` between their
coefficients. This is `Matrix.map` as a `RingEquiv`.  -/
RingEquiv.mapMatrix : {m : Type u_2} →
  {α : Type u_11} →
    {β : Type u_12} →
      [inst : Fintype m] →
        [DecidableEq m] →
          [inst_2 : NonAssocSemiring α] → [inst_3 : NonAssocSemiring β] → α ≃+* β → Matrix m m α ≃+* Matrix m m β
-- Mathlib.Analysis.Normed.Group.Basic
ne_one_of_mem_unit_sphere : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : ↑(Metric.sphere 1 1)), ↑x ≠ 1
-- Mathlib.RingTheory.WittVector.Defs
WittVector.zsmul_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (m : ℤ) (x : WittVector p R) (n : ℕ),
  (m • x).coeff n = WittVector.peval (WittVector.wittZSMul p m n) ![x.coeff]
-- Mathlib.Topology.Order.Basic
tendsto_order : ∀ {α : Type u} {β : Type v} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {f : β → α} {a : α}
  {x : Filter β},
  Filter.Tendsto f x (nhds a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
-- Mathlib.Topology.MetricSpace.Thickening
/-- For the equality, see `infEDist_cthickening`.  -/
Metric.infEDist_le_infEDist_cthickening_add : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
  Metric.infEDist x s ≤ Metric.infEDist x (Metric.cthickening δ s) + ENNReal.ofReal δ
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.map : ∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : Monoid M] [inst_2 : Monoid N]
  [MonoidHomClass F M N] (f : F) {x : M}, IsUnit x → IsUnit (f x)
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.getIndexToInclude?.go : Lean.Expr → List ℕ → OptionT Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Category.Ring.Epi
CommRingCat.epi_iff_epi : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R S)) ↔ Algebra.IsEpi R S
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.findKey : {α : Type} →
  Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) →
    Lean.Meta.DiscrTree.Key → Option (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, (m.insertIfNew k v).contains a = (k == a || m.contains a)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Canonical embedding of `SL(2, ℤ)` into `GL(2, ℝ)⁺`, bundled as a group hom.  -/
ModularGroup.coeHom : Matrix.SpecialLinearGroup (Fin 2) ℤ →* ↥(Matrix.GLPos (Fin 2) ℝ)
-- Mathlib.Topology.Closure
dense_univ : ∀ {X : Type u} [inst : TopologicalSpace X], Dense Set.univ
-- Mathlib.Order.Types.Arithmetic
_private.Mathlib.Order.Types.Arithmetic.0.OrderType.card.eq_1 : ∀ (o : OrderType.{u_1}), o.card = o.liftOn (fun α x => Cardinal.mk α) OrderType.card._proof_1✝
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.norm_sub_modPart_aux : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ), ‖↑r‖ ≤ 1 → ↑p ∣ r.num - r.num * r.den.gcdA p % ↑p * ↑r.den
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.BallPackage.mk : {β : Type u_1} →
  {α : Type u_2} →
    (β → α) →
      (r : β → ℝ) → (∀ (b : β), 0 < r b) → (r_bound : ℝ) → (∀ (b : β), r b ≤ r_bound) → Besicovitch.BallPackage β α
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateCases! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.Expr → Lean.FVarId → Array (Lean.Compiler.LCNF.Alt pu) → Lean.Compiler.LCNF.Code pu
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_singleton : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {a : α}, {a}.lcm = normalize a
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.surjective_mk' : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M], Function.Surjective ⇑(LieSubmodule.Quotient.mk' N)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- For `a = 0`, both kernels agree.  -/
HurwitzZeta.evenKernel_eq_cosKernel_of_zero : HurwitzZeta.evenKernel 0 = HurwitzZeta.cosKernel 0
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.ext_iff : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [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]
  [inst_7 : LieRing.IsNilpotent L] {χ₁ χ₂ : LieModule.Weight R L M}, χ₁ = χ₂ ↔ ∀ (x : L), χ₁ x = χ₂ x
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_iff_isLittleO : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =o[𝕜; l] g ↔ f =o[l] g
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_or : ∀ {v i : ℕ} {x y : BitVec v}, (x ||| y).getLsbD i = (x.getLsbD i || y.getLsbD i)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_iff_lt_mul' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, a / b < c ↔ a < b * c
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_lift : ∀ (a : Cardinal.{u_1}), Cardinal.lift.{w, max v u_1} (Cardinal.lift.{v, u_1} a) = Cardinal.lift.{max v w, u_1} a
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_left_π : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).left.π =
    X.mapFourδ₄Toδ₃' i₀' i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.Topology.Order.Lattice
/-- Let `L` be a lattice equipped with a topology such that `L` has continuous infimum and supremum.
Then `L` is said to be a *topological lattice*.
 -/
TopologicalLattice : (L : Type u_1) → [TopologicalSpace L] → [Lattice L] → Prop
-- Init.Data.List.Basic
List.unzip_cons : ∀ {α : Type u} {β : Type v} {t : List (α × β)} {h : α × β},
  (h :: t).unzip =
    match t.unzip with
    | (as, bs) => (h.1 :: as, h.2 :: bs)
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ioc (f (Order.succ n)) (f n)` are pairwise disjoint.  -/
Antitone.pairwise_disjoint_on_Ioc_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Function.onFun Disjoint fun n => Set.Ioc (f (Order.succ n)) (f n))
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.vComp_iso_hom_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₅] [inst_5 : CategoryTheory.Category.{v_6, u_6} C₆]
  (L₁ : CategoryTheory.Functor C₁ C₂) (L₂ : CategoryTheory.Functor C₂ C₃) (H₁ : CategoryTheory.Functor C₁ C₄)
  (H₂ : CategoryTheory.Functor C₂ C₅) (H₃ : CategoryTheory.Functor C₃ C₆) (R₁ : CategoryTheory.Functor C₄ C₅)
  (R₂ : CategoryTheory.Functor C₅ C₆) [inst_6 : CategoryTheory.CatCommSq H₁ L₁ R₁ H₂]
  [inst_7 : CategoryTheory.CatCommSq H₂ L₂ R₂ H₃] (X : C₁),
  (CategoryTheory.CatCommSq.iso H₁ (L₁.comp L₂) (R₁.comp R₂) H₃).hom.app X =
    CategoryTheory.CategoryStruct.comp (R₂.map ((CategoryTheory.CatCommSq.iso H₁ L₁ R₁ H₂).hom.app X))
      ((CategoryTheory.CatCommSq.iso H₂ L₂ R₂ H₃).hom.app (L₁.obj X))
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.applyₗ_apply_apply : ∀ {R : Type u_1} {M : Type u_4} {M₂ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (v : M) (f : M →ₗ[R] M₂),
  (LinearMap.applyₗ v) f = f v