mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.emptyGraph_eq_bot : ∀ (V : Type u), SimpleGraph.emptyGraph V = ⊥
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.coe_inj : ∀ {R : Type u_1} [inst : Zero R] {f g : ArithmeticFunction R}, ⇑f = ⇑g ↔ f = g
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.collect : Lean.Expr → Bool → Lean.Meta.Grind.CollectorM✝ Unit
-- Mathlib.Data.List.Triplewise
List.Triplewise.nil : ∀ {α : Type u_1} {p : α → α → α → Prop}, List.Triplewise p []
-- Mathlib.RingTheory.Perfection
Perfection.coeff_iterate_symm_frobeniusEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (f : Perfection R p)
  (n m : ℕ),
  (Perfection.coeff R p n) ((⇑(frobeniusEquiv (Perfection R p) p).symm)^[m] f) = (Perfection.coeff R p (n + m)) f
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_ne_bot : ∀ {α : Type u} [inst : Add α] {x y : WithBot α}, x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
PresheafOfModules.restrictScalarsObj_obj : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M' : PresheafOfModules R') (α : R ⟶ R') (X : Cᵒᵖ),
  (M'.restrictScalarsObj α).obj X = (ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.toFun_eq_coe : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N), (↑f).toFun = ⇑f
-- Mathlib.Order.Max
IsMin.snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMin x → IsMin x.2
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_comp_lTensor : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P),
  dualTensorHom R M P ∘ₗ LinearMap.lTensor (Module.Dual R M) f = LinearMap.compRight R f ∘ₗ dualTensorHom R M N
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.hom_l_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S₁ S₂ : CategoryTheory.Span Wₗ Wᵣ c c'} (self : S₁.Hom S₂) {Z : C} (h : c ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp S₂.l h) =
    CategoryTheory.CategoryStruct.comp S₁.l h
-- Mathlib.Algebra.DirectSum.Ring
/-- The canonical map from ℤ to the zeroth component of a graded ring.  -/
DirectSum.GRing.intCast : {ι : Type u_1} →
  {A : ι → Type u_2} →
    {inst : AddMonoid ι} → {inst_1 : (i : ι) → AddCommGroup (A i)} → [self : DirectSum.GRing A] → ℤ → A 0
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
_private.Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete.0.CategoryTheory.Functor.incl : (I : Type u₂) → [inst : CategoryTheory.Category.{v₂, u₂} I] → CategoryTheory.Functor (CategoryTheory.Discrete I) I
-- Init.Data.ByteArray.Basic
/-- A left fold on `ByteArray` that iterates over an array from low to high indices, computing a
running value.

Each element of the array is combined with the value from the prior elements using a function
`f`. The initial value `init` is the starting value before any elements have been
processed.

`ByteArray.foldlM` is a monadic variant of this function.
 -/
ByteArray.foldl : {β : Type v} → (β → UInt8 → β) → β → (as : ByteArray) → optParam ℕ 0 → optParam ℕ as.size → β
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasPluralDefaults.singular : {α : Sort u_1} → [self : Lean.HasPluralDefaults✝ α] → α
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.Monadic.isPlausibleSuccessorOf_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  {it' it : Std.IterM Id α},
  it'.IsPlausibleSuccessorOf it ↔
    ∃ a,
      it.internalState.next = some a ∧
        a < it.internalState.upperBound ∧
          Std.PRange.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.homologyMap_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.ShortComplex.homologyMap (φ - φ') =
    CategoryTheory.ShortComplex.homologyMap φ - CategoryTheory.ShortComplex.homologyMap φ'
-- Mathlib.Analysis.Matrix.PosDef
Matrix.eigenvalues_self_mul_conjTranspose_nonneg : ∀ {m : Type u_1} {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : RCLike 𝕜]
  (A : Matrix m n 𝕜) [inst_3 : DecidableEq m] (i : m), 0 ≤ ⋯.eigenvalues i
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite products of analytic functions are analytic  -/
Finset.analyticOnNhd_prod : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_9} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : α → E → A}
  {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) → AnalyticOnNhd 𝕜 (∏ n ∈ N, f n) s
-- Mathlib.Probability.Independence.Kernel.Indep
/-- 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.Kernel.IndepSet : {α : Type u_1} →
  {Ω : Type u_2} →
    {_mα : MeasurableSpace α} →
      {_mΩ : MeasurableSpace Ω} →
        Set Ω →
          Set Ω →
            ProbabilityTheory.Kernel α Ω →
              autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.IndepSet._auto_1 → Prop
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Under.instUniqueHomTopMkId : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      {X : T} →
        [inst_1 : P.ContainsIdentities] →
          (Y : P.Under ⊤ X) →
            Unique (CategoryTheory.MorphismProperty.Under.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯ ⟶ Y)
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The terminal object in `Type u` is `PUnit`.  -/
CategoryTheory.Limits.Types.terminalIso : ⊤_ Type u ≅ PUnit.{u + 1}
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Mul β]
  [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.Kernel.IndepFun (f i) (f j * f k) κ μ
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.IsNatPowModT.run' : ∀ {p : Prop} {a b m c : ℕ}, Mathlib.Meta.NormNum.IsNatPowModT p a b m c → p → (a.pow b).mod m = c
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] [inst_1 : StarMul α] (w : m → α) (v : n → α),
  (Matrix.vecMulVec w v).conjTranspose = Matrix.vecMulVec (star v) (star w)
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisseLimit.ultrahomogeneous : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} {M : Type w} [inst : L.Structure M]
  [inst_1 : Countable ((l : ℕ) × L.Functions l)] [inst_2 : Countable M],
  FirstOrder.Language.IsFraisseLimit K M → L.IsUltrahomogeneous M
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_atTop_zsmul_iff_nsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] [inst_1 : TopologicalSpace G] {x y : G},
  (MapClusterPt x Filter.atTop fun x => x • y) ↔ MapClusterPt x Filter.atTop fun x => x • y
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
DifferentiableAt.clog : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → f x ∈ Complex.slitPlane → DifferentiableAt ℂ (fun t => Complex.log (f t)) x
-- Mathlib.Algebra.CharP.Quotient
/-- `CharP.quotient_iff`, but stated in terms of inclusions of ideals.  -/
CharP.quotient_iff_le_ker_natCast : ∀ {R : Type u_1} [inst : CommRing R] (n : ℕ) [CharP R n] (I : Ideal R),
  CharP (R ⧸ I) n ↔ Ideal.comap (Nat.castRingHom R) I ≤ RingHom.ker (Nat.castRingHom R)
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_principal : ∀ {α : Type u} {β : Type v} {s : Set α} {f g : α → β}, f =ᶠ[Filter.principal s] g ↔ Set.EqOn f g s
-- Mathlib.Topology.Compactness.Lindelof
HereditarilyLindelof.to_Lindelof : ∀ {X : Type u} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X], LindelofSpace X
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.instToExprConstraint : Lean.ToExpr Lean.Omega.Constraint
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.forget_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.AddMonObj A] (A_1 : CategoryTheory.AddMod D A),
  (CategoryTheory.AddMod.forget A).obj A_1 = A_1.X
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.PreservesCoproduct.inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G],
  (CategoryTheory.Limits.PreservesCoproduct.iso G f).inv = CategoryTheory.Limits.sigmaComparison G f
