mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Notation
/-- A notation class for the *negative part* function: `a⁻`.  -/
NegPart : Type u_1 → Type u_1
-- Init.Data.Array.Lemmas
Array.exists_mem_iff_exists_getElem : ∀ {α : Type u_1} {P : α → Prop} {xs : Array α}, (∃ x ∈ xs, P x) ↔ ∃ i, ∃ (hi : i < xs.size), P xs[i]
-- Mathlib.Topology.MetricSpace.Completion
/-- The new distance is uniformly continuous.  -/
UniformSpace.Completion.uniformContinuous_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α], UniformContinuous fun p => dist p.1 p.2
-- Mathlib.Logic.Unique
/-- Construct `Unique` from `Inhabited` and `Subsingleton`. Making this an instance would create
a loop in the class inheritance graph.  -/
Unique.mk' : (α : Sort u) → [h₁ : Inhabited α] → [Subsingleton α] → Unique α
-- Mathlib.Order.Hom.Basic
OrderHom.mk_comp_mk : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : β → γ) (f : α → β) (hg : Monotone g) (hf : Monotone f),
  { toFun := g, monotone' := hg }.comp { toFun := f, monotone' := hf } = { toFun := g ∘ f, monotone' := ⋯ }
-- Std.Data.DTreeMap.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw`.
The `insertMany` function on `TreeSet` and `TreeSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.DTreeMap.insertMany : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {ρ : Type u_1} → [ForIn Id ρ ((a : α) × β a)] → Std.DTreeMap α β cmp → ρ → Std.DTreeMap α β cmp
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- Signs alternate along relations in the complex shape  -/
ComplexShape.EulerCharSigns.χ_next : ∀ {ι : Type u_1} {c : ComplexShape ι} [self : c.EulerCharSigns] {i j : ι},
  c.Rel i j → ComplexShape.EulerCharSigns.χ c j = -ComplexShape.EulerCharSigns.χ c i
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- A field extension `E / F` of exponential characteristic `q` is purely inseparable
if and only if for every element `x` of `E`, there exists a natural number `n` such that
`x ^ (q ^ n)` is contained in `F`.  -/
isPurelyInseparable_iff_pow_mem : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Ring E] [IsDomain E] [inst_3 : Algebra F E] (q : ℕ)
  [ExpChar F q], IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
-- Mathlib.Analysis.Convolution
/-- The symmetric definition of convolution where the bilinear operator is scalar multiplication.  -/
MeasureTheory.convolution_lsmul_swap : ∀ {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} [inst : NormedAddCommGroup F] {x : G} [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_4 : NormedSpace ℝ F]
  [inst_5 : AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] {f : G → 𝕜}
  {g : G → F}, MeasureTheory.convolution f g (ContinuousLinearMap.lsmul 𝕜 𝕜) μ x = ∫ (t : G), f (x - t) • g t ∂μ
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.IccInclusionRight.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] {a b c : α} [inst_2 : Fact (a ≤ b)],
  ContinuousMap.IccInclusionRight = ContinuousMap.IccInclusionRight
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filterMap f m).getKey? k = (m.getKey? k).pfilter fun x h' => (f x (m.get x ⋯)).isSome
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_exp : Measurable Complex.exp
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
Nat.divisors_card_eq_one_iff : ∀ (n : ℕ), n.divisors.card = 1 ↔ n = 1
-- Batteries.Data.HashMap.Basic
/-- Is the map empty?
```
(empty : Batteries.HashMap Int Int).isEmpty = true
(ofList [("one", 1), ("two", 2)]).isEmpty = false
```
 -/
