mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  k' ∈ t.alter k f ↔ if cmp k k' = Ordering.eq then (f (t.get? k)).isSome = true else k' ∈ t
-- Mathlib.Data.Finset.Image
Finset.image_eq_iff_surjOn_mapsTo : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  Finset.image f s = t ↔ Set.SurjOn f ↑s ↑t ∧ Set.MapsTo f ↑s ↑t
-- Mathlib.Data.Int.Basic
Int.natAbs_le_of_dvd_ne_zero : ∀ {m n : ℤ}, m ∣ n → n ≠ 0 → m.natAbs ≤ n.natAbs
-- Mathlib.Order.Partition.Finpartition
Finpartition.part_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α}, P.part a ∈ P.parts ↔ a ∈ s
-- Lean.LocalContext
Lean.LocalDecl.ldecl.injEq : ∀ (index : ℕ) (fvarId : Lean.FVarId) (userName : Lean.Name) (type value : Lean.Expr) (nondep : Bool)
  (kind : Lean.LocalDeclKind) (index_1 : ℕ) (fvarId_1 : Lean.FVarId) (userName_1 : Lean.Name)
  (type_1 value_1 : Lean.Expr) (nondep_1 : Bool) (kind_1 : Lean.LocalDeclKind),
  (Lean.LocalDecl.ldecl index fvarId userName type value nondep kind =
      Lean.LocalDecl.ldecl index_1 fvarId_1 userName_1 type_1 value_1 nondep_1 kind_1) =
    (index = index_1 ∧
      fvarId = fvarId_1 ∧ userName = userName_1 ∧ type = type_1 ∧ value = value_1 ∧ nondep = nondep_1 ∧ kind = kind_1)
-- Mathlib.LinearAlgebra.Matrix.RowCol
/-- `Matrix.replicateRow ι u` is the matrix with all rows equal to the vector `u`.

To get a row matrix with exactly one row, `Matrix.replicateRow (Fin 1) u` is the canonical choice.
 -/
Matrix.replicateRow : {n : Type u_3} → {α : Type v} → (ι : Type u_6) → (n → α) → Matrix ι n α
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapId : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.Pseudofunctor B C) →
          (a : B) → self.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (self.obj a)
-- Init.Data.Float.Float32
/-- Computes the floor of a floating-point number, which is the largest integer that's no larger
than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`floorf`.

Examples:
 * `Float32.floor 1.5 = 1`
 * `Float32.floor (-1.5) = (-2)`
 -/
