mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Int.Bitwise
Int.bitwise.eq_3 : ∀ (f : Bool → Bool → Bool) (m n : ℕ),
  Int.bitwise f (Int.negSucc m) (Int.ofNat n) = Int.natBitwise (fun x y => f (!x) y) m n
-- Mathlib.Order.Hom.BoundedLattice
/-- Special case of `map_compl` for Boolean algebras.  -/
map_compl' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
  [inst_2 : FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) (a : α), f aᶜ = (f a)ᶜ
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- The radius of the sum of two formal series is at least the minimum of their two radii.  -/
FormalMultilinearSeries.min_radius_le_radius_add : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p q : FormalMultilinearSeries 𝕜 E F), min p.radius q.radius ≤ (p + q).radius
-- Mathlib.Algebra.GroupWithZero.Prod
Prod.instSemigroupWithZero : {M₀ : Type u_1} → {N₀ : Type u_2} → [SemigroupWithZero M₀] → [SemigroupWithZero N₀] → SemigroupWithZero (M₀ × N₀)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Birational.symm : ∀ {X Y : AlgebraicGeometry.Scheme}, X.Birational Y → Y.Birational X
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.divRight_apply : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (x b : G),
  (Homeomorph.divRight x) b = b / x
-- Aesop.BaseM
/-- Run a `BaseM` action.  -/
Aesop.BaseM.run : {α : Type} → Aesop.BaseM α → optParam Aesop.Stats ∅ → Lean.MetaM (α × Aesop.Stats)
-- Std.Time.Format.Basic
Std.Time.FormatPart.string.inj : ∀ {val val_1 : String}, Std.Time.FormatPart.string val = Std.Time.FormatPart.string val_1 → val = val_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_add : ∀ {x : ℝ}, 0 < x → ∀ (y z : ℝ), x ^ (y + z) = x ^ y * x ^ z
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind.command : Lean.Elab.DocElabKind
-- Mathlib.Topology.Order.Lattice
Continuous.finset_inf' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} (hne : s.Nonempty),
  (∀ i ∈ s, Continuous (f i)) → Continuous (s.inf' hne f)
-- Lean.Meta.Sym.Simp.SimpM
/-- Number of steps performed so far.  -/
Lean.Meta.Sym.Simp.State.numSteps : Lean.Meta.Sym.Simp.State → ℕ
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.coe_trans : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  ↑(e.trans e') = ↑e' ∘ ↑e
-- Mathlib.Topology.Instances.EReal.Lemmas
Continuous.ereal_toENNReal : ∀ {α : Type u_2} [inst : TopologicalSpace α] {f : α → EReal}, Continuous f → Continuous fun x => (f x).toENNReal
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_orbit_of_mem_orbit : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] {a₁ a₂ : α} (m : M),
  a₂ ∈ MulAction.orbit M a₁ → m • a₂ ∈ MulAction.orbit M a₁
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_modEq_x2n_add : ∀ {a : ℕ} (a1 : 1 < a) (n j : ℕ), Pell.xn a1 (2 * n + j) + Pell.xn a1 j ≡ 0 [MOD Pell.xn a1 n]
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The local lifting through a Trivialization `T` from the base to the leaf containing `z`.  -/
Bundle.Trivialization.lift : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} → [inst_2 : TopologicalSpace Z] → Bundle.Trivialization F proj → Z → B → Z
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
eq_const_of_measurable_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] [Nonempty β] [MeasurableSpace.SeparatesPoints β] {f : α → β},
  Measurable f → ∃ c, f = fun x => c
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph.eq_1 : SimpleGraph.cycleGraph 0 = ⊥
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_const : ∀ {M : Type u_2} [inst : AddCommMonoid M] (n : ℕ) (x : M), ∑ _i, x = n • x
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D}
  {K : CategoryTheory.GrothendieckTopology D},
  (∀ (U : D), CategoryTheory.Sieve.coverByImage G U ∈ K U) → G.IsCoverDense K
