mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.nhdsWithin_target_inter : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : Y}, x ∈ e.target → ∀ (s : Set Y), nhdsWithin x (e.target ∩ s) = nhdsWithin x s
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.one_compContinuous : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : One β]
  [inst_3 : TopologicalSpace γ] (f : C(γ, α)), BoundedContinuousFunction.compContinuous 1 f = 1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α), (Set.Iio a)⁻¹ = Set.Ioi a⁻¹
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instRing : {R : Type u_3} → {c₁ c₂ c₃ : R} → [CommRing R] → Ring (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Algebra.Order.Ring.Canonical
CanonicallyOrderedAdd.toZeroLEOneClass : ∀ {R : Type u} [inst : AddZeroClass R] [inst_1 : One R] [inst_2 : LE R] [CanonicallyOrderedAdd R], ZeroLEOneClass R
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Similar to `getPatternFn?`, but operates on expressions that do not contain loose de Bruijn variables.  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.isPatternFnCandidate : Lean.Expr → Lean.Meta.Grind.CollectorM✝ Bool
-- Mathlib.Tactic.Determinant.Bird.Cert
Mathlib.Tactic.Determinant.Cert.mk.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} {subject : Q(«$α»)}
  (result : Mathlib.Tactic.Determinant.CertResult rα subject) (isZero : Bool) (subject_1 : Q(«$α»))
  (result_1 : Mathlib.Tactic.Determinant.CertResult rα subject_1) (isZero_1 : Bool),
  ({ subject := subject, result := result, isZero := isZero } =
      { subject := subject_1, result := result_1, isZero := isZero_1 }) =
    (subject = subject_1 ∧ result ≍ result_1 ∧ isZero = isZero_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, k ∉ t₁ → Std.DTreeMap.Const.get? (t₁ \ t₂) k = none
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_apply_eq_one : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M} {a : α}, s.mulIndicator f a = 1 ↔ a ∈ s → f a = 1
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonAssocSemiring α] [inst_1 : Preorder α]
  [inst_2 : NonAssocSemiring β] [inst_3 : Preorder β] [inst_4 : NonAssocSemiring γ] [inst_5 : Preorder γ] {f : β →+*o γ}
  {g₁ g₂ : α →+*o β}, Function.Injective ⇑f → (f.comp g₁ = f.comp g₂ ↔ g₁ = g₂)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.eq_touchpoint_of_isTangentAt_exsphere : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))}
  {i : Fin (n + 1)} {p : P},
  (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) → p = s.touchpoint signs i
-- Lean.Parser.Extension
Lean.Parser.ParserAttributeHook : Type
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Subarray.drop.eq_1 : ∀ {α : Type u_1} (arr : Subarray α) (i : ℕ),
  arr.drop i =
    {
      internalRepresentation :=
        { array := arr.array, start := min (arr.start + i) arr.stop, stop := arr.stop, start_le_stop := ⋯,
          stop_le_array_size := ⋯ } }
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_eq_one : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M},
  (s.mulIndicator f = fun x => 1) ↔ Disjoint (Function.mulSupport f) s
-- Mathlib.Order.Filter.Pointwise
Filter.pureMonoidHom.eq_1 : ∀ {α : Type u_2} [inst : MulOneClass α],
  Filter.pureMonoidHom = { toFun := Filter.pureMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Order.Concept
Concept.intent_ssubset_intent_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c.intent ⊂ d.intent ↔ d < c
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Any type satisfying `OrderAddMonoidIsoClass` can be cast into `OrderAddMonoidIso`
via `OrderAddMonoidIsoClass.toOrderAddMonoidIso`.  -/
instCoeTCOrderAddMonoidIsoOfOrderIsoClassOfAddEquivClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : AddZeroClass α] →
            [inst_3 : AddZeroClass β] →
              [inst_4 : EquivLike F α β] → [OrderIsoClass F α β] → [AddEquivClass F α β] → CoeTC F (α ≃+o β)
