mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α}
  {k k' fallback : α},
  cmp k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKeyD k' fallback = k
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.instNontrivialOfNonempty : ∀ {α : Type u} [Nonempty α], Nontrivial (FreeAbelianGroup α)
-- Mathlib.Data.Finset.Image
Finset.mapEmbedding_apply : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α}, (Finset.mapEmbedding f) s = Finset.map f s
-- Mathlib.Topology.Order.HullKernel
/-- Every relative-closed set of the form `T ↓∩ (↑(upperClosure F))` for `F` finite is a
relative-closed set of the form `hull T a` where `a = ⨅ F`.  -/
PrimitiveSpectrum.hull_finsetInf : ∀ {α : Type u_1} [inst : SemilatticeInf α] {T : Set α} [inst_1 : OrderTop α],
  (∀ p ∈ T, InfPrime p) → ∀ (F : Finset α), PrimitiveSpectrum.hull T (F.inf id) = Subtype.val ⁻¹' ↑(upperClosure ↑F)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_one_div_cancel : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a * (1 / a) = 1
-- Mathlib.RingTheory.Nilpotent.Basic
IsNilpotent.isUnit_sub_one : ∀ {R : Type u_1} [inst : Ring R] {r : R}, IsNilpotent r → IsUnit (r - 1)
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {_P : CategoryTheory.MorphismProperty C}
  [inst_1 : _P.IsMultiplicative] [inst_2 : SizeOf C] [inst_3 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (_P x)] (obj : C),
  sizeOf { obj := obj } = 1 + sizeOf obj
-- Init.Data.SInt.Bitwise
Int32.zero_and : ∀ {a : Int32}, 0 &&& a = 0
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.firstMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X) [inst_1 : R.HasPairwisePullbacks],
  CategoryTheory.Equalizer.Presieve.firstMap P R =
    CategoryTheory.Limits.Pi.lift fun fg =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) fg.1)
        (P.map (CategoryTheory.Limits.pullback.fst ↑fg.1.snd ↑fg.2.snd).op)
-- Mathlib.Analysis.SpecificLimits.FloorPow
/-- The sum of `1/(c^i)^2` above a threshold `j` is comparable to `1/j^2`, up to a multiplicative
constant.  -/
sum_div_pow_sq_le_div_sq : ∀ (N : ℕ) {j : ℝ},
  0 < j → ∀ {c : ℝ}, 1 < c → ∑ i ∈ Finset.range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [J.PreservesSheafification F] [inst_4 : CategoryTheory.HasWeakSheafify J B],
  J.W.IsInvertedBy (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.map_id_equiv : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.map (fun x v => v) t).Equiv t
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.pow_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f g s → ∀ (n : ℕ), AntivaryOn (f ^ n) g s
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.opOp_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.opOp C).map f = f.op.op
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.proved.inj : ∀ {script script_1 : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))},
  Aesop.NormSeqResult.proved script = Aesop.NormSeqResult.proved script_1 → script = script_1
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv : ∀ {α : Type u_1} [inst : UniformSpace α],
  UniformContinuous ⇑(UniformSpace.Completion.completionSeparationQuotientEquiv α)
-- Mathlib.LinearAlgebra.LinearPMap
/-- A dependent version of `ext`.  -/
LinearPMap.dExt : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f g : E →ₛₗ.[σ] F},
  f.domain = g.domain → (∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y) → f = g
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.mk_mul_mk : ∀ {K : Type u_1} [inst : Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K),
  ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.hom_neg_apply : ∀ {M N : AddCommMonCat} (e : M ≅ N) (s : ↑N),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Lean.Server.CodeActions.Basic
