mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listEncode.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (x : ℕ)
  (t₁ t₂ : L.Term (α ⊕ Fin x)) (h_1 : (n : ℕ) → motive n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (n l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin n)) → motive n (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (φ₁ φ₂ : L.BoundedFormula α x) → motive x (φ₁.imp φ₂))
  (h_5 : (x : ℕ) → (φ : L.BoundedFormula α (x + 1)) → motive x φ.all),
  (match x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ with
    | n, FirstOrder.Language.BoundedFormula.falsum => h_1 n
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | n, FirstOrder.Language.BoundedFormula.rel R ts => h_3 n l R ts
    | x, φ₁.imp φ₂ => h_4 x φ₁ φ₂
    | x, φ.all => h_5 x φ) =
    h_2 x t₁ t₂
-- Init.Data.ByteArray.Basic
ByteArray.Iterator.hasNext.eq_1 : ∀ (arr : ByteArray) (i : ℕ), { array := arr, idx := i }.hasNext = decide (i < arr.size)
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.fintypeBot : {G : Type u_1} → [inst : Group G] → Fintype ↥⊥
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_eq_ones : ∀ {n : ℕ} {c : Composition n}, c.reverse = Composition.ones n ↔ c = Composition.ones n
-- Init.Data.Array.Basic
Array.forIn'_eq_forIn' : ∀ {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m], Array.forIn' = forIn'
-- Mathlib.MeasureTheory.Measure.OpenPos
LE.le.isOpenPosMeasure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X}
  [μ.IsOpenPosMeasure], μ ≤ ν → ν.IsOpenPosMeasure
-- Mathlib.Analysis.Normed.Group.Defs
/-- Auxiliary class, endowing a type `α` with a function `nnnorm : α → ℝ≥0` with notation `‖x‖₊`.  -/
NNNorm : Type u_8 → Type u_8
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.step_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {array : Array β} {pos : ℕ},
  (array.iterFromIdxM m pos).step =
    pure
      (Std.Shrink.deflate
        (if h : pos < array.size then Std.PlausibleIterStep.yield (array.iterFromIdxM m (pos + 1)) array[pos] ⋯
        else Std.PlausibleIterStep.done ⋯))
-- Mathlib.Order.WithBot
WithTop.eq_of_forall_le_coe_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {x y : WithTop α} [NoTopOrder α], (∀ (a : α), x ≤ ↑a ↔ y ≤ ↑a) → x = y
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.rightAdjointMate_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] {f : X ⟶ Y} {g : Xᘁ ⟶ Z},
  CategoryTheory.CategoryStruct.comp (fᘁ) g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Yᘁ).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ (η_ X Xᘁ))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Yᘁ Y Z).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ Y Yᘁ) Z)
              (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom))))
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_15.eq_2 : ∀ (C : Type u_1) (motive : CategoryTheory.WithInitial Cᵒᵖ → Sort u_2)
  (h_1 : (x : Cᵒᵖ) → motive (CategoryTheory.WithInitial.of x)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of x => h_1 x
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_2 ()
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.equiv_iff_toList_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp},
  t₁.Equiv t₂ ↔ (Std.DTreeMap.Raw.Const.toList t₁).Perm (Std.DTreeMap.Raw.Const.toList t₂)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.ExtDTreeMap.filterMap f t).getKey? k = (t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome
-- Std.Do.Triple.SpecLemmas
withTheReader.eq_1 : ∀ (ρ : Type u) {m : Type u → Type v} [inst : MonadWithReaderOf ρ m] {α : Type u} (f : ρ → ρ) (x : m α),
  withTheReader ρ f x = MonadWithReaderOf.withReader f x
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of the reverse direction of `Matroid.singleton_dep`. -/
Matroid.IsLoop.dep : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → M.Dep {e}
-- Lean.Meta.Tactic.Grind.Main
/-- Resolves delayed metavariable assignments created inside the current `withNewMCtxDepth` block.
`instantiateMVars` only resolves a delayed assignment `?m #[xs] := ?pending` when `?pending`'s
assignment is ground (no unassigned expression metavariables). This ground restriction exists
because `val` may contain metavariables that have `fvars` in their scope. For example, if
`fvars = #[x]` and `val = ?m + x` where `x` is in the scope of `?m`, then `mkLambda` creates
`fun x => ?m + x`. If `?m` is later assigned to `f x`, the term becomes ill-formed with a
dangling free variable.

This scenario cannot occur here: metavariables created before `withNewMCtxDepth` cannot contain
free variables created by `grind`, so the conversion is safe. Only metavariables at the current
depth are processed; pre-existing delayed assignments are left untouched as they are meant to
be resolved by other tactics.

We do not need to erase the delayed assignments from `dAssignment` because they will be
discarded when `withNewMCtxDepth` restores the metavariable context.
 -/
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.resolveDelayedMVarAssignments : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Get the `i`th element of the set, by its index from left to right.

```
nth {a, b, c, d} 2 = some c
nth {a, b, c, d} 5 = none
```  -/
Ordnode.nth : {α : Type u_1} → Ordnode α → ℕ → Option α
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.bUnion_ptsOfPeriod : ∀ {α : Type u_1} (f : α → α), ⋃ n, ⋃ (_ : n > 0), Function.ptsOfPeriod f n = Function.periodicPts f
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.mul' : ∀ {G : Type u} {inst : Group G} [self : GroupFilterBasis G] {U : Set G}, U ∈ self.sets → ∃ V ∈ self.sets, V * V ⊆ U
-- Mathlib.Algebra.Group.Opposite
AddOpposite.op_sub : ∀ {α : Type u_1} [inst : SubNegMonoid α] (x y : α), AddOpposite.op (x - y) = -AddOpposite.op y + AddOpposite.op x
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.cgf_undef : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  ¬MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ → ProbabilityTheory.cgf X μ t = 0
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.of_subsingleton : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V} [Subsingleton V], G.IsEdgeReachable k u v
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.equivProd_symm_apply_left : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (x : N × G),
  (SemidirectProduct.equivProd.symm x).left = x.1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trNormal.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal (Turing.TM2.Stmt.pop k a q) =
    Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.pop a) q
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyContent_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {s t : Set ((i : ι) → α i)}
  (hP : MeasureTheory.IsProjectiveMeasureFamily P),
  s ∈ MeasureTheory.measurableCylinders α →
    t ∈ MeasureTheory.measurableCylinders α →
      s ⊆ t → (MeasureTheory.projectiveFamilyContent hP) s ≤ (MeasureTheory.projectiveFamilyContent hP) t