-- Mathlib.Algebra.Tropical.BigOperators
Finset.untrop_sum' : ∀ {R : Type u_1} {S : Type u_2} [inst : LinearOrder R] [inst_1 : OrderTop R] (s : Finset S) (f : S → Tropical R),
  Tropical.untrop (∑ i ∈ s, f i) = s.inf (Tropical.untrop ∘ f)
-- Mathlib.Tactic.NormNum.Core
/-- `norm_num` normalizes numerical expressions in the goal. By default, it supports the operations
`+` `-` `*` `/` `⁻¹` `^` and `%` over types with (at least) an `AddMonoidWithOne` instance, such as
`ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ`. In addition to evaluating numerical expressions, `norm_num` will use `simp`
to simplify the goal. If the goal has the form `A = B`, `A ≠ B`, `A < B` or `A ≤ B`, where `A` and
`B` are numerical expressions, `norm_num` will try to close it. It also has a relatively simple
primality prover (available if you import `Mathlib.Tactic.NormNum.Prime`).

This tactic is extensible. Extensions can allow `norm_num` to evaluate more kinds of expressions, or
to prove more kinds of propositions (such as, primality of natural numbers). See the `@[norm_num]`
attribute for further information on extending `norm_num`.

* `norm_num at l` normalizes at location(s) `l`.
* `norm_num [h1, ...]` adds the arguments `h1, ...` to the `simp` set in addition to the default
  `simp` set. All options for `simp` arguments are supported, in particular `←`, `↑` and `↓`.
* `norm_num only` does not use the default `simp` set for simplification. `norm_num only [h1, ...]`
  uses only the arguments `h1, ...` in addition to the routines tagged `@[norm_num]`.
  `norm_num only` still performs post-processing steps, like `simp only`, use `norm_num1` if you
  exclusively want to normalize numerical expressions.
* `norm_num (config := cfg)` uses `cfg` as configuration for `simp` calls (see the `simp` tactic for
  further details).

Examples:
```lean
example : 43 ≤ 74 + (33 : ℤ) := by norm_num
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num
```
 -/
Mathlib.Tactic.normNum : Lean.ParserDescr
-- Mathlib.Data.Finset.Defs
Finset.PiFinsetCoe.canLift' : ∀ (ι : Type u_4) (α : Type u_5) [_ne : Nonempty α] (s : Finset ι),
  CanLift (↥s → α) (ι → α) (fun f i => f ↑i) fun x => True
-- Mathlib.Algebra.Group.Defs
pow_one : ∀ {M : Type u_2} [inst : Monoid M] (a : M), a ^ 1 = a
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Bundle the action of `C` on `D` as a functor `C ⥤ D ⥤ D`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction : (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] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            CategoryTheory.Functor C (CategoryTheory.Functor D D)
-- Mathlib.RingTheory.Lasker
Submodule.isPrimary_decomposition_pairwise_ne_radical : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {s : Finset (Submodule R M)},
  s.inf id = N →
    (∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary) →
      ∃ t,
        t.inf id = N ∧
          (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
            (↑t).Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) fun J => (J.colon Set.univ).radical)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ → ∀ (f : α → β → Bool), (Std.TreeMap.filter f t₁).Equiv (Std.TreeMap.filter f t₂)
-- Batteries.CodeAction.Attr
Batteries.CodeAction.TacticCodeActions.mk.sizeOf_spec : ∀ (onAnyTactic : Array Batteries.CodeAction.TacticCodeAction)
  (onTactic : Lean.NameMap (Array Batteries.CodeAction.TacticCodeAction)),
  sizeOf { onAnyTactic := onAnyTactic, onTactic := onTactic } = 1 + sizeOf onAnyTactic + sizeOf onTactic