Lean.Server.LazyCodeAction.mk : Lean.Lsp.CodeAction → Option (IO Lean.Lsp.CodeAction) → Lean.Server.LazyCodeAction
-- Init.Data.SInt.Lemmas
Int8.lt_or_le : ∀ (a b : Int8), a < b ∨ b ≤ a
-- Mathlib.GroupTheory.Finiteness
/-- A subgroup of `G` is finitely generated if it is the closure of a finite subset of `G`.  -/
Subgroup.FG : {G : Type u_3} → [inst : Group G] → Subgroup G → Prop
-- Init.Data.Vector.Erase
Vector.set_eraseIdx_gt : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {w : i < n} {j : ℕ} {a : α} (h : j < i) (hj : j < n - 1),
  (xs.eraseIdx i w).set j a hj = (xs.set j a ⋯).eraseIdx i w
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_group_smul_right : ∀ {R : Type u_1} {G : Type u_2} [inst : CommSemiring R] [inst_1 : Group G] [inst_2 : MulAction G R]
  [SMulCommClass G R R] [IsScalarTower G R R] (x : G) (y z : R), IsCoprime y (x • z) ↔ IsCoprime y z
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.toHom_sumCongr : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H'), (f.sumCongr g).toHom = f.toHom.sum g.toHom
-- Init.Data.String.Basic
String.Pos.toSlice_inj : ∀ {s : String} {p q : s.Pos}, p.toSlice = q.toSlice ↔ p = q
-- Mathlib.Order.OmegaCompletePartialOrder
/-- `ωSup` is an upper bound of the increasing sequence  -/
OmegaCompletePartialOrder.le_ωSup : ∀ {α : Type u_6} [self : OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) (i : ℕ),
  c i ≤ OmegaCompletePartialOrder.ωSup c
-- Mathlib.RingTheory.Trace.Basic
Algebra.trace_eq_of_algEquiv : ∀ {A : Type u_7} {B : Type u_8} {C : Type u_9} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] (e : B ≃ₐ[A] C) (x : B),
  (Algebra.trace A C) (e x) = (Algebra.trace A B) x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∪ t₂ → k ∉ t₂ → k ∈ t₁
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the fourth quadrant. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open fourth quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open fourth quadrant
  for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the boundary of the fourth quadrant.

Then `‖f z‖` is bounded from above by the same constant on the closed fourth quadrant.  -/
PhragmenLindelof.quadrant_IV : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
  DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C) → (∀ x ≤ 0, ‖f (↑x * Complex.I)‖ ≤ C) → 0 ≤ z.re → z.im ≤ 0 → ‖f z‖ ≤ C
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHomClass.mk : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : AddZero M] [inst_1 : AddZero N]
  [inst_2 : FunLike F M N] [toAddHomClass : AddHomClass F M N] [toZeroHomClass : ZeroHomClass F M N],
  AddMonoidHomClass F M N
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_comp_const_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type uF} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (n : ℕ) (c : 𝕜),
  iteratedFDerivWithin 𝕜 n (fun z => f (c - z)) s = fun x => (-1) ^ n • iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {km : α}, t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- The composition of cocompact continuous maps, as a cocompact continuous map.  -/
CocompactMap.comp : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] →
          [inst_2 : TopologicalSpace γ] → CocompactMap β γ → CocompactMap α β → CocompactMap α γ
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {D₁ D₂ : F.DescentDataAsCoalgebra f} →
                (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i) →
                  autoParam
                      (∀ (i₁ i₂ : ι),
                        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
                            ((F.map (f i₁).op.toLoc).l.toFunctor.map
                              ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂))) =
                          CategoryTheory.CategoryStruct.comp (hom i₁) (D₂.hom i₁ i₂))
                      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm._autoParam →
                    D₁.Hom D₂
-- Lean.DocString.Parser
Lean.Doc.Parser.OrderedListType.ofNat : ℕ → Lean.Doc.Parser.OrderedListType
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The image (up to isomorphisms) of a `MorphismProperty C` by a functor `C ⥤ D`  -/
CategoryTheory.MorphismProperty.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.MorphismProperty C → CategoryTheory.Functor C D → CategoryTheory.MorphismProperty D
-- Init.Data.Iterators.Combinators.FilterMap
/-- *Note: This is a very general combinator that requires an advanced understanding of monads,
dependent types and termination proofs. The variants `filter` and `filterM` are easier to use and
sufficient for most use cases.*

If `it` is an iterator, then `it.filterWithPostcondition f` is another iterator that applies a monadic
predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