Batteries.HashMap.isEmpty : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → Bool
-- Mathlib.Algebra.Category.Grp.EpiMono
CommGrpCat.forget_commGrp_preserves_mono : (CategoryTheory.forget CommGrpCat).PreservesMonomorphisms
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ContinuousLinearMap.Simps.apply : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] → [inst_7 : Module R₂ M₂] → (M₁ →SL[σ₁₂] M₂) → M₁ → M₂
-- Init.Data.Vector.Range
Vector.unzip_zipIdx_eq_prod : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, (xs.zipIdx i).unzip = (xs, Vector.range' i n)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_finsetSum : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_6} (s : Finset ι) {f : ι → α → G},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) → ∫ (a : α), ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ (a : α), f i a ∂μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.Const.alter! k f t) =
        if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome
        else Std.DTreeMap.Internal.Impl.contains k' t
-- Mathlib.Data.Part
_private.Mathlib.Data.Part.0.Part.ofOption.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match some a with
    | none => h_1 ()
    | some a => h_2 a) =
    h_2 a
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.toBackwardSearcher_eq : ∀ {c : Char} {s : String.Slice},
  String.Slice.Pattern.ToBackwardSearcher.toSearcher c s =
    String.Slice.Pattern.ToBackwardSearcher.toSearcher (fun x => x == c) s
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun'_apply : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a b : α),
  IncidenceAlgebra.muFun'✝ 𝕜 b a = if a = b then 1 else -∑ x ∈ (Finset.Ioc a b).attach, IncidenceAlgebra.muFun'✝ 𝕜 b ↑x
-- Aesop.RuleSet
Aesop.LocalRuleSet.applicableForwardRulesWith : Aesop.LocalRuleSet →
  Lean.Expr → (Aesop.ForwardRule → Bool) → Lean.MetaM (Array (Aesop.ForwardRule × Aesop.PremiseIndex))
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.domSMul : ∀ {G : Type u_3} {A : Type u_4} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : MeasurableSpace A] [inst_4 : TopologicalSpace A] [inst_5 : BorelSpace A] [inst_6 : ContinuousConstSMul G A]
  {μ : MeasureTheory.Measure A} (g : Gᵈᵐᵃ) [μ.Regular], (g • μ).Regular
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CanonArgKey.mk.sizeOf_spec : ∀ (f : Lean.Expr) (i : ℕ) (arg : Lean.Expr),
  sizeOf { f := f, i := i, arg := arg } = 1 + sizeOf f + sizeOf i + sizeOf arg
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.isoClosure_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C)
  [Q.IsClosedUnderIsomorphisms], P.isoClosure ≤ Q ↔ P ≤ Q
-- Mathlib.RingTheory.LocalRing.Quotient
IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotient : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (I : Ideal R) [IsArtinianRing (R ⧸ I)],
  ∃ n, IsLocalRing.maximalIdeal R ^ n ≤ I
-- Mathlib.RingTheory.Polynomial.RationalRoot
UniqueFactorizationMonoid.instIsIntegrallyClosed : ∀ {A : Type u_1} [inst : CommRing A] [IsDomain A] [UniqueFactorizationMonoid A], IsIntegrallyClosed A
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.instReprOffset : Repr Std.Time.TimeZone.Offset
-- Mathlib.Computability.TuringMachine.Tape
Turing.Dir.left : Turing.Dir
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Except.toBool.match_1.splitter : {ε : Type u_1} →
  {α : Type u_2} →
    (motive : Except ε α → Sort u_3) →
      (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((a : ε) → motive (Except.error a)) → motive x
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.AffineTargetMorphismProperty.diagonal.congr_simp : ∀ (P P_1 : AlgebraicGeometry.AffineTargetMorphismProperty),
  P = P_1 →
    ∀ ⦃X Y : AlgebraicGeometry.Scheme⦄ (x x_1 : X ⟶ Y),
      x = x_1 → ∀ [inst : AlgebraicGeometry.IsAffine Y], P.diagonal x = P_1.diagonal x_1
-- Mathlib.Data.List.Infix
List.length_tails : ∀ {α : Type u_1} (l : List α), l.tails.length = l.length + 1
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CategoryTheory.Limits.KernelFork.map.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} {f : X ⟶ Y} (c c_1 : CategoryTheory.Limits.KernelFork f),
  c = c_1 → ∀ (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms], c.map G = c_1.map G
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.WeakRankFunction.lt : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] (self : h.WeakRankFunction α)
  {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → self.rank x < self.rank y
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.commute_inl_inr : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : DecidablePred fun x => x = 0] (m : G₀) (n : H₀),
  Commute ((MonoidWithZeroHom.inl G₀ H₀) m) ((MonoidWithZeroHom.inr G₀ H₀) n)