Float32.floor : Float32 → Float32
-- Mathlib.Algebra.Lie.Basic
LieEquiv.mk : {R : Type u} →
  {L : Type v} →
    {L' : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing L'] →
              [inst_4 : LieAlgebra R L'] →
                (toLieHom : L →ₗ⁅R⁆ L') →
                  (invFun : L' → L) →
                    autoParam (Function.LeftInverse invFun (↑toLieHom).toFun) LieEquiv.left_inv._autoParam →
                      autoParam (Function.RightInverse invFun (↑toLieHom).toFun) LieEquiv.right_inv._autoParam →
                        L ≃ₗ⁅R⁆ L'
-- Mathlib.Data.Sym.Sym2.Order
/-- The supremum of the two elements.  -/
Sym2.sup : {α : Type u_1} → [SemilatticeSup α] → Sym2 α → α
-- Init.Data.Ord.SInt
ISize.instTransOrd : Std.TransOrd ISize
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.succ : ∀ {o : Ordinal.{u}}, (Order.succ o).IsFundamentalSequence 1 fun x x_1 => o
-- Mathlib.Data.W.Basic
/-- The canonical map from the sigma type into a `WType`. Given a node `a : α`, and
its children as a function `β a → WType β`, return the corresponding tree.  -/
WType.ofSigma : {α : Type u_1} → {β : α → Type u_2} → (a : α) × (β a → WType β) → WType β
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
alternatingGroup.mem_map_kleinFour_ofSubtype : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {s : Finset α},
  s.card = 4 →
    ∀ (k : ↥(alternatingGroup α)),
      k ∈ Subgroup.map (alternatingGroup.ofSubtype s) (alternatingGroup.kleinFour ↥s) ↔
        (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {l : List α} {k : α}, k ∈ t → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKey! k = t.getKey! k
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.comp_whiskerLeft_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h')
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η)
      h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h').inv h_1))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.pushforward_comp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R),
  PresheafOfModules.pushforwardComp (CategoryTheory.CategoryStruct.id S) φ =
    (PresheafOfModules.pushforward φ).isoWhiskerLeft (PresheafOfModules.pushforwardId S) ≪≫
      (PresheafOfModules.pushforward φ).rightUnitor
-- Mathlib.Topology.Order.Lattice
OrderDual.continuousInf : ∀ (L : Type u_1) [inst : TopologicalSpace L] [inst_1 : Max L] [h : ContinuousSup L], ContinuousInf Lᵒᵈ
-- Init.System.IOError
IO.Error.inappropriateType.inj : ∀ {filename : Option String} {osCode : UInt32} {details : String} {filename_1 : Option String} {osCode_1 : UInt32}
  {details_1 : String},
  IO.Error.inappropriateType filename osCode details = IO.Error.inappropriateType filename_1 osCode_1 details_1 →
    filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1
-- Mathlib.Data.Set.Lattice.Image
Set.seq_singleton : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {a : α}, s.seq {a} = (fun f => f a) '' s
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.ae_eq_trim_iff : ∀ {α : Type u_1} {E : Type u_5} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] (hm : m ≤ m₀),
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → (f =ᵐ[μ.trim hm] g ↔ f =ᵐ[μ] g)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.union.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₁_1 : Std.ExtHashSet α), m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtHashSet α), m₂ = m₂_1 → m₁.union m₂ = m₁_1.union m₂_1
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- The type of Compact Hausdorff topological spaces satisfying an additional property `P`.  -/
CompHausLike : (TopCat → Prop) → Type (u + 1)
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- **Alias** of `ProbabilityTheory.nullSingletonClass_gaussianReal`. -/
ProbabilityTheory.noAtoms_gaussianReal : ∀ {μ : ℝ} {v : NNReal}, v ≠ 0 → MeasureTheory.NullSingletonClass (ProbabilityTheory.gaussianReal μ v)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.coe_zero : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ↑0 = 0
-- Mathlib.Algebra.Free
FreeMagma.map_mul' : ∀ {α β : Type u} (f : α → β) (x y : FreeMagma α), f <$> (x * y) = f <$> x * f <$> y
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift_desc_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K L : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
  (α' : CochainComplex.HomComplex.Cochain F L (-1)) (β' : G ⟶ L)
  (eq' :
    CochainComplex.HomComplex.δ (-1) 0 α' =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β'))
  (n n' : ℤ) (hnn' : n + 1 = n'),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f n)
      ((CochainComplex.mappingCone.desc φ α' β' eq').f n) =
    CategoryTheory.CategoryStruct.comp ((↑α).v n n' hnn') (α'.v n' n ⋯) +
      CategoryTheory.CategoryStruct.comp (β.v n n ⋯) (β'.f n)
-- Mathlib.Tactic.CategoryTheory.CheckCompositions
/-- For each composition `f ≫ g` in the goal,
which internally is represented as `CategoryStruct.comp C inst X Y Z f g`,
infer the types of `f` and `g` and check whether their sources and targets agree
with `X`, `Y`, and `Z` at "instances and reducible" transparency,
reporting any discrepancies.

An example:

```
example (j : J) :
    colimit.ι ((F ⋙ G) ⋙ H) j ≫ (preservesColimitIso (G ⋙ H) F).inv =
      H.map (G.map (colimit.ι F j)) := by

  -- We know which lemma we want to use, and it's even a simp lemma, but `rw`
  -- won't let us apply it
  fail_if_success rw [ι_preservesColimitIso_inv]
  fail_if_success rw [ι_preservesColimitIso_inv (G ⋙ H)]
  fail_if_success simp only [ι_preservesColimitIso_inv]

  -- This would work:
  -- erw [ι_preservesColimitIso_inv (G ⋙ H)]

  -- `check_compositions` checks if the two morphisms we're composing are
  -- composed by abusing defeq, and indeed it tells us that we are abusing
  -- definitional associativity of composition of functors here: it prints
  -- the following.

  -- info: In composition
  --   colimit.ι ((F ⋙ G) ⋙ H) j ≫ (preservesColimitIso (G ⋙ H) F).inv
  -- the source of
  --   (preservesColimitIso (G ⋙ H) F).inv
  -- is
  --   colimit (F ⋙ G ⋙ H)
  -- but should be
  --   colimit ((F ⋙ G) ⋙ H)

  check_compositions

  -- In this case, we can "fix" this by reassociating in the goal, but
  -- usually at this point the right thing to do is to back off and
  -- check how we ended up with a bad goal in the first place.
  dsimp only [Functor.assoc]

  -- This would work now, but it is not needed, because simp works as well
  -- rw [ι_preservesColimitIso_inv]

  simp
```
 -/
Mathlib.Tactic.CheckCompositions.tacticCheck_compositions : Lean.ParserDescr
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.shrinkYoneda.{w, v, u}.map f = CategoryTheory.FunctorToTypes.shrinkMap (CategoryTheory.yoneda.map f)
-- Mathlib.Order.Monotone.MonovaryOrder
/-- If `f : ι → α` and `g : ι → β` are monovarying, then `MonovaryOrder f g` is a linear order on
`ι` that makes `f` and `g` simultaneously monotone.
We define `i < j` if `f i < f j`, or if `f i = f j` and `g i < g j`, breaking ties arbitrarily.  -/
MonovaryOrder : {ι : Type u_1} → {α : Type u_3} → {β : Type u_4} → [LinearOrder α] → [LinearOrder β] → (ι → α) → (ι → β) → ι → ι → Prop
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- The composition of morphisms in `SingleFunctors C D A`.  -/
CategoryTheory.SingleFunctors.Hom.comp : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              {F G H : CategoryTheory.SingleFunctors C D A} → F.Hom G → G.Hom H → F.Hom H
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.instIsIsoFunctorFromLeftDerivedZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [CategoryTheory.Limits.PreservesFiniteColimits F], CategoryTheory.IsIso F.fromLeftDerivedZero
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.instRing : {R : Type u} → [inst : CommRing R] → (self : HopfAlgCat R) → Ring self.carrier
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) → aig.RefVec w → ℕ → (curr : ℕ) → curr ≤ w → aig.RefVec curr → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.measurableSet_comap : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {m : MeasurableSpace β},
  MeasurableSet s ↔ ∃ s', MeasurableSet s' ∧ f ⁻¹' s' = s
-- Init.Data.UInt.Lemmas
UInt16.zero_add : ∀ (a : UInt16), 0 + a = a
-- Mathlib.Topology.Constructions
IsOpen.inter_preimage_val_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → (IsOpen (Subtype.val ⁻¹' t) ↔ IsOpen (s ∩ t))
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_succ' : ∀ (n : ℕ),
  Finset.HasAntidiagonal.antidiagonal (n + 1) =
    Finset.cons (n + 1, 0)
      (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
        (Finset.HasAntidiagonal.antidiagonal n))
      ⋯
-- Mathlib.Algebra.Homology.Homotopy
/-- `f j (c.prev j)`.  -/
toPrev : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} → (j : ι) → ((i j : ι) → C.X i ⟶ D.X j) →+ (C.X j ⟶ D.xPrev j)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- An alternate form of the congruence relation on `M × S`, `M` a `CommMonoid` and `S` a
submonoid of `M`, whose quotient is the localization of `M` at `S`.  -/
AddLocalization.r' : {M : Type u_1} → [inst : AddCommMonoid M] → (S : AddSubmonoid M) → AddCon (M × ↥S)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.mul_cancel' : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r₁ r₂ : R} {s t : ↥S},
  r₁ * ↑s /ₒ t * (r₂ /ₒ s) = r₁ * r₂ /ₒ t
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).inv ι =
    CategoryTheory.CategoryStruct.comp S.homologyι (S.isoOpcyclesOfIsColimit hcc).inv
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b c : Bᵒᵖ} (f : a ⟶ b) (g : b ⟶ c)
  (X : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda.obj x).mapComp f g).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop f.unop X).inv
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
/-- Auxiliary definition for `extend.rightHomologyData`.  -/
HomologicalComplex.extend.rightHomologyData.isLimitKernelFork : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') →
                    {i j k : ι} →
                      {i' j' k' : ι'} →
                        (hj' : e.f j = j') →
                          (hi : c.prev j = i) →
                            (hi' : c'.prev j' = i') →
                              (hk : c.next j = k) →
                                (hk' : c'.next j' = k') →
                                  (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) →
                                    (hcocone : CategoryTheory.Limits.IsColimit cocone) →
                                      (cone :
                                          CategoryTheory.Limits.KernelFork
                                            (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯))) →
                                        CategoryTheory.Limits.IsLimit cone →
                                          CategoryTheory.Limits.IsLimit
                                            (HomologicalComplex.extend.rightHomologyData.kernelFork K e hj' hi hi' hk
                                              hk' cocone hcocone cone)
-- Mathlib.Tactic.Basic
/-- Try calling `assumption` on all goals; succeeds if it closes at least one goal.  -/
Mathlib.Tactic.tacticAssumption' : Lean.ParserDescr
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_neg_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => -f' x) =O[l] g ↔ f' =O[l] g
-- Lean.Parser.Term
Lean.Parser.Term.completion : Lean.Parser.TrailingParser
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.toHomotopy : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f₀ f₁ : C(X, Y)} → {P : C(X, Y) → Prop} → f₀.HomotopyWith f₁ P → f₀.Homotopy f₁
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isZero_X_of_isStrictlySupported : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [K.IsStrictlySupported e] (i' : ι'),
  (∀ (i : ι), e.f i ≠ i') → CategoryTheory.Limits.IsZero (K.X i')
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (x : α), Equiv.Perm.toList 1 x = []
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceOfIntLE : Lean.Meta.Simp.DSimproc
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_mul_const_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ),
  ProbabilityTheory.covariance X (fun ω => Y ω * c) μ = ProbabilityTheory.covariance X Y μ * c
