mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Coinductive
Lean.Elab.Command.CoinductiveElabData.mk.injEq : ∀ (declId : Lean.Syntax) (declName : Lean.Name) (ref : Lean.Syntax) (modifiers : Lean.Elab.Modifiers)
  (ctorSyntax : Array Lean.Syntax) (isGreatest : Bool) (declId_1 : Lean.Syntax) (declName_1 : Lean.Name)
  (ref_1 : Lean.Syntax) (modifiers_1 : Lean.Elab.Modifiers) (ctorSyntax_1 : Array Lean.Syntax) (isGreatest_1 : Bool),
  ({ declId := declId, declName := declName, ref := ref, modifiers := modifiers, ctorSyntax := ctorSyntax,
        isGreatest := isGreatest } =
      { declId := declId_1, declName := declName_1, ref := ref_1, modifiers := modifiers_1, ctorSyntax := ctorSyntax_1,
        isGreatest := isGreatest_1 }) =
    (declId = declId_1 ∧
      declName = declName_1 ∧
        ref = ref_1 ∧ modifiers = modifiers_1 ∧ ctorSyntax = ctorSyntax_1 ∧ isGreatest = isGreatest_1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alter!.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : Option β → Option β)
  (t : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.alter! k f t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      match f none with
      | none => Std.DTreeMap.Internal.Impl.leaf
      | some v => Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r' =>
      match compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.balance! k' v' (Std.DTreeMap.Internal.Impl.Const.alter! k f l') r'
      | Ordering.gt => Std.DTreeMap.Internal.Impl.balance! k' v' l' (Std.DTreeMap.Internal.Impl.Const.alter! k f r')
      | Ordering.eq =>
        match f (some v') with
        | none => l'.glue! r'
        | some v => Std.DTreeMap.Internal.Impl.inner sz k v l' r'
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.associator_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H I : CategoryTheory.Grp C),
  (CategoryTheory.MonoidalCategoryStruct.associator G H I).hom.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).hom
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The first factor of `p` in the universal coprime factorization ring of `p`.  -/
Polynomial.UniversalCoprimeFactorizationRing.factor₁ : {R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) →
            Polynomial.MonicDegreeEq (Polynomial.UniversalCoprimeFactorizationRing m k hn p) m
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `UniqueProds G` says that for any two nonempty `Finset`s `A` and `B` in `G`, `A × B`
contains a unique pair with the `UniqueMul` property. Strojnowski showed that if `G` is
a group, then we only need to check this when `A = B`.
Here we generalize the result to cancellative semigroups.
Non-cancellative counterexample: the AddMonoid `{0,1}` with 1+1=1.  -/
UniqueProds.of_same : ∀ {G : Type u_1} [inst : Semigroup G] [IsCancelMul G],
  (∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2) → UniqueProds G