-- Mathlib.Data.Set.Restrict
Set.image_val_preimage_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} {u : Set ↑t},
  Subtype.val '' t.restrictPreimage f ⁻¹' u = f ⁻¹' Subtype.val '' u
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.mem_spanningSetsIndex : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] (x : α),
  x ∈ MeasureTheory.spanningSets μ (MeasureTheory.spanningSetsIndex μ x)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instIsScalarTower : ∀ {α : Type u_1} {𝕜 : Type u_2} {𝕜' : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : NormedRing 𝕜']
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜' E] [inst_5 : IsBoundedSMul 𝕜 E] [inst_6 : IsBoundedSMul 𝕜' E]
  [inst_7 : SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E], IsScalarTower 𝕜 𝕜' ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Algebra.Prime.Lemmas
DvdNotUnit.not_isUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q : M}, DvdNotUnit p q → ¬IsUnit q
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetD_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {fallback : β},
          Std.DTreeMap.Internal.Impl.Const.getD t₁ k fallback = Std.DTreeMap.Internal.Impl.Const.getD t₂ k fallback
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- The bijection `(g ≫ l ⟶ h) ≃ (g ⟶ h ≫ r)` induced by an adjunction
`l ⊣ r` in a bicategory.  -/
CategoryTheory.Bicategory.Adjunction.homEquiv₂ : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {l : b ⟶ c} →
        {r : c ⟶ b} →
          CategoryTheory.Bicategory.Adjunction l r →
            {g : a ⟶ b} →
              {h : a ⟶ c} → (CategoryTheory.CategoryStruct.comp g l ⟶ h) ≃ (g ⟶ CategoryTheory.CategoryStruct.comp h r)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.Coindep.indep : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Coindep X → M✶.Indep X
