mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Fin.Lemmas
Fin.addCases_right : ∀ {m n : ℕ} {motive : Fin (m + n) → Sort u_1} {left : (i : Fin m) → motive (Fin.castAdd n i)}
  {right : (i : Fin n) → motive (Fin.natAdd m i)} (i : Fin n), Fin.addCases left right (Fin.natAdd m i) = right i
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnected.mk.sizeOf_spec : ∀ (sessionId : UInt64), sizeOf { sessionId := sessionId } = 1 + sizeOf sessionId
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.existsUnique : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g),
  ∃! τ,
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f g)
        (CategoryTheory.Bicategory.whiskerLeft f τ) =
      s.unit
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.parens : Lean.Option Bool
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.smul_tmul' : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R' M] (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The right unitor: `f ≫ 𝟙 b ≅ f`  -/
CategoryTheory.Bicategory.rightUnitor : {B : Type u} →
  [self : CategoryTheory.Bicategory B] →
    {a b : B} → (f : a ⟶ b) → CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) ≅ f
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_ne_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  {e : ℕ},
  e ≠ 0 → Ideal.map (algebraMap R S) p ≤ P ^ e → ¬Ideal.map (algebraMap R S) p ≤ P ^ (e + 1) → p.ramificationIdx' P ≠ 0
-- Init.Data.Int.Gcd
Int.gcd_dvd_gcd_of_dvd_right : ∀ {a b : ℤ} (c : ℤ), a ∣ b → c.gcd a ∣ c.gcd b
-- Mathlib.Data.Finsupp.Defs
/-- Given `f : α ↪ β` and `v : α →₀ M`, `Finsupp.embDomain f v : β →₀ M`
is the finitely supported function whose value at `f a : β` is `v a`.
For a `b : β` outside the range of `f`, it is zero.  -/
Finsupp.embDomain : {α : Type u_1} → {β : Type u_2} → {M : Type u_4} → [inst : Zero M] → (α ↪ β) → (α →₀ M) → β →₀ M
-- Mathlib.NumberTheory.AlmostPrime
Nat.isAlmostPrime_one_iff : ∀ {n : ℕ}, Nat.IsAlmostPrime 1 n ↔ Nat.Prime n
-- Init.Data.UInt.Lemmas
USize.ofNat_lt_iff : ∀ {n : USize} {m : ℕ}, m < USize.size → (USize.ofNat m < n ↔ m < n.toNat)
-- Init.Data.Nat.Lemmas
Nat.succ_mul_succ_eq : ∀ (a b : ℕ), a.succ * b.succ = a * b + a + b + 1
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `upperHemicontinuous_iff_forall_isOpen`. -/
UpperHemicontinuous.of_forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} [inst_1 : TopologicalSpace β],
  (∀ (x : α) (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u) → UpperHemicontinuous f
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.prod_mono : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {p p' : Submodule R M} {q q' : Submodule R M'},
  p ≤ p' → q ≤ q' → p.prod q ≤ p'.prod q'
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_symm_apply : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (p : (i : ι) → Submodule R (Ms i))
  (a : (i : ι) → Ms i ⧸ p i),
  (Submodule.quotientPi p).symm a = (Submodule.piQuotientLift p (Submodule.pi Set.univ p) (LinearMap.single R Ms) ⋯) a
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.AddMon_tensor_add_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : C) [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero
            CategoryTheory.AddMonObj.zero)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)) =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.mem_coe : ∀ {α : Type u} {f : Ultrafilter α} {s : Set α}, s ∈ ↑f ↔ s ∈ f
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.le_add_caratheodory : ∀ {α : Type u_1} (m₁ m₂ : MeasureTheory.OuterMeasure α), m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂).caratheodory
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.hom_neg_apply : ∀ {A B : ProfiniteAddGrp.{u}} (e : A ≅ B) (x : ↑B.toProfinite.toTop),
  (ProfiniteAddGrp.Hom.hom e.hom) ((ProfiniteAddGrp.Hom.hom e.inv) x) = x
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_induction : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α}
  {p : α → Prop}, p ⊤ → (∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂)) → (∀ b ∈ s, p (f b)) → p (s.inf f)