-- Qq.Typ
/-- Check that the claim `$u =QL $v` is actually true; that the two levels are defeq.  -/
Qq.QuotedLevelDefEq.check : {lhs rhs : Lean.Level} → lhs =QL rhs → Lean.MetaM Unit
-- Mathlib.Algebra.Ring.Defs
IsDomain.mk : ∀ {α : Type u} [inst : Semiring α] [toIsCancelMulZero : IsCancelMulZero α] [toNontrivial : Nontrivial α], IsDomain α
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.trailingDegree = p.support.min
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.charmatrix = (Matrix.scalar n) Polynomial.X - Polynomial.C.mapMatrix M
-- Mathlib.CategoryTheory.Distributive.Cartesian
/-- To show a category is Cartesian distributive it is enough to show it is left distributive.
The right distributivity is inferred from symmetry of the Cartesian monoidal structure.  -/
CategoryTheory.IsCartesianDistributive.of_isMonoidalLeftDistrib : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsMonoidalLeftDistrib C],
  CategoryTheory.IsCartesianDistributive C
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isoFinYonedaComponents_hom : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : Profinite) [inst_1 : Finite ↑X.toTop],
  (Condensed.isoFinYonedaComponents F X).hom =
    TypeCat.ofHom fun y x =>
      (CategoryTheory.ConcreteCategory.hom (F.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) x).op)) y
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddCommGrpCat.FilteredColimits.colimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommGrpCat),
  AddCommGrpCat.FilteredColimits.colimit F = AddCommGrpCat.of ↑(AddCommGrpCat.FilteredColimits.G F)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.quotientEquiv_mk : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) (p : P.Ring),
  P.quotientEquiv ((Ideal.Quotient.mk P.ker) p) = (algebraMap P.Ring S) p
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Nodup.cons : ∀ {α : Type u_1} {s : Multiset α} {a : α}, a ∉ s → s.Nodup → (a ::ₘ s).Nodup
-- Mathlib.CategoryTheory.GradedObject.Single
/-- The canonical isomorphism `(single j).obj X i ≅ X` when `i = j`.  -/
CategoryTheory.GradedObject.singleObjApplyIsoOfEq : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Limits.HasInitial C] →
        [inst_2 : DecidableEq J] →
          (j : J) → (X : C) → (i : J) → i = j → ((CategoryTheory.GradedObject.single j).obj X i ≅ X)
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_le_length_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys l₂ →
      (∀ (a : α), Std.Internal.List.containsKey a l₁ = true → Std.Internal.List.containsKey a l₂ = true) →
        l₁.length ≤ l₂.length
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.factorThruCoimage f)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.factorThruCoimage (F.map f)) h
-- Mathlib.CategoryTheory.Subfunctor.OfSection
CategoryTheory.Subfunctor.ofSection_image : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : Cᵒᵖ}
  (x : F.obj X) {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ F'),
  (CategoryTheory.Subfunctor.ofSection x).image f =
    CategoryTheory.Subfunctor.ofSection ((CategoryTheory.ConcreteCategory.hom (f.app X)) x)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_functions_apply₁ : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {f : L.Functions 1} {t : L.Term α}
  {v : α → M},
  FirstOrder.Language.Term.realize v (f.apply₁ t) =
    FirstOrder.Language.Structure.funMap f ![FirstOrder.Language.Term.realize v t]
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioc_Ici_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.Ici a)) (Filter.principal (Set.Ioi a))
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_rangeRestrict : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), f.rangeRestrict.range = ⊤
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.iInf_toSubfield : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Sort u_3}
  (S : ι → IntermediateField F E), (iInf S).toSubfield = ⨅ i, (S i).toSubfield
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_univ : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.zeroLocus Set.univ = ∅
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_linearMap_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective fun x => ↑x
-- Mathlib.RingTheory.Frobenius
isConj_arithFrobAt : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] (Q : Ideal S) [inst_6 : Finite G]
  [inst_7 : Algebra.IsInvariant R S G] [inst_8 : Q.IsPrime] [inst_9 : Finite (S ⧸ Q)] (Q' : Ideal S)
  [inst_10 : Q'.IsPrime] [inst_11 : Finite (S ⧸ Q')],
  Ideal.under R Q = Ideal.under R Q' → IsConj (arithFrobAt R G Q) (arithFrobAt R G Q')
