mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Ring.Compact
IsLocalRing.isOpen_maximalIdeal_pow : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [inst_5 : IsLocalRing R] [IsNoetherianRing R] (n : ℕ), IsOpen ↑(IsLocalRing.maximalIdeal R ^ n)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isSome_getElem?_toList_ric_eq : ∀ {n i : ℕ}, ((*...=n).toList[i]?.isSome = true) = (i ≤ n)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Option.isNone.eq_2 : ∀ {α : Type u_1}, none.isNone = true
-- Mathlib.RingTheory.Localization.Module
Module.Basis.localizationLocalization_repr_algebraMap : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {A : Type u_3} [inst_4 : CommSemiring A] [inst_5 : Algebra R A]
  (Aₛ : Type u_4) [inst_6 : CommSemiring Aₛ] [inst_7 : Algebra A Aₛ] [inst_8 : Algebra Rₛ Aₛ] [inst_9 : Algebra R Aₛ]
  [inst_10 : IsScalarTower R Rₛ Aₛ] [inst_11 : IsScalarTower R A Aₛ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Module.Basis ι R A) (x : A)
  (i : ι),
  ((Module.Basis.localizationLocalization Rₛ S Aₛ b).repr ((algebraMap A Aₛ) x)) i = (algebraMap R Rₛ) ((b.repr x) i)
-- Lean.Elab.Tactic.Omega.Core
/-- Insert a constraint into the problem,
without checking if there is already a constraint for these coefficients.
 -/
Lean.Elab.Tactic.Omega.Problem.insertConstraint : Lean.Elab.Tactic.Omega.Problem → Lean.Elab.Tactic.Omega.Fact → Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Order.CountableSupClosed
lowerBounds_countableInfClosure : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), lowerBounds (countableInfClosure s) = lowerBounds s
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.lie_mem_maxGenEigenspace_toEnd : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {χ₁ χ₂ : R}
  {x y : L} {m : M},
  y ∈ ((LieModule.toEnd R L L) x).maxGenEigenspace χ₁ →
    m ∈ ((LieModule.toEnd R L M) x).maxGenEigenspace χ₂ →
      ⁅y, m⁆ ∈ ((LieModule.toEnd R L M) x).maxGenEigenspace (χ₁ + χ₂)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.const_mul_left : ∀ {α : Type u_1} {F : Type u_4} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedRing R] {g : α → F} {l : Filter α}
  {f : α → R}, f =O[l] g → ∀ (c' : R), (fun x => c' * f x) =O[l] g
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- For a graded ring `⨁ᵢ 𝒜ᵢ` graded by
`[AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι]`, the irrelevant ideal refers to
`⨁_{i>0} 𝒜ᵢ`, or equivalently `{a | a₀ = 0}`. This definition is used in `Proj` construction where
`ι` is always `ℕ` so the irrelevant ideal is simply elements with `0` as 0-th coordinate.
 -/
HomogeneousIdeal.«term_₊» : Lean.TrailingParserDescr
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_div : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u v : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : Div β],
  MeasureTheory.stoppedValue (u / v) τ = MeasureTheory.stoppedValue u τ / MeasureTheory.stoppedValue v τ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.coe_finsetWalkLengthLT_eq : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : G.LocallyFinite] (n : ℕ) (u v : V),
  ↑(G.finsetWalkLengthLT n u v) = {p | p.length < n}
-- Mathlib.ModelTheory.Bundled
/-- An elementary substructure of a bundled model as a bundled model.  -/
FirstOrder.Language.ElementarySubstructure.toModel : {L : FirstOrder.Language} → (T : L.Theory) → {M : T.ModelType} → L.ElementarySubstructure ↑M → T.ModelType
-- Batteries.Data.List.Perm
List.Perm.getElem_idxBij_symm_eq_getElem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (hxy : xs.Perm ys) (i : Fin ys.length),
  xs[↑(⋯.idxBij i)] = ys[↑i]
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_mul_re : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.re (RCLike.I * z) = -RCLike.im z
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.PreservesFiniteLimitsOfFlat.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type v₁} [inst_2 : CategoryTheory.SmallCategory J] [inst_3 : CategoryTheory.FinCategory J]
  {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.RepresentablyFlat F]
  {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone (K.comp F))
  (x : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesFiniteLimitsOfFlat.lift F hc s) ((F.mapCone c).π.app x) =
    s.π.app x