-- Aesop.Check
Aesop.Check.mk : Lean.Option Bool → Aesop.Check
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.underlying_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y Z : CategoryTheory.Subobject X} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlying.map f) Z.arrow = Y.arrow
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.fderivWithin_eq_of_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s : Set E},
  f₁ =ᶠ[nhds x] f → fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
-- Mathlib.Analysis.Complex.Poisson
herglotzRieszKernel_def : ∀ (c w z : ℂ), herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackCone_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g],
  (CategoryTheory.ChosenPullbacksAlong.pullbackCone f g).snd = CategoryTheory.ChosenPullbacksAlong.snd f g
-- Init.Data.UInt.Lemmas
UInt32.toUSize_lt : ∀ {a b : UInt32}, a.toUSize < b.toUSize ↔ a < b
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_one_substInv : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) [inst_1 : Invertible ((PowerSeries.coeff 1) P)],
  (PowerSeries.coeff 1) P.substInv = ⅟((PowerSeries.coeff 1) P)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.restrictScalars_toSubfield : ∀ (K : Type u_1) {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] [inst_5 : Algebra L' L] [inst_6 : IsScalarTower K L' L]
  {E : IntermediateField L' L}, (IntermediateField.restrictScalars K E).toSubfield = E.toSubfield
-- Mathlib.FieldTheory.Normal.Defs
normal_iff : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K],
  Normal F K ↔ ∀ (x : K), IsIntegral F x ∧ (Polynomial.map (algebraMap F K) (minpoly F x)).Splits
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_natAdd_Ioc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.natAdd m) (Finset.Ioc i j) = Finset.Ioc (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_const : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {s : Set X}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  [CompleteSpace G] [MeasureTheory.IsFiniteMeasure (μ.variation.restrict s)] (c : E),
  ∫ᵛ (x : X) in s, c ∂[B; μ] = (B c) (μ s)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_finsetSum : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F}
  {B : E →L[ℝ] F →L[ℝ] G} (s : Finset ι) {f : ι → X → E},
  (∀ i ∈ s, μ.Integrable (f i)) → ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmullerAux.congr_simp : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  (x x_1 : Perfection (R ⧸ I) p), x = x_1 → ∀ (a a_1 : ℕ), a = a_1 → x.teichmullerAux a = x_1.teichmullerAux a_1