-- Mathlib.Data.Set.Image
Set.exists_subset_range_and_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {p : Set β → Prop}, (∃ s ⊆ Set.range f, p s) ↔ ∃ s, p (f '' s)
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppRight_apply_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι] (m : M) (p : ι →₀ N),
  (TensorProduct.finsuppRight R S M N ι) (m ⊗ₜ[R] p) = p.sum fun i n => fun₀ | i => m ⊗ₜ[R] n
-- Mathlib.Condensed.Discrete.Module
/-- `LightCondMod.LocallyConstant.functor` is left adjoint to the forgetful functor from light condensed
`R`-modules to `R`-modules.
 -/
LightCondMod.LocallyConstant.adjunction : (R : Type u) → [inst : Ring R] → LightCondMod.LocallyConstant.functor R ⊣ LightCondensed.underlying (ModuleCat R)
-- Mathlib.Topology.Separation.Hausdorff
Ultrafilter.lim_eq_iff_le_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [CompactSpace X] {x : X} {F : Ultrafilter X},
  F.lim = x ↔ ↑F ≤ nhds x
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
differentiableWithinAtProp_self_target : ∀ {𝕜 : 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} {E' : Type u_5}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {f : H → E'} {s : Set H} {x : H},
  DifferentiableWithinAtProp I (modelWithCornersSelf 𝕜 E') f s x ↔
    DifferentiableWithinAt 𝕜 (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x)
-- Mathlib.Tactic.Linter.MinImports
/-- The `linter.minImports.increases` regulates whether the `minImports` linter reports the
change in number of imports, when it reports import changes.
Setting this option to `false` helps with test stability.
 -/
Mathlib.Linter.linter.minImports.increases : Lean.Option Bool
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {a : C}
  {z w : (CategoryTheory.FunctorToTypes.prod F G).obj a}, z = w ↔ z.1 = w.1 ∧ z.2 = w.2
-- Mathlib.RingTheory.WittVector.WittPolynomial
xInTermsOfW_vars_subset : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), (xInTermsOfW p ℚ n).vars ⊆ Finset.range (n + 1)
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_triangle : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y}
  {x y z : X ⊕ Y}, f ∈ GromovHausdorff.candidates X Y → f (x, z) ≤ f (x, y) + f (y, z)
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given closed range as an array in ascending order.
 -/
Std.Rio.toArray : {α : Type u} →
  [Std.PRange.Least? α] →
    [inst : LT α] →
      [DecidableLT α] →
        [inst_2 : Std.PRange.UpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxo.IsAlwaysFinite α] → Std.Rio α → Array α
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCancelMonoid : {α : Type u_1} → [AddCancelMonoid α] → AddCancelMonoid (Colex α)
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofNatClamp_of_le : ∀ {n : ℕ}, UInt64.size ≤ n → (UInt64.ofNatClamp n).toNat = UInt64.size - 1
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.evalWhiskerRight_id : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} {η : f ⟶ g}
  {η₁ : f ⟶ CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b)}
  {η₂ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) ⟶
      CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b)},
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv = η₁ →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom η₁ = η₂ →
      CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) = η₂
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.neg_mem_iff : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E}
  [NormOneClass 𝕜], Balanced 𝕜 s → ∀ {x : E}, -x ∈ s ↔ x ∈ s
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.id.eq_1 : ∀ (α : Type u_2) [inst : SupSet α], sSupHom.id α = { toFun := id, map_sSup' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_inv_nnrpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a : A) {x : NNReal},
  x ≠ 0 → autoParam (0 ≤ a) CFC.nnrpow_inv_nnrpow._auto_1 → (a ^ x⁻¹) ^ x = a
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.FinValue.mk : (n : ℕ) → Fin n → Lean.Meta.Sym.FinValue
-- Mathlib.Analysis.Real.Spectrum
_private.Mathlib.Analysis.Real.Spectrum.0.QuasispectrumRestricts.termσₙ : Lean.ParserDescr
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_sum : ∀ {R : Type u} {M : Type v} {ι : Type u_3} [inst : AddCommMonoid R] [inst_1 : AddCommMonoid M] (s : Finset ι)
  (f : ι → TrivSqZeroExt R M), (∑ i ∈ s, f i).snd = ∑ i ∈ s, (f i).snd
-- Mathlib.Order.MinMax
max_lt_max_right_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max a c < max a b ↔ c < b ∧ a < b
-- Init.Data.String.PosRaw
String.Pos.Raw.ne_of_gt : ∀ {i₁ i₂ : String.Pos.Raw}, i₁ < i₂ → i₂ ≠ i₁
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.isFiniteIndex' : ∀ {G : Type u_1} [inst : Group G] (self : FiniteIndexNormalSubgroup G), self.FiniteIndex
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.foldr_eq_foldr_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  {f : α → β → δ → δ} {init : δ},
  Std.DTreeMap.Raw.foldr f init t = Array.foldr (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Raw.Const.toArray t)
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.map_addCommutator : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H₁ H₂ : AddSubgroup G) (f : G →+ G'),
  AddSubgroup.map f ⁅H₁, H₂⁆ = ⁅AddSubgroup.map f H₁, AddSubgroup.map f H₂⁆
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.forM_eq_forM : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : (a : α) → β a → m PUnit.{w + 1}},
  Std.ExtDTreeMap.forM f t = forM t fun a => f a.fst a.snd
