mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Search.Expansion.Norm
Aesop.NormM.instInhabitedState.default : Aesop.NormM.State
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.focusableGoals : Aesop.Script.StepTree → Std.HashMap Lean.MVarId ℕ
-- Mathlib.Algebra.Group.Action.Sum
Sum.instIsCentralScalar : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β] [inst_2 : SMul Mᵐᵒᵖ α]
  [inst_3 : SMul Mᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β], IsCentralScalar M (α ⊕ β)
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.isClosed_right_of_isClosed_union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → IsClosed (s ∪ t) → IsClosed t
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.hasForgetToModule : {R : Type u} → [inst : CommRing R] → CategoryTheory.HasForget₂ (QuadraticModuleCat R) (ModuleCat R)
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationData.mk.sizeOf_spec : ∀ (name : Lean.Name) (userName : String) (html : ProofWidgets.Html),
  sizeOf { name := name, userName := userName, html := html } = 1 + sizeOf name + sizeOf userName + sizeOf html
-- Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
Preorder.measurable_frestrictLe₂ : ∀ {α : Type u_1} [inst : Preorder α] {X : α → Type u_2} [inst_1 : (a : α) → MeasurableSpace (X a)]
  [inst_2 : LocallyFiniteOrderBot α] {a b : α} (hab : a ≤ b), Measurable (Preorder.frestrictLe₂ hab)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_piecewise : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    ∀ (f g : α → ENNReal) [inst : (j : α) → Decidable (j ∈ s)],
      ∫⁻ (a : α), s.piecewise f g a ∂μ = ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.equivMvPolynomial_C_C : ∀ {R : Type u_1} [inst : CommSemiring R] {a : R},
  (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C (Polynomial.C a)) = MvPolynomial.C a
-- Mathlib.Order.Bounded
Set.unbounded_lt_inter_le : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 < x2) (s ∩ {b | a ≤ b}) ↔ Set.Unbounded (fun x1 x2 => x1 < x2) s
-- Mathlib.Order.RelIso.Basic
RelEmbedding.coe_mk : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : α ↪ β}
  {h : ∀ {a b : α}, s (f a) (f b) ↔ r a b}, ⇑{ toEmbedding := f, map_rel_iff' := h } = ⇑f
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rio.toList_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_5 : Std.Rxo.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rio α}, r.iter.toList = r.toList
-- Lean.Meta.Basic
/-- Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
 -/
Lean.Meta.Cache : Type
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.ext_iff : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {f f' : M [⋀^ι]→ₗ[R] N},
  f = f' ↔ ∀ (x : ι → M), f x = f' x
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- This is (isomorphic to) the base change of the cotangent complex to `A`, but
the domain and codomains of this are more manageable.  -/
KaehlerDifferential.cotangentComplexBaseChange : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (P : Type u_2) →
          (A : Type u_3) →
            [inst_2 : CommRing P] →
              [inst_3 : CommRing A] →
                [inst_4 : Algebra P S] →
                  [inst_5 : Algebra P A] →
                    [inst_6 : Algebra R P] →
                      [inst_7 : Algebra S A] →
                        [IsScalarTower P S A] →
                          TensorProduct P A ↥(RingHom.ker (algebraMap P S)) →ₗ[A] TensorProduct P A Ω[P⁄R]
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_mul_const' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a : E → 𝔸},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 a s x →
      ∀ (b : 𝔸), fderivWithin 𝕜 (fun y => a y * b) s x = MulOpposite.op b • fderivWithin 𝕜 a s x
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
/-- Build an isomorphism in the category `HopfAlgCat R` from a
`BialgEquiv`.  -/
BialgEquiv.toHopfAlgIso : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : Ring X] →
        [inst_2 : Ring Y] →
          [inst_3 : HopfAlgebra R X] →
            [inst_4 : HopfAlgebra R Y] → (X ≃ₐc[R] Y) → (HopfAlgCat.of R X ≅ HopfAlgCat.of R Y)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- Let `T / S / R` be a tower of algebras, `T` is non-trivial and is a torsion free `S`-module,