-- Lean.Meta.Coe
/-- Coerces `expr` to the type `expectedType`.
Returns `.some (coerced, appliedCoeDecls)` on successful coercion,
`.none` if the expression cannot by coerced to that type,
or `.undef` if we need more metavariable assignments.

`appliedCoeDecls` is a list of names representing the names of the `Coe` instances that were
applied.
 -/
Lean.Meta.coerceCollectingNames? : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.LOption (Lean.Expr × List Lean.Name))
-- Mathlib.Order.RelSeries
/-- Every nonempty list satisfying the chain condition gives a relation series  -/
RelSeries.fromListIsChain : {α : Type u_1} → {r : SetRel α α} → (x : List α) → x ≠ [] → List.IsChain (fun x1 x2 => (x1, x2) ∈ r) x → RelSeries r
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin.congr_simp : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (hx : AlgebraicIndependent R x),
  hx.mvPolynomialOptionEquivPolynomialAdjoin = hx.mvPolynomialOptionEquivPolynomialAdjoin
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.strictMono_φ : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N},
  SSet.prodStdSimplex.pairingCore.IsType₂ x →
    ∀ {d : ℕ} (hd : x.dim = d), StrictMono (SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd)
-- Mathlib.Topology.Algebra.Module.Basic
linearMapOfMemClosureRangeCoe_apply : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂]
  [inst_2 : Semiring R] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module S M₂] [inst_8 : ContinuousConstSMul S M₂] [inst_9 : ContinuousAdd M₂]
  {σ : R →+* S} (f : M₁ → M₂) (hf : f ∈ closure (Set.range DFunLike.coe)),
  ⇑(linearMapOfMemClosureRangeCoe f hf) = (↑(addMonoidHomOfMemClosureRangeCoe f hf)).toFun
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- If `μ i` is a countable family of outer measures, then for every set `s` there exists
a measurable set `t ⊇ s` such that `μ i t = (μ i).trim s` for all `i`.  -/
MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim : ∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Sort u_2} [Countable ι] (μ : ι → MeasureTheory.OuterMeasure α)
  (s : Set α), ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s
-- Mathlib.Algebra.Order.UpperLower
UpperSet.commSemigroup.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  UpperSet.commSemigroup = Function.Injective.commSemigroup SetLike.coe ⋯ ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.pow_mem_pow : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α} {a : α} {n : ℕ}, a ∈ s → a ^ n ∈ s ^ n
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.finsetSum_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E} {ι : Type u_8} {μ : ι → MeasureTheory.VectorMeasure X F} {s : Finset ι},
  (∀ i ∈ s, (μ i).Integrable f) → (∑ i ∈ s, μ i).Integrable f
-- Mathlib.CategoryTheory.SingleObj
Units.toAut_inv : ∀ (M : Type u) [inst : Monoid M] (x : Mˣ), ((Units.toAut M) x).inv = (CategoryTheory.SingleObj.toEnd M) ↑x⁻¹
-- Init.Data.String.Bootstrap
String.Internal.next : String → String.Pos.Raw → String.Pos.Raw
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.guitartExact_id' : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] (F : CategoryTheory.Functor C₁ C₂),
  (CategoryTheory.TwoSquare.mk F (CategoryTheory.Functor.id C₁) (CategoryTheory.Functor.id C₂) F
      (CategoryTheory.CategoryStruct.id F)).GuitartExact
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- `P` satisfies the equalizer condition iff its precomposition by an equivalence does.  -/
CategoryTheory.regularTopology.equalizerCondition_iff_of_equivalence : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (P : CategoryTheory.Functor Cᵒᵖ D) (e : C ≌ E),
  CategoryTheory.regularTopology.EqualizerCondition P ↔
    CategoryTheory.regularTopology.EqualizerCondition (e.op.inverse.comp P)
-- Mathlib.FieldTheory.Finiteness
/-- In a Noetherian module over a division ring,
there exists a finite basis. This is the indexing `Finset`.  -/
IsNoetherian.finsetBasisIndex : (K : Type u) →
  (V : Type v) →
    [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → [IsNoetherian K V] → Finset V
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.map.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} {f : Y ⟶ X} (se : CategoryTheory.SplitMono f) (F : CategoryTheory.Functor C D),
  se.map F = { retraction := F.map se.retraction, id := ⋯ }