-- Lean.Elab.InfoTree.Types
/-- Whether `expr` should always be displayed in the language server, e.g. in hovers.  -/
Lean.Elab.TermInfo.isDisplayableTerm : Lean.Elab.TermInfo → Bool
-- Init.Data.Array.Extract
Array.size_extract_le' : ∀ {α : Type u_1} {as : Array α} {i j : ℕ}, (as.extract i j).size ≤ as.size - i
-- Init.Data.SInt.Bitwise
Int64.and_assoc : ∀ (a b c : Int64), a &&& b &&& c = a &&& (b &&& c)
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.instIsAffineHomOfIsIsoScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f], AlgebraicGeometry.IsAffineHom f
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C),
  (CategoryTheory.FunctorToTypes.binaryCoproductCocone F G).pt.obj a = (F.obj a ⊕ G.obj a)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.mem_trivialFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C] [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [HomotopicalAlgebra.Fibration f] [HomotopicalAlgebra.WeakEquivalence f], HomotopicalAlgebra.trivialFibrations C f
-- Mathlib.Data.PNat.Basic
PNat.ofNat_le_ofNat : ∀ {m n : ℕ} [inst : NeZero m] [inst_1 : NeZero n], OfNat.ofNat m ≤ OfNat.ofNat n ↔ OfNat.ofNat m ≤ OfNat.ofNat n
-- Init.GetElem
/-- Lawful `GetElem?` instances (which extend `GetElem`) are those for which the potentially-failing
`GetElem?.getElem?` and `GetElem?.getElem!` operators succeed when the validity predicate is
satisfied, and fail when it is not.
 -/
LawfulGetElem : (cont : Type u) →
  (idx : Type v) →
    (elem : outParam (Type w)) → (dom : outParam (cont → idx → Prop)) → [ge : GetElem? cont idx elem dom] → Prop
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.lift_comp_one_right_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.MonObj B] (f : A ⟶ B) (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
  {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g CategoryTheory.MonObj.one))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp f h
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback v : β}, (t.insert k v).getD k fallback = v
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The low level tape corresponding to the given tape over alphabet `Γ`.  -/
Turing.TM1to1.trTape : {Γ : Type u_1} →
  {n : ℕ} →
    {enc : Γ → List.Vector Bool n} →
      [inst : Inhabited Γ] → enc default = List.Vector.replicate n false → Turing.Tape Γ → Turing.Tape Bool
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.limitToAlgEquiv.congr_simp : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g g_1 : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop),
  g = g_1 → InfiniteGalois.limitToAlgEquiv g = InfiniteGalois.limitToAlgEquiv g_1
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.π.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m m_1 : U ⟶ X) (e_m : m = m_1)
  [inst_2 : CategoryTheory.Mono m], h.π m = h.π m_1
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.base_subset_complex`. -/
Topology.CWComplex.base_subset_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D], D ⊆ C
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- Given a finite set `s` of indices, a cylinder is the preimage of a set `S` of `∀ i : s, α i` by
the projection from `∀ i, α i` to `∀ i : s, α i`.
`measurableCylinders` is the set of all cylinders with measurable base `S`.  -/
MeasureTheory.measurableCylinders : {ι : Type u_2} → (α : ι → Type u_1) → [(i : ι) → MeasurableSpace (α i)] → Set (Set ((i : ι) → α i))
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorKer_coe : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f : N →ₗ[R] P) (x : TensorProduct R M ↥f.ker),
  ↑((LinearMap.tensorKer S M f) x) = (LinearMap.lTensor M f.ker.subtype) x
-- Init.Data.Nat.Div.Lemmas
Nat.mul_div_self_eq_mod_sub_self : ∀ {x k : ℕ}, k * (x / k) = x - x % k
-- Mathlib.Analysis.Complex.Norm
Complex.norm_two : ‖2‖ = 2
-- Batteries.Data.Fin.Basic
/-- Heterogeneous fold over `Fin n` from the left: `foldl 3 f x = f 0 (f 1 (f 2 x))`, where
`f 0 : α 0 → α 1`, `f 1 : α 1 → α 2`, etc.

This is the dependent version of `Fin.foldl`.  -/
Fin.dfoldl : (n : ℕ) → (α : Fin (n + 1) → Type u_1) → ((i : Fin n) → α i.castSucc → α i.succ) → α 0 → α (Fin.last n)
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffOn_chart : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {x : M} [IsManifold I n M],
  ContMDiffOn I I n (↑(chartAt H x)) (chartAt H x).source
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instAddAction.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {m : AddMonoid M} [inst : (i : ι) → AddAction M (α i)],
  Sigma.instAddAction = { toVAdd := Sigma.VAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Init.Data.Nat.ToString
Nat.star_eq_digitChar : ∀ {n : ℕ}, '*' = n.digitChar ↔ 16 ≤ n
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.commonTangents_comm : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s₁ s₂ : EuclideanGeometry.Sphere P), s₁.commonTangents s₂ = s₂.commonTangents s₁
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.CollectState.mk.injEq : ∀ (visited : Std.HashSet Lean.Meta.Sym.ExprPtr)
  (collectedThms : Std.HashSet (Lean.Meta.Grind.Origin × Lean.Meta.Grind.EMatchTheoremKind))
  (thms : Array Lean.Meta.Grind.EMatchTheorem) (visited_1 : Std.HashSet Lean.Meta.Sym.ExprPtr)
  (collectedThms_1 : Std.HashSet (Lean.Meta.Grind.Origin × Lean.Meta.Grind.EMatchTheoremKind))
  (thms_1 : Array Lean.Meta.Grind.EMatchTheorem),
  ({ visited := visited, collectedThms := collectedThms, thms := thms } =
      { visited := visited_1, collectedThms := collectedThms_1, thms := thms_1 }) =
    (visited = visited_1 ∧ collectedThms = collectedThms_1 ∧ thms = thms_1)
-- Mathlib.Data.Set.Basic
Set.instDistribLattice : {α : Type u} → DistribLattice (Set α)
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.Plus.mono_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] {X Y : CochainComplex.Plus C}
  (f : X ⟶ Y), CategoryTheory.Mono f ↔ CategoryTheory.Mono f.hom
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkMatchExpr : Lean.Syntax →
  Bool →
    Lean.Syntax →
      Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.CodeBlock) →
        Lean.Elab.Term.Do.CodeBlock → Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock
-- Aesop.Forward.Match.Types
Aesop.instBEqForwardRuleMatch : BEq Aesop.ForwardRuleMatch
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {D : Type u₂} {inst_3 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_4 : CategoryTheory.MonoidalCategory D} {inst_5 : CategoryTheory.BraidedCategory D}
  {toFunctor : CategoryTheory.Functor C D}
  {laxBraided : autoParam toFunctor.LaxBraided CategoryTheory.LaxBraidedFunctor.laxBraided._autoParam}
  {toFunctor_1 : CategoryTheory.Functor C D}
  {laxBraided_1 : autoParam toFunctor_1.LaxBraided CategoryTheory.LaxBraidedFunctor.laxBraided._autoParam},
  { toFunctor := toFunctor, laxBraided := laxBraided } = { toFunctor := toFunctor_1, laxBraided := laxBraided_1 } →
    toFunctor = toFunctor_1 ∧ laxBraided ≍ laxBraided_1
-- Mathlib.Data.Finset.Basic
Finset.erase_insert_eq_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), (insert a s).erase a = s.erase a
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_lift : ∀ (c : Cardinal.{v}), Cardinal.toNat (Cardinal.lift.{u, v} c) = Cardinal.toNat c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, k ∈ t₂ → Std.DTreeMap.Const.get! (t₁ ∩ t₂) k = Std.DTreeMap.Const.get! t₁ k
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_hom_apply_down : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : Cᵒᵖ) (X_1 : CategoryTheory.Sheaf J (Type (max v' v)))
  (a :
    (((J.yoneda.op.comp (CategoryTheory.sheafCompose J CategoryTheory.uliftFunctor.{v', v}).op).comp
              CategoryTheory.coyoneda).obj
          X).obj
      X_1),
  ((CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.hom.app X).app X_1)) a).down =
    CategoryTheory.uliftYonedaEquiv
      ((CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.inv.app
                  (Opposite.op
                    ((CategoryTheory.sheafCompose J CategoryTheory.uliftFunctor.{v', v}).obj
                      (J.yoneda.obj (Opposite.unop X))))).app
              X_1)
            (TypeCat.ofHom fun g =>
              CategoryTheory.CategoryStruct.comp (J.uliftYonedaCompSheafToPresheaf.inv.app (Opposite.unop X)) g)).hom'
        a)
-- Init.WFComputable
Acc.ndrec_eq_ndrecC : @Acc.ndrec = @Acc.ndrecC
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fundamentalDomain_isBounded : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [IsStrictOrderedRing K] [FloorRing K]
  [Finite ι] [HasSolidNorm K], Bornology.IsBounded (ZSpan.fundamentalDomain b)
-- Mathlib.AlgebraicGeometry.Limits
/-- The map from the empty scheme.  -/
AlgebraicGeometry.Scheme.emptyTo : (X : AlgebraicGeometry.Scheme) → ∅ ⟶ X
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.minFlt : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso C).inv.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id
      (X.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})))
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equiv'_apply : ∀ {ι' : Type u_2} {ι : Type u_10} {R : Type u_14} {M : Type u_15} {M' : Type u_16} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') [inst_5 : SMulCommClass R R M'] (f : M → M') (g : M' → M)
  (hf : ∀ (i : ι), f (b i) ∈ Set.range ⇑b') (hg : ∀ (i : ι'), g (b' i) ∈ Set.range ⇑b)
  (hgf : ∀ (i : ι), g (f (b i)) = b i) (hfg : ∀ (i : ι'), f (g (b' i)) = b' i) (i : ι),
  (b.equiv' b' f g hf hg hgf hfg) (b i) = f (b i)
-- Lean.Linter.UnusedVariables
Lean.Linter.UnusedVariables.FVarDefinition.mk : Lean.Name → Lean.Syntax → Lean.Options → Array Lean.FVarId → Lean.Linter.UnusedVariables.FVarDefinition
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.instAddGroupCarrierToAddGrp : (G : FiniteAddGrp.{u_1}) → AddGroup ↑G.toAddGrp
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.sum_le_of_monotoneOn_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α} {n : ℕ}
  {u : ℕ → α},
  MonotoneOn u (Set.Iic n) →
    (∀ i ≤ n, u i ∈ s) → ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.ExtHashMap.unitOfList l).getKeyD k fallback = fallback
-- Mathlib.Topology.Constructions
CofiniteTopology.isClosed_iff : ∀ {X : Type u} {s : Set (CofiniteTopology X)}, IsClosed s ↔ s = Set.univ ∨ s.Finite