then if `T` is an integral `R`-algebra, then `S` is an integral `R`-algebra.  -/
Algebra.IsIntegral.tower_bot : ∀ {R : Type u_1} {S : Type u_4} (T : Type u_5) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [IsDomain S] [inst_4 : Algebra R S] [inst_5 : Algebra R T] [inst_6 : Algebra S T] [Module.IsTorsionFree S T]
  [Nontrivial T] [IsScalarTower R S T] [h : Algebra.IsIntegral R T], Algebra.IsIntegral R S
-- Mathlib.Algebra.BigOperators.Fin
finPiFinEquiv_single : ∀ {m : ℕ} {n : Fin m → ℕ} [inst : ∀ (i : Fin m), NeZero (n i)] (i : Fin m) (j : Fin (n i)),
  ↑(finPiFinEquiv (Pi.single i j)) = ↑j * ∏ j, n (Fin.castLE ⋯ j)
-- Mathlib.GroupTheory.Perm.Option
Equiv.Perm.decomposeOption_symm_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (i : Option α × Equiv.Perm α),
  Equiv.Perm.decomposeOption.symm i = Equiv.swap none i.1 * Equiv.optionCongr i.2
-- Init.Data.Nat.Div.Basic
Nat.add_mul_mod_self_right : ∀ (x y z : ℕ), (x + y * z) % z = x % z
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : Std.Internal.List.containsKey (Std.Internal.List.minKey! l) l = true},
      Std.Internal.List.getKey (Std.Internal.List.minKey! l) l he = Std.Internal.List.minKey! l
-- Init.Data.Float.Model.Unpacked.Operations.Sign
/-- Returns the given float with positive sign.  -/
Float.Model.UnpackedFloat.abs : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A submagma of a cancellative magma inherits cancellation.  -/
MulMemClass.isCancelMul : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] [IsCancelMul M] (S : A),
  IsCancelMul ↥S
-- Lean.Elab.Syntax
Lean.Elab.Command.elabDeclareSyntaxCat : Lean.Elab.Command.CommandElab
-- Init.Data.Array.Extract
Array.getElem?_extract_of_succ : ∀ {α : Type u_1} {as : Array α} {j : ℕ}, (as.extract 0 (j + 1))[j]? = as[j]?
-- Init.Data.Nat.Fold
Nat.foldRev_add : ∀ {α : Type u_1} {n m : ℕ} (f : (i : ℕ) → i < n + m → α → α) (init : α),
  (n + m).foldRev f init = n.foldRev (fun i h => f i ⋯) (m.foldRev (fun i h => f (n + i) ⋯) init)
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_lcm_of_dvd_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ lcm b c
-- Mathlib.LinearAlgebra.Determinant
LinearMap.detAux_comp : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] (b : Trunc (Module.Basis ι A M)) (f g : M →ₗ[A] M),
  (LinearMap.detAux b) (f ∘ₗ g) = (LinearMap.detAux b) f * (LinearMap.detAux b) g
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.minD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {fallback : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minD fallback = t₂.minD fallback
-- Mathlib.NumberTheory.LSeries.Convergence
LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable : ∀ {f : ℕ → ℂ} {x : ℝ}, (∀ (y : ℝ), x < y → LSeriesSummable f ↑y) → LSeries.abscissaOfAbsConv f ≤ ↑x
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.instBEqPolyCnstr.beq.match_1.eq_2 : ∀ (motive : Nat.Internal.Linear.PolyCnstr → Nat.Internal.Linear.PolyCnstr → Sort u_1)
  (x x_1 : Nat.Internal.Linear.PolyCnstr)
  (h_1 :
    (a : Bool) →
      (a_1 a_2 : Nat.Internal.Linear.Poly) →
        (b : Bool) →
          (b_1 b_2 : Nat.Internal.Linear.Poly) →
            motive { eq := a, lhs := a_1, rhs := a_2 } { eq := b, lhs := b_1, rhs := b_2 })
  (h_2 : (x x_2 : Nat.Internal.Linear.PolyCnstr) → motive x x_2),
  (∀ (a : Bool) (a_1 a_2 : Nat.Internal.Linear.Poly) (b : Bool) (b_1 b_2 : Nat.Internal.Linear.Poly),
      x = { eq := a, lhs := a_1, rhs := a_2 } → x_1 = { eq := b, lhs := b_1, rhs := b_2 } → False) →
    (match x, x_1 with
      | { eq := a, lhs := a_1, rhs := a_2 }, { eq := b, lhs := b_1, rhs := b_2 } => h_1 a a_1 a_2 b b_1 b_2
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Init.Data.List.Basic
/-- Checks whether two lists have the same length and their elements are pairwise `BEq`. Normally used
via the `==` operator.
 -/
List.beq : {α : Type u} → [BEq α] → List α → List α → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- A `NormalEpiCategory` category with finite coproducts and cokernels has all coequalizers.  -/
CategoryTheory.NormalEpiCategory.hasCoequalizers : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C]
  [CategoryTheory.IsNormalEpiCategory C], CategoryTheory.Limits.HasCoequalizers C
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_val_Ico : ∀ {n : ℕ} (a b : Fin n), Finset.image Fin.val (Finset.Ico a b) = Finset.Ico ↑a ↑b
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_ofCoeff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (x : M →₀ R), (MonoidAlgebra.ofCoeff x).coeff = x
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.add_liftRight_neg : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] {f : M →+ N} {g : M → AddUnits N}
  (h : ∀ (x : M), ↑(g x) = f x) (x : M), f x + ↑(-(AddUnits.liftRight f g h) x) = 0