-- Mathlib.Data.List.Defs
/-- Monadic variant of `foldrIdx`.  -/
List.foldrIdxM : {m : Type v → Type w} → [Monad m] → {α : Type u_7} → {β : Type v} → (ℕ → α → β → m β) → β → List α → m β
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_iff' : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  autoParam (‖f (min a b)‖ₑ ≠ ⊤) intervalIntegrable_iff'._auto_1 →
    (IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.uIcc a b) μ)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_hom_app : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasBiproductsOfShape J C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C),
  CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.biproduct.ι fun j => X.obj { as := j }))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π fun j => X.obj { as := j }))
          (CategoryTheory.Limits.Pi.isoLimit X).hom))
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_setWidth' : ∀ {m n : ℕ} (ge : m ≥ n) (x : BitVec n) (i : ℕ),
  (BitVec.setWidth' ge x).getMsbD i = (decide (m - n ≤ i) && x.getMsbD (i + n - m))
-- Mathlib.Algebra.Group.ULift
ULift.inv : {α : Type u} → [Inv α] → Inv (ULift.{u_1, u} α)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to1.tr.match_1.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1to1.Λ' Γ Λ σ → Sort u_4) (l : Λ)
  (h_1 : (l : Λ) → motive (Turing.TM1to1.Λ'.normal l))
  (h_2 : (a : Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1to1.Λ'.write a q)),
  (match Turing.TM1to1.Λ'.normal l with
    | Turing.TM1to1.Λ'.normal l => h_1 l
    | Turing.TM1to1.Λ'.write a q => h_2 a q) =
    h_1 l
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.instIsAddTorsionFree : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [IsAddTorsionFree G], IsAddTorsionFree ↥H
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) (of of_1 : C),
  ({ of := of } = { of := of_1 }) = (of = of_1)
-- Mathlib.Data.List.DropRight
List.rtake_concat_succ : ∀ {α : Type u_1} (l : List α) (n : ℕ) (x : α), (l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]
-- Init.Data.UInt.Lemmas
UInt8.toUSize_toUInt16 : ∀ (n : UInt8), n.toUInt16.toUSize = n.toUSize
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_le_iff_le_sinh : ∀ {z w : UpperHalfPlane} {r : ℝ}, dist z w ≤ r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ Real.sinh (r / 2)
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.integrable_comp : ∀ {E' : Type u_2} {F' : Type u_3} {A : Type u_4} [inst : NormedAddCommGroup E'] [inst_1 : InnerProductSpace ℝ E']
  [inst_2 : FiniteDimensional ℝ E'] [inst_3 : MeasurableSpace E'] [inst_4 : BorelSpace E']
  [inst_5 : NormedAddCommGroup F'] [inst_6 : InnerProductSpace ℝ F'] [inst_7 : FiniteDimensional ℝ F']
  [inst_8 : MeasurableSpace F'] [inst_9 : BorelSpace F'] (f : E' ≃ₗᵢ[ℝ] F') [inst_10 : NormedAddCommGroup A]
  (g : F' → A), MeasureTheory.Integrable (g ∘ ⇑f) MeasureTheory.volume ↔ MeasureTheory.Integrable g MeasureTheory.volume
-- Init.Data.UInt.Lemmas
UInt32.lt_one_iff : ∀ {a : UInt32}, a < 1 ↔ a = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply : ∀ {M : Type u_4} [inst : AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)),
  ↑(AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = ↑x
-- Mathlib.RingTheory.PicardGroup
/-- Exactness of the sequence `1 → Rˣ → Aˣ → (Submodule R A)ˣ → Pic R → Pic A`
at `(Submodule R A)ˣ`.  -/
Submodule.mulExact_unitsMap_spanSingleton_unitsToPic : ∀ (R : Type u) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A], Function.MulExact ⇑(Units.map ↑(Submodule.spanSingleton R)) ⇑(Submodule.unitsToPic R A)
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_le_div_left : ∀ {a b : ENNReal}, a ≤ b → ∀ (c : ENNReal), c / b ≤ c / a
-- Init.Conv
Lean.Parser.Tactic.Conv.convSeqBracketed : Lean.ParserDescr
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.fontaineTheta_teichmuller : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) R] (x : PreTilt R p),
  (WittVector.fontaineTheta R p) ((WittVector.teichmuller p) x) = PreTilt.untilt x
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.insertIfNew.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
      Std.DTreeMap.Internal.Impl.insertIfNew k v t hl = Std.DTreeMap.Internal.Impl.insertIfNew k v_1 t hl
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.star : Lean.Elab.Tactic.ElabSimpArgResult
-- Mathlib.Logic.Basic
exists_and_exists_comm : ∀ {α : Sort u_1} {β : Sort u_2} {P : α → Prop} {Q : β → Prop}, ((∃ a, P a) ∧ ∃ b, Q b) ↔ ∃ a b, P a ∧ Q b
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Precomposition of a 1-morphism as a functor from the category of 1-morphisms `a ⟶ b` into the
category of functors `(b ⟶ c) ⥤ (a ⟶ c)`.  -/
CategoryTheory.Bicategory.precomposing : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b c : B) → CategoryTheory.Functor (a ⟶ b) (CategoryTheory.Functor (b ⟶ c) (a ⟶ c))
-- Mathlib.NumberTheory.ModularForms.Identities
SlashInvariantForm.vAdd_apply_of_mem_strictPeriods : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ]
  [SlashInvariantFormClass F Γ k] (f : F) (τ : UpperHalfPlane) {h : ℝ}, h ∈ Γ.strictPeriods → f (h +ᵥ τ) = f τ
-- Batteries.Data.Array.Scan
Array.scanr_eq_scanr_toList : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α},
  Array.scanr f init as = (List.scanr f init as.toList).toArray
-- Lean.Elab.DeclModifiers
Lean.Elab.instInhabitedVisibility.default : Lean.Elab.Visibility
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_mul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] (x : Submonoid A) (i j : HomogeneousLocalization.NumDenSameDeg 𝒜 x),
  HomogeneousLocalization.mk (i * j) = HomogeneousLocalization.mk i * HomogeneousLocalization.mk j
-- Init.Data.Array.Lemmas
List.elem_toArray : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a : α}, Array.elem a l.toArray = List.elem a l
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_map : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → β) (g : β → Option γ) (s : Multiset α),
  Multiset.filterMap g (Multiset.map f s) = Multiset.filterMap (g ∘ f) s