-- Init.Data.Order.MinMaxOn
/-- Returns either `x` or `y`, the one with the smaller value under `f`.

If `f x ≤ f y`, it returns `x`, and otherwise returns `y`.
 -/
minOn : {β : Type u_1} → {α : Sort u_2} → [inst : LE β] → [DecidableLE β] → (α → β) → α → α → α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.of_forall_mem_unit_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {m₁ m₂ : Std.DHashMap.Raw α fun x => Unit},
  m₁.WF → m₂.WF → (∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) → m₁.Equiv m₂
-- Mathlib.Tactic.MoveAdd
/-- `uniquify L` takes a list `L : List α` as input and it returns a list `L' : List (α × ℕ)`.
The two lists `L` and `L'.map Prod.fst` coincide.
The second component of each entry `(a, n)` in `L'` is the number of times that `a` appears in `L`
before the current location.

The resulting list of pairs has no duplicates.
 -/
Mathlib.MoveAdd.uniquify : {α : Type u_1} → [BEq α] → List α → List (α × ℕ)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.Limits.Fork.ofι.eq_1 : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (ι : P ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g),
  CategoryTheory.Limits.Fork.ofι ι w =
    { pt := P,
      π :=
        {
          app := fun X_1 =>
            CategoryTheory.Limits.WalkingParallelPair.casesOn (motive := fun t =>
              X_1 = t →
                (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj P).obj X_1 ⟶
                  (CategoryTheory.Limits.parallelPair f g).obj X_1))
              X_1 (fun h => ⋯ ▸ ι) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp ι f) ⋯,
          naturality := ⋯ } }
-- Lean.Parser.Extension
Lean.Parser.ParserAliasValue : Type
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The functions satisfying a local predicate satisfy the sheaf condition.
 -/
TopCat.subpresheafToTypes.isSheaf : ∀ {X : TopCat} {T : ↑X → Type u_1} (P : TopCat.LocalPredicate T),
  (TopCat.subpresheafToTypes P.toPrelocalPredicate).IsSheaf
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- If `g` is surjective, then `g.baseChange A` is surjective.  -/
LinearMap.baseChange_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : Module R N] [inst_4 : Module R P] {g : N →ₗ[R] P} (A : Type u_6)
  [inst_5 : Semiring A] [inst_6 : Algebra R A], Function.Surjective ⇑g → Function.Surjective ⇑(LinearMap.baseChange A g)