-- Mathlib.Topology.Order.LawsonTopology
/-- The Lawson topology is defined as the meet of `Topology.lower` and the `Topology.scott`.
 -/
Topology.lawson : (α : Type u_2) → [Preorder α] → TopologicalSpace α
-- Mathlib.Data.ENNReal.Basic
ENNReal.iUnion_Ico_coe_nat : ∀ {a : ENNReal}, ⋃ n, Set.Ico a ↑n = Set.Ici a \ {⊤}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₂.getKey k ⋯
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.restrict_self : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  {F : TopCat.Presheaf C X} {U : TopologicalSpace.Opens ↑X} (x : CategoryTheory.ToType (F.obj (Opposite.op U))),
  TopCat.Presheaf.restrictOpen x U ⋯ = x
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.mem_iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} [K.IsStableUnderComposition]
  [K.HasIsos] {X : C} {E F : CategoryTheory.PreZeroHypercover X} (e : E ≅ F),
  E.presieve₀ ∈ K.coverings X ↔ F.presieve₀ ∈ K.coverings X
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCancelCommMonoid : {α : Type u_1} → [AddCancelCommMonoid α] → AddCancelCommMonoid (Colex α)
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_roi_eq_mkSlice_roo_min : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ},
  Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rco.Sliceable.mkSlice xs (min (lo + 1) xs.size)...xs.size
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Cache.mk.inj : ∀ {backwardRuleName : Lean.PHashMap Lean.Name Lean.Meta.Sym.BackwardRule}
  {backwardRuleSyntax : Lean.PHashMap (ℕ × ℕ) Lean.Meta.Sym.BackwardRule}
  {simpState : Std.HashMap Lean.Elab.Tactic.Grind.SimpCacheKey Lean.Meta.Sym.Simp.State}
  {dsimpState : Std.HashMap Lean.Elab.Tactic.Grind.DSimpCacheKey Lean.Meta.Sym.DSimp.State}
  {backwardRuleName_1 : Lean.PHashMap Lean.Name Lean.Meta.Sym.BackwardRule}
  {backwardRuleSyntax_1 : Lean.PHashMap (ℕ × ℕ) Lean.Meta.Sym.BackwardRule}
  {simpState_1 : Std.HashMap Lean.Elab.Tactic.Grind.SimpCacheKey Lean.Meta.Sym.Simp.State}
  {dsimpState_1 : Std.HashMap Lean.Elab.Tactic.Grind.DSimpCacheKey Lean.Meta.Sym.DSimp.State},
  { backwardRuleName := backwardRuleName, backwardRuleSyntax := backwardRuleSyntax, simpState := simpState,
        dsimpState := dsimpState } =
      { backwardRuleName := backwardRuleName_1, backwardRuleSyntax := backwardRuleSyntax_1, simpState := simpState_1,
        dsimpState := dsimpState_1 } →
    backwardRuleName = backwardRuleName_1 ∧
      backwardRuleSyntax = backwardRuleSyntax_1 ∧ simpState = simpState_1 ∧ dsimpState = dsimpState_1