-- Mathlib.Data.Multiset.AddSub
Multiset.Nodup.erase : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) {l : Multiset α}, l.Nodup → (l.erase a).Nodup
-- Init.Data.List.Basic
List.length_concat : ∀ {α : Type u} {as : List α} {a : α}, (as.concat a).length = as.length + 1
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Characterization of differentiable functions into a vector bundle.
Version at a point within a set  -/
mdifferentiableWithinAt_totalSpace : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  (f : M → Bundle.TotalSpace F E) {s : Set M} {x₀ : M},
  MDiffAt[s] f x₀ ↔
    (MDiffAt[s] fun x => (f x).proj) x₀ ∧ (MDiffAt[s] fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Submodule.baseChange_injective : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [Module.FaithfullyFlat R A] [inst_4 : AddCommGroup M] [inst_5 : Module R M] {p q : Submodule R M},
  Submodule.baseChange A p = Submodule.baseChange A q → p = q
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.mk.injEq : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (toRingHom : A →+* B)
  (map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toRingHom x ∈ ℬ i) (toRingHom_1 : A →+* B)
  (map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toRingHom_1 x ∈ ℬ i),
  ({ toRingHom := toRingHom, map_mem := map_mem } = { toRingHom := toRingHom_1, map_mem := map_mem_1 }) =
    (toRingHom = toRingHom_1)
-- Init.Data.Array.Lemmas
Array.foldl_eq_foldlM : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {b : β} {xs : Array α} {start stop : ℕ},
  Array.foldl f b xs start stop = (Array.foldlM (fun x1 x2 => pure (f x1 x2)) b xs start stop).run
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.notMem_closure_sdiff_of_mem : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → e ∈ I → e ∉ M.closure (I \ {e})
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Decomp.0.SimpleGraph.Walk.length.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2)
  (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_1 : V) → (h : G.Adj u v_1) → (q : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h q)),
  (match u, SimpleGraph.Walk.nil with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h q => h_2 v v_1 h q) =
    h_1 ()