`f` is expected to return `PostconditionT n (ULift Bool)`, where `n` is an arbitrary monad.
The `PostconditionT` transformer allows the caller to intrinsically prove properties about
`f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior
of `f`.

**Marble diagram (without monadic effects):**

```text
it                             ---a--b--c--d-e--⊥
it.filterWithPostcondition     ---a-----c-------⊥
```

(given that `f a = f c = pure true` and `f b = f d = d e = pure false`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and
will always fail, then `it.filterWithPostcondition` will be finite -- and productive -- even if `it`
isn't.

In such situations, the missing instances can be proved manually if the postcondition bundled in
the `PostconditionT n` monad is strong enough. In the given example, a suitable postcondition might
be `fun _ => False`.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.Iter.filterWithPostcondition : {α β : Type w} →
  [Std.Iterator α Id β] →
    {m : Type w → Type w'} →
      [inst : Monad m] → (f : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)) → Std.Iter β → Std.IterM m β
-- Mathlib.Data.Set.Prod
Set.EqOn.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f f' : α → γ} {g g' : β → δ},
  Set.EqOn f f' s → Set.EqOn g g' t → Set.EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
-- Batteries.Lean.Util.EnvSearch
/-- Check constant should be returned  -/
_private.Batteries.Lean.Util.EnvSearch.0.Lean.getMatchingConstants.check : {m : Type → Type} →
  [Monad m] →
    (Lean.ConstantInfo → m Bool) → Array Lean.ConstantInfo → Lean.Name → Lean.ConstantInfo → m (Array Lean.ConstantInfo)
-- Mathlib.Data.NNReal.Defs
/-- Redo the `Nonneg.semifield` instance, because this will get unfolded a lot,
and ends up inserting the non-reducible defeq `ℝ≥0 = { x // x ≥ 0 }` in places where
it needs to be reducible(-with-instances).
 -/
NNReal.instSemifield : Semifield NNReal
-- Mathlib.CategoryTheory.Limits.Types.Images
CategoryTheory.Limits.Types.instMonoImageι : ∀ {α β : Type u} (f : α ⟶ β), CategoryTheory.Mono (CategoryTheory.Limits.Types.Image.ι f)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.nullMeasurableSet_restrict_of_subset : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  t ⊆ s → (MeasureTheory.NullMeasurableSet t (μ.restrict s) ↔ MeasureTheory.NullMeasurableSet t μ)
-- Init.Internal.Order.Basic
Lean.Order.Example.find : (ℕ → Bool) → ℕ → Option ℕ
-- Mathlib.Data.Rat.Cast.Order
/-- Extension for Rat.cast.  -/
Mathlib.Meta.Positivity.evalRatCast : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.GroupTheory.GroupAction.SubMulAction
vadd_mem_fixedPoints_of_normal : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {H : AddSubgroup G} [hH : H.Normal] (g : G)
  {a : α}, a ∈ AddAction.fixedPoints (↥H) α → g +ᵥ a ∈ AddAction.fixedPoints (↥H) α
-- Mathlib.SetTheory.Ordinal.Basic
/-- Equivalence relation on well orders on arbitrary types in universe `u`, given by order
isomorphism.  -/
Ordinal.isEquivalent : Setoid WellOrder
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- Subgroups of an additive group `Multiplicative A` are isomorphic to additive subgroups of `A`.
 -/
Subgroup.toAddSubgroup' : {A : Type u_2} → [inst : AddGroup A] → Subgroup (Multiplicative A) ≃o AddSubgroup A
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- Post-composition with the preimage of an inducing function whose range is closed preserves
upper hemicontinuity.  -/
UpperHemicontinuousAt.isInducing_comp : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {γ : Type u_5} [inst_2 : TopologicalSpace γ] {i : γ → β},
  UpperHemicontinuousAt f x →
    Topology.IsInducing i → IsClosed (Set.range i) → UpperHemicontinuousAt (fun x => i ⁻¹' f x) x
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.homDiagram_obj : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat}
  (X Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) (j : J),
  (CategoryTheory.Cat.HasLimits.homDiagram X Y).obj j =
    ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j)) X ⟶
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j)) Y)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (curr : ℕ) → motive curr.succ),
  (match 0 with
    | 0 => h_1 ()
    | curr.succ => h_2 curr) =
    h_1 ()
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_irrelevant_le : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {I : Ideal A},
  (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ I ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ I.toAddSubmonoid
-- Mathlib.GroupTheory.OrderOfElement
not_isMulTorsionFree_iff_isOfFinOrder : ∀ {G : Type u_1} [inst : CommGroup G], ¬IsMulTorsionFree G ↔ ∃ a, a ≠ 1 ∧ IsOfFinOrder a
-- Mathlib.Topology.NhdsKer
nhdsKer_pi : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] (s : (i : ι) → Set (X i)),
  nhdsKer (Set.univ.pi s) = Set.univ.pi fun i => nhdsKer (s i)