-- Lean.Elab.Calc
/-- View of a `calcStep`.  -/
Lean.Elab.Term.CalcStepView : Type
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadLift_Id : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPred} (x : Id α), ⦃ post x.run ⦄ monadLift x ⦃ post; epost ⦄
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : Type w} {inst_1 : AddMonoid A}
  {inst_2 : CategoryTheory.HasShift C A} {z : A → A → (CategoryTheory.CatCenter C)ˣ}
  {z_zero_zero : autoParam (z 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam}
  {assoc :
    autoParam (∀ (a b c : A), z (a + b) c * z a b = z a (b + c) * z b c) CategoryTheory.TwistShiftData.assoc._autoParam}
  {commShift :
    autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z a b)) A)
      CategoryTheory.TwistShiftData.commShift._autoParam}
  {z_1 : A → A → (CategoryTheory.CatCenter C)ˣ}
  {z_zero_zero_1 : autoParam (z_1 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam}
  {assoc_1 :
    autoParam (∀ (a b c : A), z_1 (a + b) c * z_1 a b = z_1 a (b + c) * z_1 b c)
      CategoryTheory.TwistShiftData.assoc._autoParam}
  {commShift_1 :
    autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z_1 a b)) A)
      CategoryTheory.TwistShiftData.commShift._autoParam},
  { z := z, z_zero_zero := z_zero_zero, assoc := assoc, commShift := commShift } =
      { z := z_1, z_zero_zero := z_zero_zero_1, assoc := assoc_1, commShift := commShift_1 } →
    z = z_1
-- Mathlib.GroupTheory.Frattini
frattini_le_comap_frattini_of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {φ : G →* H},
  Function.Surjective ⇑φ → frattini G ≤ Subgroup.comap φ (frattini H)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.piCongrLeft'_apply : ∀ {ι : Type u_2} {ι' : Type u_3} [inst : Fintype ι] [inst_1 : Fintype ι'] {Y : ι → Type u_4}
  [inst_2 : (j : ι) → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') (f : (a : ι) → Y a) (x : ι'),
  (IsometryEquiv.piCongrLeft' e) f x = f (e.symm x)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] {f : α → Bool} {k : α}
  {h' : k ∈ Std.TreeSet.Raw.filter f t} (h : t.WF), (Std.TreeSet.Raw.filter f t).get k h' = t.get k ⋯
-- Batteries.Tactic.Lint.Frontend
/-- Runs all the specified linters on all the specified declarations in parallel,
producing a list of results.
 -/
Batteries.Tactic.Lint.lintCore : Array Lean.Name →
  Array Batteries.Tactic.Lint.NamedLinter →
    optParam (Option Lean.Name) none →
      optParam Bool false →
        Lean.CoreM (Array (Batteries.Tactic.Lint.NamedLinter × Std.HashMap Lean.Name Lean.MessageData))
-- Mathlib.CategoryTheory.Adhesive.Subobject
CategoryTheory.Adhesive.instHasBinaryCoproductsSubobject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Adhesive C] {X : C},
  CategoryTheory.Limits.HasBinaryCoproducts (CategoryTheory.Subobject X)
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_multiset_prod : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  (s : Multiset α),
  0 ∉ s →
    UniqueFactorizationMonoid.normalizedFactors s.prod =
      (Multiset.map UniqueFactorizationMonoid.normalizedFactors s).sum
-- Aesop.EMap
/-- A map whose keys are expressions. Keys are identified up to defeq. We use
`reducible` transparency and treat metavariables as rigid (i.e.,
unassignable).  -/
Aesop.EMap : Type u_1 → Type u_1
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.mem_supClosure_iff : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α}, MeasureTheory.IsSetSemiring C → (s ∈ supClosure C ↔ ∃ P, ↑P.parts ⊆ C)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The category of Eilenberg-Moore coalgebras for a comonad.  -/
CategoryTheory.Comonad.Coalgebra.instCategoryStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : CategoryTheory.Comonad C} → CategoryTheory.CategoryStruct.{v₁, max u₁ v₁} G.Coalgebra
-- Init.Data.Float.Float32
/-- Efficiently computes `x * 2^i`.