-- Mathlib.Data.Vector3
Vector3.append_left : ∀ {α : Type u_1} {m : ℕ} (i : Fin2 m) (v : Vector3 α m) {n : ℕ} (w : Vector3 α n), v.append w (Fin2.left n i) = v i
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.gcorec_some : ∀ {β : Type u_1} {γ : Type u_2} {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {F : β → Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl × γ × β)}
  {op :
    γ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  [inst : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass op] {b : β} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl} {c : γ} {next : β},
  F b = some (exp, coef, c, next) →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.gcorec F op b =
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef
        (op c (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.gcorec F op next))
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
/-- A version of `Complex.deriv_cpow_const` for a real variable.  -/
Complex.deriv_ofReal_cpow_const : ∀ {c : ℂ} {x : ℝ}, x ≠ 0 → c ≠ 0 → deriv (fun x => ↑x ^ c) x = c * ↑x ^ (c - 1)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : SizeOf α] (toCompacts : TopologicalSpace.Compacts α)
  (nonempty' : toCompacts.carrier.Nonempty),
  sizeOf { toCompacts := toCompacts, nonempty' := nonempty' } = 1 + sizeOf toCompacts + sizeOf nonempty'
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.addEquivBiprod_apply_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y₁ Y₂ : C} {n : ℕ} (e : CategoryTheory.Abelian.Ext X (Y₁ ⊞ Y₂) n),
  (CategoryTheory.Abelian.Ext.addEquivBiprod e).1 =
    e.comp (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.fst) ⋯
-- Init.Data.UInt.Bitwise
UInt32.toNat_shiftRight : ∀ (a b : UInt32), (a >>> b).toNat = a.toNat >>> (b.toNat % 32)
-- Mathlib.Topology.Algebra.Group.Pointwise
compl_add_closure_zero_eq : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {t : Set G},
  t + closure {0} = t → tᶜ + closure {0} = tᶜ
-- Mathlib.MeasureTheory.Covering.DensityTheorem
/-- A Vitali family in a space with a uniformly locally doubling measure, designed so that the sets
at `x` contain all `closedBall y r` when `dist x y ≤ K * r`.  -/
IsUnifLocDoublingMeasure.vitaliFamily : {α : Type u_2} →
  [inst : PseudoMetricSpace α] →
    [inst_1 : MeasurableSpace α] →
      (μ : MeasureTheory.Measure α) →
        [IsUnifLocDoublingMeasure μ] →
          [SecondCountableTopology α] → [BorelSpace α] → [MeasureTheory.IsLocallyFiniteMeasure μ] → ℝ → VitaliFamily μ
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.ofHom_comp : ∀ {M N P : Type u} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P] (f : M →+ N) (g : N →+ P),
  AddMonCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (AddMonCat.ofHom f) (AddMonCat.ofHom g)