-- Mathlib.Data.ZMod.Basic
_private.Mathlib.Data.ZMod.Basic.0.ZMod.val.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_eq_get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} {h : k ∈ m}, m.get k h = (m.get? k).get ⋯
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of the forward direction of `Set.pairwise_bot_iff`. -/
Set.Pairwise.subsingleton : ∀ {α : Type u_1} {s : Set α}, s.Pairwise ⊥ → s.Subsingleton
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_congr_ae : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f g : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  f =ᵐ[μ] g → MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T hT g
-- Mathlib.Data.List.DropRight
List.rdrop_add : ∀ {α : Type u_1} {l : List α} (i j : ℕ), (l.rdrop i).rdrop j = l.rdrop (i + j)
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_lineMap_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P)
  (c₁ c₂ : 𝕜), nndist ((AffineMap.lineMap p₁ p₂) c₁) ((AffineMap.lineMap p₁ p₂) c₂) = nndist c₁ c₂ * nndist p₁ p₂
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.disjoint_skeleton_openCell`.

---

A skeleton and an open cell of a higher dimension are disjoint.  -/
Topology.CWComplex.disjoint_skeleton_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {m : ℕ} {j : Topology.RelCWComplex.cell C m},
  n < ↑m → Disjoint (↑(Topology.RelCWComplex.skeleton C n)) (Topology.RelCWComplex.openCell m j)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.fundamentalInterior_subset : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s : Set α},
  MeasureTheory.fundamentalInterior G s ⊆ s
-- Mathlib.Data.Nat.Choose.Factorization
/-- **Legendre's Theorem**

The multiplicity of a prime in `n!` is the sum of the quotients `n / p ^ i`. This sum is expressed
over the finset `Ico 1 b` where `b` is any bound greater than `log p n`.  -/
Nat.factorization_factorial : ∀ {p : ℕ}, Nat.Prime p → ∀ {n b : ℕ}, Nat.log p n < b → n.factorial.factorization p = ∑ i ∈ Finset.Ico 1 b, n / p ^ i
-- Mathlib.Topology.MetricSpace.Bounded
Metric.compactSpace_iff_isBounded_univ : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α], CompactSpace α ↔ Bornology.IsBounded Set.univ
-- Init.SimpLemmas
eq_true_of_decide : ∀ {p : Prop} [inst : Decidable p], decide p = true → p = True
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.right : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    (j : J) → CategoryTheory.BiconeHom J CategoryTheory.Bicone.right (CategoryTheory.Bicone.diagram j)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.pushScope : {α β σ : Type} → Lean.ScopedEnvExtension α β σ → Lean.Environment → Lean.Environment
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α} {n : ℕ}, 1 ∈ s → n ≠ 0 → s ⊆ s ^ n
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.mono_left : ∀ {α : Type u_1} [inst : Preorder α] {x y : α},
  x ≤ y → ∀ {t : Ordnode α} {o : WithTop α}, t.Bounded (↑y) o → t.Bounded (↑x) o
-- Mathlib.Algebra.GroupWithZero.Opposite
AddOpposite.instMulZeroOneClass : {α : Type u_1} → [MulZeroOneClass α] → MulZeroOneClass αᵃᵒᵖ
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.RefreshState.mk.sizeOf_spec : ∀ (curr : Thunk ProofWidgets.Html) (idx : ℕ) (next : Task (Option Unit)),
  sizeOf { curr := curr, idx := idx, next := next } = 1 + sizeOf curr + sizeOf idx + sizeOf next
-- Mathlib.Order.WithBot
WithTop.instBot : {α : Type u_1} → [Bot α] → Bot (WithTop α)
-- Lean.Meta.SameCtorUtils
/-- Given a constructor (applied to the parameters already), brings its fields into scope twice,
but uses the same variable for fields that appear in the result type, so that the resulting
constructor applications have the same type.

Passes to `k`
* the new variables
* the indices to the type class
* the fields of the first constructor application
* the fields of the second constructor application
 -/
Lean.Meta.withSharedCtorIndices : {α : Type} →
  Lean.Expr → (Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Topology.Algebra.Support
tsupport_mul_subset_right : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_9} [inst_1 : MulZeroClass α] {f g : X → α},
  (tsupport fun x => f x * g x) ⊆ tsupport g
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.subtypeDomain_def : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [inst_3 : DecidablePred p] (f : Π₀ (i : ι), β i),
  DFinsupp.subtypeDomain p f = DFinsupp.mk (Finset.subtype p f.support) fun i => f ↑↑i
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opcyclesOpIso_hom_naturality : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((HomologicalComplex.opFunctor V c).map φ.op) i)
      (K.opcyclesOpIso i).hom =
    CategoryTheory.CategoryStruct.comp (L.opcyclesOpIso i).hom (HomologicalComplex.cyclesMap φ i).op
-- Mathlib.Tactic.Translate.GuessName
_private.Mathlib.Tactic.Translate.GuessName.0.Mathlib.Tactic.GuessName.fixAbbreviationAux.match_1.eq_1 : ∀ (motive : Option String → Sort u_1) (post : String) (h_1 : (post : String) → motive (some post))
  (h_2 : Unit → motive none),
  (match some post with
    | some post => h_1 post
    | none => h_2 ()) =
    h_1 post
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsNormal.toIsWide : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C}, S.IsNormal → S.IsWide
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.homMk₁.match_1.splitter : (motive : Fin (1 + 1) → Sort u_1) →
  (i : Fin (1 + 1)) → ((isLt : 0 < 1 + 1) → motive ⟨0, isLt⟩) → ((isLt : 1 < 1 + 1) → motive ⟨1, isLt⟩) → motive i
-- Batteries.Data.String.Legacy
String.Pos.Raw.utf8GetAux.eq_2 : ∀ (x x_1 : String.Pos.Raw) (c : Char) (cs : List Char),
  String.Pos.Raw.utf8GetAux (c :: cs) x x_1 = if x = x_1 then c else String.Pos.Raw.utf8GetAux cs (x + c) x_1
-- Aesop.Rule
Aesop.SafeRuleInfo.safety : Aesop.SafeRuleInfo → Aesop.Safety
-- Mathlib.Data.ENat.Lattice
ENat.biSup_add_biSup_le : ∀ {ι : Type u_4} {κ : Type u_5} {s : Set ι} {t : Set κ},
  s.Nonempty →
    t.Nonempty →
      ∀ {f : ι → ℕ∞} {g : κ → ℕ∞} {a : ℕ∞}, (∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) → (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `b ≠ 0`. See `mul_inv_cancel_right`.  -/
mul_inv_right_le : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b : G₀}, 0 ≤ a → a * b * b⁻¹ ≤ a
-- Lean.Message
/-- Converts the unreported messages to a list, oldest message first.  -/
Lean.MessageLog.toList : Lean.MessageLog → List Lean.Message
-- Init.Prelude
/-- Transforms the value returned from an `EStateM ε σ` action using a function.
 -/
EStateM.map : {ε σ α β : Type u} → (α → β) → EStateM ε σ α → EStateM ε σ β
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'.eq_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullbackRightPullbackFstIso
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i)))
            (𝒰.f k)
            (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j)))
            (𝒰.f k) (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j) (CategoryTheory.CategoryStruct.id (𝒰.X k))
            (CategoryTheory.CategoryStruct.id X) ⋯ ⋯)
          (CategoryTheory.Limits.pullbackRightPullbackFstIso
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
              (𝒰.f k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i)).inv)
        (CategoryTheory.Limits.pullbackSymmetry (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i)
            (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)).hom)
-- Mathlib.Probability.Independence.Basic
/-- Two sets are independent if the two measurable space structures they generate are independent.
For a set `s`, the generated measurable space structure has measurable sets `∅, s, sᶜ, univ`.  -/
ProbabilityTheory.IndepSet : {Ω : Type u_1} →
  {_mΩ : MeasurableSpace Ω} →
    Set Ω → Set Ω → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IndepSet._auto_1 → Prop
-- Init.Data.Format.Basic
Std.Format.brecOn.eq : ∀ {motive : Std.Format → Sort u} (t : Std.Format) (F_1 : (t : Std.Format) → Std.Format.below t → motive t),
  Std.Format.brecOn t F_1 = F_1 t (Std.Format.brecOn.go t F_1).2
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Raw.toListRev_keysIter : ∀ {α : Type u} {β : α → Type u} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keysIter.toListRev = m.keys.reverse
-- Init.System.IO
/-- The `Task` is actively running on a thread or, in the case of a `Promise`, waiting for a call to
`IO.Promise.resolve`.
 -/
IO.TaskState.running : IO.TaskState
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_mul : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (g h : GL n R),
  (Matrix.GeneralLinearGroup.map f) (g * h) = (Matrix.GeneralLinearGroup.map f) g * (Matrix.GeneralLinearGroup.map f) h
-- Mathlib.Logic.Equiv.Set
/-- A family of equivalences between preimages of points gives an equivalence between domains.  -/
Equiv.ofPreimageEquiv : {α : Type u_3} →
  {β : Type u_4} → {γ : Type u_5} → {f : α → γ} → {g : β → γ} → ((c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})) → α ≃ β
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.isPeriodicPt_factorial_card_of_mem_periodicPts : ∀ {α : Type u_1} {f : α → α} {x : α} [inst : Fintype α],
  x ∈ Function.periodicPts f → Function.IsPeriodicPt f (Fintype.card α).factorial x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measure_interior_of_null_frontier : ∀ {α' : Type u_6} [inst : TopologicalSpace α'] [inst_1 : MeasurableSpace α'] {μ : MeasureTheory.Measure α'}
  {s : Set α'}, μ (frontier s) = 0 → μ (interior s) = μ s
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.not_cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl} {f : ℝ → ℝ},
  ¬(Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f).IsZero
-- Std.Async.System
/-- Unset an environment variable.
 -/
Std.Async.System.unsetEnvVar : String → IO Unit
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_le_iff_le_div : ∀ {a b c : Ordinal.{u_4}}, a ≠ 0 → (a * b ≤ c ↔ b ≤ c / a)
-- Aesop.RulePattern
/-- A rule pattern. For a rule of type `∀ (x₀ : T₀) ... (xₙ : Tₙ), U`, a valid rule
pattern is an expression `p` such that `x₀ : T₁, ..., xₙ : Tₙ ⊢ p : P`. Let
`y₀, ..., yₖ` be those variables `xᵢ` on which `p` depends. When `p` matches an
expression `e`, this means that `e` is defeq to `p` (where each `yᵢ` is replaced
with a metavariable) and we obtain a substitution

    {y₀ ↦ t₀ : T₀, y₁ ↦ t₁ : T₁[x₀ := t₀], ...}

Now suppose we want to match the above rule type against a type `V` (where `V`
is the target for an `apply`-like rule and a hypothesis type for a
`forward`-like rule). To that end, we take `U` and replace each `xᵢ` where
`xᵢ = yⱼ` with `tⱼ` and each `xᵢ` with `xᵢ ≠ yⱼ ∀ j` with a metavariable. The
resulting expression `U'` is then matched against `V`.
 -/