This function does not reduce in the kernel.
 -/
Float32.scaleB : Float32 → ℤ → Float32
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C),
  (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Order.CompleteLattice.Basic
iInf_neg : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : p → α}, ¬p → ⨅ (h : p), f h = ⊤
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A : C} {a : T.obj A ⟶ A}
  {unit :
    autoParam (CategoryTheory.CategoryStruct.comp (T.η.app A) a = CategoryTheory.CategoryStruct.id A)
      CategoryTheory.Monad.Algebra.unit._autoParam}
  {assoc :
    autoParam (CategoryTheory.CategoryStruct.comp (T.μ.app A) a = CategoryTheory.CategoryStruct.comp (T.map a) a)
      CategoryTheory.Monad.Algebra.assoc._autoParam}
  {A_1 : C} {a_1 : T.obj A_1 ⟶ A_1}
  {unit_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (T.η.app A_1) a_1 = CategoryTheory.CategoryStruct.id A_1)
      CategoryTheory.Monad.Algebra.unit._autoParam}
  {assoc_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (T.μ.app A_1) a_1 = CategoryTheory.CategoryStruct.comp (T.map a_1) a_1)
      CategoryTheory.Monad.Algebra.assoc._autoParam},
  { A := A, a := a, unit := unit, assoc := assoc } = { A := A_1, a := a_1, unit := unit_1, assoc := assoc_1 } →
    A = A_1 ∧ a ≍ a_1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.dense_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.ball x r ∩ s).Nonempty
-- Mathlib.GroupTheory.Divisible
Group.rootableByIntOfRootableByNat.eq_1 : ∀ (A : Type u_1) [inst : Group A] [inst_1 : RootableBy A ℕ],
  Group.rootableByIntOfRootableByNat A =
    {
      root := fun a z =>
        match z with
        | Int.ofNat n => RootableBy.root a n
        | Int.negSucc n => (RootableBy.root a (n + 1))⁻¹,
      root_zero := ⋯, root_cancel := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.universally_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Monotone CategoryTheory.MorphismProperty.universally
-- Mathlib.RingTheory.Binomial
Ring.choose_one_right : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (r : R),
  Ring.choose r 1 = r
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M},
  VectorField.mpullbackWithin I I' f 0 s = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.IsIntegral.mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] {W : WeierstrassCurve K},
  (∃ W_int, W = W_int.baseChange K) → WeierstrassCurve.IsIntegral R W
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (toCommSq : CategoryTheory.CommSq f g inl inr),
  Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr ⋯)) →
    CategoryTheory.IsPushout f g inl inr
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.LaxMonoidalFunctor.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (toFunctor : CategoryTheory.Functor C D)
  (laxMonoidal : autoParam toFunctor.LaxMonoidal CategoryTheory.LaxMonoidalFunctor.laxMonoidal._autoParam)
  (toFunctor_1 : CategoryTheory.Functor C D)
  (laxMonoidal_1 : autoParam toFunctor_1.LaxMonoidal CategoryTheory.LaxMonoidalFunctor.laxMonoidal._autoParam),
  ({ toFunctor := toFunctor, laxMonoidal := laxMonoidal } =
      { toFunctor := toFunctor_1, laxMonoidal := laxMonoidal_1 }) =
    (toFunctor = toFunctor_1 ∧ laxMonoidal ≍ laxMonoidal_1)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addCHaar_sup_le : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} (K₁ K₂ : TopologicalSpace.Compacts G),
  MeasureTheory.Measure.haar.addCHaar K₀ (K₁ ⊔ K₂) ≤
    MeasureTheory.Measure.haar.addCHaar K₀ K₁ + MeasureTheory.Measure.haar.addCHaar K₀ K₂
-- Mathlib.Algebra.Notation.Support
Function.range_subset_insert_image_mulSupport : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] (f : ι → M), Set.range f ⊆ insert 1 (f '' Function.mulSupport f)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α]
  (s : NonemptyInterval α) (n : ℕ), (n • s).toProd.1 = n • s.toProd.1