-- Mathlib.Analysis.Normed.Group.Basic
abs_norm_sub_norm_le : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), |‖a‖ - ‖b‖| ≤ ‖a - b‖
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.instSmallQuotient : ∀ {R : Type u_3} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
  [Small.{u, u_4} M], Small.{u, u_4} (M ⧸ N)
-- Aesop.Forward.State
/-- Applies a transformation to the data associated with `slot` and `inst`.
If there is no such data, the transformation is applied to `(∅, ∅)`. Returns the
new instantiation map and the result of `f`.  -/
Aesop.InstMap.modify : {α : Type} →
  Aesop.InstMap →
    Aesop.SlotIndex →
      Lean.Expr →
        (Lean.PHashSet Aesop.Match →
            Lean.PHashSet Aesop.Hyp → Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp × α) →
          Lean.MetaM (Aesop.InstMap × α)
-- Batteries.Data.AssocList
Batteries.AssocList.beq.eq_3 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst_1 : BEq β] (key : α) (value : β) (tail : Batteries.AssocList α β),
  Batteries.AssocList.nil.beq (Batteries.AssocList.cons key value tail) = false
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.eq_div_of_mul_eq_left : ∀ {R : Type u} [inst : EuclideanDomain R] {a b c : R}, b ≠ 0 → a * b = c → a = c / b
-- Mathlib.Data.Setoid.Basic
/-- Given a function `f`, lift it to the quotient by its kernel.  -/
Setoid.kerLift : {α : Type u_1} → {β : Type u_2} → (f : α → β) → Quotient (Setoid.ker f) → β
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.nsmul_singleton : ∀ {α : Type u_1} (a : α) (n : ℕ), n • {a} = Multiset.replicate n a
-- Mathlib.Data.Finset.Sum
Finset.toLeft_insert_inr : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (insert (Sum.inr b) u).toLeft = u.toLeft
-- Mathlib.Order.Hom.Set
/-- A strictly monotone surjective function from a linear order is an order isomorphism.  -/
StrictMono.orderIsoOfSurjective : {α : Type u_1} →
  {β : Type u_2} →
    [inst : LinearOrder α] → [inst_1 : Preorder β] → (f : α → β) → StrictMono f → Function.Surjective f → α ≃o β