-- Mathlib.Algebra.Azumaya.Defs
IsAzumaya.bij : ∀ {R : Type u_1} {A : Type u_2} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  [self : IsAzumaya R A], Function.Bijective ⇑(AlgHom.mulLeftRight R A)
-- Aesop.RuleSet
Aesop.LocalRuleSet.erase : Aesop.LocalRuleSet → Aesop.RuleFilter → Aesop.LocalRuleSet × Bool
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.mem₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (self : J.OneHypercover S) (i₁ i₂ : self.I₀) ⦃W : C⦄ (p₁ : W ⟶ self.X i₁) (p₂ : W ⟶ self.X i₂),
  CategoryTheory.CategoryStruct.comp p₁ (self.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (self.f i₂) →
    self.sieve₁ p₁ p₂ ∈ J W
-- Mathlib.Data.Fintype.EquivFin
instInfiniteMultisetOfNonempty : ∀ {α : Type u_1} [Nonempty α], Infinite (Multiset α)
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- The sum of two compactly generated spaces is compactly generated.  -/
instUCompactlyGeneratedSpaceSum : ∀ {X : Type w} {Y : Type x} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [UCompactlyGeneratedSpace X]
  [UCompactlyGeneratedSpace Y], UCompactlyGeneratedSpace (X ⊕ Y)
-- Init.SizeOf
Lean.ParserDescr.sepBy.sizeOf_spec : ∀ (p : Lean.ParserDescr) (sep : String) (psep : Lean.ParserDescr) (allowTrailingSep : optParam Bool false),
  sizeOf (p.sepBy sep psep allowTrailingSep) = 1 + sizeOf p + sizeOf sep + sizeOf psep + sizeOf allowTrailingSep
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.ofNat.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.rightAdjoint.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [inst_2 : R.IsLeftAdjoint], R.rightAdjoint = ⋯.choose
-- Std.Time.Date.ValidDate
Std.Time.instLawfulEqOrdValidDate : ∀ {leap : Bool}, Std.LawfulEqOrd (Std.Time.ValidDate leap)
-- Init.Data.List.Sublist
List.replicate_subset : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, List.replicate n a ⊆ l ↔ n = 0 ∨ a ∈ l
-- Mathlib.Algebra.Ring.Prod
RingHom.coe_fst : ∀ {R : Type u_1} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S], ⇑(RingHom.fst R S) = Prod.fst
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasRightResolutions_of_iso_of_essSurj_of_full : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [L.functor.EssSurj] [R.functor.Full] [R.IsInduced] [W₂'.RespectsIso]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor) [B.HasRightResolutions], T.HasRightResolutions
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).getD fallback
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates finite colimits, then `F.unop : C ⥤ D` creates finite
limits.  -/
CategoryTheory.Limits.createsFiniteLimitsUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteColimits F] → CategoryTheory.Limits.CreatesFiniteLimits F.unop
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The `L^p` product of two linear isometric equivalences.  -/
LinearIsometryEquiv.withLpProdCongr : (p : ENNReal) →
  {𝕜 : Type u_1} →
    {α : Type u_2} →
      {β : Type u_3} →
        {α' : Type u_5} →
          {β' : Type u_6} →
            [hp : Fact (1 ≤ p)] →
              [inst : Semiring 𝕜] →
                [inst_1 : SeminormedAddCommGroup α] →
                  [inst_2 : Module 𝕜 α] →
                    [inst_3 : SeminormedAddCommGroup β] →
                      [inst_4 : Module 𝕜 β] →
                        [inst_5 : SeminormedAddCommGroup α'] →
                          [inst_6 : Module 𝕜 α'] →
                            [inst_7 : SeminormedAddCommGroup β'] →
                              [inst_8 : Module 𝕜 β'] →
                                (α ≃ₗᵢ[𝕜] α') → (β ≃ₗᵢ[𝕜] β') → WithLp p (α × β) ≃ₗᵢ[𝕜] WithLp p (α' × β')
-- Init.Data.Slice.Array.Lemmas
Std.IterStep.mapIterator.eq_2 : ∀ {α : Type u} {β : Type w} {α' : Type u'} (f : α → α') (it : α),
  Std.IterStep.mapIterator f (Std.IterStep.skip it) = Std.IterStep.skip (f it)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.le_map_comap : ∀ {X Y : AlgebraicGeometry.Scheme} (J : Y.IdealSheafData) (f : X ⟶ Y), J ≤ (J.comap f).map f
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.findMin'.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → α → Sort u_2) (x : α) (h_1 : (x : α) → motive Ordnode.nil x)
  (h_2 : (size : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → (x_1 : α) → motive (Ordnode.node size l x r) x_1),
  (match Ordnode.nil, x with
    | Ordnode.nil, x => h_1 x
    | Ordnode.node size l x r, x_1 => h_2 size l x r x_1) =
    h_1 x
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_neg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P), ((signedDist (-v)) p) q = -((signedDist v) p) q
-- Batteries.Data.List.Lemmas
List.dropPrefix?_eq_some_iff : ∀ {α : Type u_1} [inst : BEq α] {l p s : List α}, l.dropPrefix? p = some s ↔ ∃ p', l = p' ++ s ∧ (p' == p) = true
-- Init.System.Promise
/-- Resolves a `Promise`.

Only the first call to this function has an effect.
 -/
IO.Promise.resolve : {α : Type} → α → IO.Promise α → BaseIO Unit
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.continuousAt_sign : ∀ {θ : Real.Angle}, θ ≠ 0 → θ ≠ ↑Real.pi → ContinuousAt Real.Angle.sign θ
-- Mathlib.Topology.Algebra.InfiniteSum.Group
summable_subtype_and_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α] {f : β → α}
  [CompleteSpace α] {s : Set β}, ((Summable fun x => f ↑x) ∧ Summable fun x => f ↑x) ↔ Summable f
-- Init.Control.Lawful.Basic
pure_seqRight : ∀ {f : Type u_1 → Type u_2} {α β : Type u_1} [inst : Applicative f] [LawfulApplicative f] (x : α) (y : f β),
  pure x *> y = y
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.toArray_eq_toArray_iter : ∀ {γ : Type u} {α β : Type v} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id], s.toArray = s.iter.toArray
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.monotone_sort : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] (f : Fin n → α), Monotone (f ∘ ⇑(Tuple.sort f))
-- Mathlib.Topology.Defs.Basic
/-- A set is closed if its complement is open  -/
IsClosed : {X : Type u} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.Order.CompleteLattice.Basic
Equiv.iInf_comp : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : InfSet α] {g : ι' → α} (e : ι ≃ ι'), ⨅ x, g (e x) = ⨅ y, g y
-- Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain
IsNoetherianRing.wfDvdMonoid : ∀ {R : Type u_1} [inst : CommSemiring R] [IsDomain R] [h : IsNoetherianRing R], WfDvdMonoid R
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_lt_comap_iff_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑f → ∀ {p q : Submodule R₂ M₂}, Submodule.comap f p < Submodule.comap f q ↔ p < q
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.MethodsRef : Type
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
CategoryTheory.Monoidal.Transported.instBraidedCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) →
          [inst_2 : CategoryTheory.MonoidalCategory C] →
            [CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory (CategoryTheory.Monoidal.Transported e)
-- Init.Data.BitVec.Lemmas
BitVec.self_eq_add_left : ∀ {w : ℕ} {x y : BitVec w}, x = y + x ↔ y = 0#w
-- Std.Data.String.ToNat
Nat.repr_inj : ∀ {m n : ℕ}, m.repr = n.repr ↔ m = n
-- Batteries.Logic
/-- **Alias** of `congrArg`. -/
congr_arg : ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
-- Init.Data.List.Basic
List.pairwise_cons : ∀ {α : Type u} {R : α → α → Prop} {a : α} {l : List α},
  List.Pairwise R (a :: l) ↔ (∀ a' ∈ l, R a a') ∧ List.Pairwise R l
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The ring equiv between the top element of `NonUnitalSubsemiring R` and `R`.  -/
NonUnitalSubsemiring.topEquiv : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → ↥⊤ ≃+* R
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.mkAddMonoidHom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ) (x : CochainComplex.HomComplex.Cocycle K L n),
  (CochainComplex.HomComplex.CohomologyClass.mkAddMonoidHom K L n) x = CochainComplex.HomComplex.CohomologyClass.mk x
-- Mathlib.RingTheory.LocalRing.ResidueField.Defs
IsLocalRing.ResidueField.field : (R : Type u_1) → [inst : CommRing R] → [inst_1 : IsLocalRing R] → Field (IsLocalRing.ResidueField R)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey!
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
EReal.instMeasurableAdd₂ : MeasurableAdd₂ EReal
-- Mathlib.Data.Multiset.MapFold
Multiset.attach_map_val : ∀ {α : Type u_1} (s : Multiset α), Multiset.map Subtype.val s.attach = s
-- Mathlib.RingTheory.HahnSeries.HahnEmbedding
instNonemptySeedRatReal : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [inst_3 : Module ℚ M]
  [inst_4 : IsOrderedModule ℚ M], Nonempty (HahnEmbedding.Seed ℚ M ℝ)
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- If `f` is continuous at `a` and differentiable on `Ioo a b`, then `f` is continuous on
`Ico a b`.  -/
_private.Mathlib.Analysis.Calculus.DerivativeTest.0.continuousOn_Ico : ∀ {f : ℝ → ℝ} {a b : ℝ}, ContinuousAt f a → DifferentiableOn ℝ f (Set.Ioo a b) → ContinuousOn f (Set.Ico a b)
-- Batteries.Classes.Order
/-- `cmp x y ≠ .gt` holds iff `x ≤ y` is true.  -/
Std.LawfulCmp.isLE_iff_le : ∀ {α : Type u_1} {inst : LE α} {inst_1 : LT α} {cmp : α → α → Ordering} [self : Std.LawfulCmp cmp] {x y : α},
  (cmp x y).isLE = true ↔ x ≤ y
-- Batteries.Data.Array.Scan
Array.scanl_map : ∀ {γ : Type u_1} {β : Type u_2} {α : Type u_3} {f : γ → β → γ} {g : α → β} (init : γ) (as : Array α),
  Array.scanl f init (Array.map g as) = Array.scanl (fun x1 x2 => f x1 (g x2)) init as
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.mk.sizeOf_spec : ∀ {α : Type u_5} {β : Type u_6} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toMonoidHom : α →* β) (map_zero' : (↑toMonoidHom).toFun 0 = 0)
  (map_add' : ∀ (x y : α), (↑toMonoidHom).toFun (x + y) = (↑toMonoidHom).toFun x + (↑toMonoidHom).toFun y),
  sizeOf { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' } =
    1 + sizeOf toMonoidHom + sizeOf map_zero'
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovary_neg`. -/
Monovary.neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β},
  Monovary f g → Monovary (-f) (-g)
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.map.eq_1 : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (T : Turing.Tape Γ),
  Turing.Tape.map f T =
    { head := f.f T.head, left := Turing.ListBlank.map f T.left, right := Turing.ListBlank.map f T.right }
-- Mathlib.Algebra.Module.Presentation.Basic
/-- If `M` admits a presentation by generators and relations, and we have a solution of the
same equations in a module `N`, then this is the canonical induced linear map `M →ₗ[A] N`.  -/
Module.Relations.Solution.IsPresentation.desc : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            {solution : relations.Solution M} →
              solution.IsPresentation →
                {N : Type v'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → relations.Solution N → M →ₗ[A] N
-- Init.Data.Option.Attach
Option.get!_attach : ∀ {α : Type u_1} {o : Option α} [inst : Inhabited { x // o = some x }], o.attach.get! = default
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is an algebraic extension, `F` is separably closed,
then `E` is also separably closed.  -/
Algebra.IsAlgebraic.isSepClosed : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E]
  [IsSepClosed F], IsSepClosed E
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- A `PreSubmersivePresentation` is submersive if its Jacobian is a unit in `S`
and the presentation is finite.
 -/
Algebra.SubmersivePresentation : (R : Type u) →
  (S : Type v) →
    Type w →
      (σ : Type t) →
        [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → [Finite σ] → Type (max (max (max t u) v) w)
-- Mathlib.GroupTheory.OrderOfElement
/-- See `Subgroup.closure_toSubmonoid_of_finite` for a version for finite groups.  -/
Subgroup.closure_toSubmonoid_of_isOfFinOrder : ∀ {G : Type u_1} [inst : Group G] {s : Set G},
  (∀ x ∈ s, IsOfFinOrder x) → (Subgroup.closure s).toSubmonoid = Submonoid.closure s
-- Init.Data.List.Attach
List.getElem_unattach : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} (i : ℕ) (h : i < l.unattach.length), l.unattach[i] = ↑l[i]
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  H.mapCone c = (CategoryTheory.Limits.Cone.functoriality F H).obj c
-- Mathlib.Topology.Closure
closure_iUnion₂_lt_nat : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} (f : ℕ → Set X),
  closure (⋃ m, ⋃ (_ : m < n), f m) = ⋃ m, ⋃ (_ : m < n), closure (f m)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun_apply' : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.convexBodySumFun x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it : Std.IterM m α)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSet_iff_indepSets_singleton : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s t : Set Ω} {m0 : MeasurableSpace Ω},
  MeasurableSet s →
    MeasurableSet t →
      ∀ (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
        ProbabilityTheory.Kernel.IndepSet s t κ μ ↔ ProbabilityTheory.Kernel.IndepSets {s} {t} κ μ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- `ms.leadingExp = ⊥` iff `ms = []`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_eq_bot : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
  s.leadingExp = ⊥ ↔ s = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_one : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.charpoly 1 = (Polynomial.X - 1) ^ Fintype.card n
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.mk.injEq : ∀ (A : Type uA) (B : A → Type uB) (A_1 : Type uA) (B_1 : A_1 → Type uB),
  ({ A := A, B := B } = { A := A_1, B := B_1 }) = (A = A_1 ∧ B ≍ B_1)
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_replicate_zero : ∀ {b k : ℕ}, Nat.ofDigits b (List.replicate k 0) = 0
-- Init.Data.List.Perm
List.filter_append_perm : ∀ {α : Type u_1} (p : α → Bool) (l : List α), (List.filter p l ++ List.filter (fun x => !p x) l).Perm l
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.instCeilDiv : {ι : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : AddCommMonoid α] →
        [inst_1 : PartialOrder α] →
          [inst_2 : AddCommMonoid β] →
            [inst_3 : PartialOrder β] → [inst_4 : SMulZeroClass α β] → [CeilDiv α β] → CeilDiv α (ι →₀ β)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.image_ι_eq : ∀ {Δ Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ CategoryTheory.Limits.image φ} [CategoryTheory.Epi e]
  {i : CategoryTheory.Limits.image φ ⟶ Δ''} [CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp e i = φ → CategoryTheory.Limits.image.ι φ = i
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.not_mem_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → k ∉ m₁ \ m₂
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.brecOn : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {motive : (a a_1 : M) → AddConGen.Rel r a a_1 → Prop} {a a_1 : M}
  (t : AddConGen.Rel r a a_1),
  (∀ (a a_2 : M) (t : AddConGen.Rel r a a_2), AddConGen.Rel.below t → motive a a_2 t) → motive a a_1 t