-- Mathlib.Data.PFunctor.Univariate.M
/-- unfold an M-type  -/
PFunctor.M.dest : {F : PFunctor.{uA, uB}} → F.M → ↑F F.M
-- Mathlib.Order.Birkhoff
/-- **Birkhoff Representation for partial orders.** Any partial order is isomorphic
to the partial order of inf-irreducible elements in its lattice of upper sets.  -/
OrderIso.infIrredUpperSet : {α : Type u_1} → [inst : PartialOrder α] → [Finite α] → α ≃o { s // InfIrred s }
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCircuit_rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v} (hu : u ∈ c.support),
  (c.rotate u hu).IsCircuit ↔ c.IsCircuit
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.mem_map : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β)
  {L : CompleteSublattice α} {b : β}, b ∈ CompleteSublattice.map f L ↔ ∃ a ∈ L, f a = b
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.CofreeEqualizer.topMap_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra),
  (CategoryTheory.Comonad.CofreeEqualizer.topMap X).f = T.map X.a
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- For an element `a` in a C⋆-algebra, TFAE:
1. `a` is strictly positive,
2. `sqrt a` is strictly positive and `a = sqrt a * sqrt a`,
3. `sqrt a` is invertible and `a = sqrt a * sqrt a`,
4. `a = b * b` for some strictly positive `b`,
5. `a = b * b` for some self-adjoint and invertible `b`,
6. `a = star b * b` for some invertible `b`,
7. `a = b * star b` for some invertible `b`,
8. `0 ≤ a` and `a` is invertible,
9. `a` is self-adjoint and has positive spectrum.  -/
CStarAlgebra.isStrictlyPositive_TFAE : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A},
  [IsStrictlyPositive a, IsStrictlyPositive (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a,
      IsUnit (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a, ∃ b, IsStrictlyPositive b ∧ a = b * b,
      ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b, ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b,
      0 ≤ a ∧ IsUnit a, IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE
-- Mathlib.Data.Int.Interval
Int.Ioo_eq_finset_map : ∀ (a b : ℤ),
  Finset.Ioo a b = Finset.map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (Finset.range (b - a - 1).toNat)
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.inr_pushoutZeroZeroIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.Limits.pushoutZeroZeroIso X Y).inv =
    CategoryTheory.Limits.pushout.inr 0 0
-- Mathlib.CategoryTheory.Localization.Opposite
CategoryTheory.Localization.isoOfHom_unop : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] {X Y : Cᵒᵖ} (w : X ⟶ Y) (hw : W.op w),
  (CategoryTheory.Localization.isoOfHom L.op W.op w hw).unop = CategoryTheory.Localization.isoOfHom L W w.unop hw
-- Init.Data.Nat.Control
_private.Init.Data.Nat.Control.0.Nat.anyM.loop : {m : Type → Type u_1} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → m Bool) → (i : ℕ) → i ≤ n → m Bool
-- Mathlib.Logic.Relation
Relation.reflGen_transGen : ∀ {α : Type u_1} {r : α → α → Prop}, Relation.ReflGen (Relation.TransGen r) = Relation.ReflTransGen r
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instIsStableUnderBaseChangeMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J K : CategoryTheory.Precoverage C)
  [J.IsStableUnderBaseChange] [K.IsStableUnderBaseChange], (J ⊓ K).IsStableUnderBaseChange
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α), G.Inc e x = ∃ y, G.IsLink e x y
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_stabilizerAddSubmonoid_iff : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] {a : α} {m : M},
  m ∈ AddAction.stabilizerAddSubmonoid M a ↔ m +ᵥ a = a
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.Fib.homMk.eq_1 : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} {a b : HasFibers.Fib p S}
  (φ : (HasFibers.ι S).obj a ⟶ (HasFibers.ι S).obj b) [inst_3 : p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ],
  HasFibers.Fib.homMk φ = (HasFibers.inducedFunctor p S).preimage (CategoryTheory.Functor.Fiber.homMk p S φ)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.mul_natCast : ∀ {x : ℝ}, Irrational x → ∀ {m : ℕ}, m ≠ 0 → Irrational (x * ↑m)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors.congr_simp : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  (a a_1 : M), a = a_1 → UniqueFactorizationMonoid.primeFactors a = UniqueFactorizationMonoid.primeFactors a_1
-- Mathlib.Algebra.Order.Sub.Basic
zero_tsub : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] (a : α), 0 - a = 0
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.exists_equivalence_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.LocallySmall.{w', v, u} C],
  (∃ J x, Nonempty (P.FullSubcategory ≌ J)) ↔ CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P