-- Mathlib.Data.Part
Part.noneDecidable : {α : Type u_1} → Decidable Part.none.Dom
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C) {Y Z : C} (f : Y ⟶ Z),
  F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f))
        (CategoryTheory.Functor.LaxMonoidal.μ F X Z))
-- Lean.Elab.InfoTree.Types
/-- Indicates that a piece of syntax was elaborated as documentation. This info is used for ordinary
documentation constructs, such as paragraphs, list items, and links. It can be used to determine
that a given piece of documentation syntax in fact has been elaborated.
 -/
Lean.Elab.DocInfo : Type
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₂₃_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₁) (k : C₃) {X Y : C₂}
  (f : X ⟶ Y), ((F.flip₂₃.obj G).obj k).map f = ((F.obj G).map f).app k
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j) {Z : C}
  (h_1 : (K.flip.total c).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c i₁ i₂ j h)
      (CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).inv.f j) h_1) =
    CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) h_1
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Intermediate stage of assembling the unit.  -/
CategoryTheory.OverPresheafAux.unitAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (η : CategoryTheory.Over A) →
        ((CategoryTheory.OverPresheafAux.restrictedYoneda A).comp
                (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A)).obj
            η ≅
          η
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addFactStep.goEq : Lean.Expr → ℕ → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Bool → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.Partition.Basic
Partition.eq_of_not_disjoint : ∀ {α : Type u_1} {s x y : α} [inst : CompleteLattice α] {P : Partition s}, x ∈ P → y ∈ P → ¬Disjoint x y → x = y
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- Reinterpret an isomorphism over an object `S` into an isomorphism in the category over `S`.  -/
CategoryTheory.Iso.asOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (S : C) →
        [inst_1 : CategoryTheory.OverClass X S] →
          [inst_2 : CategoryTheory.OverClass Y S] →
            (e : X ≅ Y) →
              [CategoryTheory.HomIsOver e.hom S] →
                CategoryTheory.OverClass.asOver X S ≅ CategoryTheory.OverClass.asOver Y S
-- Mathlib.Order.CompleteLattice.Finset
/-- Supremum of `s i`, `i : ι`, is equal to the supremum over `t : Finset ι` of suprema
`⨆ i ∈ t, s i`. This version assumes `ι` is a `Type*`. See `iSup_eq_iSup_finset'` for a version
that works for `ι : Sort*`.  -/
iSup_eq_iSup_finset : ∀ {α : Type u_2} {ι : Type u_5} [inst : CompleteLattice α] (s : ι → α), ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i
-- Mathlib.Analysis.Normed.Group.Pointwise
neg_sphere : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), -Metric.sphere x δ = Metric.sphere (-x) δ
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.instDecidableLESigma_std : {α : Type u} → {β : α → Type v} → [inst : Ord α] → DecidableLE ((a : α) × β a)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsComp'App_inv_naturality : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M N : ModuleCat R₃} (φ : M ⟶ N),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ))
      (ModuleCat.restrictScalarsComp'App f g gf hgf N).inv =
    CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf M).inv
      ((ModuleCat.restrictScalars gf).map φ)
-- Init.SimpLemmas
dite_false : ∀ {α : Sort u} {t : False → α} {e : ¬False → α}, dite False t e = e not_false
-- Mathlib.Analysis.Convex.Basic
convex_pi : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] {ι : Type u_5} {E : ι → Type u_6}
  [inst_2 : (i : ι) → AddCommMonoid (E i)] [inst_3 : (i : ι) → SMul 𝕜 (E i)] {s : Set ι} {t : (i : ι) → Set (E i)},
  (∀ ⦃i : ι⦄, i ∈ s → Convex 𝕜 (t i)) → Convex 𝕜 (s.pi t)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (left : S.LeftHomologyData) →
          (right : S.RightHomologyData) →
            (iso : left.H ≅ right.H) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp left.π (CategoryTheory.CategoryStruct.comp iso.hom right.ι) =
                    CategoryTheory.CategoryStruct.comp left.i right.p)
                  CategoryTheory.ShortComplex.HomologyData.comm._autoParam →
                S.HomologyData
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.symm_apply_eq : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α} {y : β},
  x ∈ e.source → y ∈ e.target → (↑e.symm y = x ↔ y = ↑e x)