-- Mathlib.Data.Set.Function
Set.MapsTo.iterate : ∀ {α : Type u_1} {f : α → α} {s : Set α}, Set.MapsTo f s s → ∀ (n : ℕ), Set.MapsTo f^[n] s s
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Applying the `mk_iff` attribute to an inductively-defined proposition `mk_iff` makes an `iff` rule
`r` with the shape `∀ ps is, i as ↔ ⋁_j, ∃ cs, is = cs`, where
* `ps` are the type parameters,
* `is` are the indices,
* `j` ranges over all possible constructors,
* the `cs` are the parameters for each of the constructors, and
* the equalities `is = cs` are the instantiations for each constructor for each of
  the indices to the inductive type `i`.

In each case, we remove constructor parameters (i.e. `cs`) when the corresponding equality would
be just `c = i` for some index `i`.

For example, if we try the following:
```lean
@[mk_iff]
structure Foo (m n : Nat) : Prop where
  equal : m = n
  sum_eq_two : m + n = 2
```

Then `#check foo_iff` returns:
```lean
foo_iff : ∀ (m n : Nat), Foo m n ↔ m = n ∧ m + n = 2
```

You can add an optional string after `mk_iff` to change the name of the generated lemma.
For example, if we try the following:
```lean
@[mk_iff bar]
structure Foo (m n : Nat) : Prop where
  equal : m = n
  sum_eq_two : m + n = 2
```

Then `#check bar` returns:
```lean
bar : ∀ (m n : ℕ), Foo m n ↔ m = n ∧ m + n = 2
```

See also the user command `mk_iff_of_inductive_prop`.
 -/
Mathlib.Tactic.MkIff.mkIff : Lean.ParserDescr
-- Lean.Parser.Command
Lean.Parser.Command.unsafe.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.String.Basic
String.next'_eq : ∀ (s : String) (p : String.Pos.Raw) (h : ¬String.Pos.Raw.atEnd s p = true),
  String.Pos.Raw.next' s p h = String.Pos.Raw.next s p
-- Mathlib.Algebra.Regular.Opposite
/-- **Alias** of the reverse direction of `isLeftRegular_unop`. -/
IsLeftRegular.unop : ∀ {R : Type u_1} [inst : Mul R] {a : Rᵐᵒᵖ}, IsRightRegular a → IsLeftRegular (MulOpposite.unop a)
-- Mathlib.Topology.Algebra.Support
tsupport_comp_subset : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} [inst : Zero α] [inst_1 : TopologicalSpace X] [inst_2 : Zero β]
  {g : α → β}, g 0 = 0 → ∀ (f : X → α), tsupport (g ∘ f) ⊆ tsupport f
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_I₀ : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J], (AlgebraicGeometry.Scheme.IsLocallyDirected.openCover F).I₀ = J
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.isAlgebraic_ringHom_iff_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : EquivLike FRS R S] [inst_7 : RingEquivClass FRS R S] [inst_8 : EquivLike FAB A B]
  [inst_9 : RingEquivClass FAB A B] (f : FRS) (g : FAB),
  (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → (Algebra.IsAlgebraic S B ↔ Algebra.IsAlgebraic R A)
-- Mathlib.CategoryTheory.Functor.Basic
/-- `F ⋙ G` is the composition of a functor `F` and a functor `G` (`F` first, then `G`).
 -/
CategoryTheory.Functor.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            CategoryTheory.Functor C D → CategoryTheory.Functor D E → CategoryTheory.Functor C E
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- The yoneda embedding of `Mon C` into presheaves of monoids.  -/
CategoryTheory.yonedaMon : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.Mon C) (CategoryTheory.Functor Cᵒᵖ MonCat)