-- Mathlib.Order.SupIndep
Finset.SupIndep.product : ∀ {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [inst : Lattice α] [IsModularLattice α] [inst_2 : OrderBot α]
  {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α},
  (s.SupIndep fun i => t.sup fun i' => f (i, i')) →
    (t.SupIndep fun i' => s.sup fun i => f (i, i')) → (s ×ˢ t).SupIndep f
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
/-- **Alias** of `MonoidHom.coe_finsetProd`. -/
MonoidHom.coe_finset_prod : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : CommMonoid N] (f : ι → M →* N)
  (s : Finset ι), ⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_map : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] [Std.LawfulEqOrd α] {f : α → β → γ} {k : α},
  t.WF →
    Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.map f t) k =
      Option.map (f k) (Std.DTreeMap.Internal.Impl.Const.get? t k)
-- Mathlib.Topology.ContinuousOn
ContinuousOn.preimage_mem_nhdsSetWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s → ∀ {t u t' : Set β}, u ∈ nhdsSetWithin t t' → f ⁻¹' u ∈ nhdsSetWithin (s ∩ f ⁻¹' t) (s ∩ f ⁻¹' t')
-- Lean.Meta.Tactic.Backtrack
/-- Pretty print a list of goals.
 -/
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.ppMVarIds : List Lean.MVarId → Lean.MetaM (List Std.Format)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.pairing_I : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore), h.pairing.I = h.I
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.homIsOver_of_isOverTower : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (S S' : C)
  [inst_1 : CategoryTheory.OverClass X S] [inst_2 : CategoryTheory.OverClass X S']
  [inst_3 : CategoryTheory.OverClass Y S] [inst_4 : CategoryTheory.OverClass Y S']
  [inst_5 : CategoryTheory.OverClass S S'] [CategoryTheory.IsOverTower X S S'] [CategoryTheory.IsOverTower Y S S']
  [CategoryTheory.HomIsOver f S], CategoryTheory.HomIsOver f S'
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.D₁_totalShift₁XIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁'),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁)
      (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow •
      CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')
-- Init.Data.Int.Order
Int.neg_add_le_of_le_add : ∀ {a b c : ℤ}, a ≤ b + c → -b + a ≤ c
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.ne_top : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m)
  (q :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace),
  AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q ≠ ⊤
-- Mathlib.Analysis.Calculus.MeanValue
constant_of_derivWithin_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ},
  DifferentiableOn ℝ f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, derivWithin f (Set.Icc a b) x = 0) → ∀ x ∈ Set.Icc a b, f x = f a
-- Mathlib.Algebra.Lie.DirectSum
/-- The projection map onto one component, as a morphism of Lie modules.  -/
DirectSum.lieModuleComponent : (R : Type u) →
  (ι : Type v) →
    [inst : CommRing R] →
      (L : Type w₁) →
        (M : ι → Type w) →
          [inst_1 : LieRing L] →
            [inst_2 : (i : ι) → AddCommGroup (M i)] →
              [inst_3 : (i : ι) → Module R (M i)] →
                [inst_4 : (i : ι) → LieRingModule L (M i)] → (j : ι) → (DirectSum ι fun i => M i) →ₗ⁅R,L⁆ M j
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.mk_eq_eval₂ : ∀ {A : Type u_3} {σ : Type u_4} [inst : CommRing A] (I : Ideal (MvPolynomial σ A)),
  (↑↑(Ideal.Quotient.mk I)).toFun =
    MvPolynomial.eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) fun d => (Ideal.Quotient.mk I) (MvPolynomial.X d)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite : {M N : ProfiniteAddGrp.{u}} → CoeFun (M ⟶ N) fun x => ↑M.toProfinite.toTop → ↑N.toProfinite.toTop
-- Init.Data.UInt.Lemmas
UInt8.lt_of_le_of_ne : ∀ {a b : UInt8}, a ≤ b → a ≠ b → a < b
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The index of relations to `ofFinitePresentation`.  -/
Algebra.Presentation.ofFinitePresentationRels : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [Algebra.FinitePresentation R S] → ℕ
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.mk_smul_indicatorConstLp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : M) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (b : E),
  DomMulAct.mk c • MeasureTheory.indicatorConstLp p hs hμs b = MeasureTheory.indicatorConstLp p ⋯ ⋯ b
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.proofWidgetsJsxAttrVal.quot : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_div_leOnePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] (a : α), a⁺ᵐ / a⁻ᵐ = a
-- Mathlib.Data.Finmap
Finmap.erase_union_singleton : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (s : Finmap β),
  Finmap.lookup a s = some b → Finmap.erase a s ∪ Finmap.singleton a b = s
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Turn a morphism in `AddSemigrp` back into an `AddHom`.  -/
AddSemigrp.Hom.hom : {X Y : AddSemigrp} → X.Hom Y → ↑X →ₙ+ ↑Y
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Two morphisms out of a colimit are equal if their compositions with
each cocone morphism are equal.  -/
CategoryTheory.Limits.IsColimit.hom_ext : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) {W : C}
  {f f' : t.pt ⟶ W},
  (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) f = CategoryTheory.CategoryStruct.comp (t.ι.app j) f') →
    f = f'
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.coe_comp_orderHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β), ↑(g.comp f) = (↑g).comp ↑f
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.zero : {α : Type} → Std.CloseableChannel.Zero✝ α → Std.CloseableChannel.Flavors α
-- Lean.Meta.MkIffOfInductiveProp
/-- `mkAndList [x1, x2, ...]` is defined as `x1 ∧ (x2 ∧ ...)`, or `True` if the list is empty.  -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.mkAndList : List Lean.Expr → Lean.Expr
-- Init.Data.Int.DivMod.Lemmas
Int.zero_tmod : ∀ (b : ℤ), Int.tmod 0 b = 0
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.sigmaProdDistrib_apply : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] {ι : Type u_7} {X : ι → Type u_8}
  [inst_1 : (i : ι) → TopologicalSpace (X i)] (a : ((i : ι) × X i) × Y),
  Homeomorph.sigmaProdDistrib a = ⟨a.1.fst, (a.1.snd, a.2)⟩
-- Mathlib.Algebra.Order.Field.Basic
inv_le_inv_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (a⁻¹ ≤ b⁻¹ ↔ b ≤ a)