-- Lean.Meta.Tactic.Grind.PropagateInj
_private.Lean.Meta.Tactic.Grind.PropagateInj.0.Lean.Meta.Grind.initInjFn : List Lean.Level → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Init.Data.Range.Polymorphic.PRange
/-- For every elements `init`, there exists a chain of successors that
  results in an element that has no successors.
   -/
Std.Rxi.IsAlwaysFinite.finite : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} [self : Std.Rxi.IsAlwaysFinite α] (init : α),
  ∃ n, Std.PRange.succMany? n init = none
-- Std.Data.DHashMap.RawLemmas
/-- Variant of `get!_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Raw.Const.get!_map' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited γ] {f : α → β → γ} {k : α} (h : m.WF),
  Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.map f m) k =
    (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Raw.Const.get? m k) ⋯).get!
-- Mathlib.Analysis.Complex.Hadamard
/-- The supremum of the norm of `scale f l u` on the line `z.re = 1` is the same as
the supremum of `f` on the line `z.re = u`.  -/
Complex.HadamardThreeLines.sSupNormIm_scale_right : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) {l u : ℝ},
  l < u →
    Complex.HadamardThreeLines.sSupNormIm (Complex.HadamardThreeLines.scale f l u) 1 =
      Complex.HadamardThreeLines.sSupNormIm f u
-- Init.Meta.Defs
Lean.Meta.Omega.OmegaConfig.mk.inj : ∀
  {splitDisjunctions splitNatSub splitNatAbs splitMinMax splitDisjunctions_1 splitNatSub_1 splitNatAbs_1 splitMinMax_1 :
    Bool},
  { splitDisjunctions := splitDisjunctions, splitNatSub := splitNatSub, splitNatAbs := splitNatAbs,
        splitMinMax := splitMinMax } =
      { splitDisjunctions := splitDisjunctions_1, splitNatSub := splitNatSub_1, splitNatAbs := splitNatAbs_1,
        splitMinMax := splitMinMax_1 } →
    splitDisjunctions = splitDisjunctions_1 ∧
      splitNatSub = splitNatSub_1 ∧ splitNatAbs = splitNatAbs_1 ∧ splitMinMax = splitMinMax_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_erase!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k fallback : α}, (Std.DTreeMap.Internal.Impl.erase! k t).getKeyD k fallback = fallback
-- Mathlib.GroupTheory.Index
/-- A subgroup has index dividing 2 if and only if there exists `a` such that for all `b`, at least
one of `b * a` and `b` belongs to `H`.  -/
Subgroup.index_dvd_two_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index ∣ 2 ↔ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H
-- Mathlib.Topology.Compactness.SigmaCompact
isSigmaCompact_iff_sigmaCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSigmaCompact s ↔ SigmaCompactSpace ↑s
-- Mathlib.Algebra.Order.Archimedean.Class
/-- The archimedean class of a given element.  -/
MulArchimedeanClass.mk : {M : Type u_1} →
  [inst : CommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → M → MulArchimedeanClass M
-- Mathlib.Order.Interval.Set.Image
Antitone.mapsTo_Icc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  Antitone f → Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
-- Mathlib.Topology.Bases
/-- In a second countable topological space, any topological basis contains a countable subset
which is also a topological basis.  -/
TopologicalSpace.IsTopologicalBasis.exists_countable : ∀ {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {t_1 : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis t_1 → ∃ s ⊆ t_1, s.Countable ∧ TopologicalSpace.IsTopologicalBasis s
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity between indexed sets of vertices v₁ and v₂.
Use `open scoped Similar` to access the `v₁ ∼ v₂` notation.  -/
Similar.«term_∼_» : Lean.TrailingParserDescr