-- Init.Data.List.Basic
List.zipWith.eq_1 : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (x_2 : α) (xs : List α) (y : β) (ys : List β),
  List.zipWith f (x_2 :: xs) (y :: ys) = f x_2 y :: List.zipWith f xs ys
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
HasEnoughRootsOfUnity.rootsOfUnity_isCyclic : ∀ (M : Type u_1) [inst : CommMonoid M] (n : ℕ) [HasEnoughRootsOfUnity M n], IsCyclic ↥(rootsOfUnity n M)
-- Mathlib.CategoryTheory.EssentiallySmall
/-- A category is `EssentiallySmall.{w}` if there exists
an equivalence to some `S : Type w` with `[SmallCategory S]`.  -/
CategoryTheory.EssentiallySmall : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Lean.Data.KVMap
Lean.KVMap.instValueInt : Lean.KVMap.Value ℤ
-- Init.Core
Std.Total.mk : ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a b : α), r a b ∨ r b a) → Std.Total r
-- Mathlib.Order.Booleanisation
Booleanisation.lift_lt_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, Booleanisation.lift a < Booleanisation.lift b ↔ a < b
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.trailPrec : Lean.PrettyPrinter.Parenthesizer.State → Option ℕ
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- A colimit cocone for `F : J ⥤ Type w₀` induces a colimit cocone
for `G : J ⥤ Type w₉'` when we have a natural equivalence `G.obj j ≃ F.obj j`
for all `j : J`.  -/
CategoryTheory.Functor.CoconeTypes.IsColimitCore.precompose : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} →
      {c : F.CoconeTypes} →
        c.IsColimitCore →
          {G : CategoryTheory.Functor J (Type w₀')} →
            (e : (j : J) → G.obj j ≃ F.obj j) →
              (naturality :
                  ∀ {j j' : J} (f : j ⟶ j'),
                    ⇑(e j') ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) =
                      ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)) →
                (c.precompose (fun {j'} => ⇑(e j')) ⋯).IsColimitCore
-- Mathlib.CategoryTheory.Sites.Pretopology
/-- A (Grothendieck) pretopology on `C` consists of a collection of families of morphisms with a fixed
target `X` for every object `X` in `C`, called "coverings" of `X`, which satisfies the following
three axioms:
1. Every family consisting of a single isomorphism is a covering family.
2. The collection of covering families is stable under pullback.
3. Given a covering family, and a covering family on each domain of the former, the composition
   is a covering family.

In some sense, a pretopology can be seen as Grothendieck topology with weaker saturation conditions,
in that each covering is not necessarily downward closed.

See: https://ncatlab.org/nlab/show/Grothendieck+pretopology or [MM92] Chapter III,
Section 2, Definition 2.  -/
CategoryTheory.Pretopology : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasPullbacks C] → Type (max u v)
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
/-- This is the full, faithful and exact embedding `C ⥤ ModuleCat (EmbeddingRing C)`. The fact that
such a functor exists is called the Freyd-Mitchell embedding theorem.

It is probably not a good idea to unfold this.  -/
CategoryTheory.Abelian.FreydMitchell.functor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Functor C (ModuleCat (CategoryTheory.Abelian.FreydMitchell.EmbeddingRing C))
-- Mathlib.Data.Quot
/-- Constructor for `Trunc α`  -/
Trunc.mk : {α : Sort u_1} → α → Trunc α
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Z : ChainComplex C ℕ}
  (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty
      (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) =
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.nonempty : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K), (↑C).Nonempty
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSet_iff : ∀ {Ω : Type u_1} {x : MeasurableSpace Ω} (s t : Set Ω) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepSet s t μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.nameOrBuiltinName : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Lean.Name
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.dite_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (s : Set α) (hs : MeasurableSet s)
  (f : MeasureTheory.SimpleFunc (↑s) β) (g : MeasureTheory.SimpleFunc (↑sᶜ) β) (x : α),
  (MeasureTheory.SimpleFunc.dite s hs f g) x = if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- A `bigOpBinder` is like an `extBinder` and has the form `x`, `x : ty`, or `x pred`
where `pred` is a `binderPred` like `< 2`.
Unlike `extBinder`, `x` is a term.  -/
BigOperators.bigOpBinder : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegrable_restrictScalars_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b} {𝕝 : Type u_4} [inst_5 : RCLike 𝕝] [inst_6 : NormedSpace 𝕝 F] [inst_7 : NormedSpace 𝕝 E]
  [inst_8 : LinearMap.CompatibleSMul E F 𝕝 𝕜],
  CurveIntegrable (fun t => ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ ↔ CurveIntegrable ω γ
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioc_sub_one_sub_one_eq_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] [NoMinOrder α] (a b : α), Finset.Ioc (a - 1) (b - 1) = Finset.Ico a b
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
_private.Mathlib.Combinatorics.Enumerative.Catalan.Tree.0.BinaryTree.treesOfNumNodesEq.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.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.symmetricCategory_braiding_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  (X₁ X₂ : CategoryTheory.Arrow C), (β_ X₁ X₂).inv.right = (β_ X₁.right X₂.right).inv
-- Init.Data.UInt.Bitwise
UInt32.toBitVec_shiftLeft : ∀ (a b : UInt32), (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 32)
-- Mathlib.Data.Real.Basic
Real.ofCauchy_inv : ∀ {f : CauSeq.Completion.Cauchy abs}, { cauchy := f⁻¹ } = { cauchy := f }⁻¹
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- The conclusion is the usual meaning of "glue nicely" in textbooks. It turns out to be quite
unusable, as it's about faces as sets in space rather than simplices. Further, additional structure
on `𝕜` means the only choice of `u` is `s ∩ t` (but it's hard to prove).  -/
Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s t : Finset E},
  s ∈ K.faces →
    t ∈ K.faces →
      Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∨
        ∃ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑u
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective.  -/
Subsemigroup.gciMapComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] →
      [inst_1 : Mul N] →
        {f : M →ₙ* N} → Function.Injective ⇑f → GaloisCoinsertion (Subsemigroup.map f) (Subsemigroup.comap f)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] (s s_1 : Finset β) (e_s : s = s_1) (H : s.Nonempty)
  (f f_1 : β → α), f = f_1 → s.inf' H f = s_1.inf' ⋯ f_1
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.of.sizeOf_spec : ∀ (carrier : Type u_1) [str : GroupWithZero carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Unitization.convexOn_of_convexOn_inr_comp : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {f : A → A} {s : Set A},
  (∀ (x : A), IsSelfAdjoint (f x)) → ConvexOn ℝ s (Unitization.inr ∘ f) → ConvexOn ℝ s f
-- Mathlib.Data.Set.Operations
Set.mem_image : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (y : β), y ∈ f '' s ↔ ∃ x ∈ s, f x = y
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.comp_measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {g : α → β} {γ : Type u_5} {x : MeasurableSpace γ}
  {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ},
  MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) →
    Measurable f → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyLTD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k fallback : α},
          Std.DTreeMap.Internal.Impl.getKeyLTD k t₁ fallback = Std.DTreeMap.Internal.Impl.getKeyLTD k t₂ fallback