-- Mathlib.Data.Sum.Basic
Sum.update_inr_apply_inl : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ},
  Function.update f (Sum.inr j) x (Sum.inl i) = f (Sum.inl i)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_sub_Ici : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a - x) '' Set.Ici b = Set.Iic (a - b)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.diseqs.inj : ∀ {solverId : ℕ} {ps : Lean.Meta.Grind.ParentSet} {rest : Lean.Meta.Grind.PendingSolverPropagationsData✝}
  {solverId_1 : ℕ} {ps_1 : Lean.Meta.Grind.ParentSet} {rest_1 : Lean.Meta.Grind.PendingSolverPropagationsData✝},
  Lean.Meta.Grind.PendingSolverPropagationsData.diseqs✝ solverId ps rest =
      Lean.Meta.Grind.PendingSolverPropagationsData.diseqs✝ solverId_1 ps_1 rest_1 →
    solverId = solverId_1 ∧ ps = ps_1 ∧ rest = rest_1
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algEquivOfEq_symm : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hfg : f = g), (AdjoinRoot.algEquivOfEq R f g hfg).symm = AdjoinRoot.algEquivOfEq R g f ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (t.insertIfNew k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [toSemiCartesianMonoidalCategory : CategoryTheory.SemiCartesianMonoidalCategory C] →
      ((X Y : C) →
          CategoryTheory.Limits.IsLimit
            (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
              (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))) →
        CategoryTheory.CartesianMonoidalCategory C
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β}
  (f : α → β → Option γ), m₁.Equiv m₂ → (Std.HashMap.filterMap f m₁).Equiv (Std.HashMap.filterMap f m₂)
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isInt_ratCast : ∀ {R : Type u_1} [inst : DivisionRing R] {q : ℚ} {n : ℤ},
  Mathlib.Meta.NormNum.IsInt q n → Mathlib.Meta.NormNum.IsInt (↑q) n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_leftUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X Y : C}
  (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
    g
-- Init.Data.Array.Find
Array.find?_isSome : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, (Array.find? p xs).isSome = true ↔ ∃ x ∈ xs, p x = true
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.pure_natCast : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : NatCast α] (n : ℕ), NonemptyInterval.pure ↑n = ↑n
-- Init.Data.Order.Ord
Std.LawfulEqCmp.opposite : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] [Std.LawfulEqCmp cmp], Std.LawfulEqCmp fun a b => cmp b a
-- Std.Sat.AIG.RelabelNat
_private.Std.Sat.AIG.RelabelNat.0.Std.Sat.AIG.RelabelNat.State.ofAIGAux.go.match_1.splitter : {α : Type} →
  (motive : Std.Sat.AIG.Decl α → Sort u_1) →
    (decl : Std.Sat.AIG.Decl α) →
      ((a : α) → decl = Std.Sat.AIG.Decl.atom a → motive (Std.Sat.AIG.Decl.atom a)) →
        (decl = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false) →
          ((lhs rhs : Std.Sat.AIG.Fanin) →
              decl = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)) →
            motive decl
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.comp_aeval_apply : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) {B : Type u_2} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (φ : S₁ →ₐ[R] B) (p : MvPolynomial σ R),
  φ ((MvPolynomial.aeval f) p) = (MvPolynomial.aeval fun i => φ (f i)) p
-- Batteries.Recycling.RBTree.Basic
/-- In a red-black tree, every node has a color which is either "red" or "black"
(this particular choice of colors is conventional). A nil node is considered black.
 -/
RBTree.RBColor : Type
-- Mathlib.Data.Set.Pairwise.Basic
subsingleton_setOfPred_mem_iff_pairwise_disjoint : ∀ {α : Type u_1} {ι : Type u_4} {f : ι → Set α},
  (∀ (a : α), {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Function.onFun Disjoint f)
-- Mathlib.Order.Hom.Lattice
InfHom.instPartialOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β],
  InfHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α], t.WF → ∀ {k : α}, t.contains k = true → t.getKey! k = k
-- Mathlib.Analysis.Convex.Segment
mem_openSegment_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {x y z : E},
  x ∈ openSegment 𝕜 y z ↔ ∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory C]
  {X Y : C} (f : X ⟶ Y) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit Y) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) h
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.mk_inv : ∀ (K : Type u) [inst : Field K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x : ℕ × K),
  (PerfectClosure.mk K p x)⁻¹ = PerfectClosure.mk K p (x.1, x.2⁻¹)