Aesop.RulePattern : Type
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The `i`-th face map from `⦋n⦌` to `⦋n+1⦌`  -/
SimplexCategory.δ : {n : ℕ} → Fin (n + 2) → ({ len := n } ⟶ { len := n + 1 })
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.map_eq_zero_iff : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃), Function.Injective ⇑f → ∀ {x : M}, f x = 0 ↔ x = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Count leading zeros.
 -/
Std.Tactic.BVDecide.BVUnOp.clz : Std.Tactic.BVDecide.BVUnOp
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- `0` composed with `f` is `0`  -/
CategoryTheory.Limits.HasZeroMorphisms.zero_comp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasZeroMorphisms C] (X : C)
  {Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp 0 f = 0
-- Mathlib.Combinatorics.Additive.Dissociation
Finset.prod_div_prod_mem_mulSpan : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s t u : Finset α},
  t ⊆ s → u ⊆ s → (∏ a ∈ t, a) / ∏ a ∈ u, a ∈ s.mulSpan
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
max_mul_of_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {c : R} [MulPosMono R] (a b : R),
  0 ≤ c → max a b * c = max (a * c) (b * c)
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_iff_exists_forall : ∀ {α : Type u_1} {ι : Type u_4} [Nonempty ι] (s : Set α) (f : α → ι) {r : ι → ι → Prop} [IsEquiv ι r],
  s.Pairwise (Function.onFun r f) ↔ ∃ z, ∀ x ∈ s, r (f x) z
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Characterization of multiplicative identity  -/
HomotopyGroup.one_def : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] [inst_2 : Nonempty N],
  1 = ⟦GenLoop.const⟧
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.Context.mk.inj : ∀ {commonMCtx? : Option Lean.MetavarContext} {mctx₁ mctx₂ : Lean.MetavarContext} {allowAssignmentDiff : Bool}
  {commonMCtx?_1 : Option Lean.MetavarContext} {mctx₁_1 mctx₂_1 : Lean.MetavarContext} {allowAssignmentDiff_1 : Bool},
  { commonMCtx? := commonMCtx?, mctx₁ := mctx₁, mctx₂ := mctx₂, allowAssignmentDiff := allowAssignmentDiff } =
      { commonMCtx? := commonMCtx?_1, mctx₁ := mctx₁_1, mctx₂ := mctx₂_1,
        allowAssignmentDiff := allowAssignmentDiff_1 } →
    commonMCtx? = commonMCtx?_1 ∧ mctx₁ = mctx₁_1 ∧ mctx₂ = mctx₂_1 ∧ allowAssignmentDiff = allowAssignmentDiff_1
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} {x y : CategoryTheory.Meq P S},
  x = y ↔ ∀ (I : S.Arrow), ↑x I = ↑y I