-- Batteries.Linter.UnnecessarySeqFocus
/-- Accumulates the set of tactic syntaxes that should be evaluated at least once.  -/
Batteries.Linter.UnnecessarySeqFocus.getTactics : {ω : Type} → Lean.Syntax → Batteries.Linter.UnnecessarySeqFocus.M ω Unit
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_plusFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1}
  {CD : D → Type t} [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] (K : Type t) [inst_8 : CategoryTheory.SmallCategory K]
  [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D]
  [CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)]
  [CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)],
  CategoryTheory.Limits.PreservesLimitsOfShape K (J.plusFunctor D)
-- Mathlib.LinearAlgebra.Matrix.WithConv
instInvolutiveStarWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [InvolutiveStar α] → InvolutiveStar (WithConv (Matrix m n α))
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
Then the centralizer of `A ⊗ 1 ⊆ A ⊗ B` is `C(A) ⊗ B` where `C(A)` is the center of `A`.
 -/
Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [Module.Free R B],
  Subalgebra.centralizer R ↑Algebra.TensorProduct.includeLeft.range =
    (Algebra.TensorProduct.map (Subalgebra.center R A).val (AlgHom.id R B)).range
-- Mathlib.Order.Bounds.Image
image2_lowerBounds_lowerBounds_subset : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Topology.Bornology.BoundedOperation
BoundedSub.mk : ∀ {R : Type u_1} [inst : Bornology R] [inst_1 : Sub R],
  (∀ {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s - t)) → BoundedSub R
-- Mathlib.Order.SuccPred.Tree
SubRootedTree.ext_iff : ∀ {t : RootedTree} {v₁ v₂ : SubRootedTree t}, v₁ = v₂ ↔ v₁.root = v₂.root
-- Batteries.Lean.AttributeExtra
/-- Registers a new parametric attribute. The `extra` field is a list of definitions from other modules
which will be "pre-tagged" and are not subject to the usual restriction on tagging in the same
file as the declaration.
 -/
Lean.registerParametricAttributeExtra : {α : Type} → Lean.ParametricAttributeImpl α → List (Lean.Name × α) → IO (Lean.ParametricAttributeExtra α)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.injective_iff_map_algebraMap_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {T : Type u_4} [inst_4 : CommSemiring T] (f : S →+* T),
  Function.Injective ⇑f ↔
    ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ f ((algebraMap R S) x) = f ((algebraMap R S) y)
-- Lean.Elab.Binders
/-- Sanity-checks the number of patterns in each alternative of a definition by pattern matching.
Specifically, verifies that all alternatives have the same number of patterns and that the number
of patterns is upper-bounded by the number of (dependent) arrows in the expected type.

Note: This function assumes that the number of patterns in the first alternative will be equal to
`numDiscrs` (since we use the first alternative to infer the arity of the generated matcher in
`getMatchAltsNumPatterns`).
 -/
_private.Lean.Elab.Binders.0.Lean.Elab.Term.checkMatchAltPatternCounts : Lean.Syntax → ℕ → Lean.Expr → Lean.MetaM Unit
-- Batteries.Data.List.Basic
List.dropSliceTR.go.eq_3 : ∀ {α : Type u_1} (l : List α) (m : ℕ) (a : Array α) (x_3 : α) (xs : List α) (n : ℕ),
  List.dropSliceTR.go l m (x_3 :: xs) n.succ a = List.dropSliceTR.go l m xs n (a.push x_3)
-- Mathlib.Order.Comparable
/-- **Alias** of `Relation.symmGen_of_total`. -/
IsTotal.compRel : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Total r] (a b : α), Relation.SymmGen r a b