-- Mathlib.Algebra.Module.ULift
ULift.smul_def : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (s : ULift.{u_1, u} R) (x : M), s • x = s.down • x
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_diagonal : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (d : n → R),
  (Matrix.diagonal d).charpoly = ∏ i, (Polynomial.X - Polynomial.C (d i))
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.skip?_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos.copy.skip? pat = Option.map String.Slice.Pos.copy (pos.skip? pat)
-- Init.Data.SInt.Bitwise
Int8.and_eq_neg_one_iff : ∀ {a b : Int8}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Lean.Data.PersistentArray
Lean.PersistentArray.initShift : USize
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.top_himp : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l} [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.himp Lean.Order.top P = P
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.edist_continuousRestrict : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Finite ↑𝔖] [inst_1 : PseudoMetricSpace β]
  [inst_2 : TopologicalSpace α] {f g : UniformOnFun α β 𝔖} [inst_3 : CompactSpace ↑(⋃₀ 𝔖)]
  (hf : ContinuousOn ((UniformOnFun.toFun 𝔖) f) (⋃₀ 𝔖)) (hg : ContinuousOn ((UniformOnFun.toFun 𝔖) g) (⋃₀ 𝔖)),
  edist { toFun := (⋃₀ 𝔖).domRestrict ((UniformOnFun.toFun 𝔖) f), continuous_toFun := ⋯ }
      { toFun := (⋃₀ 𝔖).domRestrict ((UniformOnFun.toFun 𝔖) g), continuous_toFun := ⋯ } =
    edist f g
-- Std.Do.Triple.Basic
/-- Unexpands Hoare triples to their high-level syntax during pretty printing.
 -/
Std.Do.unexpandTriple : Lean.PrettyPrinter.Unexpander
-- Mathlib.RingTheory.LocalRing.Pullback
RingHom.isLocalHom_pullbackFst : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Semiring T] (f : R →+* T)
  (g : S →+* T) [IsLocalHom g], IsLocalHom (f.pullbackFst g)